toReal_ofLogicRat
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not construct the reals independently of Mathlib's Bourbaki completion.
- Does not address non-Archimedean or non-standard models of the reals.
- Does not treat computability or constructive properties of the completion.
Lean usage
rw [toReal_ofLogicRat]formal statement (Lean)
120theorem toReal_ofLogicRat (q : LogicRat) : toReal (ofLogicRat q) = (toRat q : ℝ) := by
proof body
Term-mode proof.
121 rw [ofLogicRat, toReal_ofRatCore]
122
123/-! ## 4. Algebra and order by transport through `toReal` -/
124
125instance : Zero LogicReal := ⟨fromReal 0⟩
126instance : One LogicReal := ⟨fromReal 1⟩
127instance : Add LogicReal := ⟨fun x y => fromReal (toReal x + toReal y)⟩
128instance : Neg LogicReal := ⟨fun x => fromReal (-toReal x)⟩
129instance : Sub LogicReal := ⟨fun x y => fromReal (toReal x - toReal y)⟩
130instance : Mul LogicReal := ⟨fun x y => fromReal (toReal x * toReal y)⟩
131instance : Inv LogicReal := ⟨fun x => fromReal (toReal x)⁻¹⟩
132instance : Div LogicReal := ⟨fun x y => fromReal (toReal x / toReal y)⟩
133instance : LE LogicReal := ⟨fun x y => toReal x ≤ toReal y⟩
134instance : LT LogicReal := ⟨fun x y => toReal x < toReal y⟩
135