IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject
This module supplies the Lawvere natural-number object as the universal property characterizing initial Peano algebras in any LogicRealization. Researchers formalizing time as forced orbits or closing the forcing meta-theorem under self-reference cite it to equate arithmetic objects across realizations. The module consists of structure definitions and uniqueness lemmas that translate the abstract recursion property into the Recognition setting without referencing concrete Nat.
claimA Lawvere natural-number object is a triple $(N, z, s)$ such that for every pointed endomap $(X, x, f)$ there exists a unique morphism $h : N → X$ with $h(z) = x$ and $h ∘ s = f ∘ h$.
background
Universal Forcing states that any two Law-of-Logic realizations yield canonically equivalent forced arithmetic objects because those objects are initial Peano algebras. The module imports the strict discrete Boolean realization, where the carrier orbit remains periodic while the arithmetic component is the free iteration object generated by the native successor rather than any finite image inside Bool. The Lawvere characterization is introduced precisely to capture this initiality: primitive recursion exists and is unique for every target pointed endomap, making no reference to the concrete type Nat.
proof idea
This is a definition module, no proofs. It declares the IsNaturalNumberObject structure, constructs the toPeano map, and supplies the supporting lemmas isInitial, logicNat_isNNO, and realizationOrbit_equiv_logicNat that establish the universal property.
why it matters in Recognition Science
The module feeds TimeAsOrbit, which identifies the temporal sequence Tick as the canonical natural-number object forced by recognition under successor, and UniversalForcingSelfReference, which shows the meta-theorem itself fits the Law-of-Logic structural shape. It thereby supplies the initial-algebra step required for reflexive closure of the forcing theorem.
scope and limits
- Does not construct an explicit NNO inside any concrete LogicRealization.
- Does not derive the successor or zero from the J-cost or phi-ladder.
- Does not address numerical values of constants such as phi or alpha.
- Does not prove uniqueness of the NNO up to isomorphism beyond the stated lemmas.