sqrtL
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove algebraic identities for sqrtL without separate transport lemmas.
- Does not construct square root directly from the underlying logic axioms.
- Does not extend the operation to complex numbers or other number systems.
- Does not address computational evaluation or decidability questions.
formal statement (Lean)
26def sqrtL (x : LogicReal) : LogicReal := fromReal (Real.sqrt (toReal x))
proof body
Definition body.
27
28/-- Exponential on recovered reals, transported from `Real.exp`. -/