mul_crossEq_congr_left
plain-language theorem explainer
Left-multiplication by a fixed ratio orbit preserves cross-equality: if two ratio orbits agree under cross-multiplication, so do their products with any common right factor. Order and rational-arithmetic developments in the primitive recognition calculus cite this when transporting equalities through multiplication. The proof is a one-line specialization of the two-sided mul congruence via reflexivity on the right factor.
Claim. Let $a_1,a_2,b$ be ratio orbits (signed-orbit numerator over nonzero distinction-nat denominator). If $a_1$ and $a_2$ are cross-equal, i.e. $a_1.\mathrm{num}\cdot a_2.\mathrm{den}$ balances $a_2.\mathrm{num}\cdot a_1.\mathrm{den}$ as signed orbits, then $a_1\cdot b$ is cross-equal to $a_2\cdot b$.
background
In the primitive recognition calculus, a ratio orbit is an integer-style rational display: a signed orbit numerator over a nonzero distinction-nat denominator. Cross-equality is the internal PRC rational relation (K4.10): two ratio orbits are equivalent when the cross-multiplied signed orbits balance, i.e. $a.\mathrm{num}$ scaled by $b.\mathrm{den}$ balances $b.\mathrm{num}$ scaled by $a.\mathrm{den}$. This relation is defined entirely on $\delta$-orbit positions and matches rational equality of the verifier displays.
Multiplication of ratio orbits is the corresponding orbit-level product. The two-sided lemma mul_crossEq_congr already states that cross-equality is a congruence for that product in both factors. The present result is the left-only specialization used when the right factor is held fixed.
The surrounding IntegerOrder module builds the signed-orbit order surface (reflexivity, transitivity, trichotomy, sign flags) on top of these rational displays.
proof idea
One-line wrapper. Apply the two-sided congruence mul_crossEq_congr to the given left hypothesis ha : crossEq a₁ a₂ and to crossEq_refl b on the right factor. No rewriting or case analysis is needed; the goal is exactly the instance returned by that application.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (truncated subtraction, $\le$ display, absolute difference, nonnegativity flags). Congruence of cross-equality under multiplication is part of making ratio-orbit arithmetic compatible with that order surface, so equalities can be transported through products without leaving the $\delta$-orbit language.
Within Recognition Science foundation work this sits in the pre-physics arithmetic layer that underwrites later forcing-chain material (J-cost uniqueness, $\phi$, eight-tick structure). It does not itself touch T5–T8; it is bookkeeping that keeps the integer/rational order certificate self-contained.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.