tailFluxVanish
plain-language theorem explainer
tailFluxVanish supplies a one-line abbreviation that applies the tail-flux vanishing predicate to the coefficient and derivative of an RM2URadialProfile. Analysts working on the RM2U closure for the Navier-Stokes equations cite it when they need to state the boundary term condition without repeating the underlying Tendsto expression. The definition is a direct delegation to TailFluxVanish on the profile fields.
Claim. Let $P$ be a radial profile with coefficient function $A(r)$ and derivative $A'(r)$ for $r>1$. Then tailFluxVanish$(P)$ holds precisely when the boundary term satisfies $$(-A(r)) (A'(r) r^2) → 0$$ as $r→∞$.
background
RM2U.Core encodes the tail/tightness gate of the RM2U problem as a one-dimensional radial coefficient problem for fixed time and test direction. An RM2URadialProfile is the structure carrying the triple of functions $A$, $A'$, $A''$ together with the HasDerivAt hypotheses that guarantee differentiability on $(1,∞)$. TailFluxVanish itself is the predicate asserting that the scalar boundary term tends to zero at infinity under the natural topology atTop.
proof idea
one-line wrapper that applies TailFluxVanish to the A and A' fields of the supplied RM2URadialProfile.
why it matters
The definition supplies the interface used by NonParasitismHypothesis and by the theorem tailFlux_vanishes_for_galerkin that closes the ℓ=2 sector for Galerkin ancient elements. It therefore participates in the inheritance route to RM2Closed. Within the Recognition framework the construction reduces the D=3 spatial problem to a radial tail-flux condition that must be controlled to obtain the eight-tick octave dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.