add_comm'
plain-language theorem explainer
Addition commutes on LogicInt, the Grothendieck completion of LogicNat under addition. Researchers assembling the arithmetic hierarchy from logic in Recognition Science cite this to secure the additive group axioms. The proof is a one-line wrapper that transfers the claim to standard integer addition via eq_iff_toInt_eq and toInt_add, then applies the ring tactic.
Claim. Let LogicInt be the Grothendieck completion of LogicNat under addition, realized as the quotient of LogicNat × LogicNat by the induced setoid. Then for all a, b in LogicInt, a + b = b + a.
background
LogicInt is the Grothendieck completion of LogicNat under addition, constructed as the quotient of LogicNat × LogicNat by the equivalence relation that identifies pairs differing by the same natural. The transfer principle eq_iff_toInt_eq states that an equation between LogicInt elements holds if and only if the corresponding equation holds after mapping to the standard integers via toInt. The lemma toInt_add records that this map is a group homomorphism, preserving addition. The declaration sits inside the foundation layer that builds integers directly from the logical naturals before lifting to rationals and reals.
proof idea
The proof is a one-line wrapper. It rewrites the goal with eq_iff_toInt_eq, applies toInt_add to both sides of the resulting equation, and finishes with the ring tactic, which dispatches commutativity in the target integers.
why it matters
This supplies the commutativity axiom for addition on LogicInt and is invoked verbatim by the matching add_comm' theorems in RationalsFromLogic and RealsFromLogic. It thereby propagates the additive group structure through the entire arithmetic tower. Within Recognition Science it closes one of the elementary ring identities required before the phi-ladder, the eight-tick octave, and the mass formula can be stated. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.