IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject
The module introduces the Lawvere natural-number object as the universal property characterizing initial Peano algebras in the universal forcing setting. Researchers tracing the Recognition Science derivation of arithmetic from the forcing chain cite it when identifying forced objects across realizations. It is a definition module containing no proofs.
claimA triple $(N, z, s)$ is a Lawvere natural-number object when, for every pointed endomap $(X, x, f)$, there exists a unique morphism $h: N o X$ satisfying the recursion equations $h(z) = x$ and $h \circ s = f \circ h$.
background
The module sits inside the UniversalForcing development and imports the main theorem that any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects because those objects are initial Peano algebras. It also imports the Strict.DiscreteBoolean treatment of free iteration objects derived from the native generator.
The central definition states that a triple $(N, z, s)$ is a Lawvere natural-number object precisely when primitive recursion exists and is unique for every target pointed endomap $(X, x, f)$. The characterization makes no reference to the concrete type Nat and uses the field name recursor to avoid the reserved rec symbol.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the NNO definition used by TimeAsOrbit to claim that the temporal sequence Tick is the natural-number object forced by recognition, and by UniversalForcingSelfReference to show that the meta-theorem itself fits the Law-of-Logic structural shape, closing the reflexive loop.
scope and limits
- Does not assume a specific carrier set for N.
- Does not reference the concrete Nat type.
- Does not prove existence of such an object.
- Does not connect to the phi-ladder or mass formulas.