pith. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D

show as:
view Lean formalization →

The module defines the 2D Fourier mode truncation and associated operators for a finite-dimensional Galerkin model of the Navier-Stokes equations. Researchers building the Recognition Science fluids pipeline cite it as the discrete base layer (M1). It consists entirely of type and operator definitions with no theorems or proofs.

claimThe 2D Galerkin model is constructed from modes $m=(k_1,k_2)∈ℤ²$, finite truncations, velocity coefficients $u_m$, the state space, wavenumber-squared terms $k²$, Laplacian coefficients, the convection operator, the projected right-hand side, and the discrete energy functional.

background

This module introduces the finite-dimensional 2D Galerkin discretization in the ClassicalBridge.Fluids domain. Core definitions include Mode2 as a pair of integers representing a 2D Fourier mode, modeTrunc for selecting finite subsets, the set of active modes, VelCoeff for velocity coefficients on those modes, GalerkinState as the full coefficient vector, kSq for the squared wavenumber, laplacianCoeff, ConvectionOp for the projected nonlinear term, galerkinNSRHS for the right-hand side of the truncated equations, discreteEnergy, and EnergySkewHypothesis. The module imports Mathlib components for inner-product spaces, calculus, integers, finsets, and tactics to support these constructions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the base discrete 2D Galerkin model (Milestone M1) that is imported by LNALSemantics for spatial encoding, by Simulation2D for the one-step bridge, by CPM2D for the CPM core instantiation with explicit hypotheses, by ContinuumLimit2D for the embedding of truncated coefficients into the infinite Fourier state, and by Regularity2D for the top-level composition theorem that concludes an abstract continuum solution exists.

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)