RM2URadialProfile
plain-language theorem explainer
RM2URadialProfile packages a twice-differentiable scalar function A(r) for r > 1 together with its first and second derivatives under explicit differentiability conditions. Navier-Stokes researchers analyzing the RM2U tail obstruction in Galerkin approximations cite this structure to supply the radial coefficient data for energy identities and flux bounds. The declaration is a direct structure record with no proof obligations or computational content.
Claim. A structure consisting of functions $A, A', A'' : (1,∞) → ℝ$ such that $A$ is differentiable on $(1,∞)$ with derivative $A'$, and $A'$ is differentiable on $(1,∞)$ with derivative $A''$.
background
The RM2U.Core module supplies the specification layer for the RM2U tail/tightness gate in navier-dec-12-rewrite.tex, reduced to a 1D radial coefficient problem. Fix a time slice and spherical direction parameter b; the resulting scalar A(r) for r ≥ 1 carries the obstruction through the boundary term (-A(r)) · (A'(r) · r²) as r → ∞. All analytic identities are later proved in RM2U.EnergyIdentity by reusing SkewHarmGate.
proof idea
This is a structure definition that directly records the three functions and the two HasDerivAt hypotheses on the interval (1, ∞). No lemmas are applied; the record simply bundles the data required by downstream constructions such as boundaryTerm and CoerciveL2Bound.
why it matters
The structure supplies the profile type instantiated inside GalerkinAncientElement and used by bet2_for_galerkin, which shows that non-vanishing tail flux violates the energy bound. It also supports boundaryTerm and CoerciveL2Bound, closing the spec layer for the RM2U obstruction. In the Recognition framework this fills the radial-coefficient slot needed to enforce finite-energy conditions on the ℓ=2 mode.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.