Directed square-root bounds

The integer square-root bracket used by sqrtDown and sqrtUp 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_sqrtDown_eq_false_of_isFinite_of_nonnegative {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hfinite : x.isFinite = true) (hnonnegative : 0 ≤ x.toReal) : x.sqrtDown.isNaN = false

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

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

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

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

sqrtDown 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_sqrtUp_of_nonnegative {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hfinite : x.isFinite = true) (hnonnegative : 0 ≤ x.toReal) : ↑√x.toReal ≤ x.sqrtUp.toEReal

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

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

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

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

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