toInt_add
plain-language theorem explainer
The theorem shows that the recovery map toInt from the Grothendieck integers LogicInt to the standard integers preserves addition. Researchers establishing ring axioms on logic-derived integers cite this to transfer identities via reduction to Int. The proof applies double Quotient.inductionOn, reduces via toInt_mk and toNat_add, then finishes by push_cast and ring.
Claim. Let $LogicInt$ be the Grothendieck completion of $LogicNat$ under addition, and let $toInt : LogicInt → ℤ$ be the canonical recovery map. Then $toInt(a + b) = toInt a + toInt b$ for all $a, b ∈ LogicInt$.
background
LogicInt is the quotient of LogicNat × LogicNat by the setoid equivalence, forming the Grothendieck completion under addition. The map toInt is defined by lifting the core map that sends the class of (a, b) to toNat a − toNat b. The upstream theorem toNat_add states that addition on LogicNat agrees with Nat addition under the equivalence: toNat (a + b) = toNat a + toNat b.
proof idea
The proof applies Quotient.inductionOn twice to reduce to representatives p = (a, b) and q = (c, d). It rewrites using toInt_mk three times and toNat_add twice, then applies push_cast and ring to obtain equality.
why it matters
This result feeds the transfer principle eq_iff_toInt_eq used in downstream theorems such as add_assoc', add_comm', add_left_neg', and add_zero' to establish the ring structure on LogicInt by reduction to Int. It forms part of the integer construction that precedes the rationals and supports the foundation that LogicInt is isomorphic to ℤ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.