iso_map_forcedLe
plain-language theorem explainer
The canonical Peano isomorphism between forced arithmetics of any two Law-of-Logic realizations preserves and reflects the forced order relation. Anyone assembling the ordered-semiring layer of universal forcing cites this. The proof is a one-line simplification through the definition of forced order and fold-compatibility with LogicNat.
Claim. For any two Law-of-Logic realizations $R$ and $S$, and any $a,b$ in the forced Peano carrier of $R$, one has $a \le_R b$ if and only if $\Phi_{R,S}(a) \le_S \Phi_{R,S}(b)$, where $\Phi_{R,S}$ is the canonical universal-forcing Peano equivalence from $R$ to $S$.
background
A Law-of-Logic realization supplies a carrier, a comparison cost, an identity, and a step/generator action. Universal Forcing extracts from that data a forced Peano arithmetic: the initial object recovered by folding the realization's orbit onto the reference initial Peano algebra LogicNat, which already carries addition, multiplication, and a linear order.
This module upgrades the bare Peano isomorphism of CanonicalIso to the full ordered-semiring layer. Constants $0,1$, addition, multiplication, and the order $\le$ are defined on each forced carrier by transport along the fold to LogicNat. The forced order on a realization $R$ is therefore the pullback of the order on LogicNat along $R$'s fold.
The single load-bearing fact is fold-compatibility: composing the universal-forcing Peano equivalence $R\to S$ with $S$'s fold equals $R$'s fold. Both composites are Peano homomorphisms out of an initial object into LogicNat, so initiality forces them equal. Order preservation is then pure transport along that commuting triangle.
proof idea
One-line term proof by simplification. Unfold the definition of forced order on both sides; each side becomes the order comparison of the two images under the corresponding fold into LogicNat. Apply fold-compatibility to replace $S$'s fold composed with the universal-forcing equivalence by $R$'s fold. The two sides become identical, so the biconditional is reflexive.
why it matters
This is the order leg of the ordered-commutative-semiring content of universal forcing. Downstream it is packaged into the ordered-semiring isomorphism certificate, which records that for any two realizations the canonical map preserves $0$, $1$, $+$, $\times$, and $\le$. Together with the earlier Peano-iso certificate (zero/successor preservation and uniqueness), that certificate states that forced arithmetics are canonically isomorphic as ordered commutative semirings across all realizations.
In the Recognition Science forcing chain this sits in the foundation layer that makes arithmetic itself realization-independent: the invariant is not the ambient carrier but the ordered-semiring structure extracted by initiality. The module deliberately stops short of installing a Mathlib OrderedCommSemiring instance on LogicNat; the element-level homomorphism facts are what the forcing statement needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.