rm2_closed_for_galerkin
plain-language theorem explainer
rm2_closed_for_galerkin asserts that every Galerkin ancient element satisfies RM2Closed on its radial profile A. Researchers closing energy estimates for the Navier-Stokes problem inside the Recognition Science framework would cite it when confirming control of the ℓ=2 sector. The argument is a one-line wrapper that feeds the profile and its coercive L2 bound into the corresponding closure lemma.
Claim. Let $G$ be a Galerkin ancient element at truncation level $N$ equipped with an RM2U radial profile, a weighted $L^2$ moment ensuring finite energy, and a coercive $L^2$ bound from the Galerkin energy inequality. Then $RM2Closed(G.profile.A)$ holds.
background
GalerkinAncientElement packages data for an ancient Navier-Stokes solution truncated at level $N$: it carries an RM2URadialProfile (the ℓ=2 coefficient $A$), a WeightedL2Moment (finite energy via ∫ A(r)² r² dr < ∞), and a CoerciveL2Bound extracted from the Galerkin energy inequality. The module sets up the Bet1 route: the energy inequality together with the weighted moment yields boundary integrability of the operator term, which produces the non-parasitism hypothesis and finally RM2Closed. Upstream results supply the energy identity that justifies the coercive bound and the integration-gap constants used in the weighted estimates.
proof idea
The proof is a one-line wrapper that applies rm2Closed_of_coerciveL2Bound directly to G.profile and G.coercive.
why it matters
The declaration supplies the RM2Closed half of the pipeline and is invoked by rm2u_pipeline_complete, which asserts both RM2Closed and tail-flux vanishing for any Galerkin ancient element. It fills the Bet1 instantiation step that converts the Galerkin energy inequality into control of the log-critical shell moment, aligning with the Recognition Science forcing chain and the RCL identity. The module notes the Bet2 self-falsification route as a conceptually cleaner alternative that remains open for future discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.