IndisputableMonolith.NavierStokes.RM2U.RM2Closure
The module supplies the placeholder RM2Closed predicate for a radial coefficient A, defined as finiteness of its log-critical ℓ=2 tail moment. Navier-Stokes analysts working on the RM2U tail/tightness gate cite it to close the RM2 step in the pipeline. It is a definition-only module with no proofs or further structure.
claim$RM2Closed(A) := LogCriticalMomentFinite(A)$, where $A(r)$ is the scalar radial coefficient for fixed time slice $t$ and direction $b$, $r≥1$.
background
This module belongs to the RM2U layer that encodes the tail/tightness gate from navier-dec-12-rewrite.tex as a 1D radial problem. It imports the Core spec, which fixes a time $t$ and spherical test-field parameter $b$ to extract the radial coefficient $A(r)$ for $r≥1$. The definition encodes the manuscript equivalence of RM2 to boundedness of the log-critical ℓ=2 tail moment in the simplest Lean form, with a note that later refinement can target explicit fixed-frame compactness.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the RM2Closed predicate to BetInstantiation (which routes the integrability hypothesis), NonParasitism (the single hard gate), and TailFluxInstantiation (which connects Galerkin extraction to coercive conditions). It fills the placeholder for the RM2 closure step in the RM2U to RM2 pipeline.
scope and limits
- Does not prove equivalence between RM2Closed and any explicit compactness statement.
- Does not contain theorems or lemmas, only the definition.
- Does not connect the radial coefficient to the full three-dimensional Navier-Stokes equations.
- Does not address time evolution or global regularity questions.