Directed square-root bounds and tininess

In the absence of overflow, the returned values bound the real square root in the requested direction. Decimal underflow tests the exact root before rounding.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_quantum_le_of_no_overflow (f : Format) (mode : RoundingMode) (x : ℚ) (preferred : ℤ) (hfinite : (sqrtMagnitude f mode x preferred).status.overflow = false) : (sqrtPair f mode x).2 ≤ f.maxQuantum

theorem FloatLib.Floats.Formats.DecimalInterchange.le_sqrtMagnitude_towardPositive (f : Format) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hfinite : (sqrtMagnitude f RoundingMode.towardPositive x preferred).status.overflow = false) : ∃ (value : ℚ), (sqrtMagnitude f RoundingMode.towardPositive x preferred).value.toRat? = some value ∧ √↑x ≤ ↑value

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_directed_le (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.towardZero ∨ mode = RoundingMode.towardNegative) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hfinite : (sqrtMagnitude f mode x preferred).status.overflow = false) : ∃ (value : ℚ), (sqrtMagnitude f mode x preferred).value.toRat? = some value ∧ ↑value ≤ √↑x

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_error_lt_one (f : Format) (mode : RoundingMode) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hfinite : (sqrtMagnitude f mode x preferred).status.overflow = false) : ∃ (value : ℚ), (sqrtMagnitude f mode x preferred).value.toRat? = some value ∧ |↑value - √↑x| < 10 ^ sqrtQuantum f x

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_underflow_iff (f : Format) (mode : RoundingMode) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hfinite : (sqrtMagnitude f mode x preferred).status.overflow = false) : (sqrtMagnitude f mode x preferred).status.underflow = true ↔ √↑x < ↑f.minNormal ∧ (sqrtMagnitude f mode x preferred).status.inexact = true

Underflow compares the exact mathematical root with the least normal magnitude.