IndisputableMonolith.Foundation.UniversalForcing.Strict.MathlibNNO
This module bridges the LogicNat Peano surface from the strict categorical realization to Mathlib's CategoryTheory API, confirming that LogicNat carries the universal property of a natural number object. Category theorists and formalists connecting custom arithmetic constructions to the Mathlib standard library would cite it. The structure consists of targeted imports from CategoricalMathlib plus the basic category theory primitives to expose the NNO interface.
claimLogicNat satisfies the NNO universal property: given any object $X$ equipped with $z:1→ X$ and $s:X→ X$ there is a unique morphism $f$ from LogicNat to $X$ commuting with the zero and successor maps.
background
The module lives inside Foundation.UniversalForcing.Strict and imports Mathlib.CategoryTheory.Category.Basic together with IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib. The upstream CategoricalMathlib doc-comment states that it instantiates the strict categorical realization on the canonical LogicNat Peano surface and shows that LogicNat has the universal property of a natural number object in the appropriate sense. No new definitions are introduced; the module supplies the Mathlib-compatible wrapper around that prior instantiation.
proof idea
This is a bridge module, no proofs. It consists of the two listed imports that make the NNO universal property available under Mathlib's CategoryTheory namespace.
why it matters in Recognition Science
The module supplies the Mathlib NNO interface required by the sibling declarations logicNat_has_type_NNO_universal_property, logicNat_NNO_uniqueness, MathlibNNOCert and mathlibNNOCert_holds. It thereby connects the strict forcing construction to standard categorical tools inside the Recognition Science foundation layer.
scope and limits
- Does not contain any theorem proofs or sorry placeholders.
- Does not import the full Mathlib category theory library beyond Basic.
- Does not address NNO uniqueness (left to sibling logicNat_NNO_uniqueness).
- Does not treat higher categorical structures or enriched categories.