Compiler certificate for the native integer square root

The logical sqrt is the Newton iteration, which the kernel can evaluate. Compiled code runs sqrtChecked, whose floating-point candidate is accepted only after an exact square check. Both compute Nat.sqrt on every word, so the substitution is registered with @[csimp]. Runtime modules import this module to compile their calls through the checked path.

@[csimp]

theorem FloatLib.Numerics.FixedWord.IntegerSquareRoot.sqrt_eq_sqrtChecked : sqrt = sqrtChecked

Compile the native integer square root through the checked floating-point candidate.