forcedMul
plain-language theorem explainer
Forced multiplication on the forced Peano carrier of a Law-of-Logic realization: ordinary LogicNat multiplication pulled back along the orbit equivalence. Anyone proving the canonical map is a multiplicative homomorphism cites this. The body is a three-term transport: map both factors to LogicNat, multiply, map back.
Claim. For a Law-of-Logic realization $R$ and elements $a,b$ of its forced Peano carrier, the forced product is $a \cdot_R b := \Phi_R^{-1}\bigl(\Phi_R(a)\cdot\Phi_R(b)\bigr)$, where $\Phi_R$ is the orbit equivalence from that carrier onto $\mathrm{LogicNat}$.
background
Universal Forcing Part II upgrades the canonical Peano isomorphism to an ordered-semiring isomorphism. CanonicalIso already gives a unique structure-preserving bijection of Peano algebras (zero and successor). This module transports the arithmetic that Peano structure determines: constants $0,1$, addition, multiplication, and order.
LogicNat is the reference initial object: an inductive type with constructors identity (zero-cost multiplicative unit of the orbit) and step (one generator iteration). Every realization $R$ folds its forced carrier onto LogicNat via the orbit equivalence $\Phi_R$. The forced arithmetic of $R$ is the Peano algebra extracted from $R$'s identity/step data.
Multiplication on LogicNat is already recovered in ArithmeticFromLogic. Forced multiplication is that operation transported along $\Phi_R$, so the forced carrier inherits $\times$ without inventing a new recursive definition on each realization.
proof idea
Pure definition by transport, not a tactic proof. Apply the orbit equivalence $\Phi_R$ to both arguments, multiply in LogicNat (which already carries Mul), then apply $\Phi_R^{-1}$. The noncomputable marker comes from the equivalence data, not from any search. Sibling definitions forcedZero, forcedOne, forcedAdd, and forcedLe use the same fold-and-transport pattern.
why it matters
This is the multiplication arm of the ordered-semiring layer. Downstream, iso_map_forcedMul proves the canonical universal-forcing isomorphism is a homomorphism for this operation: $\Psi(a \cdot_R b) = \Psi(a) \cdot_S \Psi(b)$. That lemma, with the parallel facts for $0,1,+$, and $\le$, assembles into ForcedOrderedSemiringIsoCert, which states that forced arithmetics of any two realizations are canonically isomorphic as ordered commutative semirings.
In the forcing chain this is the arithmetic content beyond bare Peano initiality: the operations the initiality fold determines are unique across realizations. It does not yet install a Mathlib OrderedCommSemiring instance on the carriers; the certificate is element-level homomorphism data, which is what the Universal Forcing program needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.