bet1_for_galerkin
plain-language theorem explainer
Any Galerkin ancient element satisfies the alternate Bet1 boundary integrability hypothesis on its radial profile. Navier-Stokes researchers applying the RM2U closure cite this to discharge the integrability route from Galerkin data. The proof is a direct term application of the weighted-moment lemma to the finite-energy, coercive, and operator-pairing fields packaged inside the element.
Claim. Let $G$ be a Galerkin ancient element with radial profile $P$. Then the alternate Bet1 boundary integrability hypothesis holds for $P$.
background
The module RM2U Bet Instantiation supplies concrete instances of the Bet1 route for Navier-Stokes ancient solutions. A GalerkinAncientElement at truncation level $N$ packages an RM2URadialProfile together with three key properties: the weighted $L^2$ moment (finite energy: $∫_1^∞ A(r)^2 r^2 dr < ∞$), the coercive $L^2$ bound extracted from the Galerkin energy inequality, and the integrability of the rm2uOp pairing with $A r^2$ in $L^1(1,∞)$ (MODULE_DOC). These data together discharge Bet1BoundaryIntegrableHypothesisAlt on the profile, which then yields NonParasitismHypothesis and RM2Closed via the energy-identity control on finite windows (quoted: “the identity integral_rm2uOp_mul_energy_identity gives exact control”). Upstream lemmas include bet1_from_weighted_moment (TailFluxInstantiation) and the structure definitions in Core and NonParasitism.
proof idea
The proof is a one-line term wrapper that applies bet1_from_weighted_moment directly to the four fields of the input GalerkinAncientElement: its profile, finite_energy, coercive bound, and operator_pairing.
why it matters
This theorem supplies the Bet1 instantiation step that feeds bet1_original_for_galerkin (which converts to the original Bet1 interface) and betInstantiationCert (which assembles the full RM2U pipeline). It realizes the preferred Bet1 path described in the module: weighted moment plus coercivity produce boundary-term integrability in $L^1$, which yields non-parasitism and controls the ℓ=2 sector without leaving $L^2$ spaces. The construction sits inside the larger Recognition Science program of deriving Navier-Stokes regularity from the same functional equation that fixes $G$, $J$, and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.