Foundation Rationals From Logic Rat Rel Trans

The transitivity of rational equivalence

In ordinary arithmetic, two fractions are equal when their cross-products are equal: a/b equals c/d exactly when a times d equals c times b. This is the rule that lets a calculator treat 1/2 and 2/4 as the same number. The theorem called ratRel_trans in the Recognition Science framework's machine-checked library of formal theorems states that this relation is transitive: if a/b matches c/d, and c/d matches e/f, then a/b matches e/f. It is a formal, computer-verified proof that the equality of fractions behaves as it should when chained across three terms.

The theorem is not an isolated curiosity. It is one of three properties, together with reflexivity (every fraction matches itself) and symmetry (if a/b matches c/d, then c/d matches a/b), that make the matching relation an equivalence relation. An equivalence relation is what allows a collection of fractions to be partitioned into classes, each class gathering all the fractions that represent the same rational number. The framework's library proves all three properties and then uses them to define the rational numbers themselves as these equivalence classes, so the transitivity theorem is a load-bearing step in constructing the rationals from a purely logical foundation.

In Recognition Science, this construction is part of a larger program: deriving the structures of mathematics and physics from a single starting point about recognition events. The rational numbers here are not assumed as a primitive; they are built up from pairs of integers with non-zero denominators, with equality defined by the cross-product rule. The transitivity theorem ensures that this definition is coherent, that the classes do not overlap in contradictory ways. The framework's library records the proof as a theorem, meaning it has been checked by a machine against the library's axioms, with no unverified assumptions.

What the theorem does not claim is important. It does not assert that the cross-product rule is the only way to define equality of fractions, nor does it say anything about the properties of the rational numbers beyond their construction. It does not prove that the rationals are complete, that they are dense, or that they can be ordered. It establishes only the transitivity of the specific relation defined by the cross-product rule, a necessary but modest step in the larger logical edifice.

theorem ratRel_trans : ∀ {p q r : PreRat}, ratRel p q → ratRel q r → ratRel p r := by
  rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ ⟨e, f, hf⟩ hpq hqr
  -- hpq : a * d = c * b
  -- hqr : c * f = e * d
  -- goal: a * f = e * b
  -- Method: (a * f) * d = a * f * d = a * d * f = c * b * f = c * f * b = e * d * b = (e * b) * d.
  -- Cancel d ≠ 0.
  show a * f = e * b
  have key : (a * f) * d = (e * b) * d := by
    calc (a * f) * d
        = (a * d) * f := by rw [mul_assoc', mul_comm' f d, ← mul_assoc']
      _ = (c * b) * f := by rw [hpq]
      _ = (c * f) * b := by rw [mul_assoc', mul_comm' b f, ← mul_assoc']
      _ = (e * d) * b := by rw [hqr]
      _ = (e * b) * d := by rw [mul_assoc', mul_comm' d b, ← mul_assoc']
  exact mul_right_cancel hd key

theorem ratRel_refl : ∀ p : PreRat, ratRel p p := by
  intro p
  show p.num * p.den = p.num * p.den
  rfl

theorem ratRel_symm : ∀ {p q : PreRat}, ratRel p q → ratRel q p := by
  intro p q h
  show q.num * p.den = p.num * q.den
  exact h.symm

theorem ratRel_trans : ∀ {p q r : PreRat}, ratRel p q → ratRel q r → ratRel p r := by
  rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ ⟨e, f, hf⟩ hpq hqr
  -- hpq : a * d = c * b
  -- hqr : c * f = e * d
  -- goal: a * f = e * b
  -- Method: (a * f) * d = a * f * d = a * d * f = c * b * f = c * f * b = e * d * b = (e * b) * d.
  -- Cancel d ≠ 0.
  show a * f = e * b
  have key : (a * f) * d = (e * b) * d := by
    calc (a * f) * d
        = (a * d) * f := by rw [mul_assoc', mul_comm' f d, ← mul_assoc']
      _ = (c * b) * f := by rw [hpq]
      _ = (c * f) * b := by rw [mul_assoc', mul_comm' b f, ← mul_assoc']
      _ = (e * d) * b := by rw [hqr]
      _ = (e * b) * d := by rw [mul_assoc', mul_comm' d b, ← mul_assoc']
  exact mul_right_cancel hd key

instance setoid : Setoid PreRat := ⟨ratRel, ratRel_refl, ratRel_symm, ratRel_trans⟩

/-- `LogicRat` is the field of fractions of `LogicInt`. -/
def LogicRat : Type := Quotient (setoid : Setoid PreRat)

What this page does not claim

This theorem does not prove that the cross-product rule is the only possible definition of fraction equality. It does not establish any property of the rational numbers beyond their construction from equivalence classes. It does not claim that the rational numbers are complete, dense, or ordered.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/RationalsFromLogic.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: