constant_vorticity_implies_rigid_rotation
plain-language theorem explainer
A constant vorticity field ω₀ in two dimensions forces the velocity to be the rigid rotation u(x,y) = (ω₀/2)(-y, x). Navier-Stokes regularity researchers cite this to exclude finite-energy blowup profiles once the running-max normalization has produced a constant-vorticity limit. The proof is a one-line term-mode construction that directly exhibits the field and verifies the pointwise equality by reflexivity.
Claim. In two dimensions, a divergence-free velocity field $u$ whose vorticity equals the constant value $ω_0$ must satisfy $u(x,y) = (ω_0/2)(-y,x)$.
background
The module formalizes running-max normalization for sequences $t_n → T^*$ with $M_n = ‖ω(·,t_n)‖{L^∞} → ∞$. Normalized fields are obtained by rescaling with the running maximum $M̃(t)$, yielding scale-invariant bounds ‖ω̃‖{L^∞} ≤ 1. The present theorem supplies the explicit rigid-rotation form required by the 2D Biot-Savart law when vorticity is constant, as stated in the module doc-comment: once the blowup profile has constant vorticity, it must be a rigid rotation excluded by the energy constraint.
proof idea
The proof is a one-line term-mode wrapper that constructs the explicit velocity field $u(x) = (ω_0/2 · (-x.2), ω_0/2 · x.1)$ and confirms the equality holds identically by reflexivity.
why it matters
This result is invoked inside runningMaxCert to certify that any constant-vorticity limit profile must be a rigid rotation. The parent theorem runningMaxCert assembles monotonicity, boundedness, and this rigidity to close the normalization argument in NS paper Stage 5. It directly supports the energy-divergence exclusion for rigid rotations, which is recorded as a named proposition in the same module and used to rule out finite-energy solutions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.