nonParasitism_for_galerkin
plain-language theorem explainer
Any Galerkin ancient element satisfies the non-parasitism hypothesis on its radial profile. Researchers closing the RM2U pipeline for ancient Navier-Stokes solutions cite this to confirm the tail flux vanishes. The proof is a direct one-line application of the non-parasitism lemma to the Bet1 boundary integrability derived from the Galerkin finite energy and coercive bounds.
Claim. Let $G$ be a Galerkin ancient element. Then its radial profile satisfies the non-parasitism condition, i.e., the tail flux vanishes.
background
The RM2U Bet Instantiation module connects the Galerkin construction for ancient Navier-Stokes elements to the RM2U closure pipeline. A GalerkinAncientElement packages a truncation level, the ℓ=2 radial profile, a weighted L² moment ensuring finite energy, and a coercive L² bound from the Galerkin energy inequality at that level. The module documentation states that the energy inequality gives CoerciveL2Bound, the weighted moment follows from the finite-energy condition, and together these yield Bet1BoundaryIntegrableHypothesis, which produces NonParasitismHypothesis (tail flux vanishes) and then RM2Closed for the profile.
proof idea
This is a one-line wrapper that applies nonParasitism_of_bet1 to the profile of G and the Bet1 boundary integrability hypothesis obtained from bet1_original_for_galerkin G.
why it matters
This theorem supplies the non-parasitism condition required by tailFlux_vanishes_for_galerkin, which extracts TailFluxVanish and feeds into RM2Closed for the Galerkin profile. It completes the Bet1 path in the RM2U closure pipeline, linking Galerkin energy bounds to control of the ℓ=2 sector for ancient elements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.