add_assoc'
plain-language theorem explainer
Associativity of addition holds on LogicInt, the Grothendieck completion of LogicNat. Foundation developers cite this when confirming that LogicInt carries a ring structure. The proof is a one-line wrapper that transfers the identity via eq_iff_toInt_eq, expands each sum with toInt_add, and closes the resulting equation on Int with the ring tactic.
Claim. For all elements $a, b, c$ in the Grothendieck completion of the logic naturals, $(a + b) + c = a + (b + c)$.
background
LogicInt is the quotient of pairs of LogicNat elements under the relation that equates (p, q) with (r, s) precisely when p + s = q + r. The transfer principle eq_iff_toInt_eq states that two elements of LogicInt are equal if and only if their images under the canonical map toInt coincide in the standard integers. The auxiliary result toInt_add records that this map is a homomorphism for addition.
proof idea
The proof is a one-line wrapper. It rewrites the goal with eq_iff_toInt_eq, replaces each of the four occurrences of addition by its image under toInt_add, and invokes the ring tactic on the resulting identity in Int.
why it matters
The declaration supplies the associativity axiom for addition on LogicInt and is invoked by the corresponding add_assoc' statements in RationalsFromLogic and RealsFromLogic. It belongs to the block that equips LogicInt with ring operations by reduction to Int, thereby furnishing the arithmetic base required for the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.