fromInt_toInt
plain-language theorem explainer
The theorem establishes that fromInt recovers every element z of LogicInt after toInt is applied, completing one direction of the bijection between the Grothendieck completion of LogicNat and the standard integers. Researchers formalizing arithmetic foundations or transferring ring identities in Recognition Science would cite it when reducing equations on LogicInt to Int. The proof proceeds by quotient induction on the pair representative of z, followed by sign case analysis on the integer difference and application of the sound constructor for
Claim. Let LogicInt be the Grothendieck completion of LogicNat. For every $z$ in LogicInt, fromInt(toInt($z$)) = $z$.
background
LogicInt is the quotient of LogicNat × LogicNat by the equivalence (a, b) ~ (c, d) iff a + d = b + c, forming the integers via the Grothendieck construction. The maps toInt and fromInt realize the correspondence to Int, with toInt sending the class of (a, b) to (toNat a : Int) - toNat b and fromInt building the appropriate mk pair according to sign. This sits inside IntegersFromLogic, which extends the LogicNat arithmetic developed in ArithmeticFromLogic. It depends on add_comm, add_zero, fromNat_toNat, and toNat_add to verify that the recovered pair is equivalent under the setoid.
proof idea
The tactic proof introduces z and applies Quotient.inductionOn. For representative pair (a, b) it rewrites toInt_mk, then cases on toNat b ≤ toNat a. The non-negative branch obtains k via Int.eq_ofNat_of_zero_le, applies sound, and uses fromNat_toNat together with add_comm to equate the LogicNat sums. The negative branch computes m for the negSucc form, rewrites with Int.negSucc_eq, applies sound, and invokes zero_add plus the fromNat homomorphism property verified by toNat_add.
why it matters
This supplies the left inverse for equivInt : LogicInt ≃ Int, the carrier bijection that recovers standard integers inside the logic framework. It is invoked directly in eq_iff_toInt_eq to transfer equations from Int back to LogicInt. Within Recognition Science the result closes the integer layer of the foundation, enabling arithmetic identities required for mass ladders, phi-based constants, and downstream derivations such as nucleosynthesis tiers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.