add_negate
plain-language theorem explainer
For every PRC integer a, a plus its additive inverse is zero. Anyone building the PRC integer or rational field axioms cites this as the right-inverse law. The proof is a two-line reduction: injectivity of the integer display, then simplification of the signed-orbit arithmetic.
Claim. For every PRC integer $a$ (a quotient class of signed orbits under the balanced-length relation), $a + (-a) = 0$, where negation swaps the positive and negative orbit components and addition is componentwise on those orbits.
background
PRC integers are the K4.8 construction: quotient classes of signed orbits under the internal balanced-length setoid. A signed orbit carries a positive and a negative distinction-nat component; the display toInt sends it to $\mathbb{Z}$ as pos-minus-neg. Negation is the pointwise swap of those two components (named negate to avoid clashing with structure fields). Addition is componentwise on the underlying distinction nats.
The module sits in the Primitive Recognition Calculus foundation layer, which rebuilds integer and rational arithmetic from orbit data before any classical choice is introduced. Upstream, add_toInt records that addition on signed orbits agrees with ordinary integer addition under the display, and negate_toInt (used via simp) records that negation flips the sign of the display. The recovery theorem toNat_mul from ArithmeticFromLogic is among the deeper dependencies that make the distinction-nat layer match ordinary Nat.
proof idea
One short tactic proof. Apply injectivity of the toInt display on PRC integers, reducing the goal to an equality in $\mathbb{Z}$. Then simp closes it: the display of the sum is the sum of the displays (add_toInt), the display of the negation is the negation of the display (negate_toInt), and $n + (-n) = 0$ in $\mathbb{Z}$. No case split or induction is required.
why it matters
This is the additive right-inverse law for PRC integers. Downstream, RationalField.add_right_neg' is a one-line wrapper that reuses it for PRC rationals: $a + (-a) = 0$. That law is part of the field-axiom package for the choice-free rational layer built on cross-multiplication of ratio orbits.
It also feeds kernel_first_pass_certificate (K7/A2), which packages the inhabited first-pass kernel certificate (strength tags, trace syntax, judgment surface, trace logic). Establishing that the integer layer has genuine additive inverses is a prerequisite for the verifier equality judgment and the broader claim that arithmetic emerges from recognition orbits rather than being postulated.
In the Recognition Science forcing chain this sits below the T5–T8 landmarks: it is infrastructure for the arithmetic substrate, not a direct forcing step, but without it the later mass ladder and constant derivations have no integer carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.