toRat_neg'
plain-language theorem explainer
Negation on PRC rationals commutes with the verifier display into ordinary rationals: the image of $-a$ is the ordinary negative of the image of $a$. Anyone wiring the real-completion embedding from PRC rationals cites this. The proof is a one-line `simp` wrapper over the underlying quotient and integer displays.
Claim. For every PRC rational $a$ (a ratio-orbit quotient class with nonzero denominator), the verifier map $\mathrm{toRat}:\mathrm{PRCRat}\to\mathbb{Q}$ satisfies $\mathrm{toRat}(-a)=-\mathrm{toRat}(a)$.
background
PRC rationals are the K4.8 construction: nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication of orbit-level numerator and denominator. They sit in the Primitive Recognition Calculus layer that builds integers and rationals from orbit arithmetic before completing to reals.
The map toRat is the A5 verifier display: it sends a ratio orbit (or its quotient class) to an ordinary rational by dividing the integer display of the numerator by the natural display of the denominator. Spec tag A5 treats this as a transport wrapper; the internal characterization remains cross-multiplication.
Negation on PRC rationals is the induced group operation on that quotient. This lemma records that the verifier display is a homomorphism for that unary operation, so later real-completion maps can push negation through without reopening the quotient.
proof idea
One-line wrapper: simp discharges the equality by unfolding the PRC-rational negation and toRat displays down to the underlying integer/rational arithmetic, where ordinary negation already commutes with the casts.
why it matters
Feeds directly into ofRat_neg in RealCompletion, which states that the embedding of PRC rationals into the real completion intertwines negation: ofRat (-a) = -ofRat a. That parent unfolds ofRat, rewrites by this lemma, and finishes with norm_num.
In the Recognition foundation stack this is bookkeeping on the path from orbit arithmetic through rationals to the real line used by later forcing and continuum arguments. It does not itself touch T5–T8 or the J-cost law; it keeps the rational display honest so those layers can treat signed rationals as ordinary $\mathbb{Q}$ without extra casework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.