pith. sign in
module module high

IndisputableMonolith.NavierStokes.RM2U.NonParasitism

show as:
view Lean formalization →

The NonParasitism module introduces a temporary hypothesis ensuring the radial coefficient profile at a fixed time slice exhibits no parasitic behavior in the RM2U formulation. Researchers closing the Navier-Stokes regularity argument via tail-flux and Bet1 integrability conditions cite it when instantiating the energy-identity reductions. The module organizes the hypothesis through a core definition together with lemmas relating it to boundary-term integrability and the RM2 closure steps.

claimNon-parasitism hypothesis for fixed-time radial coefficient $A(r)$: the boundary term and its derivative obey the $L^1$ integrability conditions that force the tail flux to vanish at infinity, formalized as NonParasitismHypothesis together with the auxiliary statements Bet1BoundaryIntegrableHypothesis and Bet2SelfFalsificationHypothesis.

background

In the RM2U framework the Core module fixes a time $t$ and spherical direction parameter $b$ to reduce the problem to a scalar radial coefficient $A(r)$ for $r≥1$. The EnergyIdentity module reduces vanishing of the tail-flux boundary term to two integrability obligations on that term and its derivative. The RM2Closure module supplies the coercive ℓ=2 control that implies finiteness of the log-critical shell moment ∫|A|/r and boundedness of the affine obstruction.

proof idea

This is a definition module. It declares NonParasitismHypothesis and the auxiliary Bet1BoundaryIntegrableHypothesis, then records the implication lemmas nonParasitism_of_bet1, bet1_boundaryTerm_integrable_of_L2_mul_r and bet1_boundaryTerm_integrable_of_A2r_and_coercive that link the hypothesis to the integrability conditions already established in EnergyIdentity.

why it matters in Recognition Science

The module supplies the non-parasitism hypothesis instantiated by BetInstantiation for concrete Navier-Stokes ancient elements and by TailFluxInstantiation to connect Galerkin extraction to the full RM2U closure pipeline. It fills the temporary hypothesis slot required by the navier-dec-12-rewrite.tex argument for ensuring the tail/tightness gate closes without parasitic solutions.

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)