ratioOrbitEquiv_iff_toRat_eq
plain-language theorem explainer
Two ratio-orbit displays are equivalent under cross-multiplication if and only if their verifier rationals agree. Anyone building the PRC rational quotient or proving injectivity of the display map cites this bridge. The proof is a one-line alias of the already-proved cross-multiplication characterization.
Claim. For ratio orbits $a,b$ (signed-orbit numerator over a nonzero distinction-nat denominator), cross-multiplication equivalence $a\sim b$ holds if and only if the verifier displays agree: $a^{\mathbb{Q}}=b^{\mathbb{Q}}$, where $q^{\mathbb{Q}}=(\mathrm{num}\,q)^{\mathbb{Z}}/(\mathrm{den}\,q)^{\mathbb{N}}\in\mathbb{Q}$.
background
In the Primitive Recognition Calculus integer/rational layer, a ratio orbit is a display pair: a signed orbit numerator and a nonzero distinction-nat denominator (K4.7). The verifier map sends such a pair to an ordinary rational by casting numerator to $\mathbb{Z}$ and denominator to $\mathbb{N}$ and dividing.
Equivalence of ratio orbits is defined as cross-multiplication of those integer displays (K4.8), not as equality of pairs. The upstream lemma crossEq_iff_toRat_eq already shows that this cross-multiplication predicate is exactly equality of the verifier rationals, via balanced signed-orbit equality and scaling-by-nat identities on the integer casts.
This module sits under the foundation path that reconstructs $\mathbb{Q}$ from orbit arithmetic so that PRC cost can later be lifted to a quotient of ratio orbits.
proof idea
One-line term wrapper. Unfolding the definition of ratio-orbit equivalence as cross-multiplication, the claim is identical to the upstream theorem that cross-multiplication holds iff the two toRat displays agree. Apply that theorem to the two ratio orbits and stop.
why it matters
This is the setoid bridge tagged K4.8: it identifies the internal cross-multiplication relation with equality of verifier rationals, so the quotient of ratio orbits is well-defined as PRC-native rationals. Downstream, injectivity of the display on that quotient uses the equivalence direction, and the lift of PRC $J$-cost to the rational quotient (onPRCRat) relies on the same agreement to show the cost is constant on equivalence classes.
In the broader Recognition stack this is bookkeeping, not a forcing step: it does not invoke T5–T8 or the RCL. It does close the transport path (spec A5) from orbit arithmetic to ordinary $\mathbb{Q}$, which later hosts mass-ladder and cost uniqueness arguments that need a field of scalars built inside PRC rather than assumed from Mathlib alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.