crossEq_symm
plain-language theorem explainer
Cross-multiplication equivalence of rational orbits is symmetric: if a balances b under cross-multiply, then b balances a. Anyone building order, reciprocal, or cost-invariance lemmas on PRC rationals cites this. The proof unfolds the definition and hands the signed-orbit balance to its already-proved symmetry.
Claim. Let $a,b$ be rational orbits (signed-orbit numerator over a nonzero distinction-nat denominator). If $a$ and $b$ are equivalent under cross-multiplication, i.e. the scaled signed orbits $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ and $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$ are balanced, then $b$ and $a$ are likewise cross-multiplication equivalent.
background
In the Primitive Recognition Calculus integer/rational layer, a rational orbit is a display with signed-orbit numerator and nonzero distinction-nat denominator (K4.7). A signed orbit is an ordered pair of distinction nats, read as pos minus neg (K4.6).
Cross-multiplication equivalence (K4.10) is the internal PRC stand-in for rational equality: two rational orbits $a,b$ satisfy it when the scaled signed orbits $a.num$ scaled by $b.den$ and $b.num$ scaled by $a.den$ are balanced. Balance itself is a symmetric relation on signed orbits; its symmetry lemma states that if $a$ balances $b$ then $b$ balances $a$.
The module builds rationals and their arithmetic entirely on $\delta$-orbit positions, without importing classical $\mathbb{Q}$ equality as primitive.
proof idea
One-step reduction. Unfold the definition of cross-multiplication equivalence on both the hypothesis and the goal; the goal becomes symmetry of signed-orbit balance on the two scaled products. Discharge by the existing signed-orbit lemma that balance is symmetric (itself just Eq.symm after unfolding balance).
why it matters
Symmetry is the workhorse that lets every later argument flip cross-equality hypotheses without re-proving balance facts. Downstream it feeds the rational-orbit trichotomy (ltQ p q ∨ crossEq p q ∨ ltQ q p), the reciprocal-factor laws (if one cross-equals a product then each factor cross-equals the reciprocal of the other), the zero-factor exclusions for units, and the mul-crossEq-one characterizations in IntegerOrder.
On the cost side it underwrites traceDisplay_eq_of_crossEq: when a map satisfies the sans-anchor hypotheses, cross-equivalent inputs yield equal trace displays, so cost observables are well-defined on PRC rational classes. That sits under the real-character factorization path used for J-cost uniqueness (T5) and the Recognition Composition Law. About forty use sites already depend on this single flip.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.