betInstantiationCert
plain-language theorem explainer
The theorem supplies a complete certificate that the RM2U closure pipeline holds for every Galerkin ancient solution of the Navier-Stokes equations. A researcher working on the regularity problem would cite it to confirm that the weighted L2 moment and coercive bound together close both the Bet1 integrability route and the Bet2 self-falsification route. The proof is a direct term construction that populates the three fields of the certificate structure from the already-proved sibling results on Bet1 instantiation, Bet2 instantiation, and full-p
Claim. Let $G$ be a Galerkin ancient element. Then the alternate Bet1 boundary integrability hypothesis holds for its radial profile, the Bet2 self-falsification hypothesis holds for its profile, and the RM2U pipeline closes: the log-critical shell moment is finite and the tail flux vanishes.
background
A GalerkinAncientElement packages a truncation level $N$, an RM2URadialProfile (the radial coefficient in the $l=2$ sector), a weighted $L^2$ moment (finite energy from $∫|u|^2<∞$), and a coercive $L^2$ bound (from the Galerkin energy inequality). The BetInstantiationCert structure asserts that for any such element the Bet1 route, Bet2 route, and full pipeline (RM2Closed and TailFluxVanish) all hold. The module states that the energy inequality supplies the coercive bound while the finite-energy condition supplies the weighted moment; together they discharge Bet1BoundaryIntegrableHypothesisAlt and thereby NonParasitismHypothesis, closing the RM2U sector.
proof idea
The proof is a term-mode construction that directly supplies the three fields of the BetInstantiationCert structure. It references the Bet1 instantiation for Galerkin elements (which converts weighted moment plus coercive bound into the alternate Bet1 hypothesis), the Bet2 instantiation for Galerkin elements (self-falsification by contradiction on tail flux), and the rm2u_pipeline_complete theorem (which combines RM2Closed and TailFluxVanish). No tactics are used; the term simply assembles the three already-proved results.
why it matters
This declaration completes the RM2U pipeline closure for Galerkin ancient elements, as described in the module documentation on Bet instantiation via energy inequality and the Bet1/Bet2 paths. It populates the parent BetInstantiationCert structure whose three fields certify that the log-critical shell moment remains finite. In the Recognition Science framework it supports the Navier-Stokes analysis inside the RM2U sector, consistent with the eight-tick octave and $D=3$ spatial dimensions; no open scaffolding remains since the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.