Correct rounding of the binary Euclidean norm #
Exact dyadic multiplication and addition form the sum of squares. The arbitrary-mantissa square-root theorem then rounds its square root once. Neither the squares nor their sum must fit the output format, so intermediate overflow and underflow cannot change the result.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.Algebraic.toReal_sqrtPositiveDyadic
(fmt : FloatFormat)
(hfmt : fmt.isIEEE = true)
(mantissa : ℕ)
(exponent : ℤ)
(hfinite : (FiniteSqrt.sqrtPositiveDyadic fmt mantissa exponent).isFinite = true)
:
(FiniteSqrt.sqrtPositiveDyadic fmt mantissa exponent).toReal = roundAt fmt √(↑mantissa * Flocq.bpow Numerics.binaryRadix exponent)
The existing finite square-root kernel accepts any exact nonnegative dyadic radicand.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.Algebraic.toReal_hypotDyadic
(fmt : FloatFormat)
(hfmt : fmt.isIEEE = true)
(left right : Numerics.Dyadic)
(hfinite : (hypotDyadic fmt left right).isFinite = true)
:
The exact-dyadic norm rounds the square root of the real sum of squares once.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.hypot_eq_hypotDyadic
{fmt : FloatFormat}
(left right : Model fmt)
{a b : Numerics.Dyadic}
(hleft : left.toDyadic? = some a)
(hright : right.toDyadic? = some b)
:
Finite operands take the exact-dyadic norm path.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_hypot_eq_roundAt
{fmt : FloatFormat}
(left right : Model fmt)
(hfmt : fmt.isIEEE = true)
(hleft : left.isFinite = true)
(hright : right.isFinite = true)
(hfinite : (left.hypot right).isFinite = true)
:
The finite IEEE Euclidean norm is one nearest-even rounding of sqrt (x² + y²).
The exact sum may exceed the representable range. Only finiteness of the final result is required; the theorem includes subnormal inputs, signed zeros and underflow boundaries.