Foundation Reals From Logic To Real Of Logic Rat

The recovery map

The real numbers are usually taken as given: a line with no gaps, built by filling the holes between rationals. A rational number like 2/3 is an exact point on that line. The declaration toReal_ofLogicRat concerns a different route to the same destination. In the Recognition Science framework, the rationals are first recovered from a layer of pure logic, then the reals are recovered from those rationals. The declaration states that this recovery map sends each logic-built rational to the real number it ought to be, the same real number that ordinary mathematics assigns to that rational.

The construction works in two steps. First, a type called LogicRat holds rational numbers built from logical principles alone, with no appeal to measurement or geometry. Second, a type called LogicReal wraps the standard completion of the rationals, the usual way mathematicians construct the reals as limits of rational sequences. The map toReal is the bridge between them. The declaration toReal_ofLogicRat says that when a logic-built rational q is sent across this bridge, the result equals the ordinary real number that q names. In symbols: toReal (ofLogicRat q) = q, where the left q is a logic-built rational and the right q is its familiar real counterpart.

This is a coherence result, not a new number system. It guarantees that the logic-built rationals behave exactly like the rationals everyone already uses. Addition, multiplication, order, and division all agree with their standard counterparts, as do the field laws such as commutativity and associativity. The declaration is part of a machine-checked library of formal theorems, meaning a computer verified the proof step by step. The value lies in the architecture: the framework starts from logic, builds integers, then rationals, then reals, and at each stage the new objects match the classical ones exactly.

What the declaration does not claim is just as important. It does not say that the reals are defined by this map, only that the two constructions agree where both exist. It does not introduce a new real number, a new rational, or a new notion of limit. The completion engine used is the standard one from mathematics, not a novel construction. And the declaration says nothing about whether the logic-built rationals are philosophically prior to ordinary rationals; it only states a formal equivalence between two ways of reaching the same numbers.

theorem toReal_fromReal (x : ℝ) : toReal (fromReal x) = x := by
  simp [toReal, fromReal]

@[simp] theorem toReal_mul (x y : LogicReal) : toReal (x * y) = toReal x * toReal y :=
  toReal_fromReal _

@[simp] theorem toReal_div (x y : LogicReal) : toReal (x / y) = toReal x / toReal y :=
  toReal_fromReal _

theorem lt_iff_toReal_lt {x y : LogicReal} : x < y ↔ toReal x < toReal y := Iff.rfl

/-- Coerce a Mathlib rational into the Bourbaki completion. -/
noncomputable def ofRatCore (q : ℚ) : LogicReal :=
  ⟨Completion.coe' (show CompareReals.Q from q)⟩

What this page does not claim

The declaration does not define the reals, only proves agreement between two constructions. It does not claim that logic-built rationals are philosophically prior to ordinary rationals. It introduces no new real numbers, rationals, or limits.

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/RealsFromLogic.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: