iso_map_forcedAdd
plain-language theorem explainer
Between any two Law-of-Logic realizations, the unique Peano isomorphism of forced arithmetic preserves forced addition. Anyone citing the ordered-semiring layer of Universal Forcing needs this homomorphism law. The proof reduces both sides along the fold to LogicNat and uses injectivity of that fold together with fold-iso compatibility.
Claim. Let $R$ and $S$ be Law-of-Logic realizations, and let $a,b$ lie in the carrier of the forced Peano arithmetic of $R$. Write $\Phi_{R,S}$ for the canonical universal-forcing Peano equivalence $R\to S$. Then $\Phi_{R,S}(a+_R b)=\Phi_{R,S}(a)+_S\Phi_{R,S}(b)$, where $+_R$ and $+_S$ are the forced additions transported from $\mathrm{LogicNat}$.
background
Universal Forcing Part II upgrades the bare carrier bijection of Part I to a structure-preserving map of Peano algebras, then shows that map also respects the arithmetic the Peano structure determines. Each LogicRealization supplies a carrier, a comparison cost, an identity, and a step/generator; the invariant is not the ambient carrier but the arithmetic object extracted from identity/step data.
Forced addition on a realization $R$ is defined by folding $R$'s forced Peano carrier onto the reference initial object LogicNat (which already carries recovered Add), performing addition there, and folding back. The load-bearing prior fact is fold-iso compatibility: the universal forcing isomorphism composed with $S$'s fold to LogicNat equals $R$'s fold. Both composites are Peano homomorphisms from the initial forced arithmetic of $R$ into LogicNat, so initiality forces them equal.
Universes are pinned so forced Peano carriers live in Type 0 and match LogicNat, with independent cost universes for the two realizations.
proof idea
Term/tactic hybrid, three steps. Apply injectivity of $S$'s orbit equivalence (fold) into LogicNat: it is enough that both sides agree after folding to LogicNat. Unfold the definition of forced addition on each side. The key rewrite is fold-iso compatibility, which swaps the composite (fold of $S$ after the universal forcing map) for the fold of $R$; Equiv.apply_symm_apply cancels the remaining inverse. Both sides therefore reduce to the same LogicNat sum, and injectivity finishes.
why it matters
This is one of the five element-level preservation laws that inhabit the ordered-semiring isomorphism certificate. Downstream, forcedOrderedSemiringIsoCert packages zero, one, add, mul, and order preservation; this theorem supplies the add field. Together they show the canonical map is a full ordered-commutative-semiring homomorphism at the element level, not merely a Peano zero/successor iso.
In the Recognition Science forcing chain this sits in the foundation layer that makes arithmetic itself realization-independent: once addition is forced and uniquely transported, later steps that build measures, costs, and physical constants on that arithmetic inherit a single canonical structure. The module deliberately stops short of installing a Mathlib OrderedCommSemiring instance on LogicNat; the forcing statement only needs the element-wise laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.