toReal_sqrtL
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove non-negativity or monotonicity of the square root.
- Does not establish algebraic identities such as sqrt(x^2) = |x|.
- Does not extend to complex numbers or other number systems.
- Does not supply an independent definition of square root on LogicReal.
Lean usage
theorem sqrtL_nonneg (x : LogicReal) : (0 : LogicReal) ≤ sqrtL x := by rw [le_iff_toReal_le, toReal_zero, toReal_sqrtL]; exact Real.sqrt_nonneg _formal statement (Lean)
52@[simp] theorem toReal_sqrtL (x : LogicReal) :
53 toReal (sqrtL x) = Real.sqrt (toReal x) :=
proof body
One-line wrapper that applies toReal_fromReal.
54 toReal_fromReal _
55