Lean 4 formalization of Leray-Hopf weak-solution existence for the incompressible Navier-Stokes equations on the periodic 3-torus and on R^3, via the Galerkin method. Two capstone theorems are proved kernel-only (no project axioms, no sorryAx); see README.md for the exact modeling scope and claims table.