fromInt
plain-language theorem explainer
fromInt embeds standard integers into LogicInt, the Grothendieck completion of LogicNat under addition. Foundation researchers cite it when transporting arithmetic results from Mathlib's Int into the Recognition Science setting. The definition proceeds by direct case analysis on the Int constructors, delegating the natural components to fromNat.
Claim. The map fromInt : ℤ → LogicInt sends a nonnegative integer n to the class [fromNat(n), 0]_ℓ and a negative integer −(n+1) to [0, fromNat(n+1)]_ℓ, where [a, b]_ℓ denotes the equivalence class of the pair (a, b) in the quotient defining LogicInt.
background
LogicInt is the Grothendieck completion of LogicNat under addition, realized as the quotient of LogicNat × LogicNat by the setoid identifying pairs with equal differences. LogicNat is the inductive type with constructors identity (zero-cost element) and step (one application of the generator), representing the orbit {1, γ, γ², …}. The mk constructor forms the notation [a, b]_ℓ for the formal difference a − b.
proof idea
The definition is given by pattern matching on the two constructors of Int. The ofNat case applies mk to the pair (LogicNat.fromNat n, LogicNat.zero). The negSucc case applies mk to the pair (LogicNat.zero, LogicNat.fromNat (Nat.succ n)).
why it matters
fromInt supplies one leg of the bijection equivInt : LogicInt ≃ Int and is invoked by the round-trip theorems fromInt_toInt and toInt_fromInt. It is also used to construct fromRat for logic rationals and appears in eq_iff_toInt_eq. In the Recognition framework it closes the integer layer of the foundation, enabling transport of results that later involve the phi-ladder and J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.