IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib
Module realizing the natural-numbers-object (NNO) universal property for the LogicNat carrier via Lean's inductive recursor. It packages existence and uniqueness of primitive recursion (zero and successor cases) and a small certificate that the categorical Mathlib bridge holds. Downstream MathlibNNO imports this as the proved theorem core behind the CategoryTheory-facing NNO surface.
claimOn the LogicNat carrier, the primitive-recursion operator $\mathrm{rec}(z,s)$ is the unique map $N\to X$ satisfying $\mathrm{rec}(z,s)(0)=z$ and $\mathrm{rec}(z,s)(n+1)=s(n,\mathrm{rec}(z,s)(n))$. Existence and uniqueness of this NNO mediating arrow are proved, and a certificate records that the categorical Mathlib interface is satisfied.
background
Recognition Science's strict universal-forcing layer treats arithmetic structure categorically: a natural numbers object (NNO) is an initial algebra for $X\mapsto 1+X$, equivalently a Lawvere NNO with zero and successor universal for primitive recursion. The upstream Strict/Categorical hook fixes the carrier as the canonical LogicNat surface from CategoricalLogicRealization, leaving a Mathlib CategoryTheory NNO API as future refinement.
This module supplies the concrete recursion principle on that carrier. Lean's inductive type for LogicNat already carries a recursor; the module names the zero and successor computation rules and lifts them to the NNO universal property (a unique mediating homomorphism out of $N$ for any $(z,s)$ data on a target object).
Sibling content includes the recursor itself, its zero/succ equations, existence and uniqueness of the universal arrow, and a CategoricalMathlibCert bundle with a holding proof.
proof idea
Definition-and-theorem module, not a single wrapper. The recursor is implemented by Lean's built-in pattern match on the inductive LogicNat. Zero and successor computation lemmas are the standard $\beta$-rules of that recursor. Existence of the NNO mediating map is the recursor applied to target data $(z,s)$; uniqueness is by induction on LogicNat, comparing any two maps that preserve zero and successor. The certificate aggregates these facts into a single Prop that downstream bridges can cite in one step.
why it matters in Recognition Science
Feeds Foundation.UniversalForcing.Strict.MathlibNNO, whose doc states it "connects the strict categorical realization to Mathlib's CategoryTheory namespace" and "keep[s] the theorem content in the already proved CategoricalMathlib recursor universal property." Without this module, the Mathlib-facing NNO bridge would be scaffolding rather than a thin export of proved recursion.
In the broader forcing chain, a rigid NNO underwrites discrete tick structure (eight-tick octave at T7) and the countable combinatorial skeleton on which phi-ladder and cost functionals sit. The module closes the strict categorical hook's promise that LogicNat behaves as a genuine Lawvere NNO before any heavier Mathlib category API is wired in.
scope and limits
- Does not construct Mathlib's CategoryTheory.Limits NNO API or functors into an arbitrary topos.
- Does not prove initiality in a full categorical sense beyond LogicNat's inductive universal property.
- Does not derive physical constants, phi, or the eight-tick period; those live further down the forcing chain.
- Does not replace or redefine LogicNat; it only packages recursion on the existing carrier.