pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

GalerkinState

show as:
view Lean formalization →

GalerkinState N supplies the finite-dimensional vector space of velocity coefficients on the truncated Fourier modes for a 2D incompressible Navier-Stokes model on the torus. Researchers working on discrete fluid approximations cite it as the concrete state space on which the projected dynamics and energy identities are defined. The declaration is a direct type abbreviation that identifies the space with Euclidean space indexed by the product of the mode set and the two velocity components.

claimFor truncation level $N$, let $M_N$ be the finite set of truncated modes. The Galerkin state space is the Euclidean space $E = (M_N) × {0,1} → ℝ$ equipped with the standard inner product, whose elements are the pairs of velocity coefficients for each mode and each spatial component.

background

The module sets up a finite-dimensional Fourier-mode truncated model for 2D incompressible Navier-Stokes on the torus as Milestone M1. The goal is a concrete discrete state space together with the basic algebraic energy identity for the inviscid case, before any continuum limit. The upstream definition modes N produces the finite set of truncated modes as the product of intervals from -N to N in each wave-number direction. The second upstream import supplies the continuum-bridge identification of Laplacian action used later for the heat kernel.

proof idea

This is a one-line type abbreviation that directly constructs the Euclidean space over the index set (modes N) × Fin 2.

why it matters in Recognition Science

GalerkinState supplies the state space used by forty downstream declarations in ContinuumLimit2D, including coeffAt, extendByZero, duhamelRemainderOfGalerkin and the associated measurability and Duhamel-integral theorems. It realizes the finite-dimensional truncation step that precedes the continuum limit arguments and supports the algebraic energy conservation identity required for the inviscid case. The construction sits inside the ClassicalBridge domain that connects discrete Recognition Science structures to continuum fluid models.

scope and limits

formal statement (Lean)

  59abbrev GalerkinState (N : ℕ) : Type :=

proof body

Definition body.

  60  EuclideanSpace ℝ ((modes N) × Fin 2)
  61
  62/-!
  63## Discrete dynamics
  64-/
  65
  66/-- Squared wave number \( |k|^2 \) as a real number. -/

used by (40)

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

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.