boolean_freeOrbit_isNNO
The definition establishes that the free orbit generated by the strict Boolean realization, equipped with LogicNat's identity and step, satisfies the Lawvere natural-number object axioms. Researchers in categorical foundations of arithmetic cite it to confirm that carrier collapse to two elements leaves the iteration structure unchanged. The proof is a one-line wrapper reusing the prior logicNat_isNNO result.
claimLet $N$ be the free orbit of the strict Boolean realization. Then the triple $(N, z, s)$ with $z$ the identity element and $s$ the successor map from the logic-forced naturals forms a Lawvere natural-number object: for every pointed endomap $(X, x, f)$ there exists a unique $h: N → X$ such that $h(z) = x$ and $h(s(n)) = f(h(n))$.
background
The module characterizes the natural numbers forced by the Law of Logic via the Lawvere universal property: a triple $(N, z, s)$ is a natural-number object if it is initial among pointed endomaps, so that primitive recursion exists and is unique for any target. IsNaturalNumberObject encodes this as a structure with a recursor operation plus the zero, step, and uniqueness axioms. LogicNat is the inductive type with constructors identity (zero-cost element) and step (one iteration of the generator), mirroring the orbit under multiplication by the fixed point gamma. The strict Boolean realization has carrier Bool and uses xor for composition, so its free orbit collapses the carrier to the parity image while preserving the iteration maps.
proof idea
One-line wrapper that applies logicNat_isNNO after substituting the FreeOrbit carrier of strictBooleanRealization for the N parameter.
why it matters in Recognition Science
This declaration closes the gap between continuous positive-ratio realizations and the discrete Boolean case by showing the iteration object remains the same Lawvere NNO. It directly addresses the module's stated concern that iteration-counting might be smuggled in, confirming the object is forced uniformly. The result supports the broader claim that every realization's arithmetic is a natural-number object and feeds into the universal forcing construction via NNO.
scope and limits
- Does not claim the carrier of the Boolean realization is infinite.
- Does not derive concrete arithmetic identities beyond the NNO universal property.
- Does not compare to realizations outside the strict Boolean and LogicNat cases.
- Does not address computational content or decidability of the recursor.
formal statement (Lean)
291def boolean_freeOrbit_isNNO :
292 IsNaturalNumberObject
293 (N := StrictLogicRealization.FreeOrbit strictBooleanRealization)
proof body
Definition body.
294 LogicNat.identity LogicNat.step :=
295 logicNat_isNNO
296
297end Strict.DiscreteBoolean
298
299end UniversalForcing
300end Foundation
301end IndisputableMonolith