Actual unit permutations · independently counted totients

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.

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

32 kernel- and independently Lean-verified checkpoint theorems · 23 conservative definitions · 40 notation dependencies

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

55 items
EU0001 euler_coprime_mod_transport

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0002 euler_multiplier_coprime_iff

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0004 euler_modular_unit_coprime

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0005 euler_coprime_modular_unit

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0006 euler_multiplier_residue_exists

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0007 euler_multiplier_prefix_empty

The empty multiplier prefix has no residue obligations.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0008 euler_multiplier_prefix_extend

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0009 euler_multiplier_prefix_exists

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU000A euler_multiplier_prefix_entry

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU000B euler_multiplier_prefix_bounded_injective

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU000C euler_multiplier_prefix_permutation

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU000D euler_multiplier_permutation_exists

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU000E euler_unit_product_factor_exists

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU000F euler_unit_product_factor_unit_value

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0010 euler_unit_product_factor_nonunit_value

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0011 euler_unit_product_factor_coprime

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0012 euler_unit_product_prefix_empty

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0013 euler_unit_product_prefix_extend

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0014 euler_unit_product_prefix_exists

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0015 euler_unit_product_prefix_drop_last

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0016 euler_unit_product_prefix_entry

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0017 euler_unit_product_coprime

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0018 euler_unit_factor_scaled_congruence

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0019 euler_nonunit_factor_unchanged_congruence

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU001A euler_unit_scaled_prefix_drop_last

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU001B euler_unit_product_reindex_scale

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU001D euler_coprime_weighted_product_cancel

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU001E euler_unit_count_product_balance

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.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU001F euler_coprime_totient_power_value

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.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0020 euler_coprime_totient_power

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0021 euler_modular_unit_totient_power

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
EU0022 euler_theorem_for_units

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
PD0002 Lt(a,b)

Witness-defined strict order on natural numbers.

Conservative definition · notation layer 0
PD0003 Dvd(d,n)

The natural number d divides n.

Conservative definition · notation layer 0
PD0005 Coprime(a,b)

Every common divisor of a and b is one.

Conservative definition · notation layer 1
PD0007 DivRem(n,d,q,r)

q and r are a quotient and a strict remainder for n by d.

Conservative definition · notation layer 1
PD0008 ModEq(m,a,b)

Balanced-natural congruence modulo m.

Conservative definition · notation layer 0
PD0013 BetaAt(b,c,i,x)

x is the bounded beta-decoded value at index i.

Conservative definition · notation layer 0
PD0014 Product(b,c,l,z)

z is the product of a beta-coded prefix of length l.

Conservative definition · notation layer 1
PD0019 Repeat(b,c,a,l)

The decoded prefix repeats a for l positions.

Conservative definition · notation layer 1
PD0020 Pow(a,e,z)

z is the relational e-th power of a.

Conservative definition · notation layer 2
ND0182 UnitBitPrefix(n,b,c,l)

The decoded bit at i<l is one exactly for Coprime(i,n), and zero otherwise. The interval starts at zero.

Conservative definition · notation layer 2
PD0015 Sum(b,c,l,z)

z is the sum of a beta-coded prefix of length l.

Conservative definition · notation layer 1
ND0183 UnitCount(n,l,t)

An actual beta sum counts the coprime residues in 0≤i<l. This auxiliary count is total even at modulus zero.

Conservative definition · notation layer 3
ND0184 Phi(n,t)

Positive n and the actual count of canonical residues i<n coprime to n. Phi(1,1) counts residue zero; Phi excludes n=0.

Conservative definition · notation layer 4
ND0148 PermutationPrefix(b,c,l)

An actual beta-coded bijection of the finite index interval [0,l), including all bounds, injectivity, and surjectivity.

Conservative definition · notation layer 2
ND0237 Unit(a,m)

Exactly m>1 with a witnessed inverse b<m and a*b congruent to one. Unlike the old UnitResidue range, this expresses genuine invertibility at composite moduli.

Conservative definition · notation layer 1
ND0238 UnitMultiplierPrefix(a,m,b,c,l)

At every index i<l, the actual beta entry is the canonical residue of a*i. A bijection is constructed by theorem, not assumed in this graph.

Conservative definition · notation layer 2
ND0239 UnitProductFactor(m,i,v)

The independently decided weighted factor is i when Coprime(i,m), and one otherwise. It contains neither Phi nor Euler's conclusion.

Conservative definition · notation layer 2
ND0240 UnitProductPrefix(m,b,c,l)

Every actual beta entry in 0<=i<l satisfies UnitProductFactor at the same index. Product values are computed by the existing finite-product graph.

Conservative definition · notation layer 3
ND0241 UnitScaledPrefix(a,m,b,c,d,e,l)

Two genuine beta prefixes are related by modular multiplication by a precisely at coprime indices, with the other factors unchanged.

Conservative definition · notation layer 2

Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.