pith. sign in
module module high

IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation

show as:
view Lean formalization →

This module instantiates the vanishing of the tail flux for ancient Navier-Stokes elements whose ℓ=2 radial coefficient satisfies the decay |A(r)| ≤ C r^{-3/2} for r ≥ 1. The bound follows from the finite-energy condition on the original velocity field and supplies the concrete integrability checks that close the boundary term in the energy identity. Researchers working on the RM2U reduction for Navier-Stokes regularity cite it to discharge the tail contribution before invoking the Bet1 route. The argument proceeds by direct power-law estimates

claimLet $A(r)$ be the ℓ=2 radial coefficient of an ancient NS solution. If $|A(r)| ≤ C r^{-3/2}$ for $r ≥ 1$, then the tail-flux boundary term and its derivative are integrable on $[1,∞)$, so the flux vanishes at infinity and the energy identity closes.

background

RM2U.Core reduces the 3D problem at fixed time t and test direction b to the scalar radial coefficient A(r) for r ≥ 1. EnergyIdentity defines the tail-flux boundary term and reduces its vanishing at infinity to two integrability obligations on the term and its derivative. NonParasitism isolates the single hard non-parasitism hypothesis, while RM2Closure supplies the coercive ℓ=2 control that converts integrability of ∫ |A|/r into boundedness of the affine obstruction. The present module supplies the decay hypothesis |A(r)| ≤ C r^{-3/2} that follows from finite total energy of the velocity field.

proof idea

The module applies the r^{-3/2} decay bound directly to the tail-flux integrand and its derivative. It verifies the two integrability conditions required by EnergyIdentity via elementary comparison with integrable powers. The structure is a collection of direct estimates; no inductive or tactic-heavy steps are needed once the power-law bound is given.

why it matters in Recognition Science

This module feeds BetInstantiation, which connects the weighted L² moment hypothesis to the full RM2U closure pipeline. It discharges the tail-flux instantiation step in the navier-dec-12-rewrite.tex reduction, allowing the energy identity to close without residual contributions at infinity. It thereby advances the classical coercive ℓ=2 ⇒ RM2 implication while leaving the non-parasitism gate as the remaining hypothesis.

scope and limits

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (22)