Compiler certificates for restoring square root

Four word accumulators implement the two-limb recurrence for every radicand, initial state, and digit count. The compiler substitutions preserve wrapping arithmetic outside the numeric bounds of RestoringSqrt.Proof.

theorem FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootLoopWords_eq (radicand : UInt256) (steps : ℕ) (root remainder : UInt128) : rootLoopWords radicand steps root.hi root.lo remainder.hi remainder.lo = rootLoop radicand steps { root := root, remainder := remainder }

The accumulator and state recurrences agree without capacity or digit-count hypotheses.

theorem FloatLib.Numerics.FixedWord.RestoringSquareRoot.Internal.rootLoop_eq (radicand : UInt256) (steps : ℕ) (state : RestoringRootState UInt128) : rootLoop radicand steps state = RestoringSquareRoot.rootLoop radicand steps state

The word implementation agrees with rootLoop for every initial state and iteration count.

@[csimp]

theorem FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootLoop_eq_internal : rootLoop = Internal.rootLoop

Compile the state recurrence through its equal word-accumulator recurrence.

@[csimp]

theorem FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootAndRemainder_eq_internal : rootAndRemainder = Internal.rootAndRemainder

Compile the zero-initialized loop through the same word accumulators.