universal_forcing_via_NNO
plain-language theorem explainer
Any two logic realizations induce canonically equivalent iteration orbits because each orbit satisfies the Lawvere natural-number-object axioms. Foundation researchers in Recognition Science cite this to establish that forced arithmetic remains invariant across carriers. The definition is a one-line wrapper applying the uniqueness of NNO morphisms to the orbit structures of the two realizations.
Claim. For any two logic realizations $R$ and $S$, the iteration orbits $R.Orbit$ and $S.Orbit$ are canonically equivalent as natural-number objects.
background
The module develops the categorical foundation for arithmetic forced by the Law of Logic using Lawvere's natural-number-object characterization. A natural-number object is a triple $(N, z, s)$ such that for any triple $(X, x, f)$ there exists a unique map $h: N → X$ satisfying $h z = x$ and $h ∘ s = f ∘ h$. This is the statement that $N$ is the initial pointed endomap algebra. LogicNat is the inductive type with constructors identity (the zero-cost element, the multiplicative identity in the orbit) and step (one more iteration of the generator), serving as the smallest subset of positive reals closed under multiplication by the generator and containing 1. Upstream results establish that LogicNat itself forms such an object and that each realization's orbit inherits this structure via the realization orbit NNO construction.
proof idea
The definition is a one-line wrapper that invokes the equivalence constructor from the natural-number-object interface on the two realization-specific NNO structures. It relies directly on the uniqueness clause in the Lawvere definition to produce the canonical isomorphism between the orbits.
why it matters
This supplies the canonical comparison between forced arithmetic objects of any two realizations, which is reified as meta-forced-arithmetic-invariance in the self-reference module and used to prove the meta-meta-theorem. It confirms that the structure of the invariance is preserved under self-application. In the Recognition framework it shows the forced natural numbers are independent of realization choice, aligning with the universality of the forcing chain from the Law of Logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.