strict_universal_forcing_peanoEquiv
plain-language theorem explainer
Any two strict Law-of-Logic realizations induce a structure-preserving Peano isomorphism between their forced arithmetics: zero maps to zero and successor commutes. Cite this when transporting arithmetic statements across strict realizations without choosing an orbit by hand. The construction is a one-line reduction through the strict-to-lightweight functor into the existing lightweight universal-forcing Peano equivalence.
Claim. For any two strict Law-of-Logic realizations $R$ and $S$, there is a Peano-algebra equivalence between the forced arithmetic of $R$ and that of $S$: the underlying bijection sends zero to zero and intertwines the successor operations.
background
A strict logic realization packages only native comparison, composition, identity, invariance, and non-triviality data. Its arithmetic is derived from that law data, not supplied by the caller. The forced arithmetic carries a Peano algebra structure (zero and successor).
The sibling module on strict invariance already builds a bare bijection between the forced arithmetics of any two strict realizations. The lightweight Universal Forcing layer supplies a structure-preserving Peano equivalence universalForcingPeanoEquiv between forced arithmetics of lightweight realizations, together with uniqueness of such equivalences.
This module sits on the strict surface and reuses those lightweight results via the strict-to-lightweight forgetful map. The local goal is to upgrade the bare strict bijection to a unique structure-preserving Peano isomorphism forced entirely by the native law data.
proof idea
One-line wrapper. Forget each strict realization $R,S$ along StrictLogicRealization.toLightweight, then apply the lightweight constructor universalForcingPeanoEquiv to the resulting pair. The return type is already a PeanoEquiv between the forced Peano algebras, so no further transport is needed.
why it matters
In the Recognition foundation stack, universal forcing says that arithmetic is not an extra choice: once the Law-of-Logic data are fixed, the Peano structure is determined up to unique structure-preserving isomorphism. This definition is the strict-surface form of that claim: no escape hatch, no caller-supplied orbit.
It feeds the uniqueness statement in the same module (any two structure-preserving isomorphisms of the forced arithmetics agree on the underlying function) and the certificate packaging that records strict canonicality. Downstream, that uniqueness is what lets later forcing-chain steps treat the arithmetic of any strict realization as interchangeable without bookkeeping on labels.
Relative to the primer landmarks, this is pure foundation infrastructure under the T0–T8 forcing chain: it secures that the arithmetic substrate on which later steps (J-uniqueness, $\varphi$, eight-tick period, $D=3$) sit is canonically identified across strict realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.