A cubic source for the vorticity maximum, and a recorded gap in the periodic continuation criterion

For a smooth divergence-free solution of the unforced periodic Navier–Stokes equations, let M(t)=‖ω(t)‖L∞. At a spatial maximum of |ω|, M′ ≤ ω·Sω/M. The 7 October 2026 version claimed ω·Sω ≤ CCZM³ from Calderón–Zygmund theory; that step is not proved, since it needs ‖∇u‖L∞ ≤ C‖ω‖L∞, which Calderón–Zygmund theory does not give. This corrected version replaces it by the classical log-corrected (Beale–Kato–Majda / Kato–Ponce) bound, and records the uncorrected inequality as the named hypothesis PeriodicStrainLinfBound. This hypothesis is refuted in Lean for every ν > 0 by the theorem not_periodicStrainLinfBound (StrainLinfRefutation.lean), which depends only on the standard axioms propext, Classical.choice and Quot.sound; the refutation builds on the static counterexample of https://doi.org/10.5281/zenodo.23904623 and concerns the uniform bound at t = 0 (a ν,t-dependent variant for t > 0 is a different statement and is not addressed). The comparison ODE lemmas, the ceiling under a quartic sink κM⁴, and the implication from that sink to a finite Beale–Kato–Majda integral are proved in Lean 4 (CubicSource.lean). The sink itself, PeriodicQuarticVorticitySink, remains open and is never assumed. Full 96³ numerics at the vorticity maximum show no sign of a κM⁴ sink. This document does not claim a solution of the Navier–Stokes Millennium Problem. Source and Lean code: commit 16f00aa, https://github.com/BenFrohman/periodic-ns-classical-continuation/commit/16f00aa.