toReal_sqrtL
plain-language theorem explainer
The theorem shows that the transported square root on LogicReal commutes with the equivalence map to Mathlib reals. Researchers reducing analytic identities over recovered reals cite it to move square-root expressions into standard real analysis. The proof is a one-line wrapper that applies the general transport lemma toReal_fromReal to the definition of sqrtL.
Claim. Let $x$ be an element of the recovered real line. Then toReal of the transported square root satisfies toReal($sqrt_L x$) = Real.sqrt(toReal($x$)), where $sqrt_L$ is defined by pulling back Mathlib's square root through the equivalence.
background
LogicReal is the structure wrapping the Bourbaki completion of the recovered rationals, with toReal the canonical transport to Mathlib's real line. The function sqrtL is defined by applying Real.sqrt after transport and pulling the result back via fromReal. The module LogicRealTranscendentals transports standard transcendental functions through the equivalence LogicReal.equivReal so that analytic identities reduce to Mathlib while reasoning remains on LogicReal. The upstream lemma toReal_fromReal states that toReal(fromReal x) equals x for any real x.
proof idea
The proof is a one-line wrapper that applies the transport lemma toReal_fromReal. Because sqrtL x expands to fromReal(Real.sqrt(toReal x)), the lemma directly yields toReal(fromReal(Real.sqrt(toReal x))) which equals Real.sqrt(toReal x).
why it matters
This result is used by the downstream theorem sqrtL_nonneg to reduce the non-negativity statement on LogicReal to the corresponding fact on Mathlib reals. It belongs to the transport layer that lets later modules reason over LogicReal while still invoking Mathlib's real-analysis library for identities. The construction supports the overall strategy of recovering the real line via equivalence without duplicating analytic machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.