CategoryNNOInterface
plain-language theorem explainer
CategoryNNOInterface defines a structure that assembles the data for a natural-number object in a one-object categorical presentation, with fields for objects, morphisms, terminal element, NNO, zero and successor maps, and an initiality proposition. Researchers constructing Lawvere-style arithmetic realizations in the Recognition Science foundation layer would cite this when moving from Peano algebras to categorical hooks. The declaration is introduced as a plain structure definition with no lemmas or computational content.
Claim. A structure consisting of a type $Obj$ of objects, a family $Hom : Obj → Obj → Type$ of morphisms, a terminal object $terminalOrZero : Obj$, a natural-number object $nno : Obj$, a zero morphism $zeroMorphism : Hom(terminalOrZero, nno)$, a successor morphism $succMorphism : Hom(nno, nno)$, and an initiality proposition $initiality : Prop$.
background
The module supplies a categorical realization hook for the Universal Forcing program and packages the natural-number object in the initial-Peano-algebra language already used by ArithmeticOf. A LawvereNNO is defined as a structure containing a PeanoObject, a proof that the object is initial, decidable equality on its carrier, and a witness that the carrier is nontrivial. The Hom structure from ArithmeticOf consists of carrier maps that send zero to zero and commute with the successor operation. This interface deliberately collapses the object type to a singleton to avoid committing to Mathlib's full category-theory library during the current sprint.
proof idea
The declaration is a structure definition; it contains no proof body, applies no lemmas, and performs no tactic steps.
why it matters
The structure is instantiated by the downstream projection categoryInterfaceOfLawvere, which converts a LawvereNNO into this explicit interface. It occupies the foundation layer that prepares discrete logic for categorical embedding, directly supporting the transition from Peano algebras toward the forcing chain steps T0-T8. The module documentation notes that future work can replace the collapsed one-object setup with a genuine category instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.