boundaryTerm
plain-language theorem explainer
boundaryTerm associates to each RM2URadialProfile its boundary term function, obtained by feeding the profile's coefficient and derivative into the tail-flux expression. Analysts deriving the RM2U energy identity for Navier-Stokes would reference this definition when specializing the radial integration-by-parts to a concrete profile. The definition is a direct one-line wrapper around tailFlux.
Claim. For a radial profile $P$ with coefficient function $A(r)$ and derivative $A'(r)$, the boundary term is the map $rmapsto -A(r)cdot A'(r)cdot r^2$.
background
RM2URadialProfile is a structure holding a radial coefficient function $A$ together with its first and second derivatives $A'$ and $A''$, plus proofs that $A'$ is the derivative of $A$ and $A''$ of $A'$ on the interval $(1,infty)$. The module supplies the specification layer for the RM2U tail/tightness gate, expressing the obstruction through a boundary term that appears in the radial integration-by-parts identity. tailFlux supplies the explicit formula $B(r):=(-A(r))cdot(A'(r)cdot r^2)$, which matches the zero-skew-at-infinity condition from SkewHarmGate.
proof idea
one-line wrapper that applies tailFlux to the profile's A and A' fields.
why it matters
This definition supplies the concrete boundary term needed to state the vanishing condition TailFluxVanish for any profile. It sits inside the spec layer that reduces the Navier-Stokes RM2U obstruction to a one-dimensional radial problem, as described in navier-dec-12-rewrite.tex. The construction reuses the tail-flux identity already proved in the SkewHarmGate component of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.