SphericalProjection
plain-language theorem explainer
The SphericalProjection structure packages the finite-energy condition on the ℓ=2 radial profile A(r) for Navier-Stokes ancient elements, requiring positive total energy together with integrability of A(r)² r² over (1, ∞). Researchers working on the RM2U reduction cite it when converting Galerkin energy bounds into the WeightedL2Moment hypothesis via spherical-harmonic Parseval. The declaration is a bare structure definition with no proof steps.
Claim. A structure SphericalProjection(P) for an RM2U radial profile P consists of a positive real total energy E > 0 and the integrability condition ∫₁^∞ [A(r)]² r² dr < ∞, where A is the ℓ=2 coefficient of the velocity field.
background
The RM2U Tail Flux Instantiation module extracts an ℓ=2 radial profile A(r) from Galerkin approximations of ancient Navier-Stokes solutions. RM2URadialProfile supplies the functions A, A', A'' together with their derivative relations on (1, ∞). WeightedL2Moment then records the single integrability assertion ∫₁^∞ A(r)² r² dr < ∞, which is inherited from the L² norm of the full velocity field u via the spherical Parseval identity ∫ |u|² d³x = Σ ∫ |A_{ℓm}(r)|² r² dr.
proof idea
The declaration is a structure definition that directly records the total energy and the projection bound as fields. No lemmas are applied; the structure serves as a packaging device for the integrability condition that is later converted to WeightedL2Moment via the one-line wrapper weightedL2Moment_of_projection.
why it matters
SphericalProjection supplies the concrete data that instantiates WeightedL2Moment inside GalerkinAncientElement, thereby closing the chain from uniform energy bounds through spherical projection to the Bet1 integrability conditions required for tail-flux vanishing. It supports the RM2U reduction at D=3 and feeds the downstream operator-pairing and coercive estimates that connect to the phi-ladder and eight-tick octave machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.