Integer-degree root values and rounding guarantees

The delivered datum represents the signed, rounded coefficient. Carry and exact cohort selection preserve its value. Numerical bounds compare it with the real root, and power equality decides exactness without approximating an irrational result.

theorem FloatLib.Floats.Formats.DecimalInterchange.rootRound_le_coefficientBound (f : Format) (mode : RoundingMode) (s : Bool) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) : mode.rootRound s degree (x / 10 ^ (↑degree * rootQuantum f degree x)) ≤ f.coefficientBound

theorem FloatLib.Floats.Formats.DecimalInterchange.rootPair_coefficient_lt (f : Format) (mode : RoundingMode) (s : Bool) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) : (rootPair f mode s degree x).1 < f.coefficientBound

theorem FloatLib.Floats.Formats.DecimalInterchange.rootPair_quantum_ge_min (f : Format) (mode : RoundingMode) (s : Bool) (degree : ℕ) (x : ℚ) : f.minQuantum ≤ (rootPair f mode s degree x).2

theorem FloatLib.Floats.Formats.DecimalInterchange.rootPair_value (f : Format) (mode : RoundingMode) (s : Bool) (degree : ℕ) (x : ℚ) : ↑(rootPair f mode s degree x).1 * 10 ^ (rootPair f mode s degree x).2 = ↑(mode.rootRound s degree (x / 10 ^ (↑degree * rootQuantum f degree x))) * 10 ^ rootQuantum f degree x

theorem FloatLib.Floats.Formats.DecimalInterchange.rootMagnitude_valid (f : Format) (mode : RoundingMode) (s : Bool) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) : Datum.Valid f (rootMagnitude f mode s degree x preferred).value

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rootN_degree_zero (f : Format) (mode : RoundingMode) (x : Datum) : rootN f mode x 0 = invalidResult

Degree zero always delivers an invalid result, including quiet and signaling NaNs.

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

theorem FloatLib.Floats.Formats.DecimalInterchange.rootMagnitude_overflow_iff (f : Format) (mode : RoundingMode) (s : Bool) (degree : ℕ) (x : ℚ) (preferred : ℤ) : (rootMagnitude f mode s degree x preferred).status.overflow = true ↔ f.maxQuantum < (rootPair f mode s degree x).2

theorem FloatLib.Floats.Formats.DecimalInterchange.rootMagnitude_quantum_le_of_no_overflow (f : Format) (mode : RoundingMode) (s : Bool) (degree : ℕ) (x : ℚ) (preferred : ℤ) (hfinite : (rootMagnitude f mode s degree x preferred).status.overflow = false) : (rootPair f mode s degree x).2 ≤ f.maxQuantum

theorem FloatLib.Floats.Formats.DecimalInterchange.rootMagnitude_value (f : Format) (mode : RoundingMode) (s : Bool) (degree : ℕ) (x : ℚ) (preferred : ℤ) (hq : (rootPair f mode s degree x).2 ≤ f.maxQuantum) : (rootMagnitude f mode s degree x preferred).value.toRat? = some ((if s = true then -1 else 1) * ↑(mode.rootRound s degree (x / 10 ^ (↑degree * rootQuantum f degree x))) * 10 ^ rootQuantum f degree x)

theorem FloatLib.Floats.Formats.DecimalInterchange.realRoot_scaled {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) (q : ℤ) : realRoot degree ↑(x / 10 ^ (↑degree * q)) * 10 ^ q = realRoot degree ↑x

Multiplication by a positive decimal quantum commutes with the real root.

theorem FloatLib.Floats.Formats.DecimalInterchange.rootMagnitude_error_le_half (f : Format) (mode : RoundingMode) (s : Bool) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hfinite : (rootMagnitude f mode s degree x preferred).status.overflow = false) : ∃ (value : ℚ), (rootMagnitude f mode s degree x preferred).value.toRat? = some value ∧ |↑value - (if s = true then -1 else 1) * realRoot degree ↑x| ≤ 10 ^ rootQuantum f degree x / 2

theorem FloatLib.Floats.Formats.DecimalInterchange.rootMagnitude_error_lt_one (f : Format) (mode : RoundingMode) (s : Bool) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hfinite : (rootMagnitude f mode s degree x preferred).status.overflow = false) : ∃ (value : ℚ), (rootMagnitude f mode s degree x preferred).value.toRat? = some value ∧ |↑value - (if s = true then -1 else 1) * realRoot degree ↑x| < 10 ^ rootQuantum f degree x

theorem FloatLib.Floats.Formats.DecimalInterchange.rootMagnitude_inexact_iff (f : Format) (mode : RoundingMode) (s : Bool) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) (value : ℚ) (preferred : ℤ) (hfinite : (rootMagnitude f mode s degree x preferred).status.overflow = false) (hv : (rootMagnitude f mode s degree x preferred).value.toRat? = some value) : (rootMagnitude f mode s degree x preferred).status.inexact = true ↔ ↑value ≠ (if s = true then -1 else 1) * realRoot degree ↑x

theorem FloatLib.Floats.Formats.DecimalInterchange.rootMagnitude_underflow_iff (f : Format) (mode : RoundingMode) (s : Bool) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hfinite : (rootMagnitude f mode s degree x preferred).status.overflow = false) : (rootMagnitude f mode s degree x preferred).status.underflow = true ↔ realRoot degree ↑x < ↑f.minNormal ∧ (rootMagnitude f mode s degree x preferred).status.inexact = true

Underflow uses the exact root's magnitude, before rounding.