Foundation Universal Forcing Strict Categorical Mathlib Recursor Zero

The recursor's zero case

The theorem recursor_zero states a simple fact about a function called a recursor: when the recursor is given a starting value and a rule for moving to the next step, applying it to the number zero returns exactly that starting value. In symbols, if the starting value is `base` and the rule is `step`, then `recursor base step zero = base`. This is the base case of primitive recursion, the same foundation that lets a computer define addition as repeated counting or prove that every natural number is reachable from zero by repeated successors.

The declaration lives in a machine-checked library of formal theorems, a collection where every proof is verified by a computer kernel. The library constructs its own version of the natural numbers, called LogicNat, built from two ingredients: an identity element and a step operation that adds one. The recursor is the universal way to consume such a structure, and `recursor_zero` is the first of two equations that make it work. The second equation, `recursor_succ`, says that applying the recursor to a successor `n+1` is the same as applying the step rule to the recursor's result at `n`. Together they guarantee that the recursor behaves exactly like the standard recursion principle for natural numbers.

In category theory, these two equations are precisely what it means for a structure to be a natural number object (NNO): a terminal object, an endomorphism, and a unique morphism satisfying the two commuting squares. The library proves both existence and uniqueness of such a morphism for `LogicNat` in the category of types, and `recursor_zero` is the zero half of that proof. The theorem is verified with zero axioms and zero unresolved proofs, meaning the kernel checked every step.

What the declaration does not claim is broader. It does not assert that `LogicNat` is the only way to build natural numbers, nor that the category-theoretic machinery is the only route to recursion. It does not claim anything about physics, cost functions, or the forcing chain that derives constants like the golden ratio. The theorem is a bridge: it shows that a particular inductive type satisfies the universal property of a natural number object, nothing more and nothing less.

theorem recursor_zero {α : Type*} (base : α) (step : α → α) :
    recursor base step LogicNat.zero = base := rfl

/-- The NNO universal property on `LogicNat` in `Type`: existence. -/
theorem nno_universal_existence {α : Type*} (base : α) (step : α → α) :
    ∃ (f : LogicNat → α),
      f LogicNat.zero = base ∧
      ∀ n, f (LogicNat.succ n) = step (f n) :=
  ⟨recursor base step, recursor_zero base step, recursor_succ base step⟩

/-- The NNO universal property on `LogicNat` in `Type`: uniqueness. -/
theorem nno_universal_uniqueness {α : Type*} (base : α) (step : α → α)
    (f g : LogicNat → α)
    (hf_zero : f LogicNat.zero = base)
    (hf_succ : ∀ n, f (LogicNat.succ n) = step (f n))
    (hg_zero : g LogicNat.zero = base)
    (hg_succ : ∀ n, g (LogicNat.succ n) = step (g n)) :
    f = g := by
  funext n
  induction n with
  | identity =>
      rw [show LogicNat.identity = LogicNat.zero from rfl, hf_zero, hg_zero]
  | step k ih =>
      rw [show LogicNat.step k = LogicNat.succ k from rfl, hf_succ k, hg_succ k, ih]

What this page does not claim

The theorem does not assert that LogicNat is the only model of the natural numbers in any category. It does not claim anything about physics, cost functions, or the forcing chain that derives constants. It does not prove that primitive recursion is the only way to define arithmetic on natural numbers.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/UniversalForcing/Strict/CategoricalMathlib.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: