Foundation Logic Real Transcendentals Sqrt L Nonneg

A transported square root

The square root function on the real numbers has a basic property: for any real input, the output is never negative. The declaration sqrtL_nonneg establishes that the same is true for the square root function defined on the recovered real line, a structure the Recognition Science framework builds from its foundational logic. The theorem states that for every element x of the recovered reals, the square root of x is greater than or equal to zero. It is a direct translation of the standard result, not a new discovery about square roots.

The recovered real line is the framework's own copy of the real numbers, and it is equivalent to the usual real numbers through a bijection called LogicReal.equivReal. The framework defines its square root by transporting the standard square root across this equivalence: take a recovered real, map it to the usual real, apply the standard square root, and map the result back. The theorem sqrtL_nonneg is proved by unwinding this definition and applying the standard fact that the square root of a real number is nonnegative. It is a transport lemma, one of several that carry familiar properties of exponential, logarithm, and trigonometric functions onto the recovered reals.

In Recognition Science, this theorem is a small piece of infrastructure. It ensures that the recovered real line behaves like the real numbers when later modules reason about analysis. The theorem does not claim anything about the framework's deeper structures, such as the cost function or the forcing chain. It does not say that the recovered reals are the only possible real line, nor does it derive the square root from the framework's axioms. It simply states that a standard property of the square root holds in the framework's setting, because the setting is designed to mirror the standard one.

/-- Transported non-negativity of square root. -/
theorem sqrtL_nonneg (x : LogicReal) : (0 : LogicReal) ≤ sqrtL x := by
  rw [le_iff_toReal_le, toReal_zero, toReal_sqrtL]
  exact Real.sqrt_nonneg _

/-- Square root on recovered reals, transported from `Real.sqrt`. -/
def sqrtL (x : LogicReal) : LogicReal := fromReal (Real.sqrt (toReal x))

/-- Square root on recovered reals, transported from `Real.sqrt`. -/
def sqrtL (x : LogicReal) : LogicReal := fromReal (Real.sqrt (toReal x))

What this page does not claim

The theorem does not derive the square root from the framework's axioms; it transports a standard property. The theorem does not say the recovered reals are the only possible real line. The theorem does not establish any property about the cost function or the forcing chain.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/LogicRealTranscendentals.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: