add_left_neg'
plain-language theorem explainer
The theorem establishes that negation acts as a left inverse under addition for every element of the integers obtained as the Grothendieck completion of the naturals. Researchers constructing arithmetic step-by-step from logical primitives cite this when confirming that the resulting structure satisfies the additive group axioms. The proof is a one-line wrapper that reduces the identity to the standard integers via the canonical embedding and finishes by ring simplification.
Claim. For every $a$ in the Grothendieck completion of the natural numbers under addition, the equation $-a + a = 0$ holds.
background
LogicInt is the quotient of pairs of LogicNat elements under the equivalence that identifies (p, q) with (r, s) precisely when p + s equals q + r. The function toInt supplies a bijection from this quotient to the ordinary integers Int. The key upstream transfer principle states that an equality between two LogicInt elements holds if and only if the corresponding equality holds after applying toInt; separate preservation theorems show that toInt respects addition, negation, and the zero element.
proof idea
This is a one-line wrapper. It first applies the transfer principle to replace the LogicInt equation by the corresponding equation in Int, then substitutes the three preservation theorems for addition, negation, and zero, and concludes with the ring tactic.
why it matters
The result is invoked directly by the analogous left-inverse statements for the rationals and reals built in the same style. It supplies the missing additive-inverse axiom needed to equip LogicInt with a group structure, a prerequisite for the Recognition Science forcing chain that derives spatial dimension D = 3 and the eight-tick octave from the functional equation. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.