Algebraic special values and preferred zero cohorts

Reciprocal square root keeps the zero sign at its pole, including negative zero. Hypotenuse lets infinity dominate quiet NaNs but still signals any signaling NaN. Exact zeros use the preferred quantum clamped to the destination format.

theorem FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude_zero (f : Format) (mode : RoundingMode) (preferred : ℤ) : sqrtMagnitude f mode 0 preferred = { value := Datum.finite false 0 (max f.minQuantum (min preferred f.maxQuantum)) }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.square_zero (f : Format) (mode : RoundingMode) (s : Bool) (q : ℤ) : square f mode (Datum.finite s 0 q) = { value := Datum.finite false 0 (max f.minQuantum (min (q + q) f.maxQuantum)) }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.square_infinity (f : Format) (mode : RoundingMode) (s : Bool) : square f mode (Datum.infinity s) = { value := Datum.infinity false }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rsqrt_zero (f : Format) (mode : RoundingMode) (s : Bool) (q : ℤ) : rsqrt f mode (Datum.finite s 0 q) = { value := Datum.infinity s, status := { divideByZero := true } }

This is the IEEE signed-zero rule: reciprocal square root of -0 is -∞.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rsqrt_infinity (f : Format) (mode : RoundingMode) : rsqrt f mode (Datum.infinity false) = { value := Datum.finite false 0 f.minQuantum }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rsqrt_negative_infinity (f : Format) (mode : RoundingMode) : rsqrt f mode (Datum.infinity true) = invalidResult

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

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_zero (f : Format) (mode : RoundingMode) (sx sy : Bool) (qx qy : ℤ) : hypot f mode (Datum.finite sx 0 qx) (Datum.finite sy 0 qy) = { value := Datum.finite false 0 (max f.minQuantum (min (min qx qy) f.maxQuantum)) }

Both zero signs disappear in a hypotenuse; the finer operand cohort is preferred.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_infinity_quietNaN (f : Format) (mode : RoundingMode) (sx sy : Bool) (payload : ℕ) : hypot f mode (Datum.infinity sx) (Datum.nan sy false payload) = { value := Datum.infinity false }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_quietNaN_infinity (f : Format) (mode : RoundingMode) (sx sy : Bool) (payload : ℕ) : hypot f mode (Datum.nan sx false payload) (Datum.infinity sy) = { value := Datum.infinity false }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_infinity_signalingNaN (f : Format) (mode : RoundingMode) (sx sy : Bool) (payload : ℕ) : hypot f mode (Datum.infinity sx) (Datum.nan sy true payload) = nanResult f sy payload true

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_signalingNaN (f : Format) (mode : RoundingMode) (s : Bool) (payload : ℕ) (y : Datum) : hypot f mode (Datum.nan s true payload) y = nanResult f s payload true

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot_quietNaN_signalingNaN (f : Format) (mode : RoundingMode) (sx sy : Bool) (px py : ℕ) : hypot f mode (Datum.nan sx false px) (Datum.nan sy true py) = nanResult f sx px true

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_zero_neg (f : Format) (mode : RoundingMode) (s : Bool) (q n : ℤ) (hn : n < 0) : powInt f mode (Datum.finite s 0 q) n = { value := Datum.infinity (powerSign s n), status := { divideByZero := true } }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_zero_pos (f : Format) (mode : RoundingMode) (s : Bool) (q n : ℤ) (hn : 0 < n) : powInt f mode (Datum.finite s 0 q) n = { value := Datum.finite (powerSign s n) 0 (max f.minQuantum (min (q * n) f.maxQuantum)) }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_degree_zero_finite (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) : powInt f mode (Datum.finite s c q) 0 = project f mode 1 0

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_degree_zero_quietNaN (f : Format) (mode : RoundingMode) (s : Bool) (payload : ℕ) : powInt f mode (Datum.nan s false payload) 0 = project f mode 1 0

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt_signalingNaN (f : Format) (mode : RoundingMode) (s : Bool) (payload : ℕ) (n : ℤ) : powInt f mode (Datum.nan s true payload) n = nanResult f s payload true