mk_eq_mk_of_crossEq
plain-language theorem explainer
Cross-equivalent ratio orbits (balanced cross-products of signed numerators and nonzero orbit denominators) determine the same PRC rational. Anyone building the field structure on PRC rationals cites this as the quotient well-definedness step. The proof is the one-line application of quotient soundness to the cross-equality relation.
Claim. If $a$ and $b$ are ratio orbits (signed-orbit numerator over a nonzero distinction-nat denominator) and the cross-multiplication relation holds—i.e. $a.\mathrm{num}\cdot b.\mathrm{den}$ balances $b.\mathrm{num}\cdot a.\mathrm{den}$ as signed orbits—then the quotient classes agree: $\mathrm{mk}(a)=\mathrm{mk}(b)$.
background
In the Primitive Recognition Calculus, rationals are not taken as a primitive type. A ratio orbit is a pair consisting of a signed orbit numerator and a nonzero distinction-nat denominator (K4.7). Equality of such displays is internal: two ratio orbits stand in the cross-multiplication relation when the scaled signed orbits $a.num\cdot b.den$ and $b.num\cdot a.den$ are balanced (K4.10). That relation is the kernel of the quotient that produces PRC rationals.
The verifier map toRat sends a ratio orbit to an ordinary rational by dividing the integer display of the numerator by the natural display of the denominator; the internal characterization of equality is cross-multiplication, not that map. The same pattern already appears for integers-from-logic, where sound lifts an additive balance $a+d=c+b$ to equality of integer quotient classes.
Locally this module assembles the arithmetic of those quotient classes so that ring laws can be proved by transporting to the verifier integers or rationals and reflecting.
proof idea
One-line term proof: apply Quot.sound to the hypothesis that the two ratio orbits are related by cross-equality. Because mk is the quotient map for that relation, soundness immediately yields equality of classes. No further algebraic rewriting is required.
why it matters
This is the K4.8 well-definedness lemma for PRC rationals: equal cross-multiplied ratio orbits determine equal quotient rationals. Downstream ring-law proofs in the same module (associativity, commutativity, units, distributivity, and the additive inverse laws for the integer and rational structures) repeatedly need that operations on representatives descend to the quotient; this theorem is the equality engine for that descent.
In the broader Recognition foundation it closes the rational half of the integers-and-rationals-from-logic stack that underwrites later forcing and display layers. It is the direct analogue of IntegersFromLogic.sound for the cross-multiplication relation, and it keeps the internal δ-orbit arithmetic aligned with the verifier rationals without smuggling classical $\mathbb{Q}$ into the object language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.