rigid_rotation_energy_lower_bound
plain-language theorem explainer
The theorem establishes a positive lower bound on the integrated squared speed of a rigid rotation field over any disk of radius R > 0. Navier-Stokes regularity researchers cite it when excluding finite-energy ancient solutions that contain persistent nonzero rotation. The proof constructs an explicit rectangle inside the ball, verifies containment and nonnegativity, then bounds the integrand below by a positive constant whose integral equals the target expression.
Claim. For real numbers $ω_0 ≠ 0$ and $R > 0$, let $c = (ω_0/2)^2$. Then $c R^4/64 ≤ ∫_{B(0,R)} c (x_1^2 + x_2^2) dx$, where $B(0,R) ⊂ ℝ^2$ is the open disk of radius $R$ centered at the origin.
background
This lemma belongs to the Running-Max Normalization module, which encodes the first step of the Navier-Stokes regularity argument (NS Paper §3). The module builds a monotone running maximum $M̃(t) = sup_{s≤t} ‖ω(·,s)‖_{L^∞}$ from a hypothetical blow-up sequence and produces normalized fields whose sup-norm is at most 1 on rescaled coordinates. The present inequality supplies a concrete energy lower bound needed to reach a contradiction with finite-energy assumptions.
proof idea
Define $c = (ω_0/2)^2$ and the rectangle rect = [R/2, 3R/4] × [0, R/4]. Verify rect lies inside the ball of radius R, that the integrand is continuous and nonnegative, and that the integral over the ball dominates the integral over rect. On rect the integrand is bounded below by the constant $c(R/2)^2$ almost everywhere; the measure of rect equals $(R/4)^2$, so the integral over rect is at least $c(R/4)^2(R/2)^2 = c R^4/64$.
why it matters
The bound is invoked directly by rigid_rotation_infinite_energy_proved to show that any nonzero rigid rotation produces infinite energy on expanding balls, contradicting the finite-energy hypothesis for ancient solutions. It therefore closes one route to blow-up in the Navier-Stokes regularity program. Within Recognition Science the result reinforces the dimensional constraint T8 (D = 3) by exhibiting energy divergence already in planar slices and aligns with the eight-tick octave structure that forces scale-invariant quantities to diverge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.