add_right_neg'
plain-language theorem explainer
Every PRC rational is its own additive inverse: a + (-a) = 0. Anyone assembling the additive group or field structure on the PRC rational type cites this identity. The proof is a one-line wrapper that reuses the corresponding integer-level cancellation lemma.
Claim. For every PRC rational $a$, $a + (-a) = 0$.
background
PRC rationals are the nonzero-denominator ratio-orbit quotient: equivalence classes of integer ratios identified by cross-multiplication of orbit-level numerators and denominators (K4.8). They sit above the PRC integers and inherit arithmetic via the quotient.
The module builds the field operations and algebraic laws on this type. Additive inverse and the right-cancellation law $a + (-a) = 0$ are part of that package, parallel to the integer identity already proved for PRC integers.
Upstream, the integer lemma states that for every PRC integer $a$, adding $a$ to its negate yields zero, proved by injectivity of the map to ordinary integers and simplification.
proof idea
One-line wrapper: apply the integer-level right-negation theorem add_negate at the rational argument. No extra quotient reasoning appears in the body; the rational additive structure is already aligned so the integer cancellation lifts directly.
why it matters
This closes the right-inverse half of the additive group axioms for PRC rationals inside Primitive Recognition Calculus. Together with the sibling associativity and unit laws in the same module, it supplies the algebraic substrate on which later real-completion and continuity developments rest.
No downstream consumers are recorded yet; the declaration is infrastructure rather than a forcing-chain landmark. It does not touch T5–T8, the Recognition Composition Law, or the phi-ladder mass formula. Its role is strictly foundational: make the rational field usable without sorry before analysis is layered on top.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.