Is ‖S‖_{L^∞} ≤ C‖ω‖_{L^∞}? A deep check of PeriodicStrainLinfBound

Is there one constant C with ‖S u(x)‖ ≤ C‖ω u‖_∞ for every smooth, divergence-free, ℤ³-periodic field u? We prove in Lean 4/Mathlib, with no sorry and only the standard axioms, that there is not (not_staticStrainLinfBound). An explicit family u_K of divergence-free trigonometric polynomials (K odd) has: the Fourier identity S₁₁(0) = (16/π²) Σ_{k,l odd ≤ K} 1/(k²+l²) (proved: strain00_origin); the uniform vorticity bound ‖ω_K‖_∞ ≤ 36 (proved: norm_vort_le, via a formalized Gibbs/Fejér–Jackson-type bound |Σ_{k≤n} sin(kx)/k| ≤ 3; the sharper (6 Si(π)/π)² ≈ 12.5 is classical); ‖S_K‖_∞ ≥ (1/π²) log K for all odd K (proved: originStrain_ge_log). Status: StaticStrainLinfBound is refuted in Lean with no caveat. The solution-level PeriodicStrainLinfBound is false as stated only modulo classical local existence (not formalized). The sharp growth (2/π) log K is numerical only. Conditional results that do give the bound are recorded. Lean files StrainLinf.lean, StrainLinfFamily.lean and SineSumBound.lean are attached; they correspond to local commit 029a9b9, not yet pushed (the related identifier points to the last pushed commit, 216ba1c). This document does not claim a solution of the Navier–Stokes Millennium Problem.