The powers of a primitive root are pairwise incongruent (Int.primitive_root_pow_injective)

Identifier: F:int-primitive-root-pow-injective
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For n : Nat with 0 < n and a : Int a primitive root mod n -- `Int.IsPrimitiveRoot n a`, i.e. the order of a is exactly `Nat.totient n` -- the exponents below phi(n) give pairwise incongruent powers: if i, j < phi(n) and a^i = a^j (mod n) then i = j. This is the reason primitive roots are worth naming: the phi(n) powers a^0, ..., a^(phi(n)-1) enumerate the units without repetition. The proof's one interesting step is that `Coprime (a^i) n`, needed for cancellation, comes out of the ORDER RELATION itself rather than from a multiplicativity lemma the development does not have: writing t = i + f, the congruence a^i * a^f = 1 says a^f IS a modular inverse of a^i, and the Bezout extraction that turns an inverse into a coprimality was already a named helper (`coprime_of_modeq_inverse`). What this does NOT claim: this is injectivity of the power map, NOT surjectivity onto the units, and it asserts nothing about WHETHER a primitive root exists for any given n -- existence modulo a prime is not established here (ADR-1598 records the measured obstruction, the absence of a divisor-set aggregate in either prelude).

Formal statement

theorem Int.primitive_root_pow_injective : ((x0 : AxNat) -> ((x1 : Int) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat.lt AxNat.zero x0) -> ((x5 : Int.IsPrimitiveRoot x0 x1) -> ((x6 : AxNat.lt x2 (AxNat.totient x0)) -> ((x7 : AxNat.lt x3 (AxNat.totient x0)) -> ((x8 : Int.ModEq (Int.ofNat x0) (Int.pow x1 x2) (Int.pow x1 x3)) -> Eq.{1} AxNat x2 x3)))))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

3 direct dependencies 0 direct dependents

Evidence

kernel-Int.primitive_root_pow_injective

Kind: kernel-term
Status: checked

Supports: Int.primitive_root_pow_injective is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example theorem_dependency_inventory -- Int.primitive_root_pow_injective 2>/dev/null | grep -cE '^Int\.primitive_root_pow_injective[[:space:]]'

Evidence notes

Two independent failure modes, so the exit status depends on the finding rather than on the run completing: theorem_dependency_inventory exits non-zero when a NAMED filter matches nothing, and grep -c exits 1 printing 0 when the anchored line is absent. Anchored with [[:space:]], never \t -- in a scripted (GNU) grep \t is a literal t. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY: this tool builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-Int.primitive_root_pow_injective

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the integer prelude admits no Axiom, Opaque or Quotient declaration, which bounds Int.primitive_root_pow_injective.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free integer

Evidence notes

--require-axiom-free exits non-zero when the named prelude's trusted surface (Axiom + Opaque + Quotient) is not empty, and errors rather than silently passing for a prelude the run never built. A declaration cannot depend on a trusted declaration the environment does not contain, so an empty integer surface bounds every declaration in it. The per-declaration figure is the footprint column of kernel_declaration_projection, measured 0 for this row.

concrete-Int.primitive_root_pow_injective

Kind: instance-pin
Status: checked

Supports: The definitions this statement is about compute the intended values at concrete small arguments, and the discriminating negative cases FAIL: ord_8(3) = 2 (not phi(8) = 4), ord_7(3) = 6, and 3 is refutably NOT a primitive root mod 8.

Checker command

cargo test --release -p axeyum-lean-kernel --lib int_prelude::mult_order_tests -- --test-threads=4

Evidence notes

The trusted gate cannot tell you a Definition is wrong -- it type-checks either way -- so Int.IsOrder and Int.IsPrimitiveRoot are pinned by reduction at concrete small arguments. Each battery asserts BOTH what must hold and what must fail, so no run can be vacuous: three_mod_eight_is_killed_by_exactly_the_even_exponents requires hits at m in {0,2,4} and misses at {1,3,5} (the misses are the negative control for Int.pow_modeq_one_of_dvd); is_order_unfolds_to_the_intended_conjunction requires the definition to be def_eq to the intended conjunction and NOT def_eq to the variant with the positivity comparison transposed; three_has_multiplicative_order_two_mod_eight builds a witness for IsOrder 8 3 2 and a REFUTATION of IsOrder 8 3 4, which only the minimality conjunct separates. Confirm a NONZERO test count (6).

Provenance

{
  "date": "2026-09-04",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_int_prelude (crates/axeyum-lean-kernel/src/int_prelude/mult_order.rs)",
  "source": "formal.statement is Kernel::render_lean of the declared type, taken verbatim from the unfiltered emit of `cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection`; axiom_footprint is that same row's footprint column, measured 0. The prose statement and the \"what this does NOT claim\" clause are hand-written by the `primitive-roots` lane and are NOT generator output. Design record: ADR-1598.",
  "prior_art": "Classical; Gauss, Disquisitiones Arithmeticae (1801), art. 52-57. The injectivity half only; Gauss's theorem that a primitive root exists modulo every prime is NOT part of this fact."
}