sqrtL_nonneg
plain-language theorem explainer
The transported square root on LogicReal is non-negative for every input. Analysts building the Recognition Science real line from logic would reference this result when establishing order properties of the recovered reals. The short proof rewrites the order relation through the toReal equivalence and invokes the corresponding fact from Mathlib's real analysis.
Claim. For every $x$ in the recovered real line, $0$ is less than or equal to the transported square root of $x$, where the square root is obtained by applying the standard real square root after mapping to Mathlib's reals and mapping back.
background
LogicReal wraps Mathlib's completed reals via a structure to prevent global instance pollution while reusing the canonical completion of the rationals. The map toReal sends each LogicReal element to its counterpart in ℝ, and fromReal performs the inverse transport. The definition sqrtL(x) applies Real.sqrt to toReal(x) and wraps the result back via fromReal. The lemma le_iff_toReal_le equates the order on LogicReal with the order on the image under toReal. toReal_zero states that the zero element of LogicReal maps to zero in ℝ.
proof idea
The term proof rewrites the target inequality via le_iff_toReal_le, replaces the images of zero and sqrtL using toReal_zero and toReal_sqrtL, then concludes by exact application of Real.sqrt_nonneg.
why it matters
This result completes the transport of non-negativity for the square root, ensuring the recovered reals inherit the order properties needed for later analytic work in the Recognition Science foundation. It sits inside the module that equips LogicReal with standard transcendentals so that proofs can remain inside the logic-derived setting while reducing identities to Mathlib. No downstream uses are recorded yet, but the lemma supports any argument that relies on non-negative elements within the phi-ladder or forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.