IndisputableMonolith.NavierStokes.SkewHarmGate
SkewHarmGate supplies lemmas on derivative rules for powers and products together with radial integral identities for skew functions. Researchers working on the RM2U energy estimates in Navier-Stokes would cite it to reduce tail-flux boundary terms to integrability conditions. The module proceeds by direct differentiation lemmas followed by integral reductions under radial symmetry.
claimThe module establishes derivative identities $\frac{d}{dr}(r^2)=2r$ and product rules, together with the radial skew integral identity that reduces the tail flux at infinity to the pair of integrability conditions $\int_R^\infty |B(r)|dr<\infty$ and $\int_R^\infty |B'(r)|dr<\infty$.
background
The module sits inside the NavierStokes section and imports only Mathlib for real analysis. It supplies the analytic tools required by the RM2U package for handling boundary terms that arise when the energy identity is integrated to infinity. The downstream EnergyIdentity file explicitly invokes the central lemma of this module to convert the statement “tail flux vanishes at infinity” into two concrete integrability obligations on the boundary term and its derivative.
proof idea
The module is a collection of lemmas rather than a single theorem. It first records the derivative of $r^2$ and the product rule for $r^2$ times a radial function, then assembles these into the integral radial skew identity, and finally extracts the zero-at-infinity statement under the stated integrability hypotheses. Each step is a direct application of the fundamental theorem of calculus in radial coordinates.
why it matters in Recognition Science
The module is the immediate supplier of the lemma used by IndisputableMonolith.NavierStokes.RM2U.EnergyIdentity, which the downstream documentation describes as the algebraic spine of Option A. By discharging the tail-flux vanishing step it closes one of the two integrability obligations needed for the energy identity in the Navier-Stokes setting.
scope and limits
- Does not prove existence or uniqueness for the Navier-Stokes equations.
- Does not invoke the Recognition forcing chain, J-uniqueness, or phi-ladder.
- Does not treat non-radial or time-dependent boundary terms.
- Does not supply numerical verification or simulation data.