ancientDecay_implies_coercive
plain-language theorem explainer
Ancient energy decay on the ℓ=2 radial profile of an ancient Navier-Stokes solution implies the coercive L² bound consisting of integrability of A² and of (A')² r² over (1, ∞). Analysts studying the regularity of ancient solutions would cite this result to close the RM2U tail-flux hypothesis. The proof is a direct term-mode construction that invokes the two separate integrability theorems for the squared amplitude and the weighted derivative.
Claim. Let $P$ be an RM2U radial profile. If $P$ satisfies the ancient energy decay bounds $|A(r)| ≤ C r^{-3/2}$ and $|A'(r)| ≤ C r^{-5/2}$ for all $r > 1$, then $A^2$ is integrable over $(1,∞)$ and $(A')^2 r^2$ is integrable over $(1,∞)$.
background
The RM2URadialProfile is an abstract structure carrying a radial function A together with its first and second derivatives, equipped with HasDerivAt witnesses. AncientEnergyDecay is the hypothesis structure asserting power-law decay |A(r)| ≤ C r^{-3/2} and |A'(r)| ≤ C r^{-5/2} on (1,∞), which follows from the finite-energy condition on the original velocity field. CoerciveL2Bound is the target property requiring precisely that A² lies in L¹(1,∞) and (A')² r² lies in L¹(1,∞). This module instantiates the tail-flux vanishing implication for concrete ancient elements extracted via Galerkin methods, as described in the module documentation: the energy inequality gives uniform L² bounds, projection onto ℓ=2 yields the profile A(r), and the decay then supplies the required integrability.
proof idea
The proof is a one-line term that builds the CoerciveL2Bound pair by applying ancientDecay_implies_A2_integrable and ancientDecay_implies_Aprime2r2_integrable to the given profile and decay hypothesis.
why it matters
This theorem supplies the coercive L² bound required by the GalerkinAncientElement structure in the BetInstantiation module, thereby discharging one of the PDE-level inputs needed to close the RM2U argument for ancient solutions. It forms part of the chain that converts the standard energy decay of ancient Navier-Stokes elements into the integrability conditions for the bet1 boundary term. The result sits inside the broader program of deriving Navier-Stokes regularity from the Recognition Science forcing chain, specifically by instantiating the TailFluxVanishImpliesCoerciveHypothesis for Galerkin-extracted profiles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.