rigid_rotation_infinite_energy
plain-language theorem explainer
The definition encodes that a nonzero rigid rotation with angular speed ω₀ has unbounded kinetic energy in the plane, because the integral of (ω₀/2)² |x|² over balls of arbitrary radius diverges. Navier-Stokes regularity analysts cite it to exclude rigid rotations from any finite-energy ancient solution in a blowup sequence. It is introduced as a named proposition whose content is the direct negation of a uniform energy bound.
Claim. For nonzero real ω₀, there does not exist a real E such that for every R > 0 the integral over the ball of radius R centered at the origin in ℝ² of (ω₀²/4)(x₁² + x₂²) is bounded by E.
background
The Running-Max Normalization module constructs a monotone running maximum of the L^∞ vorticity norm along a sequence tₙ → T* and rescales the velocity and vorticity fields by this maximum so that the normalized vorticity is bounded by 1. This construction extracts ancient elements from a hypothetical blowup and relies only on monotone sequence properties. The local setting is the finite-energy Navier-Stokes equations on ℝ² × ℝ. The definition uses the Metric type, which re-exports the geometry and field structures needed for the ball and integral.
proof idea
The definition is a direct encoding of the infinite-energy statement as the negation of the existence of a finite uniform bound E. It applies the ball from the Metric geometry to the explicit quadratic energy density of a rigid rotation and leaves the divergence verification to the companion theorem.
why it matters
This definition supplies the structural hypothesis for the theorem rigid_rotation_infinite_energy_proved that establishes the divergence and is referenced inside the RunningMaxCert structure that certifies the normalized sequence. It fills the exclusion of rigid rotations required by the Navier-Stokes blowup argument in paper §3, consistent with the finite-energy premise used throughout the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.