toInt_add
The recovery map from the Grothendieck completion of LogicNat to the integers preserves addition. Authors proving the ring axioms on LogicInt cite it to reduce identities to the standard integers via the transfer equivalence. The argument proceeds by double quotient induction on representatives, reduction through the natural-number addition recovery, and ring normalization.
claimLet $I$ be the Grothendieck completion of LogicNat under addition, with recovery map toInt : $I$ → ℤ defined by lifting the core difference map. Then toInt($a + b$) = toInt($a$) + toInt($b$) for all $a, b$ ∈ $I$.
background
LogicInt is the quotient of LogicNat × LogicNat by the setoid equivalence, serving as the Grothendieck completion of LogicNat under addition. The constructor mk forms an element from a pair of logic naturals, and toInt is the lift of toIntCore that sends the class of (a, b) to toNat a − toNat b. The upstream result toNat_add states that the addition LogicNat carries agrees with Nat addition under the equivalence.
proof idea
The proof applies Quotient.inductionOn to both arguments. After rcasing the representatives to pairs, it rewrites using toInt_mk three times and toNat_add twice. The push_cast and ring tactics then close the algebraic identity.
why it matters in Recognition Science
This result is invoked by add_assoc', add_comm', add_zero', add_left_neg', mul_add' and add_mul' through the transfer principle that an equation in LogicInt holds iff it holds under toInt. It completes the addition-homomorphism step in the integer construction, allowing LogicInt to inherit the ring structure of Int before the rational layer is built.
scope and limits
- Does not establish the corresponding homomorphism for multiplication.
- Does not prove bijectivity of the recovery map.
- Does not extend the statement to the rational construction.
- Does not address the setoid equivalence relation beyond the induction step.
Lean usage
rw [eq_iff_toInt_eq, toInt_add, toInt_add, toInt_add, toInt_add]; ringformal statement (Lean)
323theorem toInt_add (a b : LogicInt) : toInt (a + b) = toInt a + toInt b := by
proof body
Term-mode proof.
324 induction a using Quotient.inductionOn with
325 | h p =>
326 induction b using Quotient.inductionOn with
327 | h q =>
328 rcases p with ⟨a, b⟩
329 rcases q with ⟨c, d⟩
330 show toInt (mk (a + c) (b + d)) = toInt (mk a b) + toInt (mk c d)
331 rw [toInt_mk, toInt_mk, toInt_mk]
332 rw [toNat_add, toNat_add]
333 push_cast
334 ring
335