TailFluxInstantiationCert
plain-language theorem explainer
Researchers closing the RM2U self-consistent loop for ancient Navier-Stokes solutions cite this certificate to confirm that the weighted L2 moment on the radial profile A(r) implies both Bet1 integrability and tail flux vanishing. The structure packages four conditions: the moment integrability, half-line Sobolev decay, the implication from moment plus coercive bound to Bet1, and the closure path to TailFluxVanish. It is realized as a sorry stub whose fields are populated by sibling lemmas in the same module.
Claim. A certificate structure asserting: (i) for any radial profile $P$, the weighted $L^2$ moment hypothesis implies integrability of $A(r)^2 r^2$ on $(1,∞)$; (ii) the Sobolev embedding $H^1(1,∞)↪C_0(1,∞)$ holds; (iii) weighted moment, coercive $L^2$ bound and operator pairing integrability imply the alternative Bet1 boundary integrability hypothesis; (iv) the same inputs imply vanishing of the tail flux for $A$ and $A'$; together with a count of remaining sorry statements.
background
The module instantiates the TailFluxVanishImpliesCoerciveHypothesis for concrete Navier-Stokes ancient elements extracted via Galerkin diagonal convergence. WeightedL2Moment encodes the finite-energy condition: $∫_1^∞ A(r)^2 r^2 dr < ∞$, inherited from the $L^2$ bound on the original velocity field via ℓ=2 spherical harmonic projection. SobolevH1HalfLineDecay is the classical 1D embedding: square-integrable $f$ and $f'$ on the half-line imply $f(r)→0$ as $r→∞$. OperatorPairingIntegrable requires that rm2uOp(P)·A·r² lies in L¹(1,∞).
proof idea
This declaration is a sorry stub. The downstream construction tailFluxInstantiationCert populates the fields by direct reference: moment_defined maps the WeightedL2Moment hypothesis to its integrability field, sobolev_decay calls the half-line decay lemma, bet1_from_moment applies bet1_from_weighted_moment, and closure_path applies tailFlux_vanishes_from_weighted_moment.
why it matters
This certificate closes the algebraic chain in the RM2U module by packaging the PDE-level inputs required for rm2u_self_consistent_closure. It feeds the definition tailFluxInstantiationCert, which in turn supports the self-contained closure: weighted moment → TailFluxVanish → CoerciveL2Bound → RM2Closed. In the Recognition framework it instantiates the tail flux vanishing step under D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.