CategoricalMathlibCert
plain-language theorem explainer
The natural number object certificate packages the recursor base and successor equations together with existence and uniqueness of morphisms out of the logic-forced naturals. Researchers working on the arithmetic layer of Recognition Science cite the record to confirm that the forced naturals carry the expected categorical universal property. The definition assembles four component lemmas already established in the module into a single structure with no additional proof steps.
Claim. Let $N$ be the inductive type of logic-forced natural numbers generated by an identity element and a successor constructor. The certificate structure asserts that the associated recursion operator $r$ satisfies $r(b,s,0)=b$ and $r(b,s,s(n))=s(r(b,s,n))$, that there exists a function $f:N→A$ obeying the same initial and successor equations for arbitrary type $A$, base $b$ and step $s$, and that any two such functions coincide.
background
The module bridges the strict categorical realization of universal forcing to Mathlib category theory by showing that the logic-forced naturals satisfy the universal property of a natural number object in the category of types. LogicNat is the smallest type containing an identity element and closed under a step operation, mirroring the orbit generated by multiplication by the golden ratio in the Recognition framework. The recursion operator is realized by pattern matching on the inductive constructors. Upstream, the ArithmeticFromLogic module defines the successor as one application of the generator and derives the Peano axioms as theorems from the inductive structure rather than axioms. The categorical module supplies the strict instantiation while this extension confirms the two commuting diagrams and the existence-uniqueness property without invoking full category machinery.
proof idea
The structure is populated by direct reference to the recursor zero and successor lemmas for the diagram equations together with the existence and uniqueness theorems for the universal property. As a record definition it requires no further proof steps beyond assembling the four fields from the already-proved components.
why it matters
This certificate is instantiated by the theorem that constructs the record from the individual lemmas, thereby completing the demonstration that the forced naturals carry the structure of a natural number object. It fills the gap noted in the module documentation between the strict forcing and Mathlib's categorical API. In the broader framework this supports the derivation of arithmetic from the J-uniqueness and phi fixed point by guaranteeing the expected recursion principle on the extracted naturals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.