Correct rounding of the square-root coefficient

The integer square root brackets the mathematical real square root. Exact squared comparisons then give at most half-unit error in either nearest mode and the appropriate one-sided bounds in the three directed modes.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtFloor_sq_le {x : ℚ} (hx : 0 ≤ x) : ↑(sqrtFloor x) ^ 2 ≤ x

theorem FloatLib.Floats.Formats.DecimalInterchange.lt_sqrtFloor_succ_sq {x : ℚ} (hx : 0 ≤ x) : x < (↑(sqrtFloor x) + 1) ^ 2

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtFloor_le_sqrt {x : ℚ} (hx : 0 ≤ x) : ↑(sqrtFloor x) ≤ √↑x

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrt_lt_sqrtFloor_succ {x : ℚ} (hx : 0 ≤ x) : √↑x < ↑(sqrtFloor x) + 1

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.sqrtRound_eq_floor_or_succ (mode : RoundingMode) (x : ℚ) : mode.sqrtRound x = sqrtFloor x ∨ mode.sqrtRound x = sqrtFloor x + 1

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.sqrtRound_le_floor_add_one (mode : RoundingMode) (x : ℚ) : mode.sqrtRound x ≤ sqrtFloor x + 1

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.sqrtRound_nat_sq (mode : RoundingMode) (n : ℕ) : mode.sqrtRound (↑n ^ 2) = n

Integer squares yield their exact nonnegative roots in all five rounding modes.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtFloor_midpoint_sq (n : ℕ) : sqrtFloor ((↑n + 1 / 2) ^ 2) = n

The square of an exact half-integer lies between the same two integer squares.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtRound_nearestEven_midpoint (n : ℕ) : RoundingMode.nearestEven.sqrtRound ((↑n + 1 / 2) ^ 2) = if n % 2 = 1 then n + 1 else n

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtRound_nearestAway_midpoint (n : ℕ) : RoundingMode.nearestAway.sqrtRound ((↑n + 1 / 2) ^ 2) = n + 1

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtRound_error_lt_one (mode : RoundingMode) {x : ℚ} (hx : 0 ≤ x) : |↑(mode.sqrtRound x) - √↑x| < 1

All five modes return a root less than one integer grid unit from the exact root.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtRound_error_le_half (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) {x : ℚ} (hx : 0 ≤ x) : |↑(mode.sqrtRound x) - √↑x| ≤ 1 / 2

The exact square test determines which side of the real midpoint contains the root.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtRound_towardZero_le {x : ℚ} (hx : 0 ≤ x) : ↑(RoundingMode.towardZero.sqrtRound x) ≤ √↑x

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtRound_towardNegative_le {x : ℚ} (hx : 0 ≤ x) : ↑(RoundingMode.towardNegative.sqrtRound x) ≤ √↑x

theorem FloatLib.Floats.Formats.DecimalInterchange.le_sqrtRound_towardPositive {x : ℚ} (hx : 0 ≤ x) : √↑x ≤ ↑(RoundingMode.towardPositive.sqrtRound x)