add_left_neg'
plain-language theorem explainer
The additive inverse property holds for the rationals constructed from logic: for any a in LogicRat, -a + a equals zero. Foundation builders in Recognition Science cite this when verifying the additive group axioms at the rational layer before lifting to reals. The proof is a one-line wrapper that transports the equation via toRat maps and normalizes with ring.
Claim. For any $a$ in the field of fractions LogicRat of the logic integers, $(-a) + a = 0$.
background
LogicRat is the quotient of PreRat pairs by the setoid ratRel, forming the field of fractions of LogicInt. The transfer theorem eq_iff_toRat_eq states that equality in LogicRat is equivalent to equality of the images under toRat in Mathlib's Rat. Upstream, IntegersFromLogic supplies the matching add_left_neg' for LogicInt, which this result mirrors at the next level.
proof idea
The proof is a one-line wrapper. It rewrites the goal with eq_iff_toRat_eq, replaces the operations by their images under toRat_add, toRat_neg and toRat_zero, then applies ring to obtain the zero in Mathlib's Rat.
why it matters
This theorem supplies the left-inverse axiom for addition in LogicRat and is invoked by the parallel statements in IntegersFromLogic and RealsFromLogic. It fills the rational step of the forcing chain (T0-T8) by ensuring the number system carries a field structure before the eight-tick octave and spatial dimension D=3 are imposed. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.