strict_universal_forcing
plain-language theorem explainer
Any two strict realizations of the law of logic induce canonically equivalent Peano carriers in their derived arithmetic structures. Researchers working on invariance within the universal forcing chain would cite this when showing that native law data fixes a unique free orbit. The definition is a one-line wrapper that applies the equivalence of initial Peano objects.
Claim. For any two strict logic realizations $R$ and $S$, the carrier of the Peano object in the arithmetic forced by $R$ is canonically equivalent to the carrier of the Peano object in the arithmetic forced by $S$.
background
ArithmeticOf is the structure consisting of a Peano object together with a proof that the object is initial, forced by any logic realization. StrictLogicRealization supplies a lightweight realization from which the arith extraction produces an ArithmeticOf instance. The natural equivalence between two initial Peano objects is constructed by composing the lift maps supplied by their initiality, as defined in equivOfInitial.
proof idea
The definition is a one-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic structures extracted from the two input strict realizations.
why it matters
This definition realizes the strict universal forcing claim that native law-of-logic data determines a derived free orbit and all such orbits are canonically equivalent. It supplies the invariance step required by the universal forcing theorem in the Recognition Science framework. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.