Foundation Reals From Logic Bourbaki Complete

The recovered reals

The real numbers are the continuous number line that fills the gaps between rationals like 1/2 and 2/3. A standard way to construct them, due to Augustin-Louis Cauchy and refined by Nicolas Bourbaki's school, is to take all sequences of rationals that cluster together, such as 3, 3.1, 3.14, 3.141, and declare each such Cauchy sequence to name a real number. The framework's machine-checked library of formal theorems shows this construction works starting from its own recovered rationals, which it builds from a logic layer rather than assuming numbers exist.

The declaration bourbaki_complete establishes that the framework's recovered reals, called LogicReal (a discrete record of events, in this case the events being rational approximations), are exactly the usual real numbers. The library proves the map between them preserves addition, multiplication, order, and every algebraic law, so any theorem about ordinary reals translates directly. This is a transport-first design: the framework pulls back the standard real structure along this map, meaning downstream proofs can reuse the existing real theorems without re-deriving them.

In Recognition Science, the recovery of the reals is a step in a larger chain that derives physical constants from the cost of recognition, but this file itself makes no physical claim. It proves a mathematical equivalence: the reals built from logic-rational Cauchy sequences are isomorphic to the standard reals. The construction uses Mathlib's Bourbaki completion of the rationals as its engine, and the input rationals are the framework's own recovered rationals from an earlier file.

What this does not claim is any new mathematics. The real numbers were already constructed this way in the 19th century, and the framework's contribution is showing its own logical foundation reproduces them faithfully. It also does not claim that the reals are the only possible completion, nor that the logic layer is the unique starting point. The declaration is a bridge: it says the framework's numbers behave exactly like the numbers everyone else uses, so the framework can stand on the full edifice of real analysis.

/-- `LogicReal` is the Cauchy completion of the recovered rationals, realized
through the canonical completion of `ℚ` and the equivalence `LogicRat ≃ ℚ`.

The wrapper prevents global instance pollution on `Completion ℚ` while still
letting us reuse Mathlib's completed real line. -/
structure LogicReal where
  val : CompareReals.Bourbakiℝ

theorem le_iff_toReal_le {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

This does not claim new mathematics; the Cauchy completion of the rationals dates to the 19th century. This does not claim the reals are the only possible completion of the rationals. This does not claim the logic layer is the unique starting point for constructing numbers.

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: