categoricalMathlibCert_holds
plain-language theorem explainer
LogicNat satisfies the natural number object universal property in the category of types, with its recursor obeying the zero and successor equations plus existence and uniqueness of mediating morphisms to any target type. A category theorist verifying Peano arithmetic realizations against Mathlib's CategoryTheory would cite this to confirm the strict categorical bridge. The proof is a direct term-mode construction that packages the four supporting lemmas into the certificate structure.
Claim. Let LogicNat be the inductive type with constructors zero and succ. The certificate asserts: for any type α, base : α and step : α → α, recursor base step zero = base; recursor base step (succ n) = step (recursor base step n); there exists f : LogicNat → α with f zero = base and f (succ n) = step (f n) for all n; and any two such functions f and g are equal.
background
The module bridges the strict categorical realization on LogicNat to Mathlib's CategoryTheory API. LogicNat is the inductive Peano surface used in the strict realization, equipped with a built-in recursor that performs primitive recursion via pattern matching. The certificate structure CategoricalMathlibCert packages the four NNO axioms: the two commuting equations for zero and successor, plus existence and uniqueness of the unique morphism from LogicNat to any α given base and step data.
proof idea
The proof is a one-line term-mode wrapper that constructs the CategoricalMathlibCert structure. It supplies the four fields directly by referencing the lemmas recursor_zero, recursor_succ, nno_universal_existence, and nno_universal_uniqueness.
why it matters
This theorem certifies that LogicNat carries the algebraic content of a natural number object in Type, completing the bridge to Mathlib's Nat.rec via the equivNat isomorphism as described in the module documentation. It anchors the strict categorical realization within the UniversalForcing framework by confirming the required recursion identities. The module reports zero sorry, so no open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.