module module high

`IndisputableMonolith.NavierStokes.Galerkin3D`

The module defines the 3D Galerkin discretization for the Navier-Stokes equations. It introduces modes, velocity coefficients, states, wavenumbers, Laplacian and convection operators, discrete energy, and enstrophy. These objects support equicontinuity arguments in the Fourier basis. The module is purely definitional and supplies the concrete 3D objects used by the equicontinuity results.

claimLet $M_3$ be the set of 3D modes, $c: M_3 → ℝ^3$ the velocity coefficients, $S$ the Galerkin state, $k^2$ the squared wavenumber, $Δc$ the Laplacian coefficients, $C(c)$ the convection operator, $E(c)$ the discrete energy, and $Ω(c)$ the spectral enstrophy.

background

The module works in the setting of incompressible Navier-Stokes on the 3D torus using spectral Galerkin truncation. It defines Mode3 as the discrete wavevectors, VelCoeff3 as the coefficients in the Fourier expansion of the velocity field, GalerkinState3 as the finite collection of these coefficients, kSq3 as the squared wavevector norm, laplacianCoeff3 as the viscous multiplier, ConvectionOp3 as the projected nonlinear term, galerkinNSRHS3 as the right-hand side, discreteEnergy3 as the squared L2 norm of the velocity, EnergySkewHypothesis3 as the skew-symmetry identity preserving energy, and spectralEnstrophy as the enstrophy expressed in spectral space. These rest on the inner-product and calculus structures imported from Mathlib.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions supply the concrete 3D objects required by the GalerkinEquicontinuity module, which establishes the Lipschitz constant for the Fourier coefficients and applies the McShane upper extension to obtain dense Lipschitz extension. This supplies the equicontinuity needed to pass to the limit in the Galerkin approximations.

scope and limits

Does not prove existence or regularity of solutions.
Does not include time evolution or forcing terms.
Does not address the continuous Navier-Stokes problem.
Does not treat boundary conditions or pressure projection.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NavierStokes.GalerkinEquicontinuity module_import

declarations in this module (20)

abbrev Mode3 L30
def modes3 L32
abbrev VelCoeff3 L37
abbrev GalerkinState3 L39
def kSq3 L44
lemma kSq3_nonneg L47
def laplacianCoeff3 L50
def ConvectionOp3 L53
def galerkinNSRHS3 L56
def discreteEnergy3 L62
structure EnergySkewHypothesis3 L65
def spectralEnstrophy L73
lemma spectralEnstrophy_nonneg L76
theorem inviscid_energy_deriv_zero3 L85
lemma laplacianCoeff3_inner_self_nonpos L104
theorem viscous_energy_deriv3 L121
theorem viscous_energy_nonpos3 L140
theorem viscous_energy_antitone3 L147
theorem viscous_energy_bound3 L157
theorem viscous_norm_bound3 L165