toReal
plain-language theorem explainer
The definition toReal transports each element of LogicReal, the Cauchy completion of logic-derived rationals, to Mathlib's standard real line via the canonical comparison equivalence. Researchers recovering analysis inside the Recognition Science framework cite this map when embedding recovered reals into classical theorems on complexes or algebraic rings. It is realized as a direct one-line application of compareEquiv to the wrapped Bourbaki completion.
Claim. Let LogicReal be the wrapper around the Bourbaki completion of ℚ obtained from the recovered rationals LogicRat ≃ ℚ. The map toReal : LogicReal → ℝ sends each such element to its image under the canonical equivalence with Mathlib's Cauchy reals.
background
The module RealsFromLogic recovers the real numbers from the Law-of-Logic rational layer. LogicReal is a structure wrapping CompareReals.Bourbakiℝ, Mathlib's uniform-space completion of the rational uniform space, using the equivalence LogicRat ≃ ℚ. The wrapper prevents global instance pollution while reusing the completed real line.
proof idea
This is a one-line wrapper definition that applies CompareReals.compareEquiv to the .val field of the LogicReal input.
why it matters
This transport is used to build recovered complex numbers (toComplex, toComplex_re, toComplex_im) and algebraic structures such as PhiInt in the phi-ring. It completes the recovery step from LogicRat to ℝ, enabling downstream results on transcendentals (coshL, cosL) and supporting the framework's real-analytic content for constants and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.