The viscous strain bound: what a ν,t-dependent constant can and cannot give

Negative result. The uniform bound ‖S‖∞ ≤ C‖ω‖∞ is false (Bahouri–Chemin family; Zenodo 10.5281/zenodo.23904623). This note examines the surviving variant with a constant depending on ν and t>0. It separates (i) a classical log-corrected bound, provable by standard Littlewood–Paley and parabolic-smoothing arguments but carrying a solution-dependent logarithm; (ii) the pure form ‖S(t)‖∞ ≤ c(ν,t)‖ω(t)‖∞, which remains open; and (iii) the consequence of (ii), proved in Lean 4: it yields only a lifespan (small-data) lower bound, and a bounded constant does not exclude blow-up of the comparison ODE. So even if the ν,t-dependent strain bound holds, the continuation route reduces back to the Beale–Kato–Majda criterion. Numerics for the evolved family (2D slice) show the ratio follows a + b log(1/(νt)) with b close to the heat-flow value 1/π (numerical, not proved). Lean source: ViscousStrainBound.lean, commit 346abf6: https://github.com/BenFrohman/periodic-ns-classical-continuation/commit/346abf6