mathlibNNOCert_holds
plain-language theorem explainer
The declaration certifies that LogicNat satisfies the natural numbers object universal property in Mathlib's category theory setting. Category theorists and Lean formalizers bridging strict models to Mathlib would cite this bridge result. The proof is a direct term-mode record construction that populates the two recursor fields from the upstream existence and uniqueness lemmas.
Claim. The certificate structure holds where, for any type $α$, base element $base : α$ and step function $step : α → α$, there exists a unique function $f : LogicNat → α$ satisfying $f(0) = base$ and $f(succ n) = step(f n)$ for all $n$.
background
This module forms the Mathlib NNO Bridge, connecting the strict categorical realization of LogicNat to Mathlib's CategoryTheory namespace while exposing the recursor universal property as a facing certificate. The structure MathlibNNOCert packages the existence and uniqueness clauses for the recursor on LogicNat. Upstream results supply the existence via nno_universal_existence and the uniqueness via the corresponding uniqueness theorem.
proof idea
The proof is a term-mode one-line wrapper that constructs the MathlibNNOCert record by assigning the exists_rec field directly to logicNat_has_type_NNO_universal_property and the unique_rec field to logicNat_NNO_uniqueness.
why it matters
This declaration completes the Mathlib-facing bridge for the NNO universal property inside the UniversalForcing.Strict module. It certifies the arithmetic foundation needed for downstream categorical developments, though no direct parent theorems appear in the used_by list and no open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.