IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject
Defines Lawvere natural-number objects as triples (N, z, s) with unique primitive recursion into any pointed endomap. Shows forced arithmetic of Logic realizations is such an NNO (initial among Peano algebras), and that the free orbit of the strict Boolean generator is an NNO. Universal Forcing follows: any two realizations yield canonically equivalent arithmetic. Self-reference imports this package.
claimA triple $(N, z, s)$ is a Lawvere natural-number object when for every pointed endomap $(X, x_0, f)$ there is a unique $r: N \to X$ with $r(z)=x_0$ and $r\circ s = f\circ r$. Forced arithmetic orbits of Logic realizations satisfy this property; the free iteration object of the strict Boolean generator is an NNO. Hence any two realizations have canonically equivalent forced arithmetic.
background
Universal Forcing asserts that any two Law-of-Logic realizations have canonically equivalent forced arithmetic, because those objects are initial Peano algebras. This module supplies the categorical language for that claim: Lawvere natural-number objects, characterized solely by a universal property and without reference to the ambient Nat type.
A Lawvere NNO is a triple $(N,z,s)$ such that for every target pointed endomap $(X,x,f)$ there exists a unique recursor $r:N\to X$ intertwining zero and successor. That is exactly the universal property any Peano structure must satisfy; the field name avoids Lean’s reserved structure recursor.
The strict Boolean realization supplies a concrete test case. Its carrier orbit is periodic inside Bool, but the forced arithmetic is the free iteration object generated by the native Boolean generator, not the finite image. The module compares that free orbit with the abstract Logic-native natural object.
proof idea
Definition-first module. It introduces the NNO structure (unique recursor into every pointed endomap), a forgetful map to Peano data, and an initiality lemma. It then proves the Logic-native natural object is an NNO, that realization orbits are equivalent to it, and packages Universal Forcing as initiality of that NNO. A parallel track shows the free orbit of the strict Boolean generator is an NNO, with parity/interpretation lemmas collapsing Boolean iteration onto that free object. No single master tactic proof; the argument is a chain of structure instances and equivalence lemmas.
why it matters in Recognition Science
This is the categorical spine of Universal Forcing: forced arithmetic is initial among Peano algebras, so any two Logic realizations have canonically equivalent arithmetic objects. Downstream, UniversalForcingSelfReference imports the package to show the meta-theorem itself fits the Law-of-Logic structural shape, closing the framework reflexively.
In the broader Recognition foundation, initiality of the forced NNO is what makes arithmetic (and later the forcing chain toward phi, the eight-tick octave, and D=3) independent of which concrete Logic carrier one starts from. The Boolean free-orbit instance shows the result is not vacuous: even a periodic propositional carrier yields the same free arithmetic object once one takes the strict generator orbit rather than the finite image.
scope and limits
- Does not construct the full Peano axioms from physics postulates; it only packages the NNO universal property.
- Does not identify the NNO with Lean’s native Nat beyond the stated equivalences.
- Does not treat non-strict or continuous carriers outside the DiscreteBoolean track.
- Does not derive mass, alpha, or geometric forcing steps; those sit further down the chain.
- Does not claim uniqueness of the Logic realization itself, only of its forced arithmetic up to canonical equivalence.