toReal_ofRatCore
plain-language theorem explainer
The theorem shows that embedding a standard rational q into the recovered real line via ofRatCore and then transporting via toReal recovers exactly the usual real value of q. Foundation developers in Recognition Science cite it to confirm that the Bourbaki completion step preserves the dense rational subfield without distortion. The proof is a one-line term wrapper that reduces the claim to the uniqueness of the completion map on Cauchy sequences of rationals.
Claim. For any rational number $q$, the composition of the embedding of $q$ into the Bourbaki completion of the recovered rationals followed by the canonical transport map to the standard reals equals $q$ itself.
background
The module recovers the real numbers from the Law-of-Logic rational layer. LogicRat is recovered from logic axioms and equivalent to ℚ. LogicReal is a wrapper around the Bourbaki completion of ℚ. The map toReal sends a LogicReal to ℝ by applying CompareReals.compareEquiv to the underlying completion element. ofRatCore embeds a ℚ into LogicReal by taking the completion coefficient of the corresponding Cauchy sequence.
proof idea
The proof is a term-mode one-liner. It applies simpa to the statement that the Bourbaki comparison equivalence agrees with the rational coercion on the dense embedding, invoking CompareReals.bourbakiPkg.compare_coe on the rational Cauchy sequence package.
why it matters
This result supplies the key compatibility step that lets algebraic structure be transported from ℝ to LogicReal. It is used directly by toReal_ofLogicRat to extend the compatibility to the recovered rationals. The construction completes the chain from Law of Logic through LogicRat ≃ ℚ to Completion ℚ ≃ ℝ, providing the real line for downstream Recognition Science calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.