negate_toRat
plain-language theorem explainer
Negating a ratio orbit and reading it as a rational equals ordinary additive inversion of that rational. Anyone assembling RatioOrbit arithmetic (especially subtraction) or lifting negation to the PRCRat quotient cites this. The proof unfolds the maps, rewrites via the signed-orbit integer case, clears the nonzero denominator, and finishes by ring.
Claim. For every ratio orbit $a$ (signed-orbit numerator over a nonzero distinction-nat denominator), the rational value of its pointwise negation equals the additive inverse of its rational value: $(\mathrm{negate}\,a)_{\mathbb{Q}} = -a_{\mathbb{Q}}$.
background
In the Primitive Recognition Calculus integer/rational layer, a SignedOrbit is a difference of two distinction-nats (intended meaning pos minus neg). Pointwise negate swaps those two components. A RatioOrbit (K4.7) packages a signed-orbit numerator with a nonzero distinction-nat denominator, giving a rational display built only from orbit data.
The map toRat sends such a display to an ordinary rational by casting numerator and denominator through their Nat/Int readings. The lemma den_cast_ne_zero records that the denominator cast to $\mathbb{Q}$ is nonzero, so the division is well-defined. Upstream, negate_toInt already shows that signed-orbit negation matches integer negation: $(\mathrm{negate},s).\mathrm{toInt} = -s.\mathrm{toInt}$.
This module sits under ArithmeticFromLogic and OrbitArithmetic: natural numbers arise as iteration counts (toNat), then signed and rational displays are built on top so later recognition calculus can compute with $\mathbb{Q}$ without leaving the orbit language.
proof idea
Tactic proof. Unfold negate and toRat so both sides are explicit integer-over-nat quotients in $\mathbb{Q}$. Rewrite the numerator with SignedOrbit.negate_toInt, which turns orbit negation into ordinary integer negation. Introduce hA : (a.den.toNat : $\mathbb{Q}$) $\neq 0$ from den_cast_ne_zero, then field_simp [hA]clears the common nonzero denominator.push_castaligns the remaining Nat/Int coercions, andring_nf` closes the identity $-n/d = -(n/d)$.
why it matters
This is the rational-level companion to negate_toInt: negation on ratio orbits is faithful under toRat. Downstream, sub_toRat defines subtraction as add a (negate b) and obtains $(a-b){\mathbb{Q}} = a{\mathbb{Q}}-b_{\mathbb{Q}}$ by rewriting with add_toRat and this lemma, then ringing. The simp lemma toRat_negate on the quotient type PRCRat is exactly the induction of this statement: after Quot.induction_on, it reduces to RatioOrbit.negate_toRat.
In the Recognition foundation stack this closes K4.11-style arithmetic on rational orbit displays, so later forcing and mass-ladder work can treat signed rationals as honest $\mathbb{Q}$ values rather than formal symbols. It does not itself touch T5–T8 or the J-cost; it is pure carrier arithmetic underneath those landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.