EnergyForcingHypothesis
plain-language theorem explainer
EnergyForcingHypothesis packages the assumption that tail flux vanishes for a radial profile P extracted from an ancient Navier-Stokes solution and that this vanishing yields the coercive L2 bound. Navier-Stokes analysts closing the RM2U self-consistency argument would cite it to link the energy identity to RM2Closed. The structure directly encodes the two properties obtained from half-line Sobolev embedding and the Galerkin energy bound.
Claim. Let $P$ be an RM2URadialProfile. The energy forcing hypothesis asserts that the tail flux vanishes, i.e., TailFluxVanish$(P.A, P.A')$, and that this vanishing implies the coercive $L^2$ bound CoerciveL2Bound$(P)$.
background
The module instantiates TailFluxVanishImpliesCoerciveHypothesis for concrete ancient Navier-Stokes elements obtained via Galerkin diagonal extraction. It connects the uniform energy bound ∫|∇u|² ≤ C to the radial profile A(r) via spherical harmonic projection, yielding A(r) = O(r^{-3/2}) at infinity and the integrability condition A(r)² r² = O(r^{-1}) on (1,∞). SobolevH1HalfLineDecay states that if f and f' lie in L²(1,∞) with the derivative relation, then f(r) → 0 as r → ∞; this is applied to A·r and A'·r under the weighted L² moment to obtain tail flux vanishing. CoerciveL2Bound then follows from the energy identity once tail flux vanishes.
proof idea
This is a structure definition that packages two properties. Tail flux vanishing is obtained by applying SobolevH1HalfLineDecay to the weighted L² moment on A·r and A'·r. The coercive bound is then recovered directly from the energy identity via the implication TailFluxVanish P.A P.A' → CoerciveL2Bound P.
why it matters
It supplies the hypothesis structure used by rm2u_self_consistent_closure to conclude RM2Closed P.A from the weighted L² moment. The declaration fills the step weighted moment → TailFluxVanish → CoerciveL2Bound → RM2Closed in the RM2U chain for ancient solutions. It touches the open question of discharging the weighted moment assumption from the full 3D Navier-Stokes equations without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.