Fermat's little theorem over the axiom-free naturals: a^p is congruent to a modulo any prime p

Identifier: F:fermat-little-theorem-over-constructed-naturals
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every natural number p that is prime -- primality spelled inline as the conjunction of 2 <= p and (for all d, d divides p implies d = 1 or d = p), there being no `Prime` name in this kernel -- and every natural a, a^p is congruent to a modulo p. Congruence is Nat.modEq, defined here as `modEq d a b := exists u v, a + d*u = b + d*v`, an existential over natural witnesses rather than a statement about a remainder operation. The carrier renders as `AxNat`; despite the name it is an INDUCTIVE type, not an assumed one, and the `nat` prelude's trusted surface measures 0 (axiom=0, opaque=0, quotient=0). The proof is constructive throughout: no excluded middle, no propext, no funext, no Quot.sound. This is the unrestricted form a^p = a, NOT the coprime form a^(p-1) = 1, which is not established here and needs cancellation by a modulo p (see notes).

Formal statement

theorem Nat.pow_prime_modeq_self : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) x0) (((x2 : AxNat) -> ((x3 : AxNat.dvd x2 x0) -> Or (Eq.{1} AxNat x2 (AxNat.succ AxNat.zero)) (Eq.{1} AxNat x2 x0))))) -> AxNat.modEq x0 (AxNat.pow x1 x0) x1)))

Dependencies

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

7 direct dependencies 2 direct dependents

Evidence

kernel-Nat.pow_prime_modeq_self

Kind: kernel-term
Status: checked

Supports: `Nat.pow_prime_modeq_self` is admitted by the kernel with exactly the type in formal.statement, and `Nat.add_pow_modeq_prime` -- the Frobenius identity (a+b)^p = a^p + b^p mod p that Fermat's induction rests on -- is admitted alongside it. Both are pinned by the same test, so the identity Fermat depends on cannot drift while Fermat's own statement stays fixed.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib fermat_and_frobenius_are_stated_over_primes_not_merely_positive_moduli 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

A footprint check cannot carry this claim: a theorem stating something weaker -- primality replaced by 0 < p, or the vacuous a = a -- has exactly the same empty footprint. Mutation-verified rather than assumed: transposing the exponent in the pinned string (AxNat.pow x1 x0 -> AxNat.pow x0 x1) makes cargo report `43 passed; 1 failed`, naming this test and no other; restored, 44/44 green. The test re-derives from source on every run, rebuilding the whole Nat prelude through add_declaration. Anchored on the exact `1 passed; 0 failed` count, so an unmatched filter -- which prints `running 0 tests ... ok` and exits 0 -- cannot read as success.

footprint-Nat.pow_prime_modeq_self

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] for Nat.pow_prime_modeq_self, Nat.add_pow_modeq_prime, Nat.modEq_pow and Nat.dvd_sumRange_of_forall_lt, and for everything beneath them: Nat.prime_dvd_choose, Nat.succ_mul_choose_eq, Nat.add_pow (the binomial theorem), Nat.euclid_lemma and the gcd/Bezout development. The `nat` prelude's trusted surface is 0 -- axiom=0, opaque=0, quotient=0 -- measured by nat_axiom_inventory, not asserted.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::the_nat_prelude_declares_no_axioms -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

Presence and footprint are separate properties and both are needed. Nat.euclid_lemma was admitted and axiom-free but named by NOTHING in this prelude's sweep until 2026-08-23, so it was never visited -- axiom_footprint of an unvisited name is not empty, it is unmeasured, and the two are indistinguishable in a green run. It is registered now, and Fermat depends on it transitively. The pinned count in the_build_is_deterministic is a live guard: changing 20+142 to 20+143 killed exactly one test when checked.

Provenance

{
  "date": "2026-08-23",
  "established_by": "lane agent-capability-assurance (2026-08-23) coordinating five dispatched nat_prelude lanes: Nat.pow_prime_modeq_self and Nat.add_pow_modeq_prime in crates/axeyum-lean-kernel/src/nat_prelude/fermat.rs, kernel theorems with empty axiom_footprint. The chain was Nat.succ_sub_of_le (Vandermonde lane) -> Nat.succ_mul_choose_eq and Nat.prime_dvd_choose (Euclid lane) -> Nat.modEq_pow, Nat.dvd_sumRange_of_forall_lt, the Frobenius identity and Fermat (Fermat lane), with an earlier lane's route scout establishing that the permutation proof was unreachable.",
  "source": "classical",
  "prior_art": [
    {
      "who": "Pierre de Fermat",
      "what": "the congruence a^p = a (mod p) for p prime",
      "year": 1640,
      "where": "letter to Frenicle de Bessy, 18 October 1640; stated without proof",
      "attribution": "standard attribution. Fermat stated it and did not publish a proof; the first published proof is Euler's (1736). This lane consulted no primary source."
    },
    {
      "who": "Gottfried Wilhelm Leibniz",
      "what": "an unpublished proof by the multinomial/Frobenius route",
      "year": 1683,
      "where": "unpublished manuscript, cited in the standard histories",
      "attribution": "conventional; noted because the route proved here -- via (a+b)^p = a^p + b^p mod p -- is the one attributed to Leibniz and later Euler, not Fermat's own."
    }
  ]
}