Verified native and arbitrary-precision 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. sqrtChecked_toNat does the same for the checked floating-point candidate. The native average cannot overflow, and the runtime module proves termination by a strictly decreasing guess.

checkRoot?_eq certifies the increasing-precision candidate by the defining square inequalities. sqrtRem_eq also gives the remainder, with full-precision iteration as the fallback. natSqrt_eq_sqrtNat installs both implementations as a compiler substitution for Nat.sqrt, keeping the native-word branch below 2^64.

@[simp]

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

average computes the floor of the natural-number average.

@[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 agrees with 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 with Nat.sqrt.

theorem FloatLib.Numerics.FixedWord.IntegerSquareRoot.isFloorRoot_spec {value guess : UInt64} (h : isFloorRoot value guess = true) : guess.toNat = value.toNat.sqrt

An accepted candidate is the floor square root.

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

sqrtChecked agrees with Nat.sqrt.

theorem FloatLib.Numerics.FixedWord.IntegerSquareRoot.checkRoot?_eq (value guess : ℕ) (result : ℕ × ℕ) (h : checkRoot? value guess = some result) : result = (value.sqrt, value - value.sqrt * value.sqrt)

Every accepted candidate gives the floor square root and its remainder.

theorem FloatLib.Numerics.FixedWord.IntegerSquareRoot.sqrtRem_eq (value : ℕ) : sqrtRem value = (value.sqrt, value - value.sqrt * value.sqrt)

Checked increasing-precision Newton returns the floor square root and its remainder.

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

The native and checked arbitrary-precision implementations compute the natural-number square root.

@[csimp]

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

The compiler uses native-word square root for one-word inputs and checked Newton for larger inputs.

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. The checked candidate's fallback calls Nat.sqrt.iter, never Nat.sqrt, so compiling the replacement cannot recurse through this substitution.