Global regularity for the Taylor-Green family up to |A|/nu = 28.5: a Lean proof

We prove in Lean 4 with Mathlib that the three-dimensional incompressible Navier-Stokes equations on the unit torus have a global classical solution for the Taylor-Green datum multiplied by A, whenever nu > 0 and |A| ≤ 28.5 nu. The solution is smooth up to the initial time. A symmetrised Leray estimate halves the constant in the critical Fourier inequality and gives the sufficient condition X_{-1}(u0) < 2 nu for smooth, mean-zero, divergence-free periodic data. For the Taylor-Green family, comparison with the exact heat evolution and a scalar logarithmic barrier prove the range |A|/nu ≤ 27; a first Picard correction and a generalised barrier extend it to 28.5. The same arguments give global regularity for smooth data in X_{-1}-balls around the family. The audited declarations depend only on the standard Lean axioms; the Lean kernel replayed the proofs and the independent checker nanoda accepted the exported declarations. The package contains the paper, the Lean source archive, the replay script and the audit evidence (Draft 11, snapshot 32).