Foundation Rationals From Logic From Rat To Rat

The round trip

A rational number is a ratio of two whole numbers, like 3/4 or 22/7, with the denominator never zero. The framework builds its own version of these numbers, called LogicRat, from pairs of integers. The declaration fromRat_toRat proves a round trip: if you take a rational number, translate it into the framework's pair-based structure, and then translate it back, you recover the original number exactly. The proof is a theorem in the framework's machine-checked library of formal theorems, meaning a computer verified every step.

The framework's construction starts with a pre-rational: a pair of integers (numerator, denominator) with a proof that the denominator is not zero. Two such pairs are considered the same if their cross-products match, so (1,2) and (2,4) are the same pre-rational. The framework then groups these pairs into equivalence classes, and the result is LogicRat. The fromRat function maps an ordinary rational number into this structure, and toRat maps it back out. The theorem fromRat_toRat states that for every element q of LogicRat, applying fromRat after toRat gives q itself.

This round trip is not a mere bookkeeping exercise. It establishes that the framework's LogicRat is a faithful copy of the rational numbers, not a distorted approximation. The theorem is part of a larger equivalence: the framework also proves that the two structures are interchangeable, with fromRat and toRat serving as two-way translators. Addition and multiplication in LogicRat match their ordinary counterparts, and the usual algebraic laws, such as commutativity and associativity, hold in the new setting.

In Recognition Science, the rational numbers are not assumed as a given. They are derived from more basic logical ingredients, and this theorem confirms that the derivation loses nothing. The round trip is a bridge: it shows that the framework's internal numbers behave exactly like the numbers everyone already uses. What the theorem does not claim is that this construction is the only way to build rationals, nor does it say anything about the physical world. It is a statement about mathematical structure, verified in the framework's formal library.

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

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

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 LogicRat is the only possible construction of rational numbers. It does not claim that the framework's rationals have any physical meaning or empirical content. It does not claim that the construction is computable in practice, since the definition is marked noncomputable.

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: