pith. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D

show as:
view Lean formalization →

The module supplies the mathematical objects for a truncated Fourier representation of 2D incompressible flow. Researchers working on the Recognition Science classical bridge to fluids cite these definitions when assembling the Galerkin-to-continuum pipeline. All content is definitional; no theorems are stated or proved. The central object is the 2D Fourier mode as an integer wavevector pair.

claimA 2D Fourier mode is a pair of integers $(k_1, k_2) \in \mathbb{Z}^2$. A Galerkin state consists of complex velocity coefficients on a finite truncation of such modes, equipped with a discrete Laplacian, a convection operator, and a right-hand side for the projected Navier-Stokes system, together with a discrete energy functional.

background

This module sits in the ClassicalBridge domain and introduces the basic structures for 2D spectral methods applied to fluid equations. It defines the mode as a wavevector pair, the set of modes under truncation, velocity coefficients, the state space, the squared wavenumber, the discrete Laplacian, the convection operator, the right-hand side for the Galerkin Navier-Stokes system, a discrete energy, and a hypothesis on energy skew-symmetry. The setting is the finite-dimensional projection of the 2D incompressible Navier-Stokes equations onto a Fourier basis, prior to any embedding into LNAL or continuum limits.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions here are imported by the CPM2D module to instantiate the Law of Existence for the Galerkin model, by Simulation2D to define the one-step bridge, by LNALSemantics for encoding, by ContinuumLimit2D for the embedding to infinite coefficients, and by Regularity2D for the top-level composition to a continuum solution. It fills the M1 slot in the fluids pipeline milestones.

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)