rigid_rotation_infinite_energy_proved
plain-language theorem explainer
Nonzero rigid rotations in the plane yield kinetic energy that diverges as the fourth power of the integration radius, ruling out any uniform finite-energy bound. Navier-Stokes regularity arguments cite this result to exclude constant-vorticity blowup candidates after running-max normalization. The tactic proof assumes a finite E, builds a radius R scaling with E and the rotation speed, then invokes the quartic lower-bound integral on that ball to exceed E.
Claim. Let $c = (ω_0/2)^2$. For any $ω_0 ∈ ℝ$ with $ω_0 ≠ 0$, there is no finite $E ∈ ℝ$ such that $∫_{B(0,R)} c |x|^2 dx ≤ E$ holds for every $R > 0$.
background
The module implements the running-max normalization of NS Paper §3 Step 1: given a hypothetical blowup sequence with sup-norms $M_n → ∞$, one rescales by the running maximum to produce scale-invariant fields with $‖ω̃‖∞ ≤ 1. rigid_rotation_infinite_energy is the statement that a constant vorticity field $ω ≡ ω_0 ≠ 0$ cannot satisfy any finite-energy condition on expanding balls in $ℝ^2$. It is defined as the negation of the existence of $E$ bounding the integral of $c |x|^2$ over every ball of radius $R$. The key supporting lemma rigid_rotation_energy_lower_bound supplies the explicit quartic lower bound $c R^4/64 ≤ ∫{B(0,R)} c |x|^2 dx$ for any $R > 0$.
proof idea
Assume for contradiction that a finite $E$ exists. Set $c = (ω_0/2)^2 > 0$. Apply rigid_rotation_energy_lower_bound on the unit ball to obtain $E ≥ 0$. Define $R := max(1, 64(E+1)/c)$. Verify $R ≥ 1$, $64(E+1) ≤ c R$, and the quartic comparison $c R/64 ≤ c R^4/64$. Apply the lower-bound lemma on the ball of radius $R$ to reach $c R^4/64 ≤ E$, contradicting the choice of $R$. The final nlinarith closes the inequality chain.
why it matters
The theorem supplies the rigid_rotation_energy_diverges field inside runningMaxCert, the central certificate for the normalization construction. It thereby closes the step that excludes rigid-rotation ancient solutions under the finite-energy hypothesis used throughout the Recognition Science Navier-Stokes analysis. The result aligns with the broader framework in which regularity follows from the single functional equation and the forced emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.