IndisputableMonolith.Foundation.UniversalForcing.Strict.MathlibNNO
This module bridges the strict categorical realization of LogicNat to Mathlib's CategoryTheory API. It certifies that LogicNat satisfies the universal property of a natural number object. Category theorists and formalists working on Peano surfaces in categorical foundations would cite the bridge. The module consists of imports from CategoricalMathlib plus targeted declarations linking the two systems.
claimLogicNat satisfies the NNO universal property: for any object $X$ equipped with $0:1\to X$ and $s:X\to X$ there is a unique morphism $f:\text{LogicNat}\to X$ commuting with the structure maps.
background
Recognition Science realizes its universal forcing on the canonical LogicNat Peano surface via the strict categorical construction in UniversalForcing.Strict. The upstream CategoricalMathlib module supplies the instantiation but deliberately omits Mathlib's CategoryTheory API.
This module imports Mathlib.CategoryTheory.Category.Basic together with CategoricalMathlib. It supplies the missing link so that LogicNat can be treated as an NNO inside Mathlib's category-theoretic framework.
proof idea
This is a bridging module. It imports the categorical realization and Mathlib's basic category theory, then declares the NNO universal property and its certification for LogicNat. No internal proof bodies appear at module level; the work is carried by the sibling declarations logicNat_has_type_NNO_universal_property and MathlibNNOCert.
why it matters in Recognition Science
The module supplies Mathlib-compatible NNO certification for the LogicNat surface, enabling downstream use of standard category-theory tooling inside the universal forcing chain. It directly supports the sibling results logicNat_NNO_uniqueness and mathlibNNOCert_holds, closing the interface between the custom strict realization and Mathlib.
scope and limits
- Does not redefine LogicNat or the Peano axioms.
- Does not prove the NNO property itself; that is left to sibling declarations.
- Does not import further Mathlib category-theory components beyond Category.Basic.
- Does not address non-strict or other categorical realizations.