Complete beta-coded traces · Horner power invariants · unique modular output · Constructive arithmetic

Constructive binary modular execution and power correctness

digits∈{0,1} · rᵢ₊₁≡rᵢ²a^digitᵢ (mod m) · r≡a^Horner(digits)

Nineteen independently checked constructive theorems build complete square-and-multiply traces for any supplied valid beta-coded digit prefix, prove the exact Horner/exponent power invariant, and give a unique result.

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem BE0013 and follow only the lemmas and conservative definitions supporting binary_modular_execution_result_exists_unique.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G102 milestone → theorem and definition dependencies.
Major independently established statements: BE000B binary_execution_prefix_exists · BE000C binary_modular_execution_exists · BE0010 binary_modular_execution_power_correct · BE0011 binary_modular_execution_horner_exists · BE0013 binary_modular_execution_result_exists_unique.
Independently verified Alpha v34 checked-use theorem family: 19 dependency-curried kernel-checked theorem bodies · 60 proof prerequisites · 20 linked definitions · 27 definition-dependency arrows · 794 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: G102 was OPEN at this family's Alpha-v22 first admission: complete execution was proved only for a supplied valid beta-coded digit prefix. G102 is now CLOSED in Alpha v23 for every arbitrary exponent, with actual canonical digits and operations≤3*BitLen(e)+2.