IndisputableMonolith.Foundation.RationalsFromLogic
This module builds the rational layer by defining pre-rationals as pairs of recovered integers with nonzero denominator and forming their quotient LogicRat. Number-tower recovery work and logic-native number theory cite it as the bridge from LogicInt to reals. The module is purely definitional with no theorems proved.
claimPre-rational numbers are pairs $(n,d)$ with $n,d$ integers and $d≠0$. The equivalence identifies $(n_1,d_1)$ with $(n_2,d_2)$ when $n_1 d_2 = n_2 d_1$. The quotient by this relation yields the logic rationals.
background
The module continues the logic-native number tower begun in IntegersFromLogic. It introduces PreRat as the set of pairs of integers with nonzero second component, ratRel as the standard cross-multiplication equivalence, the induced setoid, and the quotient type LogicRat together with the canonical map from integers. The local setting is the recovery of arithmetic structures directly from the Law-of-Logic without external set-theoretic assumptions.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
LogicRat supplies the rational input to RealsFromLogic for Bourbaki completion of the reals, to RecoveredTowerAxiomAudit for the full chain LogicNat → LogicInt → LogicRat → LogicReal → LogicComplex, and to LogicErdosStrausRCL for transporting rational identities. It completes the third step of the recovered tower.
scope and limits
- Does not define addition or multiplication on the quotient.
- Does not prove that the quotient is a field.
- Does not embed the integers or prove any arithmetic identities.
- Does not reference the J-function, phi-ladder, or forcing chain.
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'