Correctness of direct posit square-root packing

The integer-root prefix and its exact sticky bit select the same Posit as exact squared-boundary rounding. The proof uses rational points inside the generated root cell to bracket the mathematical square root. Both rational witnesses round to the same posit, so monotonicity identifies the rounding of the root between them.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.roundCode_eq_dyadic (format : Format) (radicand : Numerics.Dyadic) (hnegative : radicand.negative = false) : roundCode format radicand = DyadicSquareRoot.roundCode format radicand

The destination-width prefix kernel equals exact squared-boundary rounding on every nonnegative input.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.roundCode_lt_signMask (format : Format) (radicand : Numerics.Dyadic) : roundCode format radicand < format.signMaskNat

Every direct square-root code is a finite nonnegative Posit encoding.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.roundCode_lt_modulus (format : Format) (radicand : Numerics.Dyadic) : roundCode format radicand < format.modulus

Every direct square-root code lies inside the complete encoding modulus.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.ofNatBits_roundCode (format : Format) (radicand : Numerics.Dyadic) : ofNatBits (roundCode format radicand) = round format radicand

Re-encoding the selected square-root code gives the model-valued result.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.round_eq_dyadic (format : Format) (radicand : Numerics.Dyadic) (hnegative : radicand.negative = false) : round format radicand = DyadicSquareRoot.round format radicand

Direct nonnegative square-root packing equals exact squared-boundary packing.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.round_eq_dyadic_of_not_negative (format : Format) (radicand : Numerics.Dyadic) (hnonnegative : ¬radicand.toRat < 0) : round format radicand = DyadicSquareRoot.round format radicand

Direct square-root packing equals exact squared-boundary packing on its mathematical domain.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.round_eq_reference_of_nonnegative (format : Format) (radicand : Numerics.Dyadic) (hnegative : radicand.negative = false) : round format radicand = roundSqrtRat format radicand.toRat

Direct nonnegative square-root packing refines the rational specification.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.round_eq_reference_of_not_negative (format : Format) (radicand : Numerics.Dyadic) (hnonnegative : ¬radicand.toRat < 0) : round format radicand = roundSqrtRat format radicand.toRat

Refinement stated by the mathematical square-root domain condition.