forcedAdd
plain-language theorem explainer
Forced addition on a realization's Peano carrier is ordinary LogicNat addition pulled back along the canonical orbit equivalence. Anyone showing the universal forcing map is an ordered-semiring homomorphism cites this transport. The body is a one-line Equiv conjugation: map both arguments to LogicNat, add, and map back.
Claim. For a Law-of-Logic realization $R$ and elements $a,b$ of its forced Peano carrier, forced addition is $a \oplus_R b := \Phi_R^{-1}(\Phi_R(a)+\Phi_R(b))$, where $\Phi_R$ is the canonical equivalence from that carrier onto $\mathrm{LogicNat}$.
background
Universal Forcing Part II upgrades the bare Peano isomorphism of CanonicalIso to full ordered-semiring structure. Each Law-of-Logic realization $R$ supplies a carrier, comparison cost, identity, and generator; the forced arithmetic is the Peano object extracted from that identity/step data.
LogicNat is the reference initial object: an inductive type with constructors identity (zero-cost unit) and step (one generator iterate), mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$. It already carries recovered addition, multiplication, and order from ArithmeticFromLogic. Every forced carrier folds onto LogicNat via the orbit equivalence $\Phi_R = R.\mathrm{orbitEquivLogicNat}$.
Forced constants and operations are defined by transporting the LogicNat structure along that fold. The load-bearing fact later is fold-iso compatibility: both folds are Peano homs into the initial object, hence identical.
proof idea
Pure definition by transport, not a proved theorem. Apply the orbit equivalence $\Phi_R$ to both arguments, form their sum in LogicNat (which already has +), and pull the result back by $\Phi_R^{-1}$. No tactics or lemmas fire at the definition site; downstream additivity proofs then use injectivity of $\Phi_S$ and fold-iso compatibility.
why it matters
This is the element-level addition used by the ordered-semiring certificate. Downstream, iso_map_forcedAdd proves the canonical Peano equivalence intertwines forced addition on $R$ with forced addition on $S$ ("the canonical isomorphism is a homomorphism for forced addition"). That lemma is one field of ForcedOrderedSemiringIsoCert, which packages preservation of $0$, $1$, $+$, $\times$, and $\le$ across all realizations.
Together with the earlier zero/successor uniqueness certificate, this is the arithmetic half of "forced arithmetics are canonically isomorphic as ordered commutative semirings." It sits in the Universal Forcing chain that pins the discrete arithmetic skeleton before continuum and physics layers; it does not itself invoke J-cost, $\varphi$, or the T0–T8 forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.