Numerical guarantees for decimal algebraic operations

The bounds compare delivered values with the exact square, integer power, reciprocal square root, or hypotenuse. They hold for arbitrary decimal formats. The one-unit bounds cover all five rounding modes; nearest modes satisfy the half-unit bound. Overflow is excluded explicitly, as in the underlying rounders.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.square_valid (f : Format) (mode : RoundingMode) (x : Datum) : Datum.Valid f (square f mode x).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_valid (f : Format) (mode : RoundingMode) (x : Datum) (n : ℤ) : Datum.Valid f (powInt f mode x n).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rsqrt_valid (f : Format) (mode : RoundingMode) (x : Datum) : Datum.Valid f (rsqrt f mode x).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_valid (f : Format) (mode : RoundingMode) (x y : Datum) : Datum.Valid f (hypot f mode x y).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_eq_project (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (n : ℤ) (ha : a ≠ 0 ∨ 0 ≤ n) : ∃ (preferred : ℤ) (negativeZero : Bool), powInt f mode x n = project f mode (a ^ n) preferred negativeZero

A finite integer power is exactly one rational projection whenever it has no pole.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rsqrt_eq_sqrtMagnitude (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : 0 < a) : ∃ (preferred : ℤ), rsqrt f mode x = sqrtMagnitude f mode a⁻¹ preferred

Positive finite reciprocal square root uses the exact reciprocal as its radicand.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_eq_sqrtMagnitude (f : Format) (mode : RoundingMode) (x y : Datum) (a b : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) : ∃ (preferred : ℤ), hypot f mode x y = sqrtMagnitude f mode (a ^ 2 + b ^ 2) preferred

Hypotenuse uses an unrounded sum of squares, including when both operands are zero.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.square_eq_project (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) : ∃ (preferred : ℤ), square f mode x = project f mode (a ^ 2) preferred

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.square_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (square f mode x).status.overflow = false) : ∃ (value : ℚ), (square f mode x).value.toRat? = some value ∧ |value - a ^ 2| ≤ 10 ^ roundingQuantum f |a ^ 2| / 2

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.square_error_lt_one (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (square f mode x).status.overflow = false) : ∃ (value : ℚ), (square f mode x).value.toRat? = some value ∧ |value - a ^ 2| < 10 ^ roundingQuantum f |a ^ 2|

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.square_inexact_iff (f : Format) (mode : RoundingMode) (x : Datum) (a value : ℚ) (hx : x.toRat? = some a) (hfinite : (square f mode x).status.overflow = false) (hv : (square f mode x).value.toRat? = some value) : (square f mode x).status.inexact = true ↔ value ≠ a ^ 2

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.square_underflow_iff (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (square f mode x).status.overflow = false) : (square f mode x).status.underflow = true ↔ |a ^ 2| < f.minNormal ∧ (square f mode x).status.inexact = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.le_square_towardPositive (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (square f RoundingMode.towardPositive x).status.overflow = false) : ∃ (value : ℚ), (square f RoundingMode.towardPositive x).value.toRat? = some value ∧ a ^ 2 ≤ value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.square_towardNegative_le (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (square f RoundingMode.towardNegative x).status.overflow = false) : ∃ (value : ℚ), (square f RoundingMode.towardNegative x).value.toRat? = some value ∧ value ≤ a ^ 2

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.abs_square_towardZero_le (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (square f RoundingMode.towardZero x).status.overflow = false) : ∃ (value : ℚ), (square f RoundingMode.towardZero x).value.toRat? = some value ∧ |value| ≤ |a ^ 2|

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (n : ℤ) (ha : a ≠ 0 ∨ 0 ≤ n) (hfinite : (powInt f mode x n).status.overflow = false) : ∃ (value : ℚ), (powInt f mode x n).value.toRat? = some value ∧ |value - a ^ n| ≤ 10 ^ roundingQuantum f |a ^ n| / 2

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_error_lt_one (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (n : ℤ) (ha : a ≠ 0 ∨ 0 ≤ n) (hfinite : (powInt f mode x n).status.overflow = false) : ∃ (value : ℚ), (powInt f mode x n).value.toRat? = some value ∧ |value - a ^ n| < 10 ^ roundingQuantum f |a ^ n|

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_inexact_iff (f : Format) (mode : RoundingMode) (x : Datum) (a value : ℚ) (hx : x.toRat? = some a) (n : ℤ) (ha : a ≠ 0 ∨ 0 ≤ n) (hfinite : (powInt f mode x n).status.overflow = false) (hv : (powInt f mode x n).value.toRat? = some value) : (powInt f mode x n).status.inexact = true ↔ value ≠ a ^ n

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_underflow_iff (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (n : ℤ) (ha : a ≠ 0 ∨ 0 ≤ n) (hfinite : (powInt f mode x n).status.overflow = false) : (powInt f mode x n).status.underflow = true ↔ |a ^ n| < f.minNormal ∧ (powInt f mode x n).status.inexact = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rsqrt_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : 0 < a) (hfinite : (rsqrt f mode x).status.overflow = false) : ∃ (value : ℚ), (rsqrt f mode x).value.toRat? = some value ∧ |↑value - (√↑a)⁻¹| ≤ 10 ^ sqrtQuantum f a⁻¹ / 2

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rsqrt_error_lt_one (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : 0 < a) (hfinite : (rsqrt f mode x).status.overflow = false) : ∃ (value : ℚ), (rsqrt f mode x).value.toRat? = some value ∧ |↑value - (√↑a)⁻¹| < 10 ^ sqrtQuantum f a⁻¹

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x y : Datum) (a b : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (hypot f mode x y).status.overflow = false) : ∃ (value : ℚ), (hypot f mode x y).value.toRat? = some value ∧ |↑value - √(↑a ^ 2 + ↑b ^ 2)| ≤ 10 ^ sqrtQuantum f (a ^ 2 + b ^ 2) / 2

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_error_lt_one (f : Format) (mode : RoundingMode) (x y : Datum) (a b : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (hypot f mode x y).status.overflow = false) : ∃ (value : ℚ), (hypot f mode x y).value.toRat? = some value ∧ |↑value - √(↑a ^ 2 + ↑b ^ 2)| < 10 ^ sqrtQuantum f (a ^ 2 + b ^ 2)

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rsqrt_inexact_iff (f : Format) (mode : RoundingMode) (x : Datum) (a value : ℚ) (hx : x.toRat? = some a) (ha : 0 < a) (hfinite : (rsqrt f mode x).status.overflow = false) (hv : (rsqrt f mode x).value.toRat? = some value) : (rsqrt f mode x).status.inexact = true ↔ ↑value ≠ (√↑a)⁻¹

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rsqrt_underflow_iff (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : 0 < a) (hfinite : (rsqrt f mode x).status.overflow = false) : (rsqrt f mode x).status.underflow = true ↔ (√↑a)⁻¹ < ↑f.minNormal ∧ (rsqrt f mode x).status.inexact = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_inexact_iff (f : Format) (mode : RoundingMode) (x y : Datum) (a b value : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (hypot f mode x y).status.overflow = false) (hv : (hypot f mode x y).value.toRat? = some value) : (hypot f mode x y).status.inexact = true ↔ ↑value ≠ √(↑a ^ 2 + ↑b ^ 2)

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_underflow_iff (f : Format) (mode : RoundingMode) (x y : Datum) (a b : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (hypot f mode x y).status.overflow = false) : (hypot f mode x y).status.underflow = true ↔ √(↑a ^ 2 + ↑b ^ 2) < ↑f.minNormal ∧ (hypot f mode x y).status.inexact = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.le_rsqrt_towardPositive (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : 0 < a) (hfinite : (rsqrt f RoundingMode.towardPositive x).status.overflow = false) : ∃ (value : ℚ), (rsqrt f RoundingMode.towardPositive x).value.toRat? = some value ∧ (√↑a)⁻¹ ≤ ↑value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rsqrt_directed_le (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.towardZero ∨ mode = RoundingMode.towardNegative) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : 0 < a) (hfinite : (rsqrt f mode x).status.overflow = false) : ∃ (value : ℚ), (rsqrt f mode x).value.toRat? = some value ∧ ↑value ≤ (√↑a)⁻¹

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.le_hypot_towardPositive (f : Format) (x y : Datum) (a b : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (hypot f RoundingMode.towardPositive x y).status.overflow = false) : ∃ (value : ℚ), (hypot f RoundingMode.towardPositive x y).value.toRat? = some value ∧ √(↑a ^ 2 + ↑b ^ 2) ≤ ↑value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_directed_le (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.towardZero ∨ mode = RoundingMode.towardNegative) (x y : Datum) (a b : ℚ) (hx : x.toRat? = some a) (hy : y.toRat? = some b) (hfinite : (hypot f mode x y).status.overflow = false) : ∃ (value : ℚ), (hypot f mode x y).value.toRat? = some value ∧ ↑value ≤ √(↑a ^ 2 + ↑b ^ 2)

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.le_powInt_towardPositive (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (n : ℤ) (ha : a ≠ 0 ∨ 0 ≤ n) (hfinite : (powInt f RoundingMode.towardPositive x n).status.overflow = false) : ∃ (value : ℚ), (powInt f RoundingMode.towardPositive x n).value.toRat? = some value ∧ a ^ n ≤ value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_towardNegative_le (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (n : ℤ) (ha : a ≠ 0 ∨ 0 ≤ n) (hfinite : (powInt f RoundingMode.towardNegative x n).status.overflow = false) : ∃ (value : ℚ), (powInt f RoundingMode.towardNegative x n).value.toRat? = some value ∧ value ≤ a ^ n

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.abs_powInt_towardZero_le (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (n : ℤ) (ha : a ≠ 0 ∨ 0 ≤ n) (hfinite : (powInt f RoundingMode.towardZero x n).status.overflow = false) : ∃ (value : ℚ), (powInt f RoundingMode.towardZero x n).value.toRat? = some value ∧ |value| ≤ |a ^ n|