mul_crossEq_congr
plain-language theorem explainer
Cross-equality of ratio orbits is a congruence for multiplication: if a₁ ~ a₂ and b₁ ~ b₂ under the internal cross-multiplication relation, then a₁b₁ ~ a₂b₂. Anyone building the ordered field structure on PRC ratio orbits cites this. The proof is a two-line rewrite through the rational display: crossEq reduces to equality of toRat values, and mul is multiplicative on those displays.
Claim. Let $a_1,a_2,b_1,b_2$ be ratio orbits (signed-orbit numerator over nonzero distinction-nat denominator). If $a_1$ is cross-equal to $a_2$ and $b_1$ is cross-equal to $b_2$, then the product orbit $a_1 b_1$ is cross-equal to $a_2 b_2$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-like display: a signed orbit numerator over a nonzero distinction-nat denominator. Two such displays are related by cross-equality when $a.num \cdot b.den$ balances $b.num \cdot a.den$ as signed orbits. That relation is the internal PRC stand-in for rational equality, defined entirely on $\delta$-orbit positions (K4.10).
The verifier map toRat sends each ratio orbit to an ordinary rational. Upstream, cross-equality is characterized exactly by equality of those displays: crossEq $a$ $b$ if and only if $a.toRat = b.toRat$. Separately, multiplication of ratio orbits is compatible with the display: $(a b).toRat = a.toRat \cdot b.toRat$.
This module develops the order surface on signed and ratio orbits. Congruence of cross-equality under multiplication is the algebraic step that lets products respect the internal rational relation before order certificates are assembled.
proof idea
Term-mode rewrite proof in two steps. First rewrite the two hypotheses and the goal along crossEq_iff_toRat_eq, converting everything to equality of rational displays. Then rewrite both product displays with mul_toRat, substitute the rewritten hypotheses, and finish by ordinary equality of products in $\mathbb{Q}$. No case splits or induction.
why it matters
This is the two-sided multiplicative congruence for the internal rational relation on ratio orbits. Immediate specializations are the left and right one-sided forms (mul_crossEq_congr_left, mul_crossEq_congr_right), each obtained by pairing with reflexivity on the fixed factor.
Downstream it feeds integer_order_certificate, which packages the closed internal signed-orbit order surface (truncated subtraction, $\le$ display, absolute difference, nonnegativity flags). Without multiplicative congruence of cross-equality, the ratio-orbit layer could not carry a well-defined ordered multiplicative structure internal to PRC.
In the broader Recognition stack this sits in the foundation layer that builds integers and rationals from $\delta$-orbits before the forcing chain (T0–T8) and the J-cost calculus are attached. It is pure algebraic hygiene on the orbit displays, not a physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.