Foundation Rationals From Logic To Rat Core Respects

The well-defined bridge

A rational number is a ratio of two integers, like 2/3 or 15/10. The same rational can be written in many ways: 15/10 and 3/2 both name the number 1.5. A construction of the rationals from logic must therefore ensure that every way of writing a number leads to the same result. The declaration toRatCore_respects is the machine-checked proof of exactly that: two fraction pairs that are equivalent, meaning they name the same rational, are sent to the same value by the core conversion function.

In the framework's library, a pre-rational is a pair of integers with a non-zero denominator. Two pre-rationals are related when cross-multiplication agrees: p.num * q.den = q.num * p.den. This is the standard equivalence for fractions. The declaration proves that the function mapping a pre-rational to its rational value, defined as numerator divided by denominator, respects this equivalence. If two pairs are related, their computed values are equal. This is the well-definedness condition that lets the function be lifted from pairs to equivalence classes, forming the type LogicRat.

This single proof is the load-bearing step in building the rational numbers as a quotient structure. It guarantees that the map from LogicRat to the usual rationals is coherent, so that arithmetic operations like addition and multiplication, defined on the quotient, agree with ordinary rational arithmetic. The library then proves the field axioms for this construction, showing that the logical rationals behave exactly like the familiar rationals.

In Recognition Science, this is part of a larger program: deriving mathematical structure from a ledger of recognition events. The rationals are built from logic alone, with no axioms beyond the standard ones of the ambient type theory. The declaration is a technical but essential link in that chain, ensuring the constructed numbers are genuinely well-defined.

The declaration does not claim that the rationals are the only numbers, nor that this construction is the only way to build them. It does not prove that the rationals are complete or that they contain limits of all sequences. It simply establishes the coherence of one specific construction step, a necessary condition for the whole edifice to stand.

theorem toRatCore_respects :
    ∀ p q : PreRat, p ≈ q → toRatCore p = toRatCore q := by
  rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ h
  show (toInt a : ℚ) / toInt b = (toInt c : ℚ) / toInt d
  have hb_int : (toInt b : ℚ) ≠ 0 := by
    intro habs
    apply hb
    rw [eq_iff_toInt_eq, toInt_zero]
    exact_mod_cast habs
  have hd_int : (toInt d : ℚ) ≠ 0 := by
    intro habs
    apply hd
    rw [eq_iff_toInt_eq, toInt_zero]
    exact_mod_cast habs
  have h' : toInt a * toInt d = toInt c * toInt b := by
    have := congrArg toInt (show a * d = c * b from h)
    rwa [toInt_mul, toInt_mul] at this
  rw [div_eq_div_iff hb_int hd_int]
  exact_mod_cast h'

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

/-- The field-of-fractions equivalence: `(a, b) ~ (c, d)` iff
`a * d = c * b`. -/
def ratRel : PreRat → PreRat → Prop :=
  fun p q => p.num * q.den = q.num * p.den

What this page does not claim

The declaration does not prove the rationals are complete or contain limits of all sequences. The declaration does not claim this is the only way to construct the rational numbers. The declaration does not establish that the rationals are the only numbers derivable from logic.

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: