Foundation Rationals From Logic Rat Rel Refl

Reflexivity of rational equivalence

A rational number is a ratio of two whole numbers, like 2/3 or 7/4. But the same ratio can be written in many ways: 1/2, 2/4, and 3/6 all represent the same number. To build rational numbers from scratch, one first collects all pairs of whole numbers (with a non-zero denominator) and then declares two pairs equivalent when their cross-products match: a/b and c/d are equivalent exactly when a times d equals c times b. This equivalence relation is the backbone of the construction; it is what lets 1/2 and 2/4 be treated as the same object.

The declaration ratRel_refl is the reflexivity part of that relation: every pair is equivalent to itself. In symbols, for any pair p, the relation holds between p and p. This is not a deep fact; it is immediate from the definition, since a times b equals a times b. Its importance is structural. An equivalence relation must satisfy three rules: reflexivity, symmetry, and transitivity. The machine-checked library of formal theorems proves all three, and reflexivity is the first. Without it, the whole construction of rational numbers as equivalence classes would not get off the ground.

In Recognition Science, this reflexivity theorem is a small but necessary step in a larger program: building the rational numbers from logic alone, without assuming them as a primitive. The framework's library constructs a type called LogicRat as the collection of equivalence classes under this relation, and then proves that this type behaves exactly like the familiar rational numbers: addition, multiplication, and order all match. The reflexivity theorem is the first stone in that foundation.

What ratRel_refl does not claim is any fact about the size of the equivalence classes, the existence of any particular rational number, or the behavior of arithmetic. It only asserts that the relation is reflexive. It does not, by itself, prove that the relation is an equivalence relation; that requires the symmetry and transitivity theorems. And it says nothing about whether the constructed rational numbers are consistent with any prior notion of rationals; that consistency is established by later theorems, not by this one.

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

What this page does not claim

The reflexivity theorem alone does not prove that the relation is an equivalence relation. It does not establish any property of rational arithmetic. It does not claim that the constructed rationals match any prior notion of rationals.

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: