ofRat_neg
plain-language theorem explainer
Negation commutes with the embedding of PRC rationals into the real boundary: ofRat(-a) equals -ofRat(a). Algebra and analysis lemmas that treat the real boundary as a field cite this as a simp rule. The proof unfolds the embedding to ordinary rationals, rewrites by the PRC-level negation identity, and finishes by norm_num.
Claim. For every PRC rational $a$, the real-boundary embedding satisfies $\mathrm{embed}(-a) = -\mathrm{embed}(a)$, where embed sends a PRC rational to its conservative rational display as a real.
background
PRC rationals (PRCRat) are the Recognition-native rationals: nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication. Each carries a display map toRat into ordinary $\mathbb{Q}$.
In this module the real boundary carrier is built so that a PRC rational embeds by casting that display: ofRat q := (q.toRat : $\mathbb{R}$). The surrounding development (siblings ofRat_add, ofRat_mul, ofRat_inv) equips this embedding with field-homomorphism identities so later completeness and Cauchy work can treat constants as ordinary reals.
Upstream, toRat_neg' already records that PRC negation is compatible with the rational display: (-a).toRat = -a.toRat. The present lemma lifts that identity through the cast into $\mathbb{R}$.
proof idea
One short tactic proof. Unfold ofRat so both sides become casts of rational displays. Rewrite with PRCRat.toRat_neg', which replaces (-a).toRat by -a.toRat. The remaining equality of real casts is discharged by norm_num.
why it matters
RealCompletion is the K4.14/A5 layer that places PRC rationals on the real boundary via their conservative displays. Field operations on that boundary must match PRC arithmetic; this lemma is the negation half of that package (alongside add, mul, inv siblings).
No downstream users are wired yet in the graph, but the simp attribute marks it as infrastructure for any later proof that manipulates signed constant protocols, Cauchy ledgers, or null-distance quotients built from ofRat. In the broader RS forcing chain it supports the arithmetic substrate under J-cost and the phi-ladder rather than a named T-step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.