tailFlux
plain-language theorem explainer
The tailFlux definition supplies the explicit boundary term B(r) = -A(r) A'(r) r² for the radial coefficient A in the RM2U reduction of the Navier-Stokes problem. Analysts working on energy identities for ancient solutions cite this when converting the 3D integration-by-parts into a 1D tail condition at infinity. The definition is a direct algebraic transcription of the skew-harmonic gate term with no lemmas applied.
Claim. For real-valued functions $A, A': [1,∞) → ℝ$, the tail flux at radius $r$ is the boundary term $B(r) := -A(r) · (A'(r) · r²)$.
background
In the RM2U.Core module the Navier-Stokes problem is reduced to a 1D radial coefficient problem for a scalar function A(r) at fixed time and spherical direction. The tail-flux term appears in the radial integration-by-parts identity and must vanish at infinity for the coercive L2 bound to hold. The module doc states that this term matches the zeroSkewAtInfinity condition from SkewHarmGate.Radial.
proof idea
This is a one-line definition that directly encodes the boundary term as (-A r) * ((A' r) * (r ^ 2)).
why it matters
This definition is the primitive for all subsequent tail-vanishing arguments in the RM2U layer. It is used to define TailFluxVanish and boundaryTerm, and feeds into coerciveL2Bound_of_tailFluxVanish and bet2_for_galerkin which establish self-falsification for non-vanishing cases. In the Recognition framework it closes the radial energy identity step that replaces the black-box interface, linking the D=3 spatial structure to the integration gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.