crossEq_trans
plain-language theorem explainer
Cross-multiplication equivalence of ratio orbits is transitive. Anyone assembling the PRC rational field, proving recip/mul laws, or showing cost displays respect rational equality will cite this. The proof rewrites to integer cross-products, cancels the nonzero middle denominator, and closes by linear combination, staying choice-free in ℤ.
Claim. Let $a$, $b$, and $c$ be ratio orbits (each a signed-orbit numerator over a nonzero distinction-nat denominator). If the cross-multiplication relation holds between $a$ and $b$ and between $b$ and $c$, then it holds between $a$ and $c$.
background
In the Primitive Recognition Calculus, a ratio orbit is the internal stand-in for a rational: a signed orbit as numerator and a nonzero distinction-nat as denominator. Two such displays are related by cross-multiplication when the scaled signed orbits $a.num$ by $b.den$ and $b.num$ by $a.den$ are balanced. That relation is the PRC-native equality of rationals, defined entirely on $\delta$-orbit positions rather than on Mathlib's $\mathbb{Q}$.
The choice-free hub is the integer bridge: cross-multiplication holds if and only if the integer cross products agree, $a.num.toInt \cdot b.den.toNat = b.num.toInt \cdot a.den.toNat$. Unlike the $\mathbb{Q}$-display characterization, this route depends only on propositional extensionality and quotient soundness, not Classical.choice. Transitivity is the remaining equivalence axiom needed before quotienting or transporting structure along the relation.
proof idea
Rewrite both hypotheses and the goal through the integer characterization of cross-multiplication. The middle denominator's verifier Nat is nonzero as an integer (from the ratio-orbit denominator invariant, discharged by omega). Cancel that nonzero factor on the right via the integer cancellation lemma, then close the resulting bilinear identity by linear combination of the two cross-product equalities, weighted by the outer denominators. The comment in the proof flags the design choice: stay on the ℤ bridge so the argument never invokes Classical.choice.
why it matters
This is the transitivity leg of the cross-multiplication equivalence relation on ratio orbits; the sibling equivalence package packages it with reflexivity and symmetry. Downstream, IntegerOrder leans on it heavily for reciprocal and multiplication laws (reciprocal preserves the relation; products of pairs with their reciprocals are cross-equivalent to one when neither factor is zero). Cost-side consumers include equality of trace displays under cross-equivalence for sans-anchor maps, and the strengthened native-cost uniqueness target in PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved. Within the Recognition foundation it keeps rational arithmetic internal to orbit data, so later J-cost and ladder constructions can treat rationals without leaving the choice-light fragment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.