IndisputableMonolith.NavierStokes.RM2U.EnergyIdentity
This module defines the RM2U ℓ=2 radial operator and its associated energy identity for the time-slice radial coefficient problem. Researchers on the RM2U closure for ancient Navier-Stokes solutions cite it when establishing integrability and coercivity. It assembles the operator definition plus supporting identities from the Core spec and SkewHarmGate cancellations.
claimThe ℓ=2 radial operator rm2uOp acts on the scalar coefficient A(r) for r ≥ 1; its energy identity equates ∫ (rm2uOp A) ⋅ (energy integrand) dr to boundary terms obtained from integration by parts, with no time derivative or forcing present.
background
RM2U.Core supplies the Lean-side spec for the tail/tightness gate as a 1D radial coefficient problem for A(r) at fixed t and spherical direction b. SkewHarmGate supplies the skew/self-adjoint cancellations from integration by parts together with harmonic/affine tail mode bookkeeping. The module packages the ℓ=2 case in the time-slice setting of navier-dec-12-rewrite.tex.
proof idea
This is a definition module, no proofs. It collects the operator rm2uOp together with concrete energy identities (bet1_boundaryTerm_deriv_integrand_eq, integral_rm2uOp_mul_energy_identity) that rest on the cancellation lemmas imported from SkewHarmGate.
why it matters in Recognition Science
The module feeds BetInstantiation (connecting weighted L² moments to RM2U closure), NonParasitism (isolating the hard hypothesis), ProjectedPDE (evolution hypothesis interface), and TailFluxInstantiation (coercive hypothesis from tail flux vanishing). It supplies the energy identity step required by the RM2U pipeline.
scope and limits
- Does not incorporate time derivatives or external forcing.
- Does not formalize the full 3D Navier-Stokes projection.
- Does not discharge the non-parasitism hypothesis.
- Does not treat the complete time-dependent evolution.