Native integer square root for band parameters

Main results

• BandPreparation.exec_root: successive squared comparisons compute the ordinary natural square root within 5 * sqrt k + 6 instructions, with every trial square proved to fit.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_root {w : ℕ} (k : ℕ) (x : WordRAM.Data 96) (hk : x.regs count = k) (ho : x.regs one = 1) (hfit : WordRAM.Fits w (4 * k + 4)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w rootCode x y (5 * k.sqrt + 6) ∧ y.regs root = k.sqrt ∧ y.regs square = k.sqrt * k.sqrt ∧ y.mem = x.mem ∧ ∀ (i : Fin 96), i ≠ root → i ≠ square → i ≠ temporary → i ≠ limit → y.regs i = x.regs i

The root loop uses only increment, multiplication and unsigned comparison. The bound on trial squares is derived from the original count, including the first failing trial.