The constructed Nat is THE natural numbers, up to unique isomorphism

Identifier: F:nat-peano-categoricity
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

The constructed `Nat` satisfies the Peano axioms (zero is not a successor, successor is injective, and induction holds), and CONVERSELY every structure (N, z, s) satisfying those three axioms is in structure-preserving bijection with it: the iterator `Nat.Peano.iter N z s` sends zero to z and successor to s, and is injective and surjective. It is moreover the unique such map. The statement is universe-polymorphic, so it quantifies over Peano structures in every universe, not one chosen one.

Formal statement

theorem Nat.Peano.categorical.{u} : ((x0 : Sort (u)) -> ((x1 : x0) -> ((x2 : ((x2 : x0) -> x0)) -> ((x3 : ((x3 : x0) -> Not (Eq.{u} x0 x1 (x2 x3)))) -> ((x4 : ((x4 : x0) -> ((x5 : x0) -> ((x6 : Eq.{u} x0 (x2 x4) (x2 x5)) -> Eq.{u} x0 x4 x5)))) -> ((x5 : ((x5 : ((x5 : x0) -> Prop)) -> ((x6 : x5 x1) -> ((x7 : ((x7 : x0) -> ((x8 : x5 x7) -> x5 (x2 x7)))) -> ((x8 : x0) -> x5 x8))))) -> And (And (Eq.{u} x0 (AxNat.Peano.iter.{u} x0 x1 x2 AxNat.zero) x1) (((x6 : AxNat) -> Eq.{u} x0 (AxNat.Peano.iter.{u} x0 x1 x2 (AxNat.succ x6)) (x2 (AxNat.Peano.iter.{u} x0 x1 x2 x6))))) (And (((x6 : AxNat) -> ((x7 : AxNat) -> ((x8 : Eq.{u} x0 (AxNat.Peano.iter.{u} x0 x1 x2 x6) (AxNat.Peano.iter.{u} x0 x1 x2 x7)) -> Eq.{1} AxNat x6 x7)))) (((x6 : x0) -> Exists.{1} AxNat (fun (x7 : AxNat) => Eq.{u} x0 (AxNat.Peano.iter.{u} x0 x1 x2 x7) x6))))))))))

Dependencies

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

0 direct dependencies 1 direct dependents

Evidence

kernel-Nat.Peano.categorical

Kind: kernel-term
Status: checked

Supports: Every Peano structure is in structure-preserving bijection with the constructed Nat, and the axiom footprint of the witness is empty.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example characterization_status 2>/dev/null) && test "$(printf '%s\n' "$out" | grep -Ec '^nat-categoricity[[:space:]]+Nat[.]Peano[.]categorical[[:space:]]+\[\][[:space:]]')" -ge 1

Evidence notes

The grep is anchored on the declaration name AND on an EMPTY footprint column, so neither a renamed theorem nor one that grew a dependency on a trusted declaration can satisfy it. The `&&` is load-bearing: `characterization_status` is itself a checker that exits non-zero when any entry is not a `Declaration::Theorem`, when any footprint is non-empty, when the population changes, or when any injected `Weakening` is ACCEPTED by the kernel -- so this command fails both on a missing row and on a package whose hypotheses stopped being load-bearing. Verified 2026-08-17: the command exits 0, and the same command with a non-existent declaration name exits 1.

kernel-Nat.Peano.zero_ne_succ

Kind: kernel-term
Status: checked

Supports: Peano 1: zero is not a successor. Proved by a Prop-valued Nat.rec discriminator, not assumed.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example characterization_status 2>/dev/null) && test "$(printf '%s\n' "$out" | grep -Ec '^peano-axiom[[:space:]]+Nat[.]Peano[.]zero_ne_succ[[:space:]]+\[\][[:space:]]')" -ge 1

Evidence notes

This was the one Peano axiom the Nat prelude did not carry -- its module docs said `n != succ n`-style discrimination was absent -- so it is the row that actually moved. `Nat.Peano.succ_injective` and `Nat.Peano.induction` restate the other two in this module and are discharged by `Nat.succ_injective` and the kernel-generated `Nat.rec`, so a prelude statement that drifts becomes a kernel rejection here rather than a silently different axiom.

kernel-Nat.Peano.iter_unique

Kind: kernel-term
Status: checked

Supports: The comparison map is the UNIQUE structure-preserving map out of Nat, which is what makes the isomorphism canonical rather than merely existent.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example characterization_status 2>/dev/null) && test "$(printf '%s\n' "$out" | grep -Ec '^nat-universal-property[[:space:]]+Nat[.]Peano[.]iter_unique[[:space:]]+\[\][[:space:]]')" -ge 1

Evidence notes

Existence is `Nat.Peano.iter` (a definition by `Nat.rec`) with `iter_zero`/`iter_succ` holding definitionally; uniqueness is this theorem. Together they are the universal property of Nat as the initial iteration algebra.

nat-trusted-surface-empty

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Nat prelude's whole trusted surface is empty, which bounds every individual footprint by [].

Checker command

cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free nat --require-axiom-free logic

Evidence notes

Enumerates the built Nat environment over the FULL trusted surface (Axiom/Opaque/Quotient), not `Declaration::Axiom` alone, and exits non-zero on any member. Measured 2026-08-17: logic=0, nat=0.

Provenance

{
  "date": "2026-08-17",
  "established_by": "axeyum-lean-kernel characterization module (agent-characterization lane)",
  "source": "hand-built foundational library; the statement is the standard second-order categoricity of Peano arithmetic, authored here rather than imported"
}