toRat_recip
plain-language theorem explainer
The classical rational display of a PRC reciprocal equals the field inverse of that display. Anyone transporting PRC arithmetic into Mathlib ℚ (boundedness moduli, J-cost continuity targets, Cauchy order) cites this simp lemma. Proof is quotient induction that hands off to the ratio-orbit reciprocal display law.
Claim. For every PRC rational $a$ (a cross-multiplication quotient class of ratio orbits), the verifier display satisfies $\mathrm{toRat}(a^{-1}) = (\mathrm{toRat}(a))^{-1}$ in $\mathbb{Q}$.
background
PRC rationals are quotient classes of ratio orbits under cross-multiplication equivalence: two orbits are identified when the signed-orbit products of numerator and denominator balance. The constructor builds a class from a ratio orbit; the verifier display sends each class to a classical rational in $\mathbb{Q}$.
Reciprocal is the field-style inverse on that quotient (nonzero-denominator orbits). The module builds integer and rational structure choice-free from $\delta$-orbit arithmetic, with cross-multiplication as the internal equality hub. Upstream, crossEq defines that balance entirely on signed orbit positions; the integer quotient soundness lemma underpins the setoid.
Local setting is the Primitive Recognition Calculus integer/rational layer: internal laws stay on orbit arithmetic, while toRat is only a conservative classical display for verifier checks.
proof idea
Quotient induction on the PRC rational exposes a ratio-orbit representative. The goal becomes the representative-level claim that the reciprocal orbit displays to the inverse of the representative display. That identity is exactly the existing ratio-orbit reciprocal display lemma, applied directly. No cross-multiplication reduction or ring work happens at this layer; the simp attribute makes the bridge automatic for classical displays downstream.
why it matters
This is the display bridge for inverses when PRC constructions are checked against classical $\mathbb{Q}$. Downstream, the boundedness-modulus theorem unfolds the PRC delta and simp-reduces its display to $1/8$ using the mul and recip display laws. Real product continuity builds a density factor $\rho = \varepsilon(1+\varepsilon)^{-1}$ on PRC rationals and needs the display of that inverse. Null-equivalence order congruence for Cauchy sequences also routes through reciprocal displays.
In the Recognition foundation stack the lemma keeps the classical verifier honest while internal field laws remain on the ${\mathrm{propext},,\mathrm{Quot.sound}}$ basis (the module note after the proof stresses that the choice-free laws deliberately avoid routing through toRat).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.