ForcedOrderedSemiringIsoCert
plain-language theorem explainer
Certificate structure packing five preservation laws: the canonical Peano isomorphism between forced arithmetics of any two Law-of-Logic realizations sends forced 0 to 0, forced 1 to 1, and intertwines addition, multiplication, and order. Cited by anyone using the ordered-semiring layer of Universal Forcing. Pure structure definition; the inhabitant is filled later from the iso_map_* lemmas.
Claim. A certificate asserting that for any two Law-of-Logic realizations $R$ and $S$, the canonical Peano equivalence $e_{R,S}$ between their forced arithmetics satisfies $e_{R,S}(0_R)=0_S$, $e_{R,S}(1_R)=1_S$, $e_{R,S}(a+_R b)=e_{R,S}(a)+_S e_{R,S}(b)$, $e_{R,S}(a\cdot_R b)=e_{R,S}(a)\cdot_S e_{R,S}(b)$, and $a\le_R b$ if and only if $e_{R,S}(a)\le_S e_{R,S}(b)$.
background
Universal Forcing extracts, from each Law-of-Logic realization, a forced Peano arithmetic on the orbit of the identity under the step generator. A realization supplies a carrier, a comparison cost, an identity, and a step action; the invariant target is not the ambient carrier but the arithmetic object recovered from that identity/step data.
CanonicalIso already upgrades the bare carrier bijection to a unique structure-preserving Peano isomorphism (zero and successor). This module is Part II: it transports the arithmetic that the initial object LogicNat already carries (addition, multiplication, linear order, constants 0 and 1) along each realization's fold orbitEquivLogicNat, defining forced operations on every forced carrier.
The load-bearing fact is fold-iso compatibility: composing the universal forcing map with $S$'s fold equals $R$'s fold, by initiality of Peano homomorphisms into LogicNat. Forced addition (and likewise mul, le, 0, 1) is defined by transporting the corresponding LogicNat operation along that fold.
proof idea
No proof body: this is a structure definition whose five fields are propositions. Each field quantifies over a pair of realizations $R,S$ and states that the underlying equivalence of universalForcingPeanoEquiv R S preserves one piece of ordered-semiring data (forced zero, one, add, mul, or le). Inhabitation is deferred to a separate definition that plugs in the five iso_map_forced* lemmas.
why it matters
Closes the ordered-semiring layer of Universal Forcing. Together with the earlier Peano certificate (zero/successor preservation and uniqueness), it states that forced arithmetics are canonically isomorphic as ordered commutative semirings across all realizations. The sole downstream consumer is the inhabitant forcedOrderedSemiringIsoCert, which fills every field from the corresponding iso_map_* lemma.
In the Recognition framework this is foundation infrastructure, not a physics constant: it guarantees that arithmetic extracted from any Law-of-Logic realization is the same ordered semiring, so later forcing steps (T0–T8 chain, J-cost uniqueness, phi fixed point) do not depend on a choice of realization. Scope note from the module: the certificate is element-level homomorphism content; it does not install a Mathlib OrderedCommSemiring instance on LogicNat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.