equivInt
plain-language theorem explainer
The integers constructed as the Grothendieck completion of the logic naturals stand in bijection with the standard integers. Foundation researchers cite this bijection to import the ring structure from the standard model into the logic setting. The definition assembles the equivalence by pairing the forward recovery map with its inverse and the two already-proven inverse theorems.
Claim. The maps sending equivalence classes of logic-natural pairs to their integer differences and the explicit inverse sending non-negative integers to classes with zero in the second component (and negatives to classes with zero in the first) form an equivalence between the Grothendieck completion of the logic naturals and the standard integers.
background
LogicInt is the Grothendieck completion of LogicNat under addition, realized as the quotient of pairs of logic naturals by the equivalence that identifies (a, b) with (c, d) precisely when a + d equals b + c. This construction turns the additive monoid of logic naturals into a group, exactly as the standard integers arise from the naturals.
proof idea
The definition constructs the equivalence by setting the forward function to the recovery map, the inverse function to the explicit embedding of standard integers, and supplying the two inverse theorems as the left and right inverse proofs.
why it matters
This equivalence supplies the carrier identification required to transfer the ring operations from the standard integers, as indicated by the module comment on ring-homomorphism properties that immediately follows. It closes the foundational step that recovers classical arithmetic inside the logic construction, supporting the claim that the forcing chain yields the integers without extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.