IndisputableMonolith.Foundation.RationalsFromLogic
The module constructs the rational layer of the logic-recovered number tower by defining pre-rationals as pairs of integers with nonzero denominator and quotienting by the standard fraction equivalence. Researchers recovering the reals or transporting number-theoretic results would cite it. The module is entirely definitional, introducing types, the relation, and the quotient with no theorems inside.
claimLet $\mathbb{Z}$ be the integers recovered from logic. A pre-rational is a pair $(a,b)$ with $b \neq 0$. The equivalence relation on pre-rationals is given by cross-multiplication: $(a,b) \sim (c,d)$ when $ad=bc$. The logic rationals are the quotient of the pre-rationals by this relation.
background
This module belongs to the foundation layer that recovers the classical number system from the Law of Logic. It follows the integers module and supplies the input for the reals module that follows. The setting uses the integers as the base type on which pairs are formed.
A pre-rational is a pair of integers with nonzero denominator. The equivalence relation identifies pairs that represent the same fraction via the usual cross-multiplication test, and the module records reflexivity, symmetry, and transitivity of that relation before forming the quotient.
The module imports only the integers module and is itself imported by the reals recovery, the tower audit, and the Erdős-Straus adapter.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the rational layer that the reals module uses to complete to the reals via Bourbaki completion of the recovered rationals, that the tower audit imports to pin the full sequence from naturals through complexes, and that the Erdős-Straus adapter uses to transport the classical theorem surface. It completes the third step in the recovered number tower.
scope and limits
- Does not verify that the quotient satisfies the field axioms.
- Does not exhibit an isomorphism to the standard rationals.
- Does not contain any arithmetic lemmas or identities.
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'