Foundation Reals From Logic Logic Real Recovered From Completion

Recovering the real numbers

The real numbers are the complete ordered field: the number system that fills every gap between rationals, so that every Cauchy sequence of rationals converges to a real. In the 1870s, Richard Dedekind and Georg Cantor gave the first rigorous constructions of this system from the rationals, using cuts and Cauchy sequences respectively. The Recognition Science framework reproduces this classical construction, but starts from a far more primitive base: not the rationals as given, but rationals recovered from a logical layer.

The framework's Cauchy sequence is the standard one: a sequence of rationals whose terms get arbitrarily close to each other beyond any chosen distance. The library defines LogicReal, a type whose elements are equivalence classes of such sequences, exactly as in Cantor's construction. The key theorem is that this object is isomorphic to the ordinary real numbers: the map toReal sends each LogicReal to its corresponding real, and it is a bijection preserving addition, multiplication, and order. This is not a new kind of real number; it is the same real line, built from a different basement.

The construction proceeds in stages. The framework first defines LogicNat, the natural numbers as logical objects, then integers, then rationals, and finally completes the rationals by Cauchy sequences to obtain the reals. Each stage is a formal theorem in the machine-checked library of formal theorems. The completion itself uses the standard mathematical tool of uniform-space completion, the same mechanism that produces the reals from the rationals in any modern treatment.

What this does not claim is more interesting than what it does. It does not claim that the real numbers are created by logic, only that they can be recovered from a logical starting point. It does not claim that this construction is simpler than the classical ones, only that it is possible within the framework's axioms. And it does not claim that the framework's physics, with its golden ratio and forcing chains, depends on this particular construction; the reals could be built in any of the standard ways and the physics would follow unchanged.

The payoff is architectural. The framework aims to derive physics from a single logical ledger of recognition events, and this theorem closes a gap: it shows that the real numbers, the arena in which all of physics is written, can be reached from the framework's own foundations without importing the reals as an unexamined primitive. The real line is not an assumption; it is a theorem.

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

theorem fromReal_toReal (x : LogicReal) : fromReal (toReal x) = x := by
  cases x
  simp [toReal, fromReal]

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

/-- A recovered-rational Cauchy sequence. The Cauchy predicate is measured
after transport to Mathlib's `ℚ`, using the standard uniform structure on
`ℚ`. This is the exact point where the recovered rational layer enters the
Cauchy completion. -/
structure CauchySeqLogicRat where
  seq : ℕ → LogicRat
  cauchy_toRat : CauchySeq (fun n => toRat (seq n))

/-- Embed a recovered rational into `LogicReal`. -/
noncomputable def ofLogicRat (q : LogicRat) : LogicReal :=
  ofRatCore (toRat q)

What this page does not claim

This construction creates the real numbers from nothing; it recovers them from a logical layer that already includes natural numbers. The framework's physics theorems, such as the forcing chain, rely on this specific construction of the reals. The construction is simpler or more efficient than Dedekind cuts or Cantor's original Cauchy sequence approach.

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: