tailFluxInstantiationCert
plain-language theorem explainer
This declaration supplies the TailFluxInstantiationCert structure that wires the weighted L2 moment integrability, Sobolev half-line decay, Bet1 boundary integrability, and tail-flux vanishing path for radial profiles in the RM2U Navier-Stokes setting. Researchers closing energy estimates for ancient solutions via Galerkin extraction would cite it to obtain the coercive L2 bound from the moment hypothesis. The construction is a direct structure instantiation that reads the A2r2 integrability from the hypothesis and delegates the remaining three
Claim. The certificate asserts: for every radial profile $P$ with WeightedL2Moment, the integral $∫_1^∞ (A(r))^2 r^2 dr$ is finite; Sobolev $H^1$ half-line decay holds for pairs of functions $f,f'$; Bet1 boundary integrability follows from WeightedL2Moment, CoerciveL2Bound and OperatorPairingIntegrable; and the path from those three hypotheses to tail-flux vanishing is given by the weighted-moment lemma.
background
The RM2U Tail Flux Instantiation module connects Galerkin diagonal convergence to the Bet1 integrability conditions needed for the coercive L2 bound. WeightedL2Moment P encodes the finite integral $∫_1^∞ (P.A r)^2 r^2 dr$, which arises from the energy inequality $∫ |∇u|^2 ≤ C$ after projection onto the ℓ=2 spherical harmonic and Parseval on $S^2$. The module docstring states that energy decay of ancient elements gives $A(r) = O(r^{-3/2})$, hence $A(r)^2 r^2 = O(r^{-1})$ which is integrable on $(1,∞)$. Upstream results include the CPM2D bridge that packages Galerkin defect and energy-gap meanings, and the IntegrationGap.A that supplies the active-edge count used in the forcing chain.
proof idea
The definition is a structure literal. The moment_defined field is the one-line wrapper fun _ hW => hW.hA2r2 that extracts the integrability directly from the hypothesis. The sobolev_decay field applies the lemma sobolev_H1_half_line_decay. The bet1_from_moment field applies bet1_from_weighted_moment and the closure_path field applies tailFlux_vanishes_from_weighted_moment, each passing the profile together with the moment, coercivity and pairing hypotheses.
why it matters
This certificate discharges the concrete inputs required by rm2u_self_consistent_closure, which shows that energy forcing plus the weighted moment yields RM2Closed. It supplies the tail-flux vanishing step that precedes the coercive L2 bound inside the RM2U closure for ancient Navier-Stokes elements. In the Recognition framework it instantiates the hypothesis_interface that links the eight-tick octave and D=3 spatial projection to the Bet1 integrability condition. No downstream uses are recorded; the open question is whether the Sobolev decay can be strengthened beyond the half-line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.