add_left_neg'
plain-language theorem explainer
Every recognition rational has a left additive inverse: -a + a equals zero. Field-structure and certificate authors cite it when assembling the additive group laws on PRC rationals. The proof is a one-line wrapper of the existing negate-add identity.
Claim. For every recognition rational $a$ (a ratio-orbit quotient class with nonzero denominator), the left additive inverse satisfies $-a + a = 0$.
background
PRC rationals are the K4.8 construction: nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication of orbit-level numerator and denominator. They sit in the Primitive Recognition Calculus stack that builds number systems from recognition primitives rather than from classical set-theoretic quotients alone.
Additive structure on these classes is already defined (addition, zero, negation). The sibling lemmas add_assoc', zero_add', and add_zero' supply the other monoid laws; this declaration supplies the left-inverse law that upgrades the monoid to a group.
Upstream, negate_add on the integer layer states that adding an integer to its negation yields zero, proved by injectivity of the integer embedding and simplification. Parallel left-inverse theorems exist for logic integers, logic rationals, and logic reals, each reduced through the corresponding embedding.
proof idea
One-line wrapper: apply negate_add at the given recognition rational. No further rewriting or case analysis is required; the integer-rational layer already discharges the identity, and the rational constructor inherits it directly.
why it matters
This is one of the five additive fields packed into rational_field_certificate, which records commutativity, associativity, zero laws, and left negation as a single certificate object. That certificate is the hand-off point from raw PRC rational arithmetic to the abstract field interface used by later foundation modules.
It mirrors the same left-inverse law on logic integers, logic rationals, and logic reals, keeping the FromLogic and PRC stacks aligned. In the broader Recognition Science forcing chain this is pure scaffolding for the number hierarchy (not a T5–T8 forcing step), but without it the rational field cannot be certified and the climb to reals stalls.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.