IndisputableMonolith.NavierStokes.RM2U.RM2Closure
The module supplies a placeholder definition equating RM2 closedness of a radial coefficient to finiteness of its log-critical ell-two tail moment. Workers on the RM2U pipeline for Navier-Stokes would reference this encoding of the manuscript's boundedness condition. It is a definition-only module that later refinements can replace with a compactness statement.
claimA time-slice coefficient $A$ satisfies the RM2 closure condition precisely when its log-critical moment of order two remains finite: $\mathrm{RM2Closed}(A) \coloneqq \mathrm{LogCriticalMomentFinite}(A)$.
background
This module belongs to the RM2U specification layer for the tail and tightness gate in the Navier-Stokes analysis. It builds directly on the Core module, which fixes a time slice and a spherical test direction to produce the scalar radial coefficient $A(r)$ for $r \geq 1$. The setting is the one-dimensional radial problem obtained by refactoring the three-dimensional PDE gate.
The upstream Core module describes the RM2U tail/tightness gate refactored into a 1D radial coefficient problem. The present module encodes the manuscript equivalence of RM2 to boundedness of the log-critical $\ell=2$ tail moment in the simplest Lean-friendly form.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The definition supplies the central object used by the BetInstantiation, NonParasitism, and TailFluxInstantiation modules to complete the RM2U to RM2 pipeline. It encodes the manuscript equivalence of RM2 to boundedness of the log-critical ell-two tail moment, allowing the rest of the closure argument to proceed cleanly.
scope and limits
- Does not refine the definition to an explicit fixed-frame compactness statement.
- Does not prove equivalence between this encoding and other formulations of RM2.
- Does not address the non-parasitism hypothesis or its PDE translation.