IndisputableMonolith.NavierStokes.RM2U.BetInstantiation
This module packages the ancient Navier-Stokes Galerkin element at truncation level N as the concrete data source for extracting the RM2U profile. Researchers applying the RM2U reduction to the regularity problem cite it for the Galerkin instantiation step that connects Fourier extraction to the Bet integrability conditions. The module assembles imports from Core, EnergyIdentity, NonParasitism, RM2Closure and TailFluxInstantiation into a single coherent object without internal proofs.
claimAn ancient NS Galerkin element at truncation level $N$ is a finite-dimensional projection of a time-dependent divergence-free velocity field satisfying the projected Navier-Stokes equations on the sphere, from which the radial coefficient $A(r)$ and tail-flux boundary terms are extracted for the RM2U gate.
background
The RM2U framework reduces the 3D Navier-Stokes regularity question to a 1D radial coefficient problem for $A(r)$ with $r \geq 1$, using a fixed time $t$ and spherical test direction $b$. Core supplies the tail-flux boundary term and the two integrability obligations that replace the vanishing-at-infinity condition. EnergyIdentity supplies the algebraic reduction of that boundary term via the SkewHarmGate lemma. NonParasitism isolates the single hard hypothesis that must still be verified for the Galerkin data. RM2Closure encodes the coercive $\ell=2$ control that yields finiteness of the log-critical shell moment and hence boundedness of the affine obstruction. TailFluxInstantiation already connects Galerkin diagonal convergence to the Bet1 integrability conditions.
proof idea
This is a definition module, no proofs. It imports the five upstream modules and declares the GalerkinAncientElement structure together with the derived Bet1, Bet2, non-parasitism and RM2-closure instances that the pipeline expects.
why it matters in Recognition Science
The module supplies the missing concrete object that lets the RM2U pipeline reach the fully classical closure steps in RM2Closure and the BetInstantiationCert. It therefore completes the Galerkin extraction leg of the argument in navier-dec-12-rewrite.tex, feeding directly into rm2u_pipeline_complete and the final certification that the ancient element satisfies the RM2U gate.
scope and limits
- Does not discharge the non-parasitism hypothesis.
- Does not treat the full 3D regularity question.
- Does not contain the Fourier extraction or equicontinuity lemmas themselves.
- Does not address non-Galerkin ancient solutions.
depends on (5)
declarations in this module (10)
-
structure
GalerkinAncientElement -
theorem
bet1_for_galerkin -
theorem
bet1_original_for_galerkin -
theorem
nonParasitism_for_galerkin -
theorem
tailFlux_vanishes_for_galerkin -
theorem
rm2_closed_for_galerkin -
theorem
bet2_for_galerkin -
theorem
rm2u_pipeline_complete -
structure
BetInstantiationCert -
theorem
betInstantiationCert