iso_map_forcedOne
plain-language theorem explainer
Between any two Law-of-Logic realizations, the unique Peano isomorphism of universal forcing sends the forced multiplicative unit of the source to that of the target. Anyone citing the ordered-semiring layer of universal forcing needs this unit-preservation fact. The proof is a short injectivity argument: both sides fold to the same LogicNat one via fold-iso compatibility.
Claim. For any two Law-of-Logic realizations $R$ and $S$, if $\Phi_{R,S}$ is the canonical Peano isomorphism of universal forcing, then $\Phi_{R,S}(1_R)=1_S$, where $1_R$ and $1_S$ are the forced multiplicative units transported from the initial Peano object along each realization's fold to $\mathrm{LogicNat}$.
background
A Law-of-Logic realization supplies a carrier, a comparison cost, an identity element, and a step/generator action. Universal forcing extracts from that data a Peano algebra and a unique structure-preserving isomorphism between any two such algebras. The prior module upgraded the bare carrier bijection to a Peano isomorphism respecting zero and successor.
This module lifts that map to the arithmetic the Peano structure determines. Each realization folds canonically onto the reference initial object $\mathrm{LogicNat}$ via its orbit equivalence. Arithmetic ($0$, $1$, $+$, $\times$, $\le$) is recovered on $\mathrm{LogicNat}$ and transported back along the fold, yielding the forced constants and operations on each carrier.
The load-bearing fact is fold-iso compatibility: composing the universal forcing isomorphism with $S$'s fold equals $R$'s fold. Both composites are Peano homomorphisms from the initial forced arithmetic of $R$ into $\mathrm{LogicNat}$, so initiality forces them equal. Unit preservation is one of the elementary consequences.
proof idea
Term-mode proof by injectivity of $S$'s fold $\mathrm{orbitEquivLogicNat}$. After unfolding the definition of the forced one on both sides, fold-iso compatibility rewrites the image of the source unit under the composite fold, and the standard equivalence identity $\mathrm{apply}\circ\mathrm{symm}=\mathrm{id}$ cancels the remaining inverse. Both sides therefore agree after folding into $\mathrm{LogicNat}$, hence agree on the carrier of $S$.
why it matters
Unit preservation is one of the five element-level clauses that inhabit the ordered-semiring isomorphism certificate. That certificate packages zero, one, addition, multiplication, and order preservation for the canonical map, completing the arithmetic layer of universal forcing beyond bare Peano structure.
In the Recognition Science forcing chain this sits in the foundation: the unique Peano isomorphism is forced to be a full ordered-commutative-semiring homomorphism at the element level, so the arithmetic recovered from identity and step data is realization-independent. Downstream work that treats the forced carrier as an ordered semiring cites the certificate, which in turn cites this lemma for the $1\mapsto 1$ clause.
The module deliberately stops short of installing a Mathlib OrderedCommSemiring instance on the carriers; the forcing statement only needs the elementwise homomorphism facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.