Independent check of Millenium/NavierStokes.lean against the Clay problem statement

Hello — this is a note rather than a bug report, plus two optional questions.

As part of an independent verification of the Navier-Stokes breakdown claim published on 8 September, I read `FormalConjectures/Millenium/NavierStokes.lean` clause by clause against Fefferman's official Clay problem description. I am not a mathematician; I did this because the OpenAI Lean development uses your statement as its Comparator challenge, so whether that statement is faithful determines what a passing kernel check actually establishes.

My conclusion was that it is faithful. Every condition in Fefferman's (C) has a corresponding named field, with nothing added and nothing dropped: (1) the equation, (2) incompressibility, (3) the initial condition, (4) and (5) the decay bounds on datum and force, (6) smoothness of p and u on R^n × [0, ∞), and (7) square-integrability with uniformly bounded energy. The periodic theorem likewise matches (D), including the pressure-periodicity condition from the Clay errata.

I also want to record a correction on my own side, in case it is useful to anyone doing the same exercise. A text extract in my working notes had (6) and (7) transposed, glossing (6) as bounded energy and (7) as smoothness. Your mapping is the correct one. I only caught it by going back to the PDF.

Question one, optional. Is there anything in the formalization you would flag as a place where it is faithful to the letter of Fefferman's text while admitting something a specialist would call a technicality? I looked at the force class, the energy condition and the smoothness requirement and found nothing, but "I looked and found nothing" is the weakest sentence in my notes, and an expert eye would differ from mine.

Question two, optional. Is the commit I read still the one you would point someone at? It was 8bf45ed70d48b2b2a501de9c00b26bfa38c573ee.

No obligation to answer either. Thanks for making the formalization public — having a statement written independently of, and prior to, the claim being tested against it is the single most useful provenance fact available in this whole exercise.

Start with FormalConjectures/Millenium/NavierStokes.lean and compare its named conditions with Fefferman's official Clay problem description, using commit 8bf45ed70d48b2b2a501de9c00b26bfa38c573ee as the reference point. Done would be an expert-confirmed note identifying any technicality or confirming that the formalization is faithful.

Written by the indexing model from the issue text.