add_zero'
plain-language theorem explainer
The theorem establishes that zero acts as the additive identity for LogicInt, the Grothendieck completion of LogicNat under addition. Researchers constructing the integer layer from logical naturals cite it when verifying ring axioms in sequence. The proof is a one-line wrapper that transfers the claim to the standard integers via the toInt embedding and simplifies the resulting equation.
Claim. For any element $a$ of the Grothendieck completion $LogicInt$ of $LogicNat$, $a + 0 = a$.
background
LogicInt is the quotient of pairs from LogicNat by the equivalence that equates pairs with identical differences, realizing the Grothendieck completion under addition. The transfer principle eq_iff_toInt_eq asserts that an equality holds in LogicInt precisely when the images under toInt are equal in the standard integers. Upstream lemmas establish that toInt preserves addition and sends the constructed zero to the integer zero.
proof idea
The proof is a one-line wrapper that applies eq_iff_toInt_eq to move the equation to the integer level, substitutes the preservation properties toInt_add and toInt_zero, and finishes with the ring tactic on the resulting identity in Int.
why it matters
This supplies the additive identity axiom for LogicInt and is invoked directly by the matching add_zero' statements in the rationals and reals constructions. It completes one step in the sequential verification of ring structure on the integers built from logical naturals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.