Foundation Universal Forcing Strict Categorical Mathlib

The natural number bridge

The natural numbers are the counting numbers 0, 1, 2, and so on, with the operation of adding one. In mathematics, they are often characterized by a universal property: given any starting point and any rule for moving one step forward, there is exactly one way to define a function on all natural numbers that starts at that point and follows that rule at every step. This is the principle of primitive recursion, and it is what makes the natural numbers a natural number object (NNO) in the category of types.

Recognition Science builds its own copy of the natural numbers, called LogicNat, as part of its discrete ledger of recognition events. The framework's machine-checked library of formal theorems now proves that this internal copy has the full universal property of an NNO. The module defines a recursor, a function that given a base value and a step function produces a function on LogicNat. It then proves the two defining equations: applying the recursor to zero gives the base, and applying it to a successor gives the step applied to the previous result. These are exactly the commuting-square equations that the NNO universal property requires.

The module also proves existence and uniqueness of such a function for any base and step. Existence means a function satisfying the equations always exists; uniqueness means any two such functions are equal. Together these establish that LogicNat has the algebraic content of an NNO in the category of types, equivalent in content to the standard natural numbers once transported along the isomorphism between LogicNat and the usual Nat type. The proofs are checked by the machine, with zero axioms beyond the standard three and zero sorry placeholders.

In Recognition Science, this result matters because it shows the framework's internal counting device is not ad hoc. The discrete ledger of recognition events, built from the forced cost function, supports the same recursion principle that underlies all ordinary arithmetic. This is a structural bridge: the framework's natural numbers are genuinely natural, not a private construction that happens to look similar. The module does not invoke heavy category-theoretic machinery; it proves the two structural identities directly, which is sufficient for the bridge.

What this changes is that any result in the framework that depends on recursion over its internal numbers can now be transported to and from standard mathematics. A reader who knows the universal property of natural numbers in category theory can recognize the same structure here. The framework's ledger is not a separate universe of arithmetic; it is the same arithmetic, built from a different starting point and verified by machine.

/-- The LogicNat primitive recursion principle, implemented via Lean's
    built-in pattern matching on the inductive type. -/
def recursor {α : Type*} (base : α) (step : α → α) : LogicNat → α
  | LogicNat.identity => base
  | LogicNat.step n => step (recursor base step n)

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

theorem recursor_succ {α : Type*} (base : α) (step : α → α) (n : LogicNat) :
    recursor base step (LogicNat.succ n) = step (recursor base step n) := 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]

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

This module does not prove that LogicNat is the only natural number object in the framework. It does not invoke Mathlib's full category theory API for limits or initial objects. It does not establish the physical interpretation of the ledger; that remains a separate question.

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: