Proof: Let round(x) = f64-rounding of x.
Let 2k ≤ n < 2k+1, 0 ≤ k < 32.
If n2 can't be represented exactly, then:
round(n2) ≥ n2 + 1 - 22k+1-53 > n2 - 22k-52 + 22k-106 ≥ n2 - 2k-52n + 22k-106 = (n - 2k-53)2
round(n2) ≤ n2 + 22k+1-53 < n2 + 22k-52 + 22k-106 ≤ n2 + 2k-52n + 22k-106 = (n + 2k-53)2
n - 2k-53 < √(round(n2)) < n + 2k-53
round(√(round(n2))) = n
It follows from this that if you want floor(sqrt(x)) for x in u64, then compute in f64, round down to u64, and subtract 0 or 1.