toReal_ofLogicRat
plain-language theorem explainer
The theorem shows that embedding a recovered rational into the recovered reals and transporting via toReal recovers exactly the standard real associated to its rational image. Foundation-layer developers cite it when moving algebraic identities from Mathlib reals back into LogicReal. The proof is a direct term rewrite that unfolds ofLogicRat followed by toReal_ofRatCore.
Claim. For a recovered rational $q$, the transport of its embedding into the recovered reals equals its image under the rational-to-real map: $toReal(ofLogicRat(q)) = (toRat(q) : ℝ)$.
background
The module recovers the reals from the Law-of-Logic rationals. LogicRat is the field of fractions of LogicInt, equipped with the isomorphism toRat : LogicRat → ℚ. LogicReal is a wrapper around Mathlib's Bourbaki completion of ℚ, and toReal supplies the canonical equivalence to the standard ℝ. The embedding ofLogicRat q is defined by ofRatCore (toRat q), placing the rational directly into the completion. This transport-first design lets algebra and order on LogicReal be pulled back from ℝ so that downstream theorems reduce to ordinary real analysis. The result depends on the upstream definitions ofLogicRat and toReal_ofRatCore together with the equivalence LogicRat ≃ ℚ from RationalsFromLogic.
proof idea
The proof is a term-mode one-liner. It rewrites by the definition of ofLogicRat, which expands to ofRatCore (toRat q), then applies toReal_ofRatCore to obtain the image in ℝ.
why it matters
The theorem closes the rational-to-real transport step in the foundation chain and is invoked directly by toComplex_ofLogicRat in ComplexFromLogic. It realizes the module's recovery statement LogicRat ≃ ℚ ⊢ Completion ℚ ≃ ℝ. Within Recognition Science it supplies the real line needed for later physical derivations while reusing Mathlib's completion without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.