IndisputableMonolith.Foundation.IntegersFromLogic
Constructs the integers as the Grothendieck group of the additive monoid of logic-derived naturals. Pairs of LogicNat are quotiented by the difference relation (a,b)~(c,d) iff a+d=c+b, yielding LogicInt with zero, one, and the embedding of naturals. Downstream rational and tower-audit modules import this layer. The module is definitional: setoid, quotient, and basic constructors.
claimFrom the additive monoid of logic naturals, form the integers as the Grothendieck group: pairs $(a,b)$ of naturals represent formal differences $a-b$, under the equivalence $(a,b)\sim(c,d)$ iff $a+d=c+b$. The quotient is $\mathrm{LogicInt}$, with canonical embedding of naturals, zero, and one.
background
Recognition Science rebuilds the number tower from a Law-of-Logic substrate rather than assuming classical $\mathbb{Z}$ as primitive. The prior module ArithmeticFromLogic supplies LogicNat together with its additive monoid structure.
This module applies the standard Grothendieck construction for the group completion of a commutative monoid. On pairs of LogicNat one defines the relation $(a,b)\sim(c,d)$ precisely when $a+d=c+b$; the pair stands for the formal difference $a-b$. Reflexivity, symmetry, and transitivity are recorded so that the relation is a setoid, and LogicInt is the corresponding quotient type.
Constructors include the class map mk, a soundness lemma for the relation, the embedding ofLogicNat of naturals into integers, and the distinguished elements zero and one.
proof idea
Definition module, not a single theorem. It introduces the relation intRel, proves the three equivalence laws (refl, symm, trans), packages them as a setoid, and forms the quotient LogicInt. Remaining declarations are constructors and basic identities (mk, sound, ofLogicNat, ofLogicNat_zero, zero, one) obtained directly from the quotient API and the monoid operations on LogicNat.
why it matters in Recognition Science
LogicInt is the second rung of the recovered number tower LogicNat → LogicInt → LogicRat → LogicReal → LogicComplex. RationalsFromLogic imports this module to build fractions of integers; RecoveredTowerAxiomAudit imports it so that the named recovery and transport theorems for the whole tower sit behind a single #print axioms surface. Without a logic-native integer layer, the later rational and real reconstructions would still depend on classical Mathlib integers rather than on the Law-of-Logic substrate.
scope and limits
- Does not construct multiplication or the ordered ring structure on LogicInt.
- Does not prove universality of the Grothendieck group beyond the quotient definition.
- Does not define rationals, reals, or complexes; those live in downstream modules.
- Does not discharge classical axiom audits; RecoveredTowerAxiomAudit only aggregates the tower.
used by (2)
depends on (1)
declarations in this module (42)
-
def
intRel -
theorem
intRel_refl -
theorem
intRel_symm -
theorem
intRel_trans -
instance
setoid -
def
LogicInt -
def
mk -
theorem
sound -
def
ofLogicNat -
theorem
ofLogicNat_zero -
def
zero -
def
one -
def
neg -
def
add -
def
mul -
def
toIntCore -
theorem
toIntCore_respects -
def
toInt -
def
fromInt -
theorem
toInt_mk -
theorem
toInt_fromInt -
theorem
fromInt_toInt -
def
equivInt -
theorem
toInt_zero -
theorem
toInt_one -
theorem
toInt_add -
theorem
toInt_neg -
theorem
toInt_mul -
theorem
eq_iff_toInt_eq -
theorem
add_assoc' -
theorem
add_comm' -
theorem
zero_add' -
theorem
add_zero' -
theorem
add_left_neg' -
theorem
mul_assoc' -
theorem
mul_comm' -
theorem
one_mul' -
theorem
mul_one' -
theorem
mul_add' -
theorem
add_mul' -
theorem
mul_eq_zero -
theorem
mul_right_cancel