tailFlux_vanishes_for_galerkin
plain-language theorem explainer
For any Galerkin ancient element the tail flux between its radial profile A and derivative A' vanishes. Navier-Stokes researchers closing the RM2U pipeline cite this to confirm control of the ℓ=2 sector under the weighted L² moment and coercive bound. The proof is a one-line wrapper that extracts the tailFluxVanish field from the non-parasitism result already established for Galerkin elements.
Claim. Let $G$ be a Galerkin ancient element with radial profile $A$. Then TailFluxVanish$(A,A')$ holds.
background
The RM2U Bet Instantiation module constructs ancient Navier-Stokes solutions via Galerkin truncations at finite level N. GalerkinAncientElement packages the truncation N, an RM2URadialProfile (the ℓ=2 radial coefficient), WeightedL2Moment (finite energy ∫ A² r² dr < ∞ from the projected L² bound), and CoerciveL2Bound (from the Galerkin energy inequality). These two hypotheses together imply Bet1BoundaryIntegrableHypothesis, which yields NonParasitismHypothesis and therefore the vanishing of the tail flux.
proof idea
One-line wrapper that applies nonParasitism_for_galerkin to G and projects the tailFluxVanish component.
why it matters
The result feeds rm2u_pipeline_complete, which asserts both RM2Closed and TailFluxVanish for any Galerkin ancient element, and is used by bet2_for_galerkin as the Bet1 route. It instantiates the preferred Bet1 path (weighted moment plus coercive bound) inside the Navier-Stokes RM2U closure, bypassing the self-falsification argument of Bet2. The declaration touches the open regularity question by securing the log-critical shell moment under the Galerkin hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.