Foundation Universal Forcing Strict Categorical Mathlib Nno Universal Uniqueness

The uniqueness of counting

Counting is the first act of mathematics: you start at zero, and each step adds one. The declaration nno_universal_uniqueness proves a precise version of the claim that this procedure is unique. If two functions from the counting numbers to any type both send zero to the same starting value, and both apply the same step function at every successor, then the two functions are identical. The theorem is a formal statement in the framework's machine-checked library of formal theorems, and it is proved with no axioms beyond the standard three [propext, Classical.choice, Quot.sound].

The result belongs to a classical branch of mathematics called category theory. In category theory, a natural number object (NNO) is a structure that supports exactly this kind of unique recursion. The framework's counting numbers, called LogicNat, satisfy the NNO universal property in the category of types: for any type A, any base element, and any step function, there is exactly one function from LogicNat to A that respects the recursion. The declaration proves the uniqueness half of that property. The existence half is proved separately; together they show that LogicNat has the algebraic content of a natural number object.

What the declaration does not claim is equally important. It does not claim that LogicNat is the only possible counting system in any absolute sense. It establishes uniqueness within the specified universal property: given the same base and step, the recursive function is unique. It does not assert that the framework's counting numbers are the only model of arithmetic, nor does it claim anything about the physical world. The theorem is a structural fact about the framework's logic, not an empirical statement.

The practical consequence is that the framework's counting numbers behave exactly as ordinary natural numbers do. Any recursive definition, whether it computes a sum, a product, or a more complex function, is determined by its base case and its step case. This uniqueness is what makes recursive definitions trustworthy: there is no ambiguity in how they extend from zero to every number. The declaration closes a potential gap in the framework's foundations, ensuring that its counting numbers are not merely a formal curiosity but a well-behaved structure with the same universal property that characterizes the natural numbers in any category.

/-- 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]

/-- 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]

theorem categoricalMathlibCert_holds : CategoricalMathlibCert :=
{ recursor_zero_eq := @recursor_zero
  recursor_succ_eq := @recursor_succ
  universal_existence := @nno_universal_existence
  universal_uniqueness := @nno_universal_uniqueness }

What this page does not claim

The declaration does not claim that LogicNat is the only possible model of arithmetic. It does not claim anything about the physical world or empirical measurements. It does not assert uniqueness outside the specified universal property with given base and step functions.

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: