Euler's totient theorem over the constructed integers (Int.euler_totient_theorem)

Identifier: F:int-euler-totient-theorem
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Euler's totient theorem, over the constructed integers: for every n : Nat with 0 < n and every a : Int coprime to n, a raised to the totient of n is congruent to 1 modulo n. The totient is NOT imported or axiomatised -- it is this kernel's own `AxNat.countRange (fun k => AxNat.beq (AxNat.gcd k n) 1) n`, the count of k in [0,n) coprime to n, so the statement is self-contained in the constructed naturals and integers. (At n = 1 that count is 1, since gcd(0,1) = 1; at n > 1 the k = 0 term is excluded because gcd(0,n) = n.) Established here rather than imported: `proof_route` is `kernel-lean` and `Kernel::axiom_footprint` for this declaration is EMPTY, measured by `theorem_axiom_footprint` as `integer Int.euler_totient_theorem 0`, in a prelude whose 1054 theorems are all axiom-free with 0 trusted declarations. What this does NOT claim: no statement about efficiency, no decision procedure, and no converse -- the hypothesis 0 < n and the coprimality hypothesis are both load-bearing and neither is discharged here.

Formal statement

theorem Int.euler_totient_theorem : ((x0 : AxNat) -> ((x1 : Int) -> ((x2 : AxNat.lt AxNat.zero x0) -> ((x3 : Int.Coprime x1 (Int.ofNat x0)) -> Int.ModEq (Int.ofNat x0) (Int.pow x1 (AxNat.countRange (fun (x4 : AxNat) => AxNat.beq (AxNat.gcd x4 x0) (AxNat.succ AxNat.zero)) x0)) Int.one))))

Dependencies

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

30 direct dependencies 2 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.euler_totient_theorem

Kind: kernel-term
Status: checked

Supports: Int.euler_totient_theorem 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.euler_totient_theorem 2>/dev/null | grep -cE '^Int\.euler_totient_theorem[[: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.euler_totient_theorem

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the integer prelude's trusted surface is empty, which bounds Int.euler_totient_theorem.

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, including Int.euler_totient_theorem. This is a whole-prelude bound, not a per-declaration measurement; the per-declaration figure is the footprint column of kernel_declaration_projection, measured 0 for this row.

Provenance

{
  "date": "2026-08-31",
  "curation": "curated",
  "generated_by": "scripts/gen-kernel-facts.py",
  "established_by": "axeyum-lean-kernel build_int_prelude (crates/axeyum-lean-kernel/src/int_prelude/)",
  "source": "Derived mechanically from the unfiltered emit of `cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection`, which prints one TSV row per declaration whose fields are (prelude, kind, display name, axiom-footprint size, direct type declarations, direct declarations, direct theorems, Kernel::render_lean(declaration.ty())). formal.statement is that last field verbatim; depends_on is the direct-theorem column intersected with this ledger's registered facts; axiom_footprint is the footprint-size column, cross-checked by the whole-prelude nat_axiom_inventory run recorded in the second evidence row. No field was hand-transcribed and no prose was authored."
}