But just to clarify: is either of them actually addressing the real Navier-Stokes, or will it turn out we'll end up with two pairs of proofs about something irrelevant to the actual problem?

This is the formalization that was proven in Lean. As of now at least, it's believed to be a correct statement of the problem.

https://github.com/google-deepmind/formal-conjectures/blob/8...

Nobody is claiming they've misformalized Navier-Stokes.