Directed square-root bounds

The integer square-root bracket used by sqrt x (mode := .down) and sqrt x (mode := .up) encloses the exact real square root after restoring its dyadic scale. For descriptors with fmt.isIEEE = true, directed dyadic rounding yields extended-real lower and upper bounds on finite nonnegative inputs, including negative zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtDyadicBracket_sound (fmt : FloatFormat) (d : Numerics.Dyadic) (hsign : d.negative = false) : (sqrtDyadicBracket fmt d).lower.toReal ≤ √d.toReal ∧ √d.toReal ≤ (sqrtDyadicBracket fmt d).upper.toReal

The dyadic endpoints computed by sqrtDyadicBracket enclose the exact square root.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_nonneg_of_isFinite_of_signBit_eq_false {fmt : FloatFormat} (x : Model fmt) (hfinite : x.isFinite = true) (hxsign : x.signBit = false) : 0 ≤ x.toReal

A finite value with clear sign bit has nonnegative real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_sqrt_down_eq_false_of_isFinite_of_nonnegative {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hfinite : x.isFinite = true) (hnonnegative : 0 ≤ x.toReal) : isNaN (x.sqrt IEEERoundingMode.down) = false

Downward square root is non-NaN on finite nonnegative inputs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_sqrt_up_eq_false_of_isFinite_of_nonnegative {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hfinite : x.isFinite = true) (hnonnegative : 0 ≤ x.toReal) : isNaN (x.sqrt IEEERoundingMode.up) = false

Upward square root is non-NaN on finite nonnegative inputs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_sqrt_down_le_of_nonnegative {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hfinite : x.isFinite = true) (hnonnegative : 0 ≤ x.toReal) : toEReal (x.sqrt IEEERoundingMode.down) ≤ ↑√x.toReal

Downward square root encloses the exact square root from below for every finite value with nonnegative real semantics, including negative zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_sqrt_up_of_nonnegative {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hfinite : x.isFinite = true) (hnonnegative : 0 ≤ x.toReal) : ↑√x.toReal ≤ toEReal (x.sqrt IEEERoundingMode.up)

The exact square root is bounded above by upward square root for every finite value with nonnegative real semantics, including negative zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_sqrt_down_le {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hfinite : x.isFinite = true) (hxsign : x.signBit = false) : toEReal (x.sqrt IEEERoundingMode.down) ≤ ↑√x.toReal

Downward square root bounds the exact square root from below on finite inputs with a clear sign bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_sqrt_up {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hfinite : x.isFinite = true) (hxsign : x.signBit = false) : ↑√x.toReal ≤ toEReal (x.sqrt IEEERoundingMode.up)

Upward square root bounds the exact square root from above on finite inputs with a clear sign bit.