Public integer-root semantics

For a negative degree, the exact rational magnitude is inverted before rounding. The real specification is the signed root of that magnitude. Negative nonzero operands require an odd degree. Zero signs and preferred exponents are specified separately because a rational value does not retain either.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.integerRootRadicand (n : ℤ) (a : ℚ) : ℚ

Exact rational radicand for a signed integer degree.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.integerRootRadicand_nonneg (n : ℤ) (a : ℚ) : 0 ≤ integerRootRadicand n a

noncomputable def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.integerRoot (n : ℤ) (a : ℝ) : ℝ

Signed real root, with inversion for negative degree. Its numeric domain excludes degree zero and negative operands at an even degree.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.integerRoot_pow_natAbs (n : ℤ) (hn : n ≠ 0) (a : ℝ) (hdom : a < 0 → n % 2 = 1) : integerRoot n a ^ n.natAbs = if n < 0 then a⁻¹ else a

Raising the real specification to the positive degree magnitude recovers the input, or its reciprocal for a negative degree.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.integerRoot_cast (n : ℤ) (a : ℚ) : (if decide (a < 0) = true then -1 else 1) * realRoot n.natAbs ↑(integerRootRadicand n a) = integerRoot n ↑a

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.abs_integerRoot (n : ℤ) (a : ℚ) : |integerRoot n ↑a| = realRoot n.natAbs ↑(integerRootRadicand n a)

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_eq_rootMagnitude (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : a ≠ 0) (n : ℤ) (hn : n ≠ 0) (hdom : a < 0 → n % 2 = 1) : ∃ (preferred : ℤ), rootN f mode x n = rootMagnitude f mode (decide (a < 0)) n.natAbs (integerRootRadicand n a) preferred

Every nonzero finite operand in the real domain takes exactly one root-rounding path.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : a ≠ 0) (n : ℤ) (hn : n ≠ 0) (hdom : a < 0 → n % 2 = 1) (hfinite : (rootN f mode x n).status.overflow = false) : ∃ (value : ℚ), (rootN f mode x n).value.toRat? = some value ∧ |↑value - integerRoot n ↑a| ≤ 10 ^ rootQuantum f n.natAbs (integerRootRadicand n a) / 2

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_error_lt_one (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : a ≠ 0) (n : ℤ) (hn : n ≠ 0) (hdom : a < 0 → n % 2 = 1) (hfinite : (rootN f mode x n).status.overflow = false) : ∃ (value : ℚ), (rootN f mode x n).value.toRat? = some value ∧ |↑value - integerRoot n ↑a| < 10 ^ rootQuantum f n.natAbs (integerRootRadicand n a)

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_inexact_iff (f : Format) (mode : RoundingMode) (x : Datum) (a value : ℚ) (hx : x.toRat? = some a) (ha : a ≠ 0) (n : ℤ) (hn : n ≠ 0) (hdom : a < 0 → n % 2 = 1) (hfinite : (rootN f mode x n).status.overflow = false) (hv : (rootN f mode x n).value.toRat? = some value) : (rootN f mode x n).status.inexact = true ↔ ↑value ≠ integerRoot n ↑a

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_underflow_iff (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : a ≠ 0) (n : ℤ) (hn : n ≠ 0) (hdom : a < 0 → n % 2 = 1) (hfinite : (rootN f mode x n).status.overflow = false) : (rootN f mode x n).status.underflow = true ↔ |integerRoot n ↑a| < ↑f.minNormal ∧ (rootN f mode x n).status.inexact = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.le_rootN_towardPositive (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : a ≠ 0) (n : ℤ) (hn : n ≠ 0) (hdom : a < 0 → n % 2 = 1) (hfinite : (rootN f RoundingMode.towardPositive x n).status.overflow = false) : ∃ (value : ℚ), (rootN f RoundingMode.towardPositive x n).value.toRat? = some value ∧ integerRoot n ↑a ≤ ↑value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_towardNegative_le (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : a ≠ 0) (n : ℤ) (hn : n ≠ 0) (hdom : a < 0 → n % 2 = 1) (hfinite : (rootN f RoundingMode.towardNegative x n).status.overflow = false) : ∃ (value : ℚ), (rootN f RoundingMode.towardNegative x n).value.toRat? = some value ∧ ↑value ≤ integerRoot n ↑a

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.abs_rootN_towardZero_le (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : a ≠ 0) (n : ℤ) (hn : n ≠ 0) (hdom : a < 0 → n % 2 = 1) (hfinite : (rootN f RoundingMode.towardZero x n).status.overflow = false) : ∃ (value : ℚ), (rootN f RoundingMode.towardZero x n).value.toRat? = some value ∧ |↑value| ≤ |integerRoot n ↑a|

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_zero_pos (f : Format) (mode : RoundingMode) (s : Bool) (q n : ℤ) (hn : 0 < n) : rootN f mode (Datum.finite s 0 q) n = { value := Datum.finite (s && decide (n % 2 = 1)) 0 (max f.minQuantum (min (q / ↑n.natAbs) f.maxQuantum)) }

Positive-degree zero is exact. Even degrees clear its sign; odd degrees preserve it.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_zero_neg (f : Format) (mode : RoundingMode) (s : Bool) (q n : ℤ) (hn : n < 0) : rootN f mode (Datum.finite s 0 q) n = { value := Datum.infinity (s && decide (n % 2 = 1)), status := { divideByZero := true } }

Negative-degree zero is a pole with the same odd-degree sign rule.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_degree_zero_finite (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) : rootN f mode (Datum.finite s c q) 0 = invalidResult

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_degree_zero_infinity (f : Format) (mode : RoundingMode) (s : Bool) : rootN f mode (Datum.infinity s) 0 = invalidResult

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_negative_even (f : Format) (mode : RoundingMode) (c : ℕ) (q n : ℤ) (hc : c ≠ 0) (hn : n ≠ 0) (he : n % 2 = 0) : rootN f mode (Datum.finite true c q) n = invalidResult