toRat_injective
plain-language theorem explainer
The display map from PRC rationals (quotient classes of ratio orbits) into ordinary rationals is injective. Field and J-cost constructions on the quotient cite it to push equalities of displayed values back to equality of classes. The proof is a short Quot.ind reduction that invokes the cross-multiplication characterization of the setoid.
Claim. Let $Q$ be the quotient of ratio orbits by the cross-multiplication equivalence (nonzero-denominator pairs of signed orbits). The display map $\mathrm{toRat}: Q \to \mathbb{Q}$ is injective: if two classes display the same rational, they are equal as classes.
background
PRC rationals are the quotient type of ratio orbits under the setoid that identifies two orbits precisely when their numerators and denominators cross-multiply. A ratio orbit carries a signed-orbit numerator and a positive natural denominator; its verifier display is the ordinary rational $\mathrm{num}/\mathrm{den}$.
The key upstream fact is that two ratio orbits are setoid-equivalent if and only if their displays agree in $\mathbb{Q}$. That biconditional is the transport form of the internal cross-multiplication relation (spec tag A5). Integer and rational soundness lemmas from the logic-native constructions supply the same pattern one level down: equality of cross products yields equality of quotient classes.
Locally this sits in the K4.8 block that builds the PRC rational type and its display before defining arithmetic and the lifted J-cost.
proof idea
Tactic proof. Introduce two PRC rationals $a,b$ and a hypothesis that their displays agree. Apply Quot.ind on each to reduce to ratio-orbit representatives. On representatives, apply Quot.sound and discharge the setoid relation by the reverse direction of ratioOrbitEquiv_iff_toRat_eq, which converts display equality into cross-multiplication equivalence. No arithmetic simplification is needed beyond that biconditional.
why it matters
Injectivity of the display is the standard bridge that lets field identities and metric identities be proved in $\mathbb{Q}$ and then pulled back to PRC rationals. Downstream, the rational-field cancel laws (div_mul_cancel, mul_div_cancel) open with apply toRat_injective and finish by field_simp. The lift of J-cost to the quotient (onPRCRat) and its normalization invariance both invoke the same injectivity. Cauchy and ordered-field material uses it to show the PRC J-cost distance vanishes on the diagonal and is symmetric. It also appears in the first-pass kernel certificate chain (K7/A2), so the foundation layer treats the display as a faithful verifier embedding rather than a mere projection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.