Foundation Universal Forcing Strict Mathlib Nno Mathlib Nnocert

The certificate

The natural numbers are the counting numbers: zero, one, two, and so on, with the rule that each has a successor. A recognition ledger, a discrete record of events, needs such a counting structure to index its ticks. The declaration MathlibNNOCert is a formal certificate, a machine-checked package, that bundles two properties. First, for any type with a starting point and a step function, there exists a function from the framework's counting numbers to that type that sends zero to the start and each successor to the step. Second, that function is unique: any two such functions agree everywhere. Together these say the framework's counting numbers form a natural number object, the categorical way of saying they are the natural numbers up to structure.

The two properties are not new theorems in themselves. They are already proved in another module, CategoricalMathlib, which establishes the recursor universal property. MathlibNNOCert repackages those results under a single name and connects them to Mathlib's CategoryTheory namespace, the standard library of categorical structures. The certificate exists to make the bridge explicit: the framework's own counting numbers, LogicNat, satisfy the same universal property that characterizes natural numbers in any category. The theorem mathlibNNOCert_holds simply assembles the two existing proofs into the certificate structure. It is a definitional convenience, a named container, not a fresh mathematical discovery.

What the certificate does not claim is just as precise. It does not claim that LogicNat is the only natural number object, nor that it is isomorphic to any particular implementation such as Mathlib's own Nat. It claims only that the universal property holds: existence and uniqueness of the recursion function. The certificate says nothing about the cost function, the golden ratio, or any other part of the Recognition Science forcing chain. It is a narrow, local statement about counting structure, deliberately scoped so that the rest of the framework can rely on it without re-proving the recursion property. The payoff is modularity: one clean certificate, one place to look, one property to trust.

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 }

What this page does not claim

The certificate does not claim LogicNat is the only natural number object or that it is isomorphic to Mathlib's Nat. The certificate says nothing about the cost function, the golden ratio, or any other part of the forcing chain. The certificate does not introduce new mathematical content beyond repackaging the two existing theorems.

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: