rm2u_pipeline_complete
plain-language theorem explainer
The declaration establishes that the RM2U pipeline closes for any Galerkin ancient element, yielding both RM2 closure on the ℓ=2 radial profile and vanishing tail flux. Navier-Stokes regularity researchers would cite it to confirm control over the ℓ=2 mode under the Bet1 energy route. The proof is a direct term constructor that pairs the two supporting lemmas obtained from the weighted moment and coercive bound.
Claim. Let $G$ be a Galerkin ancient element consisting of truncation level $N$, an ℓ=2 radial profile $A$ with finite weighted $L^2$ moment and coercive $L^2$ bound. Then the RM2 closed condition holds for $A$ and the tail flux vanishes for $A$ and its derivative $A'$.
background
The module instantiates the Bet1 route for Navier-Stokes ancient elements by linking the weighted $L^2$ moment hypothesis to RM2U closure. A GalerkinAncientElement packages truncation level $N$, the RM2URadialProfile for the ℓ=2 coefficient, WeightedL2Moment ensuring ∫ A(r)² r² dr < ∞ from finite energy, and CoerciveL2Bound from the Galerkin energy inequality at level $N$ (see module doc). The local setting uses the energy inequality to obtain Bet1BoundaryIntegrableHypothesis, which yields NonParasitismHypothesis and finally RM2Closed.
proof idea
The proof is a term-mode one-line wrapper. It applies the constructor to the pair of lemmas rm2_closed_for_galerkin G and tailFlux_vanishes_for_galerkin G, each obtained upstream via the Bet1 path from the finite weighted moment and coercive bound on the profile.
why it matters
This result completes the RM2U pipeline instantiation and supplies the pipeline field in the downstream betInstantiationCert theorem. It advances the Bet1 energy route toward global regularity by showing the ℓ=2 mode remains controlled, which combines with the TF Pinch to exclude other modes. In the Recognition Science framework it supports deriving regularity from the functional equation and energy identities without invoking external analytic tools.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.