Foundation Rationals From Logic

The rationals, rebuilt

A rational number is any number that can be written as a fraction of two whole numbers, like 3/4 or -7/2, where the bottom number is not zero. The standard way to build them, used in mathematics and in the formal libraries that underpin proof assistants, starts with ordered pairs. The pair (2, 4) and the pair (1, 2) are different pairs, but they name the same rational number, because 2 times 2 equals 4 times 1. The construction groups all such equivalent pairs into one object, and that object is the rational number 1/2.

In Recognition Science, the framework's machine-checked library of formal theorems repeats this classical construction, but it does so on top of its own logical integers. The module defines a pre-rational, a discrete record of a numerator and a non-zero denominator, then declares two pre-rationals equivalent when their cross-products match. The equivalence relation is reflexive, symmetric, and transitive, which makes it a proper setoid, and the rationals themselves are the resulting quotient type. This is not a new kind of number; it is the same rationals, rebuilt from the framework's own foundations.

The module then proves that this rebuilt structure behaves exactly like the familiar rationals. Addition, multiplication, negation, zero, and one are all defined, and the library checks the field laws: addition and multiplication are commutative and associative, multiplication distributes over addition, and adding a number to its negative gives zero. Each law is a theorem, not an assumption. The proofs are short because the module defines a map from its logical rationals to the standard rationals, and the map preserves all the operations, so the field laws follow from the standard ones.

The central result is an equivalence: the logical rationals and the standard rationals are the same structure. The module constructs a bijection between them and proves it respects addition and multiplication. In plain language, the framework has shown that its own rational numbers are not a lookalike or a shadow; they are the real thing, with all the same arithmetic. This matters because the framework aims to derive physics from logic alone, and the rationals are the first infinite number system it needs. The module is the foundation under that derivation, and the machine-checked proof is what makes the foundation load-bearing.

/-- A pre-rational is a pair `(num, den)` with `den ≠ 0`. -/
structure PreRat where
  num         : LogicInt
  den         : LogicInt
  den_nonzero : den ≠ 0

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

/-- Carrier equivalence between recovered rationals and Mathlib rationals. -/
noncomputable def equivRat : LogicRat ≃ ℚ where
  toFun := toRat
  invFun := fromRat
  left_inv := fromRat_toRat
  right_inv := toRat_fromRat

theorem toRat_add (a b : LogicRat) : toRat (a + b) = toRat a + toRat b := by
  induction a using Quotient.inductionOn with
  | h p =>
    induction b using Quotient.inductionOn with
    | h q =>
      rcases p with ⟨a, b, hb⟩
      rcases q with ⟨c, d, hd⟩
      show toRat (mk (a * d + c * b) (b * d) _) =
        toRat (mk a b hb) + toRat (mk c d hd)
      simp only [toRat_mk, toInt_add, toInt_mul]
      push_cast
      have hbq : (toInt b : ℚ) ≠ 0 := by
        intro h; apply hb; rw [eq_iff_toInt_eq, toInt_zero]; exact_mod_cast h
      have hdq : (toInt d : ℚ) ≠ 0 := by
        intro h; apply hd; rw [eq_iff_toInt_eq, toInt_zero]; exact_mod_cast h
      field_simp [hbq, hdq]

theorem toRat_mul (a b : LogicRat) : toRat (a * b) = toRat a * toRat b := by
  induction a using Quotient.inductionOn with
  | h p =>
    induction b using Quotient.inductionOn with
    | h q =>
      rcases p with ⟨a, b, hb⟩
      rcases q with ⟨c, d, hd⟩
      show toRat (mk (a * c) (b * d) _) =
        toRat (mk a b hb) * toRat (mk c d hd)
      simp only [toRat_mk, toInt_mul]
      push_cast
      have hbq : (toInt b : ℚ) ≠ 0 := by
        intro h; apply hb; rw [eq_iff_toInt_eq, toInt_zero]; exact_mod_cast h
      have hdq : (toInt d : ℚ) ≠ 0 := by
        intro h; apply hd; rw [eq_iff_toInt_eq, toInt_zero]; exact_mod_cast h
      field_simp [hbq, hdq]

What this page does not claim

This module does not derive the real numbers or any analytic structure beyond the rationals. The construction does not introduce new arithmetic laws; it proves the standard field laws for a new representation. The framework's rationals are not claimed to be physically real; the module is a logical foundation, not a physical model.

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: