realizationOrbit_equiv_logicNat
plain-language theorem explainer
Every Law-of-Logic realization induces an orbit that forms a natural-number object in the Lawvere sense, and this orbit is canonically equivalent to the arithmetic object LogicNat forced directly by the Law of Logic. Categorical logicians and foundations researchers would cite this to establish that the natural numbers are uniquely determined by the forcing axioms without presupposing Peano arithmetic. The proof is a direct one-line application of the uniqueness theorem for natural-number objects to the two NNO structures.
Claim. For any Law-of-Logic realization $R$, the orbit generated by its zero element and generator step is canonically isomorphic to the natural numbers induced by the Law of Logic: $Orbit(R) ≃ LogicNat$.
background
The module establishes the Lawvere characterization of natural numbers in the context of Universal Forcing. A natural-number object consists of a type $N$ with zero $z$ and successor $s$ such that for any pointed endomap $(X, x, f)$, there is a unique recursion map $h: N → X$ with $h z = x$ and $h ∘ s = f ∘ h$. LogicNat is the inductive type with constructors identity (zero-cost element) and step, representing the orbit {1, γ, γ², ...} under the generator. Upstream, LogicRealization supplies the carrier, cost, zero, and step for each realization, while IsNaturalNumberObject encodes the universal property. The module proves that both LogicNat and each realization's orbit satisfy this property.
proof idea
The definition applies the canonical equivalence between any two natural-number objects. It invokes IsNaturalNumberObject.equiv on the fact that the realization orbit satisfies the NNO axioms (via realizationOrbit_isNNO) and that LogicNat does (via logicNat_isNNO). This yields the isomorphism directly from the uniqueness of the recursor.
why it matters
This declaration completes the universality argument at the arithmetic level: every realization of the Law of Logic carries the same natural-number object up to canonical isomorphism. It directly supports the claim in the module documentation that the iteration object is unchanged across realizations, including the discrete Boolean case. In the Recognition Science framework, this anchors the forcing chain by showing that the natural numbers emerge identically from any Law-of-Logic structure, prior to introducing the phi-ladder or spatial dimensions. No open questions are flagged here, but it closes the gap between abstract forcing and concrete arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.