IndisputableMonolith.Foundation.IntegersFromLogic
This module defines LogicInt via the Grothendieck construction on LogicNat pairs under the relation (a,b) ~ (c,d) iff a+d=c+b. It is imported by RationalsFromLogic and the tower audit to continue the logic-derived number system. The module consists entirely of definitions and basic quotient constructions with no theorems proved inside it.
claimThe equivalence relation on pairs of LogicNat given by $(a,b)sim(c,d)$ iff $a+d=c+b$, where the class of $(a,b)$ represents the formal difference $a-b$. LogicInt is the quotient setoid under this relation.
background
The module imports ArithmeticFromLogic, which supplies the type LogicNat and its addition. It forms the second stage of the recovered number tower LogicNat to LogicInt to LogicRat to LogicReal to LogicComplex. The Grothendieck relation is the standard device that turns a commutative monoid into a group by formal differences.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
Supplies LogicInt to RationalsFromLogic and to the audit surface in RecoveredTowerAxiomAudit whose doc states the goal is to pin the named recovery theorems for the full tower. Also feeds LogicLedgerInterop for transfer to the integer-ledger phase-budget surface. It completes the integer step in the logic-to-arithmetic recovery.
scope and limits
- Does not prove that LogicInt forms a ring.
- Does not embed LogicInt into the standard integers.
- Does not derive any mass or constant formulas.
- Does not invoke the forcing chain or J-uniqueness.
used by (3)
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