LogicInt
plain-language theorem explainer
The integers arise as the Grothendieck completion of the logic-native naturals by quotienting ordered pairs under the equivalence that identifies (a, b) with (c, d) precisely when a plus d equals b plus c. Foundation researchers cite the construction to obtain a native integer carrier before ring operations are defined. The definition is the direct application of the Quotient constructor to the pre-established setoid on those pairs.
Claim. Let $N_L$ be the naturals forced by the law of logic. The logic-native integers are the quotient $Z_L = (N_L times N_L)/sim$, where $(a,b) sim (c,d)$ if and only if $a + d = b + c$.
background
The logic-native naturals form an inductive type whose identity constructor stands for the zero-cost element and whose step constructor iterates the generator, reproducing the orbit under multiplication by the forcing constant. The setoid on pairs encodes the Grothendieck equivalence that renders addition cancellative and well-defined on the quotient. The module belongs to the foundation layer that derives arithmetic directly from the law of logic, importing the natural-number construction together with the primitive-distinction axioms.
proof idea
The declaration is a one-line definition that applies the Quotient constructor to the setoid instance already established on pairs of logic-native naturals.
why it matters
LogicInt supplies the carrier for all subsequent integer operations in the module, including addition, negation, and the transfer principle that reduces ring identities to the standard integers. It completes the step from naturals to integers inside the forcing chain, enabling the later construction of rationals and the calibration of constants such as the inverse fine-structure constant. Downstream results such as add_assoc' and add_comm' inherit their proofs from the quotient structure via the equivalence to Int.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.