Exact square roots at the rounding scale

Integer division by a square commutes with the floor square root. Applying this at a power of two retains the guard bit, while comparison with the reconstructed square recovers the sticky bit. These identities preserve the entire extended mantissa and the unpacked rounding result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ScaledSqrt.sqrt_div_square (n d : ℕ) : (n / (d * d)).sqrt = n.sqrt / d

Dividing a radicand by an integer square commutes with its floor square root.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ScaledSqrt.sqrt_shift (n k : ℕ) : (n >>> (2 * k)).sqrt = n.sqrt >>> k

Discarding twice as many radicand bits gives exactly the shifted floor square root.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ScaledSqrt.shift_extended_succ (em : Float.Model.UnpackedFloat.ExtendedMantissa) (k : ℕ) : em >>> (k + 1) = { mantissa := em.mantissa / 2 ^ (k + 1), roundBit := em.mantissa / 2 ^ k % 2 != 0, stickyBit := em.mantissa % 2 ^ k != 0 || em.roundBit || em.stickyBit }

A positive extended-mantissa shift has one guard bit and the exact discarded-bit sticky flag.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ScaledSqrt.shifted_eq (n k : ℕ) : shifted n k = Float.Model.UnpackedFloat.ExtendedMantissa.ofMantissaAndAccuracy n.sqrt (accuracy n n.sqrt) >>> k

The reduced radicand preserves every field of the original shifted extended mantissa.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ScaledSqrt.round_eq (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) (n : ℕ) (e : ℤ) : round spec sign n e = Float.Model.UnpackedFloat.roundWithAccuracy spec sign n.sqrt e (accuracy n n.sqrt)

Scaling before the root preserves the complete unpacked result, including normalization.