sqrtL
plain-language theorem explainer
The definition equips LogicReal with square root by transporting Mathlib's Real.sqrt through the equivalence maps toReal and fromReal. Workers extending real analysis inside the Recognition Science recovered reals cite this when they need the operation on the logic-derived line. The construction is a direct one-line wrapper that composes the two transport functions around the standard square root.
Claim. Let $x$ be an element of the recovered real line LogicReal. Define $sqrt_L(x) := fromReal(Real.sqrt(toReal(x)))$, where toReal and fromReal are the canonical equivalence maps between LogicReal and the standard reals.
background
LogicReal is the structure that realizes the Cauchy completion of the recovered rationals via the equivalence LogicRat ≃ ℚ, with toReal and fromReal supplying the isomorphism to Mathlib's ℝ. The module LogicRealTranscendentals defines the standard transcendental functions on this recovered line by transport through that equivalence, so that later modules can work directly over LogicReal while reducing analytic identities to Mathlib's library.
proof idea
One-line wrapper that applies fromReal to Real.sqrt composed with toReal.
why it matters
This supplies the square root operation required by the downstream theorems sqrtL_nonneg and toReal_sqrtL. It belongs to the initial layer of transported transcendentals that lets the Recognition framework build analytic structure on the logic-derived reals without re-proving real-analysis results. The definition therefore supports the overall passage from the PrimitiveDistinction axioms through RealsFromLogic to the full set of real functions used in later modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.