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.rootLoopImpl_eq_rootLoop (radicand : UInt256) (steps : ℕ) (state : RestoringRootState UInt128) : rootLoopImpl radicand steps state = rootLoop radicand steps state

The word implementation preserves every initial state and iteration count.

@[csimp]

theorem FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootLoop_eq_rootLoopImpl : rootLoop = rootLoopImpl

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

@[csimp]

theorem FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootAndRemainder_eq_rootAndRemainderImpl : rootAndRemainder = rootAndRemainderImpl

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