crossEq_equivalence

In the Primitive Recognition Calculus integer/rational layer, a ratio orbit is a display with signed-orbit numerator and nonzero distinction-nat denominator. Cross-multiplication equality says two such displays $a,b$ are related when the scaled signed orbits $a.\mathrm{num}\cdot b.\mathrm{den}$ and $b.\mathrm{num}\cdot a.\mathrm{den}$ are balanced. The doc states this is "the internal PRC rational relation, defined entirely on δ-orbit positions."

Balance of signed orbits is the underlying integer-level equality used in place of classical rational equality, so the development stays choice-free on the orbit side. Reflexivity, symmetry, and transitivity of that balance relation have already been lifted to cross-multiplication as three separate lemmas.

Term-mode Equivalence record. Fill refl by crossEq_refl (unfold and apply signed-orbit balance reflexivity), symm by crossEq_symm (balance symmetry), and trans by crossEq_trans (route through the integer bridge, cancel the nonzero middle denominator, close by linear combination). No new algebra is done here.

Packages the three cross-multiplication lemmas into a single Mathlib-style Equivalence, which is exactly what ratioOrbitEquiv_equivalence needs: that downstream theorem is a one-line application of this result. In the K4 sequence this is the bridge from K4.10 (cross-multiplication as the internal rational relation) to K4.8 ("Ratio-orbit equivalence is cross-multiplication"). It lets later PRC work treat ratio-orbit equality as a genuine equivalence without leaving the δ-orbit calculus or invoking classical choice on ℚ displays.