Foundation Rationals From Logic To Rat From Rat

The two-way bridge

A rational number is any number that can be written as a fraction of two whole numbers, like 3/4 or -7/2. The framework's library of formal theorems builds its own version of these numbers from a more basic structure: a pair of integers, with the second one not zero, where two pairs are considered equal if their cross-products match, so (1,2) and (2,4) name the same value. This new type, called LogicRat, is a ledger, a discrete record of events, in this case the record of all possible fractions.

The declaration toRat_fromRat is the return trip. It proves that every rational number in the standard sense can be brought into this ledger, and that the journey back out returns you to exactly where you started. More precisely, it shows that for any standard rational q, converting q into the ledger and then converting the result back yields q itself. This is not a guess or a convention; it is a theorem checked by the machine, with no gaps in its chain of reasoning.

The theorem matters because it makes the ledger a faithful copy, not a caricature. The library also proves that addition and multiplication in the ledger behave exactly like their ordinary counterparts: adding two ledger values and then converting to a standard rational gives the same result as converting first and then adding. The two-way bridge means any calculation done in the ledger can be translated without loss into the familiar language of fractions.

What the declaration does not claim is just as important. It does not say the ledger is the only way to build rational numbers, nor that the ledger's construction is simpler than the standard one. It only establishes a precise correspondence: the ledger and the standard rationals are interchangeable for the purposes of arithmetic. The bridge is exact, but it is a bridge between two equal partners, not a claim that one side is the true home of fractions.

/-- The other round trip: every logic-native rational is recovered from
its image in Mathlib's `Rat`. This is the key injectivity theorem for
the transport API. -/
theorem fromRat_toRat : ∀ q : LogicRat, fromRat (toRat q) = q := by
  intro q
  induction q using Quotient.inductionOn with
  | h p =>
    rcases p with ⟨a, b, hb⟩
    show fromRat (toRat (mk a b hb)) = mk a b hb
    rw [toRat_mk]
    apply sound
    -- It remains to prove `fromInt ((a/b).num) * b = a * fromInt ((a/b).den)`.
    rw [eq_iff_toInt_eq, toInt_mul, toInt_mul, toInt_fromInt, toInt_fromInt]
    have hb_rat : (toInt b : ℚ) ≠ 0 := by
      intro h
      apply hb
      rw [eq_iff_toInt_eq, toInt_zero]
      exact_mod_cast h
    have hden_rat : (((toInt a : ℚ) / toInt b).den : ℚ) ≠ 0 := by
      exact_mod_cast (ne_of_gt ((toInt a : ℚ) / toInt b).den_pos)
    have hq :
        ((((toInt a : ℚ) / toInt b).num : ℚ) /
          (((toInt a : ℚ) / toInt b).den : ℚ))
          = (toInt a : ℚ) / toInt b := by
      exact_mod_cast ((toInt a : ℚ) / toInt b).num_div_den
    have hcross :
        (((toInt a : ℚ) / toInt b).num : ℚ) * (toInt b : ℚ)
          = (toInt a : ℚ) * (((toInt a : ℚ) / toInt b).den : ℚ) := by
      rwa [div_eq_div_iff hden_rat hb_rat] at hq
    exact_mod_cast hcross

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 ledger is not claimed to be the only way to construct rational numbers. The construction is not claimed to be simpler than the standard definition. The bridge does not claim that the ledger and standard rationals are identical, only that they are interchangeable for arithmetic.

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: