logicNatNNO_has_category_interface
plain-language theorem explainer
The result establishes that the categorical interface projected from the canonical Lawvere natural-number object in the logic realization has inhabited initiality. Researchers building categorical arithmetic bridges inside the universal forcing chain would cite this step. The proof is a direct trivial constructor that follows immediately from the way the interface is assembled from the initial Peano object.
Claim. The initiality condition of the categorical interface obtained by projecting the canonical Lawvere natural-number object supplied by the logic realization is inhabited.
background
The module supplies a categorical/Lawvere-style realization hook for the Universal Forcing program. It packages the natural-number object idea in the same initial-Peano-algebra language used by ArithmeticOf, without rebuilding category theory from scratch. The canonical arithmetic object is defined as the initial Peano object that remains realization-independent at this stage, with its surface given by logicNatPeano and logicNat_initial. The projection categoryInterfaceOfLawvere collapses a LawvereNNO to a one-object CategoryNNOInterface whose hom-sets are taken from the PeanoObject and whose terminal and NNO fields are unit markers.
proof idea
The proof is a one-line wrapper that applies the trivial constructor to the initiality field of the projected interface. The field is already populated by the direct construction of logicNatNNO from the initial Peano object and the subsequent projection, so no further lemmas or tactics are required.
why it matters
This declaration closes the first explicit bridge from the canonical arithmetic realization to a Lawvere-style categorical interface inside the forcing program. It sits downstream of the initial Peano algebra and the logicNatNNO definition, preparing the ground for categorical invariants that will later feed into the eight-tick octave and spatial-dimension forcing steps. No downstream uses are recorded yet, leaving the result as a scaffolding link whose parent is the overall categorical realization goal stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.