Foundation Rationals From Logic Eq Iff To Rat Eq

The recognition ledger's rationals

Rational numbers are the quotients of integers, like 3/4 or -7/2, with a denominator that is never zero. The Recognition Science framework builds its own version of these numbers, called logic rationals, as a discrete record of events: a pair of integer entries, a numerator and a non-zero denominator, grouped so that 2/4 and 1/2 count as the same entry. The declaration eq_iff_toRat_eq proves the bridge between this internal ledger and the familiar rationals: two logic rationals are equal if and only if their ordinary rational values are equal.

This is an equivalence, not a one-way map. The proof shows that the ledger's equality relation, built from the cross-multiplication rule p.num * q.den = q.num * p.den, lines up exactly with equality of the rational numbers they represent. The framework then uses this bridge to prove that its logic rationals form a field: addition, multiplication, negation, and the distributive law all hold, with proofs that rewrite through the equivalence to the standard rational arithmetic. The result is a complete algebraic structure, not just a notation.

In Recognition Science, the point of this construction is that the ledger is the primitive object. The framework derives the rational numbers from its own logic of discrete events, then proves that this derived structure is indistinguishable from the classical rationals. The machine-checked library of formal theorems records this as a proved equivalence, with no hidden assumptions beyond the standard foundations of logic.

What the declaration does not claim is that it defines the rational numbers from scratch. It builds a new representation and proves it equivalent to the existing one. It also does not claim that the rationals are the only numbers the framework can build; the construction is a foundation for further number systems, not a claim about their uniqueness. The proof is a bridge, not a replacement.

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]

What this page does not claim

The declaration does not define the rational numbers from scratch; it builds a new representation equivalent to the existing rationals. The proof does not show that logic rationals are the only number system the framework can construct. The equivalence does not imply that the framework's ledger is the same object as the classical rationals, only that they are isomorphic.

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: