Decimal coefficient range for arbitrary integer-degree roots

Dividing the integer decimal logarithm by the positive degree determines a fitting root grid. The argument uses exact powers and applies to any format.

theorem FloatLib.Floats.Formats.DecimalInterchange.rootScaleShift_upper (p : ℕ) {degree : ℕ} (hn : 0 < degree) {x : ℚ} (hx : 0 ≤ x) : x < 10 ^ (degree * (p + rootScaleShift p degree x))

theorem FloatLib.Floats.Formats.DecimalInterchange.rootQuantum_ge_min (f : Format) (degree : ℕ) (x : ℚ) : f.minQuantum ≤ rootQuantum f degree x

theorem FloatLib.Floats.Formats.DecimalInterchange.div_rootQuantum_lt (f : Format) {degree : ℕ} (hn : 0 < degree) {x : ℚ} (hx : 0 ≤ x) : x / 10 ^ (↑degree * rootQuantum f degree x) < ↑f.coefficientBound ^ degree

The scaled radicand is strictly below the power of the coefficient bound.