nno_universal_existence
plain-language theorem explainer
The theorem asserts that LogicNat satisfies the existence half of the natural-number-object universal property in the category of types: for any base value and successor map on a type α there exists a recursion function realizing the Peano equations. Foundations researchers in Recognition Science cite it when confirming that the arithmetic surface forced by the Law of Logic carries the initial recursion structure. The proof is the one-line term that packages the recursor definition together with its zero and successor identities.
Claim. For any type $α$, given an element $b ∈ α$ and a function $s : α → α$, there exists a function $f : LogicNat → α$ such that $f(0) = b$ and $f(succ n) = s(f n)$ for all $n$.
background
LogicNat is the inductive type with constructors identity (zero) and step, introduced in ArithmeticFromLogic as the orbit generated by the multiplicative generator under the Law of Logic. The recursor is the primitive recursion operator defined by pattern matching: it returns the base on identity and applies the step function recursively on step n. The module CategoricalMathlib bridges the strict categorical realization to Mathlib by proving that these recursion identities match the NNO commuting squares once transported along the LogicNat ≃ Nat equivalence.
proof idea
The proof is a direct term-mode construction that supplies the recursor as the witness function together with the two lemmas recursor_zero and recursor_succ as the required equalities. No tactics are used; the term is simply the triple consisting of the recursor application and the two reflexivity proofs.
why it matters
This existence statement, together with its uniqueness counterpart, is assembled into the CategoricalMathlibCert record and is invoked to prove that LogicNat carries the NNO universal property. It closes the bridge from the strict forcing construction in Categorical to Mathlib's category-theoretic language, confirming that the arithmetic surface forced by the Law of Logic behaves as the initial object under recursion. In the broader Recognition Science framework it supplies the concrete model for the natural-number structure underlying the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.