rm2uOp
plain-language theorem explainer
The definition supplies the explicit second-order radial differential operator for the ℓ=2 mode in the reduced Navier-Stokes model. Researchers analyzing energy estimates in the Recognition Science framework cite it to rewrite boundary terms and derive coercive bounds. It is introduced as a direct algebraic expression without additional lemmas or reductions.
Claim. Let $A$ be a twice-differentiable radial function. The operator at radius $r > 0$ is given by $-A''(r) - (2/r) A'(r) + (6/r^2) A(r)$.
background
The module provides the algebraic spine for Option A in the Navier-Stokes analysis. It reduces tail-flux vanishing at infinity to two integrability obligations on the boundary term and its derivative, using the skew-harmonic gate. The radial profile packages the function $A$ together with its first and second derivatives for energy estimates on $(1,∞)$. Upstream results include the ledger factorization that calibrates the J-cost and the phi-forcing structures that enforce the D=3 reduction and the eight-tick octave.
proof idea
The definition is a direct transcription of the differential expression. It is applied verbatim in the algebraic identity that rewrites the derivative of the boundary term as the operator pairing minus the coercive nonnegative terms.
why it matters
This operator definition underpins the energy identity theorems in the same module, including the integral identity on finite windows and the coercive L2 bound obtained once the tail flux vanishes. It advances the Recognition Science program by supplying a concrete algebraic handle on the ℓ=2 mode, consistent with the phi-ladder and the forcing chain from T5 to T8. It leaves open the incorporation of full time-dependent forcing into the hypothesis interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.