toReal_zero
plain-language theorem explainer
The theorem asserts that the zero element of the recovered real line maps to the standard zero under the transport equivalence to ordinary reals. Workers on the logic-derived reals cite it when reducing identities or inequalities at the origin in downstream analytic statements. The argument is a direct specialization of the general transport theorem for the from-real embedding.
Claim. Let $L$ be the recovered real line obtained as the Cauchy completion of the logic-derived rationals. The canonical transport map $t : L → ℝ$ satisfies $t(0) = 0$.
background
The module recovers the real numbers from the Law of Logic by first obtaining the logic rationals equivalent to ℚ, then completing via Mathlib's Bourbaki construction. LogicReal is the wrapper structure around the completed reals that avoids global instance pollution while permitting reuse of standard real algebra and order. The transport map sends each recovered real to its Mathlib counterpart via the comparison equivalence, so that all properties pull back along this map.
proof idea
One-line wrapper that applies the general transport theorem toReal_fromReal at the zero real.
why it matters
It supports transport of analytic properties to the recovered reals and is invoked directly in the proofs of positivity for the exponential and non-negativity for the square root on the recovered line. The result fills the zero case inside the reals-from-logic construction, guaranteeing that the additive identity behaves as expected under the equivalence with standard reals. No open questions are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.