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; 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 records the positive irrational tail: zero means the scaled radicand was a perfect square. At an exact half-way discarded-bit pattern, any nonzero square-root remainder moves 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 formats not represented by Lean's conventional IEEE model.

The radicand and root use natural-number arithmetic; exponents use Int. IntegerSquareRoot.sqrtNat uses the proved UInt64 kernel when the scaled radicand fits and Nat.sqrt for larger inputs.

@[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 deliberately retains the established logical model and native replacement theorem. The non-IEEE branch follows the complete 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 directly 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; other descriptors use their policy-aware fields. Both paths call sqrtPositiveDyadic, which selects the conventional IEEE model or the descriptor-aware integer square-root kernel.