zero_add'
plain-language theorem explainer
The theorem establishes that zero is a left additive identity on LogicInt, the Grothendieck completion of LogicNat under addition. Foundation developers cite it when propagating additive identities from naturals through integers to rationals and reals in the Recognition Science arithmetic layer. The proof is a one-line wrapper that transfers the equation via the toInt equivalence and reduces it by ring tactics on the standard integers.
Claim. Let $Z$ denote the Grothendieck completion of the natural numbers under addition. Then $0 + a = a$ for every element $a$ in $Z$.
background
LogicInt is the quotient of pairs of LogicNat elements under the equivalence (a,b) ~ (c,d) iff a + d = b + c, yielding the integers via the Grothendieck construction. The function toInt supplies a bijection to the standard integers Int that preserves addition, with toInt_zero recovering the zero element and eq_iff_toInt_eq serving as the transfer principle that equates equality in LogicInt with equality after applying toInt. This declaration appears in the IntegersFromLogic module, which builds integer arithmetic directly from the logical base before lifting the same identities to LogicRat and LogicReal.
proof idea
The proof is a one-line wrapper. It rewrites the goal with eq_iff_toInt_eq to move the equation into the image under toInt, substitutes toInt_add and toInt_zero to obtain the standard integer identity 0 + toInt a = toInt a, and closes with the ring tactic.
why it matters
This supplies the left zero identity for addition on LogicInt and is reused verbatim to establish the corresponding zero_add' theorems for LogicRat and LogicReal. It completes one incremental step in constructing ring structure from the logical foundation, ensuring consistency with the standard integers via the toInt embedding. In the Recognition Science framework it supports the arithmetic layer that later hosts the phi-ladder mass formulas and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.