ofLogicRat
plain-language theorem explainer
The embedding maps a recovered rational into the logic-derived real line by recovering its standard rational value and coercing that value into the Bourbaki completion. Researchers reconstructing analysis from the law-of-logic layer cite this map when lifting rational identities to the completed space. The construction is a direct composition of the rational recovery function with the core embedding into the completion.
Claim. Let $q$ be a recovered rational. The embedding of $q$ into the recovered reals is the image of the recovered standard rational under the canonical coercion into the Cauchy completion of the rationals.
background
The module recovers the real numbers from the logic rationals by using Mathlib's Bourbaki completion of the standard rationals. LogicReal is a thin wrapper around the Bourbaki real that isolates the recovered structure and prevents global instance pollution. The overall recovery chain runs from the law of logic through recovered naturals and integers to LogicRat, which is equivalent to the standard rationals, and then completes to the recovered reals. The upstream recovery map sends a recovered rational to its standard counterpart, while the core coercion embeds any standard rational into the completion.
proof idea
The definition is a one-line wrapper that applies the core coercion to the result of the rational recovery map on the input. It depends only on the upstream recovery map from the rationals module and the core coercion defined earlier in the same file.
why it matters
This supplies the rational-to-real step required by the complex embedding in the complex module and by the transport theorem that equates the recovered real with the standard real after applying the recovery map. It completes the completion stage in the logic-to-reals recovery sequence, allowing every real-analytic statement to be transported back to the logic-derived structures. The step supports the foundation layer that ultimately feeds the derivation of physical constants from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.