weightedL2Moment_of_projection
plain-language theorem explainer
The spherical projection of a finite-energy velocity field onto the ℓ=2 harmonic immediately supplies the weighted L² moment on the radial profile A(r). Analysts of ancient Navier-Stokes solutions cite this bridge to pass from the global L² bound to the integrability condition required for the Bet1 hypothesis. The proof is a direct one-line construction that copies the projection_bound field into the WeightedL2Moment structure.
Claim. Let $P$ be an RM2U radial profile. If $P$ admits a spherical projection (i.e., the ℓ=2 coefficient satisfies $∫_1^∞ [A(r)]^2 r^2 dr < ∞$ via Parseval), then $P$ satisfies the weighted L² moment hypothesis $∫_1^∞ [A(r)]^2 r^2 dr < ∞$.
background
The RM2URadialProfile is an abstract structure carrying a radial function $A : ℝ → ℝ$ together with its first and second derivatives $A'$ and $A''$, each equipped with HasDerivAt witnesses on $(1, ∞)$ (from Core). SphericalProjection $P$ is a structure asserting that the total energy is positive and that the ℓ=2 projection satisfies the L² integrability $∫_1^∞ A(r)^2 r^2 dr < ∞$; this follows from the finite-energy condition on the full velocity field $u$ via spherical harmonic decomposition and Parseval's identity on the sphere. WeightedL2Moment $P$ is the proposition that the same integral is finite, serving as the hypothesis needed for operator pairing integrability and tail flux vanishing in the RM2U closure. This declaration sits in the TailFluxInstantiation module, which connects Galerkin-extracted ancient elements to the Bet1 integrability conditions.
proof idea
The proof is a one-line wrapper that constructs the WeightedL2Moment structure by supplying the projection_bound field from the given SphericalProjection hypothesis.
why it matters
This result feeds the GalerkinAncientElement structure in the BetInstantiation module, which packages the data for ancient NS elements at finite truncation level. It closes one link in the chain from the energy inequality through spherical projection to the weighted L² moment required for the tail flux vanishing hypothesis. In the Recognition Science setting it supports the instantiation of the coercive hypothesis for the Navier-Stokes ancient solution problem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.