Vorticity-Direction Regularity Criteria and the Projection Gap of the Frohmanian Tether: A Conditional Note

We state precisely the classical vorticity-direction regularity criteria of Constantin and Fefferman (Lipschitz direction) and of Beirão da Veiga and Berselli (½-Hölder direction) for the three-dimensional incompressible Navier–Stokes equations, record elementary lemmas about the direction field that we have kernel-checked in Lean 4, and explain how these criteria relate to the velocity projection Π_u used in the Frohmanian tether, in particular the projection gap where ω ∥ u. Status: The Constantin–Fefferman and Beirão da Veiga–Berselli criteria are classical results and are assumed as named hypotheses, not formalized. Only the elementary direction-field lemmas are proved in Lean 4 (0 sorry; axioms propext, Classical.choice, Quot.sound only), in BenFrohman/frohmanian-tether-geometric at commit b740838. This note does not prove global regularity and makes no claim on the Clay Millennium problem.