Executable compact finite square root

The compiled path consumes the sign, significand, and exponent from FiniteKernel.Components, avoiding a second storage decode. Conventional IEEE descriptors use the unpacked-model kernel, and other descriptors use an arbitrary-precision integer square root. Correctness proofs live in Sqrt.Proof.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.targetExponent (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) : ℤ

Destination dyadic exponent for the rounded square root of a positive exact dyadic.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.roundRoot (root remainder shift : ℕ) : ℕ

Round an integer square-root approximation after discarding shift low root bits.

remainder is the square-root remainder, zero when the scaled radicand is a perfect square. At a half-way discarded-bit pattern, a nonzero remainder puts the exact result above the tie.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtGeneral (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) : Model fmt

Descriptor-aware positive square root for descriptors that are not conventional IEEE.

The radicand and root use natural-number arithmetic, and exponents use Int. The root is computed at the destination scale with one guard bit and an exact sticky flag, so a large exponent gap does not force an oversized integer square root.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtPositiveDyadic (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) : Model fmt

Positive finite square root from an exact dyadic.

The IEEE branch uses the logical model NativeModelSqrt.sqrt and its native replacement theorem. The non-IEEE branch follows the descriptor and never converts through Float.Model.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtComponents? (fmt : FloatFormat) (value : FiniteKernel.Components) : Option (Model fmt)

Square root of already-decoded positive finite components.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtPositive? {fmt : FloatFormat} (x : Model fmt) : Option (Model fmt)

Square root of a positive finite nonzero value from compact decoded fields.

none means that the input is exceptional, negative, or zero.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtFields? (fmt : FloatFormat) (sign : Bool) (exponent mantissa : ℕ) : Option (Model fmt)

Square root from scalar finite fields.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtPositiveRuntime? {fmt : FloatFormat} (x : Model fmt) : Option (Model fmt)

Compiled positive square root with scalar field decoding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtPositiveRuntime {fmt : FloatFormat} (x : Model fmt) (_hfinite : x.isFinite = true) (_hnonzero : x.isZero = false) (_hpositive : x.signBit = false) : Model fmt

Square root of a value already classified as positive, finite, and nonzero.

The evidence is erased. IEEE descriptors decode the storage word once, and other descriptors read their policy-aware fields. Both paths call sqrtPositiveDyadic, which selects the conventional IEEE model or the descriptor-aware integer square-root kernel.