ratioOrbitEquiv_equivalence

In the Primitive Recognition Calculus integer/rational layer, a ratio orbit (K4.7) packages a signed-orbit numerator with a nonzero distinction-nat denominator. Two such displays are identified when their cross-multiplications agree: that predicate is the content of ratio-orbit equivalence (K4.8).

The same module already proves that the underlying cross-multiplication relation is reflexive, symmetric, and transitive, and packages those three lemmas into a single Equivalence record. The present declaration simply transports that record along the definitional equality between the named ratio-orbit relation and cross-multiplication.

The local setting is foundation-level orbit arithmetic: integers and rationals are built from distinction orbits before any appeal to classical $\mathbb{Q}$ or to the $J$-cost functional.

One-line wrapper. The relation is definitionally identical to cross-multiplication on ratio orbits, so the proof applies the already-assembled equivalence record for that predicate (itself built from the three lemmas for reflexivity, symmetry, and transitivity).

This is the equivalence half of the setoid for quotient-native PRC rationals. The immediate consumer packages the relation together with this proof into a Mathlib setoid, whose quotient classes are the nonzero-denominator ratio-orbit rationals identified by cross-multiplication.

That quotient is the carrier on which later foundation material can define arithmetic and compare orbit-level rationals to the classical field. It sits upstream of cost uniqueness and the forcing chain only indirectly: it supplies the rational display language in which rung gaps, mass yardsticks, and related $\varphi$-ladder quantities are eventually stated, without yet invoking $J$, $\varphi$, or the eight-tick octave.