Executable rational-free exact posit square-root rounding

A finite posit is dyadic, although its square root need not be. Correct rounding does not require constructing the root: for c ≥ 0 and x ≥ 0, c ≤ sqrt x exactly when c² ≤ x. This module performs every search and threshold decision with shared exact-dyadic multiplication and comparison. The rational and real-valued refinement theorems live in SquareRoot.Proof, so real numbers do not enter executable kernels.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicSquareRoot.lowerCode (format : Format) (radicand : Numerics.Dyadic) : ℕ

For a nonnegative radicand, the greatest nonnegative code whose squared value does not exceed it.

The standard code interval is searched logarithmically. Squaring a decoded candidate is exact and does not introduce a host floating-point or real-number oracle.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicSquareRoot.roundCode (format : Format) (radicand : Numerics.Dyadic) : ℕ

Correctly round the nonnegative square root of an exact dyadic radicand.

Zero is recognized from its significand. Positive values use exact squared comparisons for underflow, the lower-code search, the appended-bit threshold, and the tie-to-even decision. Arithmetic callers reject negative radicands before calling this helper.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicSquareRoot.round (format : Format) (radicand : Numerics.Dyadic) : Model format

Pack the code selected by exact dyadic square-root rounding.