Foundation Universal Forcing Strict Categorical Mathlib Nno Universal Existence

The universal property

In mathematics, a natural number object (NNO) is a way to say what the counting numbers are without mentioning counting. In a category, it is a starting point, a way to move one step forward, and the guarantee that any process built from a base case and a step rule has exactly one path through the whole sequence. The framework's own number type, LogicNat, satisfies this property in the category of types. The declaration nno_universal_existence proves the existence half: for any base value and any step function, there is a function from LogicNat to that value that sends zero to the base and sends each successor to the step applied to the previous result.

This is not a new mathematical fact. It is the same content as the standard recursion principle for the natural numbers, transported along an isomorphism between LogicNat and the usual Nat type. The proof is a formal bridge: it shows that the framework's bespoke counting numbers carry the algebraic structure that mathematicians already expect. The companion declaration nno_universal_uniqueness proves that this function is unique, so the two halves together form the full universal property. The machine-checked library of formal theorems records both results with no gaps and no extra axioms.

In Recognition Science, this matters because the framework builds its physics from a discrete ledger, a record of distinct events. The counting numbers are the spine of that ledger, and this theorem confirms that the spine behaves like ordinary arithmetic. It is a structural check, not a physical prediction. It says the framework's numbers can count; it does not say what they count.

The declaration does not claim that LogicNat is the only natural number object, nor that the framework's physical claims follow from it. It does not invoke the full category-theoretic machinery of limits and initial objects; the proof works directly with the recursion principle. The result is a clean identification of structure, nothing more.

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

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

What this page does not claim

The declaration does not prove that LogicNat is the unique natural number object in any category. It does not invoke the full category-theoretic machinery of limits and initial objects. It makes no physical claim about what the counting numbers describe.

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: