toRat_inv'
plain-language theorem explainer
Multiplicative inverse on PRC rationals commutes with the verifier display into ordinary rationals. Anyone building field operations or the real-completion bridge from ratio-orbit classes cites this. The proof is a one-line simplification against the inverse and display definitions.
Claim. For every recognition-calculus rational $a$ (a nonzero-denominator ratio-orbit quotient class), the verifier display of its multiplicative inverse equals the field inverse of its display: if $\iota$ sends a class to $\mathbb{Q}$, then $\iota(a^{-1}) = \iota(a)^{-1}$.
background
PRC rationals are the quotient of ratio orbits by cross-multiplication equality of orbit-level numerator and denominator (nonzero denominator). They are the K4.8 carrier on which field structure is built before completing to reals.
The display map sends a ratio orbit to an ordinary rational by dividing the integer lift of the numerator by the natural lift of the denominator. Spec tag A5 treats this as a transport wrapper: internal equality is cross-multiplication, while the display is only a verifier face into $\mathbb{Q}$.
The local module assembles integer and rational structure from orbit arithmetic. Inverse on the quotient is the field inverse of that display target; this lemma records that the two routes agree.
proof idea
One-line simp proof. Unfolding the quotient inverse and the display into $\mathbb{Q}$ reduces both sides to the same reciprocal of a ratio of integer lifts, so the simplifier closes the goal with no manual rewriting.
why it matters
Needed to push division and inversion through the display. Downstream, the rational-field lemma for division rewrites via the companion multiplication identity and this inverse identity. The real-completion map uses it so that embedding a reciprocal equals the reciprocal of the embedding (ofRat inverse). It also sits in the dependency cone of the first-pass kernel certificate (K7/A2), which packages inhabited judgment and trace surfaces for the primitive recognition calculus.
In the broader forcing chain this is bookkeeping, not a T5–T8 landmark: it keeps the rational layer honest so later continuity and completeness arguments can treat displayed field operations as ordinary $\mathbb{Q}$ arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.