mul_crossEq_congr_right
plain-language theorem explainer
Left multiplication by a fixed ratio orbit preserves cross-equivalence of the right factors. Anyone building the internal order or field laws on PRC ratio orbits cites this congruence. The proof is a one-line specialization of two-sided multiplication congruence, feeding reflexivity on the left factor.
Claim. Let $a,b_1,b_2$ be ratio orbits (signed-orbit numerator over nonzero distinction-nat denominator). If $b_1$ and $b_2$ are cross-equivalent, i.e. $b_1.\mathrm{num}\cdot b_2.\mathrm{den}$ balances $b_2.\mathrm{num}\cdot b_1.\mathrm{den}$ as signed orbits, then $a\cdot b_1$ is cross-equivalent to $a\cdot b_2$.
background
In the Primitive Recognition Calculus integer layer, a ratio orbit is a display of a rational: a signed orbit numerator over a nonzero distinction-nat denominator (K4.7). Cross-equivalence is the internal rational equality relation: two ratio orbits match when the cross-multiplied signed orbits balance (K4.10), equivalently when their verifier rational displays agree.
Multiplication of ratio orbits is defined so that it matches ordinary rational multiplication on those displays. The two-sided lemma already states that if both factors are replaced by cross-equivalent partners, the products remain cross-equivalent. The present statement is the right-factor specialization used when the left multiplier is held fixed.
Local setting is the IntegerOrder module, which closes the signed-orbit order surface and the algebraic laws needed for an internal ordered field of ratio orbits.
proof idea
One-line wrapper. Apply the two-sided congruence mul_crossEq_congr to the pair of left factors $(a,a)$ and the given right factors $(b_1,b_2)$, supplying reflexivity of cross-equivalence on $a$ via crossEq_refl and the hypothesis on the right pair. No separate rewriting is needed here; the parent lemma already reduces through crossEq_iff_toRat_eq and mul_toRat.
why it matters
Feeds the integer-order certificate that declares the internal signed-orbit order surface closed, and is used by the reciprocal-pair commutation lemma that relates products of nonzero ratio orbits and their reciprocals back to the unit under cross-equivalence. Without right-congruence of multiplication, the ratio-orbit monoid cannot be treated as well-defined on cross-equivalence classes, blocking the ordered-field fragment of PRC.
This sits in the foundation layer beneath the forcing chain: ratio orbits and their cost displays are the discrete substrate on which J-cost uniqueness (T5) and the self-similar fixed point $\varphi$ (T6) are later read. It does not itself force $\varphi$ or the eight-tick octave; it only keeps the rational arithmetic coherent so those later steps can quote a clean ordered structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.