Euler's theorem for units — Exact Proof Explorer

Balanced congruence transports actual common-divisor coprimality, even at modulus zero or one.

Multiplication by a coprime multiplier preserves and reflects precisely the unit predicate used by Phi.

An actual bounded inverse implies the frozen common-divisor coprimality graph.

Above modulus one, coprimality constructs the blueprint's actual bounded inverse without assuming it.

Actual Euclidean division constructs a canonical residue of every multiplied index, including index zero.

The empty multiplier prefix has no residue obligations.

Append the actual next canonical residue, preserving every earlier decoded multiplier value.

HA induction builds the complete beta-coded multiplier prefix; no map or bijection is supplied as a premise.

Every decoded map entry, not just its construction witness, has the required bound and balanced congruence.

Coprime modular cancellation makes the genuinely constructed full multiplier map a bounded injection.

The multiplier map has actual bounded, injective, and surjective prefix evidence, not an assumed permutation label.

Every coprime multiplier at every positive modulus constructs a genuine canonical finite permutation, including modulus one.

Construct the actual weighted factor by the independent decidable coprimality predicate.

At a genuine unit index the weighted factor is the index itself.

A nonunit index contributes exactly one, not a zero or an assumed cancellable residue.

Every weighted factor is coprime to the modulus, including the modulus-one zero factor.

The empty weighted-factor prefix is valid for any beta codes.

Actually append the independently chosen next factor while preserving every earlier factor.

HA induction constructs all coprime-weighted factors; their list is never an endpoint assumption.

Restrict an actual weighted-factor prefix to its predecessor interval.

The weighted-factor choice holds for every actual decoded entry, independently of beta encoding.

The entire actual unit-weighted product is coprime to m; this is the proved cancellation premise.

A unit index contributes exactly one multiplier factor under the actual residue permutation.

A nonunit index and its image both contribute one, so neither adds to the exponent.

Restrict the independently specified unit-scaled action to its predecessor prefix.

Actual beta composition along the multiplier permutation scales precisely the factors counted by Phi.

Cancel the proved coprime finite product in a balanced congruence, including the valid modulus-one case.

Induction on the actual independently counted zero-based unit prefix proves the exact power/product congruence; no Euler conclusion or unit-count oracle is a premise.

For every positive modulus and any actual Phi and Pow values, construct all finite permutation/product witnesses and prove the Euler congruence by coprime cancellation.

Construct the actual exponentiation witness for Euler's theorem at every positive modulus, without supplying a power, factor list, or permutation.

The exact actual-inverse Unit graph suffices for a constructed Euler power; no prime-modulus restriction is introduced.

Full exact G014: m>1 and a genuinely witnessed modular unit and independently counted Phi imply an actual Pow witness congruent to one.