Correct rounding of integer posit roots

Raising nonnegative values to a positive integer power preserves order, so exact power comparisons agree with comparison against the real root. The shared comparator-rounding theorem then supplies correct rounding. The root-characterization theorem applies to any nonnegative real root. Its real-power corollary supplies a root for every nonnegative rational radicand and positive degree.

theorem FloatLib.Floats.Formats.Posit.Model.RootRounding.compareRoot_eq_real (q : ℚ) (n : ℕ) (x : ℝ) (hx : 0 ≤ x) (hn : n ≠ 0) (heq : x ^ n = ↑q) (candidate : ℚ) : compareRoot q n candidate = cmp x ↑candidate

Exact power comparison agrees with every rational comparison against a nonnegative root.

theorem FloatLib.Floats.Formats.Posit.Model.RootRounding.round_eq_real (format : Format) (q : ℚ) (n : ℕ) (x : ℝ) (hx : 0 ≤ x) (hn : n ≠ 0) (heq : x ^ n = ↑q) : round format q n = RealRounding.roundPositive format x

Model-valued exact root rounding agrees with real rounding of a characterized root.

theorem FloatLib.Floats.Formats.Posit.Model.RootRounding.round_eq_rpow (format : Format) (q : ℚ) (n : ℕ) (hq : 0 ≤ q) (hn : n ≠ 0) : round format q n = RealRounding.roundPositive format (↑q ^ (↑n)⁻¹)

For positive degree and nonnegative radicand, exact root rounding rounds q ^ (1 / n).

theorem FloatLib.Floats.Formats.Posit.Model.rootN_eq_roundPositive {format : Format} (value : Model format) {q : ℚ} (degree : ℤ) (hvalue : value.toRat? = some q) (hq : 0 ≤ q) (hdegree : degree ≠ 0) (hdomain : q ≠ 0 ∨ 0 < degree) : value.rootN degree = RealRounding.roundPositive format (↑q ^ (↑degree)⁻¹)

A nonnegative finite integer root rounds the exact real power q ^ (1 / degree).

The degree is nonzero; a zero radicand additionally requires positive degree. Negative degrees are covered by inverting the exact rational radicand, before any rounding.

theorem FloatLib.Floats.Formats.Posit.Model.rootN_eq_neg_roundPositive {format : Format} (value : Model format) {q : ℚ} (degree : ℤ) (hvalue : value.toRat? = some q) (hq : q < 0) (hodd : degree % 2 ≠ 0) : value.rootN degree = (RealRounding.roundPositive format ((-↑q) ^ (↑degree)⁻¹)).neg

For a negative finite input and odd integer degree, the signed real root is rounded once.

Its magnitude is (-q) ^ (1 / degree). This statement specifies the real branch explicitly, including negative odd degrees, without relying on real powers of a negative base.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.rootN_nar {format : Format} (degree : ℤ) : (nar format).rootN degree = nar format

Integer roots propagate NaR for every degree.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.rootN_degree_zero {format : Format} (value : Model format) : value.rootN 0 = nar format

Degree zero has no defined integer-root operation.

theorem FloatLib.Floats.Formats.Posit.Model.rootN_zero_of_neg {format : Format} (degree : ℤ) (hdegree : degree < 0) : (zero format).rootN degree = nar format

Negative-degree roots of zero are not finite real numbers.

theorem FloatLib.Floats.Formats.Posit.Model.rootN_zero_of_pos {format : Format} (degree : ℤ) (hdegree : 0 < degree) : (zero format).rootN degree = zero format

Every positive-degree root of zero is zero.

theorem FloatLib.Floats.Formats.Posit.Model.rootN_eq_nar_of_neg_even {format : Format} (value : Model format) {q : ℚ} (degree : ℤ) (hvalue : value.toRat? = some q) (hq : q < 0) (heven : degree % 2 = 0) : value.rootN degree = nar format

Even-degree roots of a negative finite input are not real.