toRat_negate
plain-language theorem explainer
Negation on PRC rationals commutes with the verifier map to ordinary rationals: the display of the negated class is the ordinary negative of the display. Anyone building arithmetic on the PRC rational quotient cites this as a simp lemma. The proof is quotient induction reducing to the already-proved ratio-orbit identity.
Claim. For every PRC rational $a$ (a quotient class of ratio orbits with nonzero denominator), the verifier display satisfies $\mathrm{toRat}(-a) = -\mathrm{toRat}(a)$ in $\mathbb{Q}$.
background
In the Primitive Recognition Calculus, integers are built from signed orbits and rationals from ratio orbits: a numerator signed orbit over a nonzero distinction-nat denominator. PRCRat is the quotient of those ratio orbits by cross-multiplication equivalence (K4.8).
The map toRat is a verifier display only: it sends a ratio orbit to $(n{:}\mathbb{Q})/(d{:}\mathbb{Q})$ and lifts to the quotient. Spec tag A5 treats it as a transport wrapper; the internal characterization remains cross-multiplication. Negation on signed orbits swaps the positive and negative parts; it lifts first to ratio orbits, then to PRCRat.
The orbit-level fact already on the shelf is negate_toRat: for any ratio orbit $q$, $(\mathrm{negate}, q).\mathrm{toRat} = -q.\mathrm{toRat}$, proved by unfolding, the signed-orbit integer identity, and field_simp on the nonzero denominator cast.
proof idea
Term-mode proof by quotient induction. Apply Quot.induction_on to the PRCRat argument, reducing the goal to the representative ratio orbit. The reduced goal is exactly RatioOrbit.negate_toRat, which is invoked directly. No extra algebraic work at the quotient level.
why it matters
This is the negation half of the K4 arithmetic package that makes the PRC rational display a ring homomorphism into $\mathbb{Q}$. Its sole recorded consumer is toRat_sub, which defines subtraction as add a (negate b) and rewrites via toRat_add and this lemma, then closes with ring.
In the broader Recognition foundation, rationals sit under the forcing chain that later yields $J$-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). A faithful rational display is scaffolding for cost and mass formulas stated in RS-native units; without negation commuting with toRat, subtraction and absolute differences on the ladder would not match ordinary $\mathbb{Q}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.