Foundation Universal Forcing Strict Mathlib Nno

The Mathlib bridge

The natural numbers are usually introduced by counting: zero, then one, then two, and so on. Category theory gives a sharper definition. A natural numbers object (NNO) in a category is a thing with a distinguished starting point and a successor step such that any other structure with a starting point and a step has exactly one structure-preserving map from the NNO to it. This universal property is what makes the natural numbers the natural numbers: it pins down their behavior without relying on a particular construction.

The framework's own counting numbers, called LogicNat, are built from a zero and a successor function. The module MathlibNNO.lean proves that LogicNat satisfies the NNO universal property. Specifically, it proves two theorems. First, for any type α, any base element, and any step function on α, there exists a function from LogicNat to α that sends zero to the base and sends each successor to the step applied to the previous value. Second, that function is unique: any two functions satisfying those conditions are equal. Together these two statements are exactly the universal property of a natural numbers object.

The module also packages these two theorems into a structure called MathlibNNOCert, which bundles the existence and uniqueness statements as a single certificate. A further theorem, mathlibNNOCert_holds, assembles the certificate from the two proved theorems. The point of this packaging is interoperability: the framework's counting numbers can be used anywhere Mathlib, the standard mathematical library for the Lean proof assistant, expects a natural numbers object. This is a bridge, not a new result. The universal property itself was already proved in the categorical recursor module; MathlibNNO.lean merely exposes it in the form Mathlib's category theory namespace recognizes.

In Recognition Science, this bridge matters because the framework's foundational claims flow from a single forced cost function, and the counting numbers are part of that foundation. The framework models natural numbers as a discrete ledger, a record of successive recognition events. The theorem here shows that this ledger-based counting has the same universal behavior as the standard natural numbers, so the framework's arithmetic is not a separate exotic system but a realization of the same structure mathematicians already use.

theorem logicNat_has_type_NNO_universal_property :
    ∀ {α : Type*} (base : α) (step : α → α),
      ∃ (f : LogicNat → α),
        f LogicNat.zero = base ∧
        ∀ n, f (LogicNat.succ n) = step (f n) :=
  @nno_universal_existence

theorem logicNat_NNO_uniqueness :
    ∀ {α : Type*} (base : α) (step : α → α)
      (f g : LogicNat → α),
      f LogicNat.zero = base → (∀ n, f (LogicNat.succ n) = step (f n)) →
      g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
      f = g :=
  @nno_universal_uniqueness

theorem mathlibNNOCert_holds : MathlibNNOCert :=
{ exists_rec := logicNat_has_type_NNO_universal_property
  unique_rec := logicNat_NNO_uniqueness }

theorem logicNat_has_type_NNO_universal_property :
    ∀ {α : Type*} (base : α) (step : α → α),
      ∃ (f : LogicNat → α),
        f LogicNat.zero = base ∧
        ∀ n, f (LogicNat.succ n) = step (f n) :=
  @nno_universal_existence

structure MathlibNNOCert where
  exists_rec :
    ∀ {α : Type*} (base : α) (step : α → α),
      ∃ (f : LogicNat → α),
        f LogicNat.zero = base ∧
        ∀ n, f (LogicNat.succ n) = step (f n)
  unique_rec :
    ∀ {α : Type*} (base : α) (step : α → α)
      (f g : LogicNat → α),
      f LogicNat.zero = base → (∀ n, f (LogicNat.succ n) = step (f n)) →
      g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
      f = g

What this page does not claim

This module does not prove the universal property from scratch; it re-exposes an existing proof. This module does not show that LogicNat is the only natural numbers object in the framework's category. This module does not establish any connection between the natural numbers and the fine-structure constant.

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/MathlibNNO.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: