lt_iff_toReal_lt
plain-language theorem explainer
Order on the recovered reals coincides exactly with the standard order after transport by toReal. Foundation proofs that lift inequalities from Mathlib reals cite this equivalence. The statement holds by reflexivity because the order predicate on LogicReal is introduced by pullback along the transport map.
Claim. For $x, y$ in the Cauchy completion of the logic-derived rationals, $x < y$ if and only if the image of $x$ under the transport map is strictly less than the image of $y$ in the standard reals.
background
The RealsFromLogic module recovers the real numbers from the law-of-logic rationals by completing LogicRat via Mathlib's Bourbaki completion of ℚ. LogicReal is a wrapper structure around CompareReals.Bourbakiℝ that isolates the recovered line and prevents global instance pollution on the completion. The map toReal sends each wrapped element to its counterpart in ℝ via the canonical comparison equivalence.
proof idea
The proof is the one-line reflexivity Iff.rfl. Because the less-than relation on LogicReal is defined precisely by requiring that x < y holds exactly when toReal x < toReal y, the biconditional is immediate from the transport definition.
why it matters
The equivalence is invoked inside expL_logL to transport the positivity hypothesis and reduce the inverse property to Real.exp_log, and inside expL_pos to transport positivity of the exponential. It closes the order-transport loop in the foundation layer, letting recovered analysis reuse standard real theorems. In the Recognition Science setting this supports passage from logic rationals to the completed reals required for the phi-ladder and dimensional forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.