Foundation Rationals From Logic To Rat Zero

The zero element

A rational number is any number that can be written as a ratio of two whole numbers, such as 3/4 or -7/2. The number zero fits this definition as the ratio 0/1. In the Recognition Science framework, the rational numbers are not taken as a starting point; they are built from more basic pieces. The framework first constructs a type called LogicRat, a discrete record of equivalence classes of pairs of integers with non-zero denominators, then defines arithmetic operations on it. The declaration toRat_zero is a theorem in the framework's machine-checked library of formal theorems that connects this internally built zero to the standard rational zero.

Specifically, the theorem states that the function which maps a framework-built rational number to an ordinary rational number sends the framework's zero to the number 0. This is a structural guarantee: the zero element inside the framework is not a new or exotic object, but is exactly the familiar zero of the rational numbers. The proof is direct, using the definition of the framework's zero as the pair (0, 1) and the definition of the mapping function. This result is part of a larger effort in the framework to show that its internally constructed number systems behave identically to the standard ones.

The theorem is one of several that establish the framework's rational numbers are a faithful copy of the usual rationals. Other theorems in the same library prove that the mapping function preserves addition and multiplication, and that the framework's rational numbers are in fact equivalent as a structure to the standard rational numbers. The zero theorem is a small but necessary piece of this equivalence: it ensures that the identity element for addition is carried over correctly.

In Recognition Science, this matters because the framework aims to derive mathematical structure from a single starting point: a ledger of recognition events. The rational numbers, and their zero element, are part of that derivation. The theorem toRat_zero shows that even the most basic arithmetic object, zero, is not assumed but is constructed and then verified to match the classical definition.

theorem toRat_zero : toRat (0 : LogicRat) = 0 := by
  show toRat (mk 0 1 _) = 0
  rw [toRat_mk, toInt_zero, toInt_one]
  norm_num

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

/-- 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

The theorem does not claim that the framework's zero is the only zero, nor that the construction of rational numbers is unique. The theorem does not claim that the framework's rational numbers are the same as the standard rational numbers in every respect, only that they are equivalent as a structure.

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: