CoerciveL2Bound
plain-language theorem explainer
The CoerciveL2Bound definition packages the two weighted L2 integrability conditions on the radial coefficient A(r) and its derivative for RM2U profiles in the exterior domain. Navier-Stokes analysts working inside the Recognition Science reduction of the Millennium problem cite it as the concrete analytic gate that must be reached to close the tail obstruction. It is introduced as a direct definition that simply asserts membership of A squared and (A') squared times r squared in L1 over (1, infinity).
Claim. For a radial profile $P$ equipped with coefficient functions $A(r)$ and $A'(r)$ on $r>1$, the coercive $L^2$ bound holds when both $A(r)^2$ and $[A'(r)]^2 r^2$ belong to $L^1((1,∞),dr)$.
background
The RM2U.Core module reduces the Navier-Stokes tail/tightness gate to a one-dimensional radial coefficient problem for fixed time and spherical test direction. The structure RM2URadialProfile supplies the abstract profile consisting of the functions A, A', A'' together with the HasDerivAt hypotheses that certify differentiability on the half-line (1,∞).
proof idea
This declaration is a direct definition that packages the two integrability statements. No lemmas are applied; it simply asserts the required membership in the weighted L1 spaces on the exterior interval.
why it matters
CoerciveL2Bound supplies the analytic target used by coerciveL2Bound_of_tailFluxVanish and betInstantiationCert to certify the Galerkin ancient element. It fills the ℓ=2 coefficient integrability slot in the manuscript RM2U obstruction analysis, thereby supporting boundary-term control in the energy identity. The definition therefore links the Navier-Stokes reduction to the broader Recognition forcing chain by furnishing the L2 closure that blocks parasitic growth at infinity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.