ancientDecay_implies_Aprime2r2_integrable
plain-language theorem explainer
AncientEnergyDecay for an RM2URadialProfile implies integrability of (A')² r² over (1, ∞). This supplies the second half of the CoerciveL2Bound used in tail-flux estimates for ancient Navier-Stokes solutions. The proof applies the general rpow-decay integrability lemma and reduces the bound to an r^{-3} majorant via algebraic manipulation of exponents.
Claim. Suppose $P$ is an RM2URadialProfile and $hD$ encodes the decay $|A'(r)| ≤ C r^{-5/2}$ for $r > 1$ with $C > 0$. Then the function $r ↦ (A'(r))^2 r^2$ is integrable over $(1, ∞)$.
background
RM2U.TailFluxInstantiation connects Galerkin-extracted ancient solutions to the integrability conditions required for the Bet1 boundary term. An RM2URadialProfile consists of a radial function $A$ together with its first and second derivatives $A'$ and $A''$, each satisfying the appropriate differentiability conditions on $(1,∞)$. The structure AncientEnergyDecay packages the decay estimates $|A(r)| ≤ C r^{-3/2}$ and $|A'(r)| ≤ C r^{-5/2}$ that follow from the finite-energy condition on the original velocity field.
proof idea
The tactic proof refines integrableOn_Ioi_of_rpow_decay with exponent -3 and the positivity of $C$. It then introduces a point $r > 1$, establishes non-negativity, applies gcongr to the deriv_decay bound, and performs rpow rewrites to reduce the majorant to $C^2 r^{-3}$. The final calc confirms the inequality chain.
why it matters
This theorem supplies one of the two integrability conditions needed to construct CoerciveL2Bound from AncientEnergyDecay, which in turn feeds the proof that tail flux vanishes. It closes the second half of the chain from energy decay to the Bet1 integrability condition required for the TailFluxVanishImpliesCoerciveHypothesis. In the Recognition Science setting it instantiates the concrete decay estimates that arise once the eight-tick octave and $D=3$ have fixed the decay rates for the ancient solution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.