logicReal_recovered_from_completion
The theorem establishes that the recovered real line LogicReal is canonically equivalent to the standard reals via the transport maps toReal and fromReal. A foundation researcher reconstructing analysis from the Law of Logic would invoke this equivalence to transfer theorems from Mathlib's reals back to the logic-derived objects. The proof is a direct pairing of the two one-directional lemmas already established in the same module.
claimThe maps $toReal : LogicReal → ℝ$ and $fromReal : ℝ → LogicReal$ are mutual inverses: for every recovered real $x$, $fromReal(toReal(x)) = x$, and for every standard real $x$, $toReal(fromReal(x)) = x$.
background
LogicReal is a wrapper around Mathlib's Bourbaki completion of ℚ, built on the equivalence LogicRat ≃ ℚ recovered from the logic layer. The map toReal extracts the underlying Mathlib real via the canonical comparison equivalence compareEquiv, while fromReal inserts a standard real into the wrapper by applying the inverse equivalence. This sits inside the recovery pipeline described in the module: Law of Logic yields LogicNat, LogicInt, LogicRat, whose uniform completion produces LogicReal equivalent to ℝ. The module adopts a transport-first API so that all algebraic and order structures on LogicReal are defined by pullback along toReal, reducing every statement to an existing theorem on ℝ. The two supporting lemmas fromReal_toReal and toReal_fromReal establish the separate directions of the equivalence.
proof idea
The proof is the term ⟨fromReal_toReal, toReal_fromReal⟩, which directly assembles the two already-proved direction lemmas into the required conjunction.
why it matters in Recognition Science
This declaration completes the recovery of the real numbers from the logic-derived rationals, closing the chain from Law of Logic through rationals to the completed reals. It justifies the transport API in the module documentation, allowing all subsequent analysis to reduce to standard real theorems. No open questions are flagged here, but the result underpins any downstream use of real analysis within the Recognition Science framework.
scope and limits
- Does not construct the reals from scratch without Mathlib's completion engine.
- Does not define algebraic operations on LogicReal independently of transport.
- Does not address computability or constructive properties of the recovered reals.
- Does not extend the equivalence to non-Archimedean or higher-dimensional completions.
formal statement (Lean)
213theorem logicReal_recovered_from_completion :
214 (∀ x : LogicReal, fromReal (toReal x) = x) ∧
215 (∀ x : ℝ, toReal (fromReal x) = x) :=
proof body
Term-mode proof.
216 ⟨fromReal_toReal, toReal_fromReal⟩
217
218end LogicReal
219
220end
221
222end RealsFromLogic
223end Foundation
224end IndisputableMonolith