boolean_freeOrbit_isNNO
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.