toInt
plain-language theorem explainer
The recovery map from the Grothendieck completion LogicInt to ordinary integers is realized by lifting the difference function on pairs of naturals. Researchers building the integer ring inside Recognition Science cite this map when reducing equations on LogicInt to arithmetic in Int. The definition is a direct application of the quotient lift constructor once the core difference map is shown to respect the equivalence.
Claim. The function toInt sends an equivalence class $[a, b]$ in LogicInt to the integer $a - b$, where subtraction is performed after embedding the underlying naturals into Int.
background
LogicInt is the quotient of LogicNat × LogicNat by the equivalence relation of the Grothendieck construction for integers under addition. The core map toIntCore sends a pair $(a, b)$ to (toNat a : Int) - (toNat b : Int). The theorem toIntCore_respects proves that this difference is invariant under the equivalence, so the map descends to the quotient.
proof idea
This definition is a one-line wrapper that applies Quotient.lift to toIntCore using the respect theorem toIntCore_respects.
why it matters
This map supplies the forward direction of the bijection equivInt between LogicInt and Int. It is invoked in eq_iff_toInt_eq to transfer equations and in the proofs of mul_eq_zero and mul_right_cancel by reduction to the corresponding statements in Int. The construction completes the recovery of the integer ring from the logic-based foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.