negate_add
plain-language theorem explainer
Additive inverses cancel on recognition integers: the sum of the negation of a with a itself is the zero class. Anyone assembling the abelian-group or ring laws on PRC integers, or lifting them to PRC rationals, cites this identity. The proof injects both sides into ordinary integers via the toInt display and simplifies.
Claim. For every recognition integer $a$ (a quotient class of signed orbits under the balanced-length relation), $\mathrm{add}(\mathrm{negate}(a), a) = 0$, where negation swaps the positive and negative orbit components and $0$ is the zero class.
background
PRC integers are the quotient of signed orbits by the internal balanced-length relation (K4.8). A signed orbit carries a positive and a negative distinction-nat component; its integer display is $\mathrm{toInt} = \mathrm{pos.toNat} - \mathrm{neg.toNat}$. The zero class is the class of the balanced empty pair.
Pointwise negation swaps the two components of a signed orbit (named negate to avoid clashing with structure fields). Addition of signed orbits adds the positive parts and the negative parts separately; the quotient operation descends because balanced length is a congruence. The companion lemma add_toInt records that this addition agrees with ordinary integer addition under the display.
The local module builds integer and rational arithmetic from recognition primitives without routing through Mathlib's classical choice for the core algebraic laws.
proof idea
One short tactic proof. Apply injectivity of the integer display toInt on the quotient, reducing the goal to an equality in $\mathbb{Z}$. Then simp rewrites using the display lemmas for negation, addition, and zero (negate_toInt, add_toInt, zero_toInt), which yield $(-n) + n = 0$ in $\mathbb{Z}$ and close the goal.
why it matters
This is the left-inverse law for addition on PRC integers. Downstream, RationalField.add_left_neg' is literally a one-line application of it, supplying $-a + a = 0$ on PRC rationals and thereby the additive-group fragment of the recognition-derived field. Without this cancellation, the quotient constructions cannot host a ring or field instance, so the bridge from primitive recognition orbits to ordinary arithmetic stalls at the integer layer.
In the broader Recognition Science stack this sits in the foundation layer that reconstructs $\mathbb{Z}$ and $\mathbb{Q}$ from distinction orbits before the forcing chain (T0–T8) and the J-cost calculus are interpreted numerically. It is pure algebraic scaffolding, not a physics claim, but every later numeric display depends on the group laws being available here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.