EU0001 euler_coprime_mod_transportBalanced 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 StableEU0002 euler_multiplier_coprime_iffMultiplication 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 StableEU0004 euler_modular_unit_coprimeAn 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 StableEU0005 euler_coprime_modular_unitAbove 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 StableEU0006 euler_multiplier_residue_existsActual 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 StableEU0007 euler_multiplier_prefix_emptyThe 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 StableEU0008 euler_multiplier_prefix_extendAppend 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 StableEU0009 euler_multiplier_prefix_existsHA 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 StableEU000A euler_multiplier_prefix_entryEvery 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 StableEU000B euler_multiplier_prefix_bounded_injectiveCoprime 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 StableEU000C euler_multiplier_prefix_permutationThe 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 StableEU000D euler_multiplier_permutation_existsEvery 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 StableEU000E euler_unit_product_factor_existsConstruct 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 StableEU000F euler_unit_product_factor_unit_valueAt 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 StableEU0010 euler_unit_product_factor_nonunit_valueA 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 StableEU0011 euler_unit_product_factor_coprimeEvery 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 StableEU0012 euler_unit_product_prefix_emptyThe 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 StableEU0013 euler_unit_product_prefix_extendActually 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 StableEU0014 euler_unit_product_prefix_existsHA 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 StableEU0015 euler_unit_product_prefix_drop_lastRestrict 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 StableEU0016 euler_unit_product_prefix_entryThe 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 StableEU0017 euler_unit_product_coprimeThe 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 StableEU0018 euler_unit_factor_scaled_congruenceA 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 StableEU0019 euler_nonunit_factor_unchanged_congruenceA 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 StableEU001A euler_unit_scaled_prefix_drop_lastRestrict 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 StableEU001B euler_unit_product_reindex_scaleActual 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 StableEU001D euler_coprime_weighted_product_cancelCancel 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 StableEU001E euler_unit_count_product_balanceInduction 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 StableEU001F euler_coprime_totient_power_valueFor 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 StableEU0020 euler_coprime_totient_powerConstruct 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 StableEU0021 euler_modular_unit_totient_powerThe 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 StableEU0022 euler_theorem_for_unitsFull 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 StablePD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0PD0003 Dvd(d,n)The natural number d divides n.
Conservative definition · notation layer 0PD0005 Coprime(a,b)Every common divisor of a and b is one.
Conservative definition · notation layer 1PD0007 DivRem(n,d,q,r)q and r are a quotient and a strict remainder for n by d.
Conservative definition · notation layer 1PD0008 ModEq(m,a,b)Balanced-natural congruence modulo m.
Conservative definition · notation layer 0PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0PD0014 Product(b,c,l,z)z is the product of a beta-coded prefix of length l.
Conservative definition · notation layer 1PD0019 Repeat(b,c,a,l)The decoded prefix repeats a for l positions.
Conservative definition · notation layer 1PD0020 Pow(a,e,z)z is the relational e-th power of a.
Conservative definition · notation layer 2PD0024 BoundedPrefix(b,c,l)Every decoded entry below l is itself below l.
Conservative definition · notation layer 1PD0025 InjectivePrefix(b,c,l)Equal decoded values below l have equal indices.
Conservative definition · notation layer 1ND0182 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 2PD0015 Sum(b,c,l,z)z is the sum of a beta-coded prefix of length l.
Conservative definition · notation layer 1ND0183 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 3ND0184 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 4PD0026 SurjectivePrefix(b,c,l)Every value below l occurs at an index below l.
Conservative definition · notation layer 1ND0148 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 2ND0237 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 1ND0023 CanonicalModularResidue(m,a,r)A strictly bounded canonical natural residue r<m together with exact balanced congruence to a modulo m.
Conservative definition · notation layer 1ND0238 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 2ND0239 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 2ND0240 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 3ND0241 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.