Actual unit permutations · independently counted totients · Constructive arithmetic

Euler's theorem for units

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

m>1 ∧ Unit(a,m) ∧ Phi(m,t) ⇒ ∃w. Pow(a,t,w) ∧ ModEq(m,w,1)

Follow the constructed multiplier permutation, the weighted finite product, and the count-prefix induction to an actual power congruent to one.

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

Exact certificate

Fully expanded arithmetic

Inspect all 1203 native tactic lines and 91 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem EU0022 and follow only the lemmas and conservative definitions supporting euler_theorem_for_units.

Trace prerequisites →
Zoom between mathematical scales: research checkpoint map → research domain → proof family → G014 milestone → theorem and definition dependencies.
Major independently established statements: EU000D euler_multiplier_permutation_exists · EU0017 euler_unit_product_coprime · EU001E euler_unit_count_product_balance · EU0020 euler_coprime_totient_power · EU0022 euler_theorem_for_units.
Public research checkpoint, independently verified: 32 theorems in a complete dependency-closed HA bundle · 91 proof prerequisites · 23 linked definitions · 40 definition-dependency arrows · 1203 exact tactic lines. Not Alpha-enrolled; no Alpha checked-use authority; not Stable. Alpha v30 remains 3222 theorems and Stable remains 432. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 210 bundle nodes; SHA-256 1edfcb7021a0869c2493383c75dea367d757be0b77f36fc6ad3f5fd18ed38210. Inspect the checkpoint receipt, literal bundle, and source files →
Exact mathematical boundary: The exact G014 theorem is proved in this research checkpoint for m>1 and genuinely invertible a. Phi counts coprime residues independently of the conclusion. The broader coprime theorem also handles m=1 by congruence, not by asserting that one is a canonical remainder. No multiplicative-order or RSA theorem is claimed. The published atlas and Alpha membership are unchanged.