pith. machine review for the scientific record. sign in
structure definition def or abbrev high

LogicReal

show as:
view Lean formalization →

LogicReal wraps Mathlib's Bourbaki completion of the rationals to serve as the recovered real line obtained from the logic-derived rationals. Researchers recovering number systems in the Recognition Science foundation cite it to transport theorems from standard analysis back to the logic layer without global instance clashes. The definition is a one-field structure that isolates the completion while preserving the equivalence LogicRat ≃ ℚ.

claimThe recovered real numbers are the structure whose single field is an element of the Bourbaki completion of the rationals, obtained by completing the recovered rationals that are equivalent to the standard rationals.

background

The module recovers the real numbers from the Law-of-Logic layer. It starts from LogicNat and LogicInt, reaches LogicRat via the equivalence to ℚ supplied by RationalsFromLogic, and applies Mathlib's uniform-space completion to produce the reals. The type LogicReal is introduced precisely as a wrapper around CompareReals.Bourbakiℝ to avoid polluting global instances on the completion while still allowing reuse of all existing real-line results. Algebra and order on the recovered reals are defined by transport along the canonical comparison map to Mathlib's Cauchy reals.

proof idea

The declaration is a structure definition consisting of a single field val of type CompareReals.Bourbakiℝ. No tactics or lemmas are applied; the construction is the wrapper itself.

why it matters in Recognition Science

LogicReal supplies the real numbers required by LogicComplex in ComplexFromLogic and by the bootstrap theorem real_supports_logic in DomainBootstrap. It completes the recovery chain from recovered rationals to reals, enabling downstream transport of analytic statements into the logic-derived setting. The wrapper touches the open question of whether the completion can be internalized without external Mathlib dependence.

scope and limits

formal statement (Lean)

  66structure LogicReal where
  67  val : CompareReals.Bourbakiℝ
  68
  69namespace LogicReal
  70
  71/-- Transport a recovered real to Mathlib's real line. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more