rm2u_closed_for_ancient_element
plain-language theorem explainer
An ancient Navier-Stokes element whose radial profile satisfies the weighted L2 moment and coercive L2 bound obeys the RM2 closure condition. Workers on regularity criteria for ancient solutions cite this to complete the RM2U reduction chain. The proof is a direct one-line application of the lemma that turns the coercive bound into RM2 closure.
Claim. Let $P$ be a radial profile with radial function $A$. If the weighted $L^2$ moment holds, i.e., $A^2 r^2$ is integrable on $(1,∞)$, and the coercive $L^2$ bound holds, then $A$ satisfies the RM2 closure condition.
background
The module treats ancient Navier-Stokes elements obtained by Galerkin diagonal extraction. The energy inequality supplies a uniform bound on ∫ |∇u|². Projection onto the ℓ=2 spherical harmonic yields the radial profile A(r) with the Parseval relation ∫₁^∞ A'(r)² r² dr ≤ ∫ |∇u|². Ancient decay supplies A(r) = O(r^{-3/2}), which makes A(r)² r² = O(r^{-1}) integrable on (1,∞). WeightedL2Moment packages exactly this integrability: ∫₁^∞ A(r)² r² dr < ∞. CoerciveL2Bound is the hypothesis that the operator pairing and tail flux vanish, supplied by the EnergyIdentity and NonParasitism modules.
proof idea
The proof is a one-line wrapper that applies rm2Closed_of_coerciveL2Bound to the given profile and the coercive hypothesis.
why it matters
This declaration completes the four-step RM2U pipeline listed in the module doc-comment: weighted moment plus operator pairing yields Bet1 integrability, which yields tail-flux vanishing, which yields the coercive bound, which yields RM2 closure. It therefore supplies the final link that lets the Galerkin-extracted ancient element satisfy the RM2 closed condition. The result sits inside the Recognition Science treatment of Navier-Stokes regularity and closes the concrete instantiation of TailFluxVanishImpliesCoerciveHypothesis for finite-energy ancient elements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.