Roots of dimension constants

A count can overflow its scalar representation while its square root is representable. The configured scalar context then uses FloatLib's rational-root algorithm before packing the result. The refinement below concerns that exceptional branch, for any IEEE descriptor and lossless codec. Ordinary counts keep the cast-then-root schedule. Native hardware execution is a separate boundary.

theorem TorchLean.ConfiguredBinary.toReal_sqrtNat_of_cast_overflow {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (n : ℕ) (hformat : format.isIEEE = true) (hoverflow : (FloatLib.Floats.Formats.BinaryInterchange.Model.ofRat format (↑n) FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearest true).status.overflow = true) (hfinite : FloatLib.Floats.ExecFloat.Binary.isFinite (Context.sqrtNat n) = true) : (FloatLib.Floats.ExecFloat.Binary.toModel (Context.sqrtNat n)).toReal = FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt format √↑n

Recover a representable root without first rounding an overflowing count.

The result is nearest-even rounding of the exact real square root, not the square root of a saturated or infinite cast. Finiteness is required because the real rounding model has no infinity.