mul_respects_cross
plain-language theorem explainer
Cross-equivalence of ratio orbits is a congruence for multiplication: if a₁ ~ a₂ and b₁ ~ b₂ under cross-multiplication, then a₁b₁ ~ a₂b₂. Anyone building the PRC rational field cites this to descend orbit multiplication to the quotient. The proof rewrites to integer cross-products and closes by a two-term linear combination of the hypotheses.
Claim. Let $a_1,a_2,b_1,b_2$ be ratio orbits (each a signed-orbit numerator over a nonzero distinction-nat denominator). If $a_1$ is cross-equivalent to $a_2$ and $b_1$ is cross-equivalent to $b_2$, then the product orbits $a_1 b_1$ and $a_2 b_2$ are cross-equivalent.
background
In the Primitive Recognition Calculus, a ratio orbit is a display of a rational: a signed orbit as numerator and a nonzero distinction-nat as denominator. Two such displays are identified by cross-equivalence: $a$ and $b$ are related when the scaled signed orbits $a.num\cdot b.den$ and $b.num\cdot a.den$ are balanced. That relation is the internal PRC stand-in for rational equality, defined entirely on $\delta$-orbit positions.
The choice-free hub is the integer characterization: cross-equivalence holds iff the integer cross products agree, $a.num.toInt\cdot b.den.toNat = b.num.toInt\cdot a.den.toNat$. Unlike the $\mathbb{Q}$-display bridge, this stays in $\mathbb{Z}$ and needs only propext and Quot.sound. Multiplication of ratio orbits is defined componentwise from signed-orbit multiplication and distinction-nat multiplication; the recovery maps $toInt$ and $toNat$ intertwine those with ordinary integer and natural multiplication.
proof idea
Rewrite both hypotheses and the goal through the integer cross-product characterization. Unfold ratio-orbit multiplication, then simplify the resulting integer expressions with the recovery lemmas for signed-orbit multiplication and distinction-nat multiplication, followed by push_cast. The goal becomes an equality of integer bilinear forms in the four cross products; it is discharged by linear_combination of the two rewritten hypotheses, with coefficients built from the opposite factors' numerator and denominator integers.
why it matters
This is the congruence lemma that lets multiplication descend to PRC rationals. The parent definition (K4.11) builds mul : PRCRat → PRCRat → PRCRat by Quot.lift₂ on ratio-orbit multiplication; both well-definedness obligations are exactly instances of this theorem (one factor fixed by reflexivity of cross-equivalence). Without it, the quotient carrier cannot inherit a multiplication from the orbit level.
In the broader foundation stack, PRC rationals sit above integers-from-logic and arithmetic-from-logic, supplying the rational layer that later feeds mass ladders and coupling constants. The lemma is pure algebraic bookkeeping on the forcing chain's number system, not a physics claim, but it is load-bearing for every downstream rational operation stated on the quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.