iso_map_forcedMul
plain-language theorem explainer
Between any two logic realizations, the canonical universal-forcing Peano equivalence preserves forced multiplication on the forced arithmetic carriers. Cite this when assembling the ordered-semiring layer of Universal Forcing (Part II). The proof injects through the target realization's fold to LogicNat and discharges by fold-isomorphism compatibility plus Equiv algebra.
Claim. For logic realizations $R$ and $S$, and elements $a,b$ of the forced Peano carrier of $R$, if $\Phi_{R,S}$ is the canonical universal-forcing Peano equivalence, then $\Phi_{R,S}(a \cdot_R b) = \Phi_{R,S}(a) \cdot_S \Phi_{R,S}(b)$, where $\cdot_R$ and $\cdot_S$ are the multiplications transported along each realization's fold to $\mathrm{LogicNat}$.
background
Universal Forcing Part II upgrades the bare carrier bijection of CanonicalIso to arithmetic structure. Each LogicRealization supplies a carrier, comparison cost, identity, and step action; the invariant is not the ambient carrier but the arithmetic object extracted from identity/step data. Forced arithmetic on a realization is obtained by folding its Peano surface onto the reference initial object LogicNat (which already carries recovered Add, Mul, and order from ArithmeticFromLogic) and transporting the operations back.
Forced multiplication is that transport: multiply after folding both arguments to LogicNat, then fold back. The load-bearing prior fact is fold-isomorphism compatibility: composing the universal forcing isomorphism with $S$'s fold equals $R$'s fold. Both maps are Peano homomorphisms from the initial forced arithmetic of $R$ into LogicNat, so initiality forces them equal. Carriers are pinned to Type 0 so they match LogicNat and initiality uniqueness typechecks.
proof idea
Short tactic proof. Apply injectivity of $S$'s orbit equivalence into LogicNat (so it suffices to check equality after folding both sides). Then simp with the definition of forced multiplication, fold-isomorphism compatibility, and the standard Equiv identity that applying an equivalence after its inverse cancels. Both sides reduce to the same LogicNat product of the folded images, so equality follows. No induction on the Peano carrier is needed; initiality is already packaged in the fold-compatibility lemma.
why it matters
This is the multiplicativity clause of the element-level ordered-commutative-semiring content for the canonical map. Downstream it is wired directly into forcedOrderedSemiringIsoCert as preserves_mul, alongside the sibling facts for zero, one, addition, and order. Together those inhabit the certificate that the universal forcing isomorphism is a full ordered-semiring homomorphism between forced arithmetic carriers.
In the Recognition Science forcing program this sits after the Peano-algebra uniqueness of CanonicalIso and before any claim that distinct realizations share one arithmetic. It does not itself invoke the T0–T8 chain, J-cost uniqueness, or the eight-tick octave; those live upstream in the foundation stack that justifies why realizations exist. The open enrichment left explicit by the module is bundling LogicNat as a Mathlib OrderedCommSemiring instance, which is deliberately out of scope here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.