Foundation Reals From Logic To Real Of Rat Core

The rational core

The real numbers are usually built from the rationals by filling in the gaps. The declaration toReal_ofRatCore is a small piece of that construction inside the Recognition Science framework's machine-checked library of formal theorems. It states that a rational number, when placed into the framework's real number type, maps back to the same rational value under the comparison map. In plainer terms, the rationals sit inside the reals exactly as expected, with no distortion.

The framework's real numbers, called LogicReal, are a wrapper around a standard completion of the rationals. The map toReal sends each LogicReal to its corresponding real number. The declaration toReal_ofRatCore says that for any rational q, the real number obtained from q is just q itself. This is a coherence property: the framework's rationals and reals agree on the rational core, so later theorems can move freely between the two without worrying about translation errors.

This declaration does not claim that the framework invented a new kind of real number. It uses Mathlib's existing completion of the rationals as its engine. It does not claim that the real numbers are unique, nor that this construction is the only possible one. It does not claim anything about the physical constants or the forcing chain that the framework derives elsewhere. It is a technical bridge, not a discovery.

In Recognition Science, the point is that the reals are recovered from a logic-derived rational layer. The framework models a path from the law of logic through rationals to reals, and toReal_ofRatCore is the hinge that makes the path coherent. For a reader, the practical consequence is that any theorem about the usual real numbers can be read back as a theorem about the framework's reals, because the rational core matches.

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

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

/-- Transport a recovered real to Mathlib's real line. -/
noncomputable def toReal (x : LogicReal) : ℝ :=
  CompareReals.compareEquiv x.val

What this page does not claim

This declaration does not claim that the real numbers are uniquely determined by the rationals. It does not claim that the framework's reals differ from the standard reals in any substantive way. It does not claim any physical significance for the rational core itself.

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: