BetInstantiationCert
plain-language theorem explainer
The BetInstantiationCert structure bundles three routes confirming RM2U pipeline closure for any Galerkin ancient element: the alternative Bet1 boundary integrability hypothesis on the profile, the Bet2 self-falsification hypothesis, and the conjunction of RM2 closure with tail flux vanishing. A researcher working on global regularity for the Navier-Stokes equations would cite this to lock down control of the ℓ=2 radial mode under finite energy and coercive L² bounds. The definition is a direct structure constructor that assembles the routes as
Claim. A structure certifying RM2U closure on a Galerkin ancient element $G$, with fields: the alternative Bet1 boundary integrability hypothesis holding for the profile of $G$; the Bet2 self-falsification hypothesis holding for the profile of $G$; and the conjunction that the RM2 closure condition holds on the profile component $A$ together with vanishing tail flux between $A$ and $A'$.
background
The RM2U Bet Instantiation module connects weighted L² moments and Galerkin energy inequalities to the full RM2U closure pipeline for ancient Navier-Stokes elements. A GalerkinAncientElement at truncation level $N$ packages an RM2URadialProfile (the ℓ=2 radial coefficient), a WeightedL2Moment ensuring ∫ A(r)² r² dr < ∞ from finite energy, and a CoerciveL2Bound from the Galerkin energy inequality at level $N$. The module strategy uses the Bet1 path (weighted moment plus coercive bound yields boundary integrability, hence non-parasitism and RM2 closure) and the Bet2 path (self-falsification by contradiction on divergent subsequences). Upstream results supply the active edge count $A$ and gravitational constant $G$ in RS-native form, but the local setting rests on the energy identity and integration gap from the foundation.
proof idea
This is a structure definition with empty proof body. It functions as a direct constructor that packages the three routes (bet1_for_galerkin, bet2_for_galerkin, and rm2u_pipeline_complete) without further reduction steps.
why it matters
The certificate supplies the bundled evidence that the RM2U pipeline closes for Galerkin ancient elements, feeding directly into the downstream theorem betInstantiationCert that constructs the full instance. It fills the Navier-Stokes regularity step by showing the ℓ=2 mode remains controlled, which combines with the TF Pinch to yield global regularity. In the Recognition Science framework this instantiates the closure analogous to the T5–T8 forcing chain, enforcing self-similar control via the phi-ladder on the radial profile. It closes the Bet instantiation scaffolding without leaving open hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.