realizationOrbit_equiv_logicNat
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not construct an explicit bijection between the orbit and LogicNat beyond the abstract isomorphism.
- Does not extend to higher-order structures such as categories of realizations.
- Does not address computational aspects or decidability of the equivalence.
- Does not incorporate the phi-ladder or physical constants.
formal statement (Lean)
220noncomputable def realizationOrbit_equiv_logicNat (R : LogicRealization.{0, 0}) :
221 R.Orbit ≃ LogicNat :=
proof body
Definition body.
222 IsNaturalNumberObject.equiv (realizationOrbit_isNNO R) logicNat_isNNO
223
224/-- The Lawvere universality statement: any two realizations have iteration
225orbits that satisfy the natural-number-object property, hence are
226canonically equivalent. -/