Common-divisor invariance · terminal-state identification · anchored linear bound · Constructive arithmetic

Constructive Euclidean gcd transport and anchored traces

gcd(a,b)=gcd(b,a mod b) · terminal(a,b)=gcd(a,b) · steps≤b

Twenty independently checked constructive theorems transport divisibility and gcd invariants through actual Euclidean steps, identify the terminal history state with its gcd, and establish a complete anchored linear bound.

Open the definition-aware map Read the final theorem See campaign milestone G101

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 550 native tactic lines and 32 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem GT0012 and follow only the lemmas and conservative definitions supporting euclidean_anchored_execution_linear_bound.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G101 milestone → theorem and definition dependencies.
Major independently established statements: GT000F euclidean_trace_terminal_gcd_exists · GT0010 euclidean_execution_terminal_identified · GT0011 euclidean_anchored_execution_exists · GT0012 euclidean_anchored_execution_linear_bound.
Independently verified Alpha v34 checked-use theorem family: 20 dependency-curried kernel-checked theorem bodies · 32 proof prerequisites · 19 linked definitions · 23 definition-dependency arrows · 550 exact tactic lines · first admitted v22 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 240 bundle nodes; SHA-256 95e5f8a3baef113721d748f9d7071864b4bf9511737a27a1272d2695428fb938.
Exact mathematical boundary: G101 was OPEN at this family's Alpha-v22 first admission: its complete anchored trace and actual terminal gcd were proved but its logarithmic bound was not. G101 is now CLOSED in Alpha v23, including the exact first-order bound steps≤2*BitLen(b)+1.