add_zero'
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove commutativity, associativity, or other ring axioms.
- Does not treat multiplication or the full ring structure.
- Does not address embeddings into rationals or reals.
formal statement (Lean)
382theorem add_zero' (a : LogicInt) : a + (0 : LogicInt) = a := by
proof body
One-line wrapper that applies rw.
383 rw [eq_iff_toInt_eq, toInt_add, toInt_zero]; ring
384