Actual Euclidean histories · independent gcd witnesses · strict two-step halving · Constructive arithmetic

Constructive Euclidean execution and complexity

a = bq+r · r<b · 2rᵢ₊₂<rᵢ · steps≤b

Fifteen independently checked constructive theorems produce complete beta-coded Euclidean histories, independent relational gcd witnesses, strict two-step halving and an actual linear step 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 372 native tactic lines and 34 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem EC000F and follow only the lemmas and conservative definitions supporting euclidean_gcd_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: EC0006 euclidean_two_step_halving · EC000D euclidean_execution_exists · EC000F euclidean_gcd_execution_linear_bound.
Independently verified Alpha v34 checked-use theorem family: 15 dependency-curried kernel-checked theorem bodies · 34 proof prerequisites · 9 linked definitions · 8 definition-dependency arrows · 372 exact tactic lines · first admitted v21 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 209 bundle nodes; SHA-256 65ecae7cb6b3e102790efa281451db3da5ab83868afcf9d57e6656f7a3eafda0.
Exact mathematical boundary: G101 was OPEN when this family was first admitted in Alpha v21. It is now CLOSED in Alpha v23: the actual anchored Euclidean history, terminal gcd, and exact bound steps≤2*BitLen(b)+1 are proved.