Bet1BoundaryIntegrableHypothesisAlt
plain-language theorem explainer
Alternate Bet-1 boundary integrability hypothesis for an RM2U radial profile P requires integrability of the weighted boundary term (-A)A'x² over (1,∞), integrability of the rm2uOp pairing with A x², and the coercive L² bound on P. Researchers closing the RM2U pipeline for Galerkin ancient elements in the Recognition Science Navier-Stokes analysis cite this interface. The declaration is a structure definition that packages the three conditions to enable conversion to the original Bet-1 hypothesis.
Claim. Let $P$ be an RM2URadialProfile with radial coefficient $A$ and derivative $A'$. The alternate Bet-1 hypothesis holds if the boundary integrand satisfies $A(x) A'(x) x^2$ integrable over $(1,∞)$, the pairing of the RM2U radial operator with $A(x) x^2$ is integrable over $(1,∞)$, and the coercive $L^2$ bound on $P$ holds.
background
The RM2U.NonParasitism module isolates non-parasitism as the vanishing of the tail-flux boundary term at infinity for the ℓ=2 coefficient. An RM2URadialProfile is the structure supplying a function $A:ℝ→ℝ$ together with its first and second derivatives $A'$ and $A''$ that satisfy the HasDerivAt conditions on the half-line $(1,∞)$. The CoerciveL2Bound imported from Core asserts integrability of both $A^2$ and $(A')^2 r^2$ over $(1,∞)$. The rm2uOp is the explicit radial operator $rm2uOp(P,r) = -A''(r) - (2/r)A'(r) + (6/r^2)A(r)$, obtained from the algebraic identity that rewrites the Bet-1 boundary-term derivative.
proof idea
This is a structure definition with three fields. The first field asserts integrability of the boundary integrand $(-P.A x)(P.A' x)x^2$ over $(1,∞)$. The second field asserts integrability of the rm2uOp pairing with $P.A x^2$. The third field requires the CoerciveL2Bound on $P$. No lemmas or tactics are invoked; the declaration directly packages the three conditions.
why it matters
The structure supplies the alternate Bet-1 interface used by bet1_of_bet1Alt to recover the original Bet1BoundaryIntegrableHypothesis and by BetInstantiationCert to certify the full RM2U pipeline for any Galerkin ancient element. It converts weighted $L^2$ moments and coercive bounds into the algebraic conditions needed for tail-flux vanishing. In the Recognition Science setting it supports closure of the RM2U to RM2 step while leaving the core non-parasitism hypothesis as the remaining gate, consistent with the D=3 spatial dimensions and the integration-gap unit A=1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.