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

FourierState2D

show as:
view Lean formalization →

FourierState2D is the type of maps assigning a 2-vector velocity coefficient to every integer pair mode on the torus. Analysts formalizing the continuum limit of 2D Galerkin approximations cite it as the codomain for pointwise convergence statements. The declaration is a direct one-line abbreviation that composes the upstream Mode2 and VelCoeff types.

claimLet $M = ℤ × ℤ$ be the set of 2D Fourier modes and let $V = ℝ²$ be the space of velocity coefficients. The full Fourier state space is the function space $M → V$.

background

Mode2 is the type of 2D Fourier modes, defined as pairs of integers $(k_1, k_2)$. VelCoeff is the type of velocity Fourier coefficients at a single mode, realized as the Euclidean space $ℝ²$. GalerkinState N is the corresponding finite-dimensional object whose domain is the finite set of modes with max-norm at most N. The module ContinuumLimit2D constructs a Lean-checkable pipeline from families of such truncated states to a candidate continuum object; the present abbreviation supplies the infinite target space in which the limit trajectory lives.

proof idea

One-line abbreviation that directly equates FourierState2D to the function type Mode2 → VelCoeff, inheriting the definitions of both components from the Galerkin2D module.

why it matters in Recognition Science

The type supplies the codomain for the limit map u : ℝ → FourierState2D inside the theorem continuum_limit_exists and the structure ConvergenceHypothesis. It thereby completes the identification step that turns uniform bounds on Galerkin approximants into a candidate continuum Fourier trajectory. In the Recognition framework this definition marks the interface between the finite Galerkin truncation (T7 octave structure) and the full Fourier representation needed for the 2D continuum limit.

scope and limits

formal statement (Lean)

  37abbrev FourierState2D : Type := Mode2 → VelCoeff

proof body

Definition body.

  38
  39/-!
  40## Embedding: GalerkinState N → FourierState2D
  41
  42We extend a truncated state by zero outside the truncation window.
  43-/
  44
  45/-- Read a single component coefficient at mode `k` (zero if `k ∉ modes N`). -/

used by (40)

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

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.