Real rounding and exceptional policies for binary roots

Reciprocal square root rounds the square root of the exact reciprocal radicand. Integer roots round the nonnegative root of the exact magnitude, inverting that magnitude before rounding for negative degrees. Negative odd roots restore the sign after choosing the real branch. The theorems include subnormal outputs and exact midpoint ties. Only IEEE overflow is excluded.

Zero policies are stated separately because the real numbers have neither signed zero nor infinity. In particular rsqrt(-0) has the negative overflow sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rsqrt_of_isZero {fmt : FloatFormat} (value : Model fmt) (hzero : value.isZero = true) : value.rsqrt = nativeOverflow fmt value.signBit

Reciprocal square root preserves the sign of a zero pole, including negative zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rootN_of_isNaN {fmt : FloatFormat} (value : Model fmt) (degree : ℤ) (hnan : value.isNaN = true) : value.rootN degree = value.quietNaN

A NaN input is quieted for every degree, keeping its payload.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rootN_zero {fmt : FloatFormat} (value : Model fmt) (hnan : value.isNaN = false) : value.rootN 0 = invalidResult fmt

Degree zero is invalid for every other input, including infinities and signed zeros.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rootN_of_isZero {fmt : FloatFormat} (value : Model fmt) (degree : ℤ) (hzero : value.isZero = true) (hdegree : degree ≠ 0) : value.rootN degree = if degree < 0 then nativeOverflow fmt (value.signBit && degree % 2 != 0) else zero fmt (value.signBit && degree % 2 != 0)

Odd roots retain the sign of zero, while even roots select a positive zero or positive pole.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_rsqrt_eq_roundAt {fmt : FloatFormat} (value : Model fmt) (hfmt : fmt.isIEEE = true) (hvalue : value.isFinite = true) (hzero : value.isZero = false) (hsign : value.signBit = false) (hfinite : value.rsqrt.isFinite = true) : value.rsqrt.toReal = roundAt fmt (√value.toReal)⁻¹

Reciprocal square root of a finite positive operand is one nearest-even rounding of 1 / sqrt x. The reciprocal radicand is exact, so an intermediate rounded square root cannot affect the result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Algebraic.root_radicand_rpow (q : ℚ) (degree : ℤ) : ↑(if degree < 0 then q⁻¹ else q) ^ (↑degree.natAbs)⁻¹ = ↑q ^ (↑degree)⁻¹

Negative integer degrees invert the radicand before taking its nonnegative root.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_rootN_eq_roundAt {fmt : FloatFormat} (value : Model fmt) (degree : ℤ) (hfmt : fmt.isIEEE = true) (hvalue : value.isFinite = true) (hzero : value.isZero = false) (hdegree : degree ≠ 0) (hdomain : value.signBit = false ∨ degree % 2 ≠ 0) (hfinite : (value.rootN degree).isFinite = true) : (value.rootN degree).toReal = roundAt fmt (if value.signBit = true then -|value.toReal| ^ (↑degree)⁻¹ else |value.toReal| ^ (↑degree)⁻¹)

A finite nonzero integer root rounds the chosen real branch once.

Even degrees require a clear sign bit, while odd degrees allow either sign. Negative degrees are reciprocal roots. The absolute value and the sign select the negative odd real branch, so the statement does not rely on the convention for real exponentiation of negative bases.