pith. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D

show as:
view Lean formalization →

This module supplies the finite-dimensional 2D Fourier-mode truncation of the incompressible Navier-Stokes equations that serves as the base layer (M1) for the LNAL fluids pipeline. Workers on the Recognition Science continuum bridge cite it for the explicit definitions of Mode2, GalerkinState, and the associated operators. The module contains only definitions and named hypotheses; no theorems are proved.

claimA 2D Fourier mode is a pair of integers $(k_1,k_2)$. The Galerkin state is a finite collection of velocity coefficients indexed by such modes, equipped with the discrete Laplacian coefficient, convection operator, right-hand side of the projected Navier-Stokes equation, and a discrete energy functional together with the EnergySkewHypothesis.

background

The module sits at the root of the ClassicalBridge.Fluids hierarchy and introduces the objects needed for a finite-dimensional 2D Galerkin model. Mode2 is defined as a 2D Fourier mode $(k_1,k_2)$, with derived quantities kSq, laplacianCoeff, ConvectionOp, galerkinNSRHS, discreteEnergy, and the EnergySkewHypothesis. These structures encode the projection of the 2D incompressible Navier-Stokes equations onto a finite set of Fourier modes, providing the discrete state space used by all downstream milestones.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the five downstream files that complete the 2D pipeline: LNALSemantics (M2), Simulation2D (M3), CPM2D (M4), ContinuumLimit2D (M5), and Regularity2D (M6). Regularity2D composes all prior stages to obtain an abstract existence statement for a continuum solution; the present module supplies the concrete finite-dimensional starting objects required by that composition.

scope and limits

used by (5)

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

declarations in this module (19)