IndisputableMonolith.Foundation.RationalsFromLogic
This module recovers the rational numbers from the integers built via the law of logic. It introduces PreRat as pairs of integers with nonzero denominator, equips them with the equivalence ratRel, and forms the quotient LogicRat. Researchers tracing the logic-native number tower cite it when constructing reals or auditing recovery steps. The module consists entirely of definitions and relation lemmas with no complex proofs.
claimA pre-rational is a pair $(n,d)$ with $n,d$ integers and $d$ nonzero. The relation identifies $(n_1,d_1)$ with $(n_2,d_2)$ precisely when $n_1 d_2 = n_2 d_1$. The quotient by this equivalence yields LogicRat, the logic-recovered rationals.
background
The module continues the foundation recovery of arithmetic from logic, importing the integer layer and using Mathlib setoids. PreRat is the raw pair type with nonzero denominator. ratRel is the equivalence relation on these pairs, setoid packages it, and LogicRat is the resulting quotient type. This supplies the third stage of the tower LogicNat to LogicInt to LogicRat.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the rational layer in the recovered tower LogicNat to LogicInt to LogicRat to LogicReal to LogicComplex. It is imported by RealsFromLogic to complete LogicRat to reals via Bourbaki completion, by RecoveredTowerAxiomAudit to pin the named recovery theorems, and by LogicErdosStrausRCL to transport rational identities through LogicRat.toRat.
scope and limits
- Does not derive field operations or ordering on LogicRat.
- Does not address completeness or real-number constructions.
- Does not prove arithmetic identities beyond the quotient definition.
- Does not assume or recover classical reals inside the logic layer.
used by (3)
depends on (1)
declarations in this module (40)
-
structure
PreRat -
def
ratRel -
theorem
ratRel_refl -
theorem
ratRel_symm -
theorem
ratRel_trans -
instance
setoid -
def
LogicRat -
def
mk -
theorem
sound -
def
ofLogicInt -
def
zero -
def
one -
def
neg -
def
add -
def
mul -
def
toRatCore -
theorem
toRatCore_respects -
def
toRat -
def
fromRat -
theorem
toRat_mk -
theorem
toRat_fromRat -
theorem
fromRat_toRat -
def
equivRat -
theorem
eq_iff_toRat_eq -
theorem
toRat_zero -
theorem
toRat_one -
theorem
toRat_neg -
theorem
toRat_add -
theorem
toRat_mul -
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'