Exactness of seeded integer roots

Integer Newton iteration preserves an upper bound on the floor root. Once the guesses stop decreasing, the defining adjacent-power inequalities identify the floor root. The radicand's binary logarithm provides the initial bound for every positive degree.

theorem FloatLib.Numerics.IntegerRoot.newton_eq_nthRoot (degree value : ℕ) : newton degree value = degree.nthRoot value

The seeded Newton root is the floor root for every input and degree.