Foundation Universal Forcing Strict Mathlib Nno Logic Nat Nno Uniqueness

The uniqueness of the counting type

The natural numbers, 0, 1, 2, and so on, are usually introduced as the counting numbers. A deeper property they have is that they support recursion: given any starting value and any rule for moving from one value to the next, there is exactly one way to define a function on all natural numbers that starts at the given value and follows the rule at each step. This is what lets a programmer write a loop and what lets a mathematician define addition, multiplication, and factorial in a single sweep.

The Recognition Science framework encodes this property for its own formal type LogicNat, a discrete record of events that behaves like the natural numbers. The theorem logicNat_NNO_uniqueness, proved in the framework's machine-checked library of formal theorems, states the uniqueness half of the recursion property: if two functions both start at the same base value and both follow the same step rule at every input, then the two functions are equal. Its companion theorem, logicNat_has_type_NNO_universal_property, states the existence half: a function with the required behavior always exists. Together the two theorems form a universal property, a precise way of saying that LogicNat is the canonical object for recursive definitions.

The proof is not a new mathematical discovery about the ordinary natural numbers. It is a formal bridge: it takes an already proved recursor universal property from the categorical side of the framework and exposes it under the Mathlib namespace, the standard library of the framework's proof assistant. The declaration MathlibNNOCert packages both the existence and uniqueness theorems into a single certificate, and mathlibNNOCert_holds records that the certificate is satisfied. The practical effect is that any later framework theorem that needs recursion on LogicNat can cite this bridge instead of re-proving the property.

What the theorem does not claim is just as important. It does not say that LogicNat is the only possible set of natural numbers, only that any structure with the same recursion property is isomorphic to it in the categorical sense. It does not assert that the natural numbers are the counting numbers of the physical world, nor does it derive arithmetic from recognition events. It establishes a structural uniqueness result within the framework's type theory, and nothing more. A reader who wants to know what the natural numbers are, as opposed to how they behave under recursion, must look elsewhere.

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 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 mathlibNNOCert_holds : MathlibNNOCert :=
{ exists_rec := logicNat_has_type_NNO_universal_property
  unique_rec := logicNat_NNO_uniqueness }

What this page does not claim

This theorem does not claim that LogicNat is the only possible set of natural numbers, only that any structure with the same recursion property is isomorphic to it. This theorem does not assert that the natural numbers are the counting numbers of the physical world. This theorem does not derive arithmetic from recognition events.

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: