ancientDecay_implies_tailFlux_vanish
plain-language theorem explainer
Ancient energy decay bounds on the ℓ=2 radial profile A(r) of an ancient Navier-Stokes solution imply that the tail flux vanishes at spatial infinity. Researchers working on the Navier-Stokes regularity problem cite this to close boundary terms in integrated energy identities. The proof is a direct ε-δ argument that combines the supplied power-law decay estimates on A and A' to obtain an explicit 1/r upper bound on the flux magnitude.
Claim. Let P be an RM2U radial profile. Suppose there exists C > 0 such that |A(r)| ≤ C r^{-3/2} and |A'(r)| ≤ C r^{-5/2} for all r > 1. Then the tail flux vanishes: lim_{r→∞} |A(r) · A'(r) · r²| = 0.
background
The module instantiates tail-flux vanishing for ancient Navier-Stokes elements obtained via Galerkin diagonal extraction. AncientEnergyDecay is the structure that records the decay inherited from the L² integrability of the original velocity field: |A(r)| ≤ C r^{-3/2} and |A'(r)| ≤ C r^{-5/2} for r ≥ 1, together with the positivity of C. This decay is the concrete consequence of projecting the finite-energy condition onto the ℓ=2 spherical harmonic mode, which preserves the weighted L² moment ∫₁^∞ A(r)² r² dr < ∞.
proof idea
The proof unfolds TailFluxVanish into Metric.tendsto_atTop and performs an ε-δ argument. It selects the threshold max(2, C²/ε + 1), invokes the two decay hypotheses to bound the product |A(r)| |A'(r)| by C² r^{-4}, then algebraically reduces the expression |A(r) A'(r) r²| to C²/r. The final comparison uses le_trans, sq_pos_of_pos, and standard real-analysis facts on powers and inverses to verify the bound is smaller than ε for all larger r.
why it matters
This result supplies the tail-flux vanishing hypothesis required by the RM2U closure for ancient solutions. It completes one link in the chain that converts the uniform Galerkin energy bound into the weighted L² moment and operator-pairing integrability conditions needed for the Bet1 boundary-term estimate. Within the Recognition framework it supplies the concrete decay that follows from the eight-tick octave and D = 3 for the Navier-Stokes projection; the module docstring records that all theorems here are proved without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.