Verified native-word integer square root

sqrtIter_toNat identifies the native Newton iteration with Nat.sqrt.iter, and sqrt_toNat proves that its initialization computes the floor square root. The native average cannot overflow. The runtime module proves termination by a strictly decreasing guess.

natSqrt_eq_sqrtNat installs a compiler substitution for Nat.sqrt, using this implementation below 2^64 and the arbitrary-precision definition otherwise.

@[simp]

theorem FloatLib.Numerics.FixedWord.IntegerSquareRoot.average_toNat (left right : UInt64) : (average left right).toNat = (left.toNat + right.toNat) / 2

The overflow-free native average has its ordinary natural-number value.

@[simp]

theorem FloatLib.Numerics.FixedWord.IntegerSquareRoot.sqrtIter_toNat (value guess : UInt64) : (sqrtIter value guess).toNat = Nat.sqrt.iter value.toNat guess.toNat

The native Newton iteration is exactly Lean's natural-number iteration.

@[simp]

theorem FloatLib.Numerics.FixedWord.IntegerSquareRoot.sqrt_toNat (value : UInt64) : (sqrt value).toNat = value.toNat.sqrt

Native-word integer square root agrees exactly with Nat.sqrt.

theorem FloatLib.Numerics.FixedWord.IntegerSquareRoot.sqrtNat_eq_sqrt (value : ℕ) : sqrtNat value = value.sqrt

The bounded native implementation preserves natural-number square root.

@[csimp]

theorem FloatLib.Numerics.FixedWord.IntegerSquareRoot.natSqrt_eq_sqrtNat : Nat.sqrt = sqrtNat

The compiler uses native-word square root whenever the input fits in one word.

This @[csimp] theorem is global: every module that imports it, in particular everything that imports FloatLib.Kernels, compiles Nat.sqrt to sqrtNat, including uses unrelated to FloatLib. The substitution is sound by sqrtNat_eq_sqrt, and the fallback branch of sqrtNat is the unchanged logical definition, so only inputs below 2^64 take a different code path.