OperatorPairingIntegrable
plain-language theorem explainer
Operator pairing integrability defines the condition that the product of the RM2U radial operator applied to a profile, the amplitude function A, and r squared remains integrable over (1, infinity) with respect to Lebesgue measure. Analysts working on regularity questions for ancient Navier-Stokes solutions or on closing Bet1 boundary estimates in the Recognition Science Navier-Stokes module would reference this property. The definition is a direct statement of L1 membership whose supporting analysis decomposes the operator into three terms and
Claim. Let $P$ be a radial profile with amplitude function $A(r)$. Operator pairing integrability holds when the map $rmapsto rm2uOp(P,r)cdot A(r)cdot r^2$ lies in $L^1((1,infty))$, where $rm2uOp(P,r)=-A''(r)-(2/r)A'(r)+(6/r^2)A(r)$.
background
The RM2U Tail Flux Instantiation module connects Galerkin-extracted ancient Navier-Stokes elements to the integrability conditions required for the Bet1 boundary term. A radial profile consists of a function $A$ together with its first and second derivatives $A'$ and $A''$ that satisfy the differentiability conditions on $(1,infty)$. The rm2uOp is the second-order differential expression that algebraically rewrites the Bet-1 boundary term derivative as $-A''-(2/r)A'+(6/r^2)A$ for $rneq0$ (from the EnergyIdentity module). Upstream, the AncientEnergyDecayFull structure supplies the pointwise decay bounds on $A$, $A'$, and $A''$ that make the integrability hold, while the module docstring records that the projection from the full velocity field preserves the $L^2$ bounds needed for the radial profile.
proof idea
The declaration is a direct definition of the integrability predicate. The accompanying docstring sketches the classical Hölder analysis: expand the product into the three terms $-A''Ar^2$, $-2A'Ar$, and $6A^2$; bound the middle term by Cauchy-Schwarz or AM-GM using the coercive $L^2$ bound; then apply additivity of integrable sets three times.
why it matters
This definition supplies the integrability link used to construct Bet1 boundary integrability from a weighted $L^2$ moment and a coercive bound in bet1_from_weighted_moment, and thereby to obtain tail-flux vanishing. It supports the TailFluxInstantiationCert and the self-consistent RM2U closure for ancient elements. In the Recognition Science framework it discharges the classical PDE step of the TailFluxVanishImpliesCoerciveHypothesis for three-dimensional flows, completing the chain from Galerkin extraction to RM2Closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.