pith. sign in
module module moderate

IndisputableMonolith.NavierStokes.RM2U.NonParasitism

show as:
view Lean formalization →

The module states a temporary non-parasitism hypothesis on the radial coefficient profile at a fixed time slice. Researchers closing the RM2U gate for Navier-Stokes ancient solutions cite the hypothesis when linking energy identities to integrability. The module assembles the hypothesis with related boundary integrability lemmas that connect to the coercive control steps.

claimLet $A(r)$ denote the radial coefficient for $r$ at least 1 at fixed time $t$ and test parameter $b$. The non-parasitism hypothesis requires that this profile satisfies an integrability condition that prevents parasitic growth in the weighted tail moments.

background

The RM2U framework recasts the Navier-Stokes tail problem as a one-dimensional radial coefficient equation for $A(r)$, $r$ at least 1, at fixed time $t$ and spherical direction $b$. Core defines the tail-flux boundary term. EnergyIdentity reduces vanishing of the tail flux to two integrability obligations for the boundary term and its derivative. RM2Closure hosts the coercive ell equals 2 control implying finiteness of the log-critical shell moment integral of absolute value of A over r, and hence boundedness of the affine obstruction.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the non-parasitism hypothesis instantiated in BetInstantiation to connect weighted L2 moments to the RM2U closure pipeline and in TailFluxInstantiation to link Galerkin extraction to the Bet1 integrability conditions. It fills the temporary hypothesis slot in the navier-dec-12-rewrite.tex development for the RM2U tail gate.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (61)