Six Birds for Navier-Stokes: A Mechanized No-Zeno Scaffold

Energy estimates for the three-dimensional incompressible Navier–Stokes equations bound the kinetic energy, but they do not stop velocity gradients from concentrating in ever smaller regions. This is why the classical regularity criteria, such as Beale–Kato–Majda, ask for control of a peak quantity. This paper builds a multiscale decision scaffold, inspired by the Six Birds framework, around a different question: can activity cascade to arbitrarily fine scales in finite time, a Zeno cascade? The scaffold keeps three kinds of statement apart. Proved in Lean. If every refinement step costs a fixed quantum of work, and the work available per unit time at depth j is bounded by a capacity whose reciprocals have divergent sum, then no Zeno cascade occurs. Route-stable reductions have at most polynomial capacity growth. In a finite model, a uniform capacity certificate over inputs that include localized tests forces a pointwise bound on the gain. Proved on paper, or stated as open hypotheses. We define the subgrid bridge with sharp Fourier shells and show that on a strong solution it returns the actual closure force. Energy alone bounds the power that the bridge supplies to shell j by C 25j/2‖u0‖23. That bound is too weak to certify divergence. An explicit three-mode field shows that no bound of the form ‖∇u‖∞‖uj‖22 holds for this power. Measured. An anti-localization certificate on initial data passes band-limited random fields (maxj κj ≈ 2.1) and rejects a localized shell wavepacket (κ ≈ 404). We do not prove the Clay regularity statement, and we do not show that the certificate persists under the flow. The Navier–Stokes inequalities that a proof along these lines would still need are listed explicitly.