Public square-root semantics

These results cover zero's sign and preferred quantum, invalid negative inputs, and the real numerical error of a finite nonnegative operand. The public error bound includes zero rather than assuming the input is strictly positive.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.sqrt_zero (f : Format) (mode : RoundingMode) (s : Bool) (q : ℤ) : sqrt f mode (Datum.finite s 0 q) = { value := Datum.finite s 0 (max f.minQuantum (min (q / 2) f.maxQuantum)) }

Square root preserves either zero sign and clamps the floored half-exponent to the format's quantum range.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.sqrt_negative (f : Format) (mode : RoundingMode) (c : ℕ) (hc : c ≠ 0) (q : ℤ) : sqrt f mode (Datum.finite true c q) = invalidResult

A negative nonzero finite operand raises invalid and returns a quiet NaN.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.sqrt_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (ha : 0 ≤ a) (hfinite : (sqrt f mode x).status.overflow = false) : ∃ (value : ℚ), (sqrt f mode x).value.toRat? = some value ∧ |↑value - √↑a| ≤ 10 ^ sqrtQuantum f a / 2

The returned square root has at most half a decimal grid unit of real error.