bet1_original_for_galerkin
plain-language theorem explainer
This result shows that the radial profile of a Galerkin ancient element satisfies the original Bet1 boundary integrability hypothesis. Analysts of the RM2U closure pipeline for ancient Navier-Stokes solutions cite it to link Galerkin energy bounds to the non-parasitism condition. The proof is a one-line wrapper that applies the conversion lemma from the alternate Bet1 hypothesis supplied by the Galerkin data.
Claim. Let $G$ be a Galerkin ancient element with radial profile $P$. Then $P$ satisfies the original Bet1 boundary integrability hypothesis: the boundary term from the RM2U energy identity is integrable over $[1,∞)$.
background
The RM2U Bet Instantiation module supplies concrete Bet1 realizations for ancient Navier-Stokes elements built by Galerkin truncation. A GalerkinAncientElement packages a truncation level $N$, an RM2URadialProfile $P$, the weighted L2 moment condition (finite energy: ∫ A(r)² r² dr < ∞), the coercive L2 bound from the Galerkin energy inequality, and operator pairing integrability. The module doc states that the energy inequality yields the coercive bound while the finite-energy condition supplies the weighted moment; together they discharge Bet1BoundaryIntegrableHypothesis P.
proof idea
The proof is a one-line wrapper applying bet1_of_bet1Alt to the alternate Bet1 hypothesis produced by bet1_for_galerkin on the input GalerkinAncientElement. This converts the alternate interface (operator-pairing form) into the original Bet1BoundaryIntegrableHypothesis.
why it matters
This declaration completes the original Bet1 interface for Galerkin elements and feeds directly into nonParasitism_for_galerkin, which yields NonParasitismHypothesis on the profile. It advances the RM2U closure pipeline by confirming tail-flux vanishing and ℓ=2 sector control via the energy-identity route. In the Recognition Science setting it instantiates the preferred Bet1 path (weighted moment plus coercive bound) that leads to RM2Closed, consistent with the module strategy of deriving non-parasitism from finite-window energy identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.