toInt_fromInt
plain-language theorem explainer
The theorem shows that every integer recovers exactly after embedding into the logic-native integer type and extracting back. Researchers assembling the bijection between standard integers and those built from the Law of Logic cite this to close the integer round-trip. The proof works by case split on the sign of the integer, followed by rewriting with the natural-number extraction lemmas and constructor simplification.
Claim. For every integer $n$, the composition of the embedding from integers to logic-native integers followed by the extraction map returns $n$. The embedding sends non-negative $n$ to the pair consisting of the logic natural $n$ and zero, and negative values to the pair of zero and the logic natural for the absolute value.
background
LogicNat is the inductive type with constructors identity (representing zero) and step, forming the orbit under the generator as the smallest subset of positive reals closed under multiplication by the generator and containing 1. LogicInt is the quotient of pairs of LogicNat by the integer relation. The embedding fromInt maps Int.ofNat n to the pair (fromNat n, zero) and Int.negSucc n to (zero, fromNat (succ n)). The extraction toInt recovers the integer by applying the natural extraction to the components of the pair.
proof idea
Case analysis on the integer splits into ofNat and negSucc branches. The ofNat case rewrites via the mk definition of toInt, applies the natural round-trip toNat_fromNat and toNat_zero, then simplifies the ofNat constructor. The negSucc case rewrites via mk, applies toNat_zero and toNat_fromNat, then simplifies using the negSucc_eq identity.
why it matters
This supplies the right inverse for the carrier bijection equivInt between LogicInt and Int. It is invoked directly in the definitions of fromRat and the round-trip theorems toRat_fromRat and fromRat_toRat when transporting to rationals. The result completes the integer layer required before introducing the J-cost function and the phi-ladder in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.