G101 fully proved · actual beta histories · terminal gcd · logarithmic complexity · Constructive arithmetic

Certified logarithmic Euclidean algorithm

∀a b ℓ. BitLen(b,ℓ) ⇒ ∃g k. AnchoredEuclid(a,b,g,k) ∧ k≤2ℓ+1

Seventeen independently checked constructive theorems perform genuine power-of-two induction over actual Euclidean divisions, identify the encoded terminal gcd, and establish the exact formal logarithmic complexity 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 499 native tactic lines and 48 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem EL0011 and follow only the lemmas and conservative definitions supporting euclidean_gcd_execution_logarithmic_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G101 milestone → theorem and definition dependencies.
Major independently established statements: EL000C euclidean_log_trace_below_power · EL000E euclidean_log_trace_bound · EL000F euclidean_log_execution_strong · EL0010 euclidean_gcd_execution_logarithmic_bound · EL0011 euclidean_gcd_execution_logarithmic_exists.
Independently verified Alpha v34 checked-use theorem family: 17 dependency-curried kernel-checked theorem bodies · 48 proof prerequisites · 19 linked definitions · 25 definition-dependency arrows · 499 exact tactic lines · first admitted v23 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 617 bundle nodes; SHA-256 cc0051da2cac31e382c79223999d448a1119f62aa448f1c7f68a6b9c3edf9d11.
Exact mathematical boundary: The exact G101 milestone is fully proved, including the stronger checked bound k≤2·BitLen(b), a real beta-coded execution, and its actual terminal gcd. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch.

Separate complete second-wave branches: Full T13 proof · Alpha v27.