bet2_for_galerkin
plain-language theorem explainer
Any Galerkin ancient element satisfies the Bet2 self-falsification hypothesis on its radial profile. Researchers closing the RM2U pipeline for Navier-Stokes regularity cite this to complete the Bet instantiation without relying on operator pairing. The proof proceeds by reductio: the assumption of non-vanishing tail flux is contradicted by applying the integrability result that the coercive L2 bound forces the boundary term to vanish.
Claim. For every Galerkin ancient element $G$, the Bet2 self-falsification hypothesis holds on the radial profile of $G$. Equivalently, a non-vanishing tail flux contradicts the coercive $L^2$ bound derived from the Galerkin energy inequality.
background
The module instantiates Bet hypotheses for concrete Navier-Stokes ancient elements. A GalerkinAncientElement is a structure containing truncation level $N$, an RM2URadialProfile (the ℓ=2 radial coefficient), a WeightedL2Moment ensuring finite energy via ∫ A(r)² r² dr < ∞, and a CoerciveL2Bound extracted from the Galerkin energy inequality at level $N$ (see REFERENCED_DEFS). The local setting is the RM2U closure pipeline: energy inequality plus weighted moment yields Bet1BoundaryIntegrableHypothesis, which yields NonParasitismHypothesis and finally RM2Closed on the profile. The Bet2 path supplies a self-falsification route that bypasses the operator-pairing step present in the alternate Bet1 path (MODULE_DOC).
proof idea
The term-mode proof constructs Bet2SelfFalsificationHypothesis by introducing the negation of tail-flux vanishing. It obtains the contradiction via exact application of the upstream lemma tailFlux_vanishes_for_galerkin (which itself rests on CoerciveL2Bound implying L¹ integrability of the boundary term), then discharges the assumption with absurd. The argument is therefore a one-line wrapper that reduces Bet2 to the already-established integrability result for Galerkin elements.
why it matters
This declaration supplies the bet2_route field inside betInstantiationCert, which certifies that the full RM2U pipeline (Bet1 or Bet2 route plus rm2u_pipeline_complete) is closed for any Galerkin ancient element. It fills the Bet2 instantiation step described in the module strategy, connecting the energy inequality directly to NonParasitismHypothesis and RM2Closed. In the Recognition Science setting this supports control of the ℓ=2 mode, complementing the TF Pinch for global regularity; the result remains local to Galerkin truncations and does not yet address the full T0-T8 forcing chain or the alpha band constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.