Directed rounding of signed integer-degree roots

Upward and downward coefficient rounding exchange roles for negative results. The resulting signed datum bounds the exact signed real root.

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

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

theorem FloatLib.Floats.Formats.DecimalInterchange.abs_rootMagnitude_towardZero_le (f : Format) (s : Bool) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hfinite : (rootMagnitude f RoundingMode.towardZero s degree x preferred).status.overflow = false) : ∃ (value : ℚ), (rootMagnitude f RoundingMode.towardZero s degree x preferred).value.toRat? = some value ∧ |↑value| ≤ realRoot degree ↑x