IndisputableMonolith.NavierStokes.SkewHarmGate
This module supplies derivative rules and integral identities for radial skew-harmonic functions to control tail fluxes at infinity. Researchers deriving energy identities in the Navier-Stokes setting cite it when converting boundary terms into integrability conditions. The structure chains basic differentiation lemmas into radial integral reductions via direct application of Mathlib analysis primitives.
claimThe module establishes derivative facts such as $d/dr(r^2)=2r$ and the integral identity $I = 0$ for radial skew functions under decay, together with the implication that integrability of the boundary term and its derivative forces the tail flux to vanish at infinity.
background
The module operates inside the Navier-Stokes subdomain of Recognition Science, where energy estimates require control of surface terms at spatial infinity. It introduces radial skew identities that reduce flux integrals to statements about integrability of a function and its radial derivative. The single import is Mathlib, which supplies the underlying real-analysis primitives for derivatives and improper integrals.
proof idea
The module first records elementary derivative facts for powers and products, then assembles them into the central radial skew integral identity. Subsequent lemmas apply the identity to obtain vanishing at infinity once integrability of the integrand and its derivative is assumed.
why it matters in Recognition Science
The module supplies the reduction step that turns the tail-flux boundary term into two integrability obligations. It is invoked directly by IndisputableMonolith.NavierStokes.RM2U.EnergyIdentity, which describes itself as the algebraic spine of Option A and uses these lemmas to close the energy identity argument.
scope and limits
- Does not address non-radial or time-dependent cases.
- Does not prove existence or uniqueness for Navier-Stokes solutions.
- Does not supply numerical bounds or explicit decay rates.
- Limits applicability to functions whose radial derivative is integrable at infinity.