ratioOrbitEquiv
plain-language theorem explainer
Ratio-orbit equivalence identifies two rational orbit displays exactly when cross-multiplied numerator-denominator products balance as signed orbits. Anyone building the quotient of primitive recognition calculus (PRC) rationals cites this relation as the setoid carrier. The definition is a one-line alias of the internal cross-multiplication predicate on orbit positions.
Claim. For ratio orbits $a$ and $b$ (each a signed-orbit numerator over a nonzero distinction-nat denominator), declare $a\sim b$ when the scaled products $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ and $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$ are balanced as signed orbits.
background
In the primitive recognition calculus, a ratio orbit is the internal display of a rational: a signed orbit numerator over a nonzero distinction-nat denominator. Equality of such displays cannot be raw structural equality, because many pairs represent the same rational.
The upstream cross-multiplication predicate states that two ratio orbits are related when $a.num$ scaled by $b.den$ balances $b.num$ scaled by $a.den$ as signed orbits. That predicate is defined entirely on $\delta$-orbit positions, with no appeal to classical $\mathbb{Q}$. The present declaration simply names that relation as ratio-orbit equivalence (K4.8).
The surrounding module builds integer and rational arithmetic from orbit data before any classical embedding, so this equivalence is the native identification used later to form quotient rationals.
proof idea
One-line definitional wrapper: the relation is definitionally identical to the cross-multiplication predicate on ratio orbits. No tactics or lemmas are invoked at this site; all mathematical content lives in the body of that predicate (balance of the two scaled signed-orbit products).
why it matters
This relation is the carrier of the setoid for quotient-native PRC rationals. Downstream, it is shown to be an equivalence relation by reduction to the corresponding fact for cross-multiplication, and it is proved equivalent to equality of the classical rational displays obtained by the verifier map. Those two facts assemble the setoid whose quotient classes are the PRC rationals identified by orbit-level cross-multiplication.
In the Recognition foundation stack this is the K4.8 step that turns orbit arithmetic into a genuine rational type without smuggling classical $\mathbb{Q}$ into the definition. It sits under the integer-rational layer that later supports cost uniqueness and the forcing chain, rather than under T5--T8 directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.