G102 fully proved · arbitrary exponents · actual digit codes · exact cost bound · Constructive arithmetic

Canonical binary digits and certified repeated squaring

∀a e m>1. ∃r k. BinaryPow(a,e,m,r,k) ∧ r≡aᵉ (mod m) ∧ k≤3·BitLen(e)+2

Twenty-four independently checked constructive theorems extract canonical beta-coded binary digits from every exponent, execute a genuine square-and-multiply trace, prove its modular-power result, and certify the exact logarithmic operation bound.

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

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 812 native tactic lines and 63 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem BD0018 and follow only the lemmas and conservative definitions supporting binary_modular_execution_logarithmic_bound.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G102 milestone → theorem and definition dependencies.
Major independently established statements: BD000A binary_exponent_digit_prefix_exists · BD0012 binary_digit_operation_count_bound · BD0014 binary_modular_exponent_coded_execution_exists · BD0016 binary_modular_exponent_coded_execution_exists_unique · BD0017 binary_modular_execution_bitlength_bound · BD0018 binary_modular_execution_logarithmic_bound.
Independently verified Alpha v34 checked-use theorem family: 24 dependency-curried kernel-checked theorem bodies · 63 proof prerequisites · 25 linked definitions · 39 definition-dependency arrows · 812 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 G102 milestone is fully proved for every natural exponent and every modulus greater than one, including actual canonical digits, a beta-coded accumulator execution, modular-power correctness, and the formal bound k≤3·BitLen(e)+2. 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.