rm2u_self_consistent_closure
plain-language theorem explainer
The theorem shows that an RM2U radial profile satisfying the weighted L2 moment integrability and the energy forcing hypothesis yields RM2 closure. Navier-Stokes analysts working on ancient solutions via spherical-harmonic reduction would cite it to confirm the reduced model is self-contained. The proof is a one-line application of the coercive L2 bound implication to the closedness predicate.
Claim. Let $P$ be an RM2U radial profile. If the weighted $L^2$ moment condition holds, i.e., $A(r)^2 r^2$ is integrable on $(1,∞)$, and the energy forcing hypothesis is given (supplying tail-flux vanishing together with the coercive $L^2$ bound), then RM2Closed($P.A$), equivalently the log-critical moment of $A$ is finite.
background
The module instantiates tail-flux vanishing for ancient Navier-Stokes elements obtained by Galerkin diagonal extraction. WeightedL2Moment is the structure asserting ∫₁^∞ A(r)² r² dr < ∞, inherited from the finite-energy condition on the original velocity field via ℓ=2 projection. EnergyForcingHypothesis packages two facts: tail-flux vanishing (from 1D Sobolev embedding on A·r and A'·r) and the map from that vanishing to the coercive L2 bound via the energy identity.
proof idea
One-line wrapper that applies rm2Closed_of_coerciveL2Bound to the coercive bound extracted by feeding the tail-flux vanishing field of the energy forcing hypothesis into its coercive_from_tfv component.
why it matters
The result closes the self-contained RM2U loop: weighted moment implies tail-flux vanish, which yields coercive L2 bound, which yields RM2Closed. It supplies the concrete instantiation of TailFluxVanishImpliesCoerciveHypothesis inside the Galerkin setting for ancient solutions. In the Recognition framework it supports the reduction of the D=3 problem to a 1D radial profile whose mass scaling follows the phi-ladder. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.