TailFluxVanish
plain-language theorem explainer
The declaration defines the property that the radial tail-flux term for an RM2U profile vanishes at spatial infinity. Navier-Stokes analysts working on Galerkin approximations cite it to close energy estimates in the RM2U pipeline. The definition directly encodes the limit condition on the tailFlux boundary term using Mathlib's Tendsto notation.
Claim. Let $A, A' : ℝ → ℝ$. The tail flux vanishes at infinity when the limit as $r → ∞$ of $(-A(r)) · (A'(r) · r^2)$ equals zero.
background
In the RM2U.Core module the radial coefficient $A(r)$ for $r ≥ 1$ is the ℓ=2 sector of a fixed-time slice in the Navier-Stokes problem. The tail-flux term is given by tailFlux A A' r := (-A r) · (A' r · r²), which matches the boundary contribution in the radial integration-by-parts identity. This setup forms the spec layer for the tail/tightness gate, ensuring finite energy bounds without parasitic contributions at infinity. Upstream results supply the active-edge count A from IntegrationGap and Masses.Anchor, which encodes the φ-power balance at D = 3, together with the Actualization operator that maps configurations to realized states.
proof idea
This is a direct definition that restates the vanishing condition as Tendsto (fun r => tailFlux A A' r) atTop (𝓝 0). No lemmas are invoked; the declaration serves as an abbreviation for the limit property used in downstream theorems.
why it matters
The definition is invoked in rm2u_pipeline_complete and BetInstantiationCert, which certify that any Galerkin ancient element satisfies both RM2Closed and TailFluxVanish. It fills the tail/tightness gate in the navier-dec-12-rewrite.tex by guaranteeing the boundary term vanishes, thereby preventing energy leakage at infinity. Within the Recognition Science framework it supports the D = 3 spatial dimensions and the eight-tick octave by controlling radial profiles. It touches the open question of whether every ancient solution obeys the vanishing condition without further hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.