MathlibNNOCert
plain-language theorem explainer
MathlibNNOCert packages the existence and uniqueness of recursors over LogicNat, certifying that this inductive type satisfies the natural numbers object universal property. Category theorists or foundation researchers bridging custom arithmetic to Mathlib's CategoryTheory namespace would cite the record. The declaration is a pure structure definition with no internal proof steps, delegating the actual existence and uniqueness content to sibling lemmas.
Claim. The structure consists of an existence field asserting that for every type $A$, base element $b:A$ and step map $s:A→ A$, there is a function $f$ from LogicNat to $A$ with $f(0)=b$ and $f(s(n))=s(f(n))$ for all $n$, together with a uniqueness field asserting that any two such functions coincide.
background
LogicNat is the inductive type with constructors identity (zero-cost element) and step, mirroring the smallest subset of positive reals closed under multiplication by the generator γ and containing 1, as forced by the Law of Logic. The module supplies a bridge from the strict categorical realization in CategoricalMathlib to Mathlib's CategoryTheory namespace, exposing the recursor universal property already proved there. Upstream results include the successor definition succ n := .step n in ArithmeticFromLogic and the locality of the step operation in CellularAutomata.
proof idea
The declaration is a structure definition that directly declares the two fields exists_rec and unique_rec; no lemmas are applied and no tactics are used inside this declaration.
why it matters
This structure supplies the type instantiated by the downstream theorem mathlibNNOCert_holds, which assembles the certificate from the sibling lemmas logicNat_has_type_NNO_universal_property and logicNat_NNO_uniqueness. It completes the categorical bridge required for the forcing chain from logic to arithmetic, supporting the NNO universal property that underpins the T0-T8 landmarks and the derivation of Peano structure without positing axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.