RM2Closed
plain-language theorem explainer
RM2Closed defines the closure property for a radial coefficient A by requiring finiteness of its log-critical moment in the simplified Navier-Stokes model. Researchers on Galerkin ancient solutions cite it when showing that coercive L2 bounds close the RM2U pipeline to BetInstantiationCert. The definition is a direct alias to LogCriticalMomentFinite, packaging the manuscript's one-line Cauchy-Schwarz step that L2 control on A implies L1 control on A/r.
Claim. For a radial function $A : (1,∞) → ℝ$, the predicate RM2Closed($A$) holds if and only if the log-critical shell moment $∫_1^∞ |A(r)|/r dr$ is finite.
background
In the RM2U.RM2Closure module the predicate RM2Closed acts as an interface hypothesis that encodes the classical closure step from coercive ℓ=2 control to boundedness of the affine obstruction. The log-critical shell moment is the integral ∫ |A(r)|/r dr over (1,∞), whose finiteness is the concrete content of RM2 in this model. The module doc states that the file hosts the coercive ℓ=2 ⇒ RM2 steps from navier-dec-12-rewrite.tex and keeps the final RM2 statement abstract to avoid scattering assumptions.
proof idea
This is a one-line definition that directly aliases RM2Closed A to LogCriticalMomentFinite A. No lemmas or tactics are invoked; the alias packages the equivalence for downstream use in rm2Closed_of_coerciveL2Bound and the Bet instantiation theorems.
why it matters
RM2Closed supplies the target property for the RM2 closure inside the Navier-Stokes RM2U pipeline. It is invoked by rm2_closed_for_galerkin, BetInstantiationCert and rm2u_pipeline_complete to certify that coercive L2 bounds on any Galerkin ancient element imply a finite log-critical moment. The definition fills the interface role described in the module doc, connecting the manuscript's Cauchy-Schwarz argument to the Recognition framework's classical fluid bridge at D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.