toInt_zero
plain-language theorem explainer
The recovery map toInt from the Grothendieck integers LogicInt to the standard integers sends the zero element to zero. Researchers establishing the ring isomorphism between LogicInt and ℤ cite this as the base case for the additive identity. The proof reduces directly by unfolding zero as the mk constructor on LogicNat.zero, applying toInt_mk, and invoking toNat_zero.
Claim. The recovery map satisfies $toInt(0) = 0$, where the zero on the left is the additive identity in the Grothendieck completion of LogicNat and the zero on the right is the standard integer zero.
background
LogicInt is defined as the quotient of pairs of LogicNat elements under the setoid equivalence, serving as the Grothendieck completion under addition. The map toInt : LogicInt → Int is obtained by lifting the core map that sends a pair (a, b) to toNat a - toNat b. Upstream, LogicNat is the inductive type with identity and step constructors forced by the Law of Logic, while toNat_zero states that toNat sends the zero of LogicNat to the natural number zero. This sits inside the module section on ring-homomorphism properties of toInt as part of recovering the standard integers from the logic foundation.
proof idea
The proof unfolds the zero element of LogicInt as mk LogicNat.zero LogicNat.zero. It applies toInt_mk to rewrite the expression as toNat zero - toNat zero. It then invokes toNat_zero on both sides and simplifies the resulting 0 - 0 to obtain zero.
why it matters
This lemma is invoked in the proofs of add_zero', zero_add', add_left_neg' and mul_eq_zero, which transfer the ring axioms on LogicInt through the map toInt. It completes the verification that toInt preserves the additive identity, forming part of the recovery theorem equivInt : LogicInt ≃ Int and the subsequent ring isomorphism. In the Recognition framework it confirms that the integers extracted from the logic foundation match the standard model at the additive identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.