Fix a stale link for the math.integer.isqrt correctness proof

[mdickinson]

The math.integer C source contains a link to an old proof of correctness for the math.integer.isqrt algorithm. That old proof, written in the obsolete language Lean 3, no longer exists at the given URL. This PR:

• updates the URL to point to the current proof, written in Lean 4
• removes the "an equivalent recursive algorithm" hedge, since the Lean 4 proof directly proves correctness of the iterative form of the algorithm

I didn't create an issue for this trivial comment-only change. Let me know if you think it needs one.

[mdickinson]

I updated the URL to use a permalink, to reduce the likelihood of the link breaking in the future. There's a tradeoff here: Lean 4 evolves fairly rapidly, so there's a risk that the permalink version will eventually not compile. (The project locks the version of Lean 4 that it builds against, so the build won't break purely because a new version of Lean 4 with backwards-incompatible changes has been released. But there are other possible evolutionary failure modes.)

[StanFromIreland]

LGTM

[miss-islington-app]

Thanks @mdickinson for the PR, and @StanFromIreland for merging it 🌮🎉.. I'm working now to backport this PR to: 3.15.
🐍🍒⛏🤖

[bedevere-app]

GH-154698 is a backport of this pull request to the 3.15 branch.

[StanFromIreland]

Earlier backports will have to be done manually.