Preferred cohorts of exact square roots

An exact representable square root is returned at the valid exponent closest to the preferred exponent. The public operation uses the floor of half the operand exponent, as required by IEEE 754-2019 §5.4.1.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_quantum_closest (f : Format) (mode : RoundingMode) (c : ℕ) (q preferred : ℤ) (hvalid : Datum.Valid f (Datum.finite false c q)) (d : ℕ) (r : ℤ) (hout : (sqrtMagnitude f mode ((↑c * 10 ^ q) ^ 2) preferred).value = Datum.finite false d r) (e : ℕ) (t : ℤ) (he : Datum.Valid f (Datum.finite false e t)) (hvalue : ↑c * 10 ^ q = ↑e * 10 ^ t) : |preferred - r| ≤ |preferred - t|

Exact square-root projection minimizes the distance to the preferred exponent.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.sqrt_quantum_closest (f : Format) (mode : RoundingMode) (a : ℕ) (b : ℤ) (c : ℕ) (q : ℤ) (hvalid : Datum.Valid f (Datum.finite false c q)) (hroot : ↑a * 10 ^ b = (↑c * 10 ^ q) ^ 2) (d : ℕ) (r : ℤ) (hout : (sqrt f mode (Datum.finite false a b)).value = Datum.finite false d r) (e : ℕ) (t : ℤ) (he : Datum.Valid f (Datum.finite false e t)) (hvalue : ↑c * 10 ^ q = ↑e * 10 ^ t) : |b / 2 - r| ≤ |b / 2 - t|

The public square root uses the closest valid exponent to the floor of half the input quantum. The exact-root hypothesis ranges over every representable nonnegative root, including zero.