Correctness of rational-free exact posit square-root rounding

A finite posit is dyadic, although its square root need not be. This module proves that exact squared comparisons agree with the rational-comparison specification and then connects that specification to rounding Real.sqrt. Real numbers remain confined to this proof layer.

theorem FloatLib.Floats.Formats.Posit.Model.lowerSqrtCode_eq_realRounding_lowerCode (format : Format) (radicand : ℚ) (hradicand : 0 ≤ radicand) : lowerSqrtCode format radicand = RealRounding.lowerCode format √↑radicand

The squared rational search and the real square-root search select the same lower posit code.

This is the order-theoretic bridge behind executable square-root rounding: for nonnegative values, x² ≤ r is equivalent to x ≤ Real.sqrt r.

theorem FloatLib.Floats.Formats.Posit.Model.roundSqrtCode_eq_roundPositiveCode (format : Format) (radicand : ℚ) (hradicand : 0 ≤ radicand) : roundSqrtCode format radicand = RealRounding.roundPositiveCode format √↑radicand

Squared-comparison square-root rounding is exactly real-valued rounding of Real.sqrt.

The proof covers the standard's nonzero-underflow saturation, exact roots, overflow saturation, appended-bit boundary, and tie-to-even rule for every static posit width.

theorem FloatLib.Floats.Formats.Posit.Model.roundSqrtRat_eq_roundPositive (format : Format) (radicand : ℚ) (hradicand : 0 ≤ radicand) : roundSqrtRat format radicand = RealRounding.roundPositive format √↑radicand

Model-valued squared-comparison rounding equals real rounding of Real.sqrt.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicSquareRoot.lowerCode_eq_reference (format : Format) (radicand : Numerics.Dyadic) : lowerCode format radicand = lowerSqrtCode format radicand.toRat

The dyadic square search follows exactly the reference rational search.

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

Dyadic squared-comparison rounding selects exactly the rational specification's code.

The sign premise is the domain condition for square root. Negative finite inputs are handled as NaR by the arithmetic operation before reaching this rounder.

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

Rational-free nonnegative square-root rounding refines the reference model rounder.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicSquareRoot.round_eq_realRounding_sqrt_of_nonnegative (format : Format) (radicand : Numerics.Dyadic) (hnegative : radicand.negative = false) : round format radicand = RealRounding.roundPositive format √↑radicand.toRat

Exact-dyadic square-root execution equals real-valued rounding of the mathematical square root.

This theorem is the end-to-end semantic statement for the runtime rounder. It introduces no real-number computation: Real.sqrt occurs only on the noncomputable specification side.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicSquareRoot.negative_eq_false_of_not_toRat_neg (radicand : Numerics.Dyadic) (hsignificand : radicand.significand ≠ 0) (hnonnegative : ¬radicand.toRat < 0) : radicand.negative = false

A nonzero dyadic whose rational value is not negative carries a clear sign bit.

Square-root rounders state their domain condition as ¬radicand.toRat < 0; this lemma converts that condition into the sign-field premise used by the refinement theorems.

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

The same refinement theorem stated by the mathematical square-root domain condition.

This form is convenient for arithmetic dispatch: exact comparison with zero proves the premise without exposing the dyadic carrier's sign field.