AncientEnergyDecay
plain-language theorem explainer
An ancient Navier-Stokes element in the RM2U projection satisfies pointwise decay bounds on its ℓ=2 radial coefficient A(r) and first derivative. Workers on the tail-flux vanishing step in the Navier-Stokes regularity problem cite this structure to supply the integrability hypotheses. The declaration is a bare structure definition that packages the C-bound and the two decay inequalities for r > 1.
Claim. Let $P$ be an RM2URadialProfile. The structure AncientEnergyDecay$(P)$ consists of a constant $C > 0$ together with the pointwise estimates $|A(r)| ≤ C r^{-3/2}$ and $|A'(r)| ≤ C r^{-5/2}$ for all $r > 1$.
background
The module connects Galerkin diagonal extraction of ancient Navier-Stokes solutions to the Bet1 integrability conditions required for tail-flux vanishing. An RM2URadialProfile is the structure that isolates the ℓ=2 spherical-harmonic coefficient A(r) of a fixed-time slice, together with its first and second derivatives and the HasDerivAt conditions on (1,∞). Upstream results supply the uniform energy bound ∫|∇u|² ≤ C that survives projection onto the radial profile, so that the L² norms of A' r and A r become the objects whose integrability must be verified once decay is imposed.
proof idea
This is a structure definition that directly records the positivity of C and the two pointwise decay inequalities. No lemmas are invoked; the four fields are the statement itself.
why it matters
The structure supplies the hypothesis for the four implication theorems that derive A²-integrability, (A')² r²-integrability, the full CoerciveL2Bound, and TailFluxVanish. It therefore closes the link from the Galerkin-extracted energy inequality to the boundary-term vanishing required for the coercive estimate in the RM2U closure. In the Recognition Science setting it instantiates the concrete decay needed to discharge the TailFluxVanishImpliesCoerciveHypothesis for the Navier-Stokes case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.