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

extendByZero

show as:
view Lean formalization →

extendByZero embeds a finite Galerkin velocity state into the infinite Fourier coefficient space by zero-padding all modes outside the truncation window. Analysts constructing 2D Navier-Stokes continuum limits cite this map when lifting discrete trajectories to candidate limit objects in Fourier space. The definition is realized directly as a pointwise function that assembles each mode's velocity vector from the two component values supplied by coeffAt.

claimFor a Galerkin state $u$ (an element of the Euclidean space over the finite set of modes $N$ crossed with two velocity components), the zero-extension map sends $u$ to the function $u^0 : Mode_2 → ℝ^2$ defined by $u^0(k) = (c_0(k), c_1(k))$, where each $c_j(k)$ equals the stored coefficient of $u$ when $k$ belongs to the truncation and equals zero otherwise.

background

The ContinuumLimit2D module supplies the Lean-checked pipeline shape for passing from finite-dimensional 2D Galerkin approximations on the torus to a continuum Fourier limit object. GalerkinState N is the Euclidean space of real coefficients indexed by the finite set of modes up to N together with the two velocity components. FourierState2D is the type of all functions from Mode2 (all integer pairs) to velocity coefficients, representing the full infinite expansion of a 2D velocity field.

proof idea

The definition is a direct lambda expression that, for each mode k, builds the 2-vector of coefficients by invoking coeffAt on the two Fin 2 indices. No lemmas are applied; the construction is purely by cases on membership in the finite mode set, with the zero branch supplied by the else clause of coeffAt.

why it matters in Recognition Science

This definition supplies the canonical embedding required by the ConvergenceHypothesis structure, which packages a candidate limit trajectory together with the pointwise convergence statement from the approximants. It is invoked in the construction of the limit object inside continuum_limit_exists and in the coefficient-bound transfer theorems that close the uniform-bounds hypothesis. Within the Recognition Science framework it realizes the concrete embedding step of the M5 milestone that makes the dependency graph for the continuum limit explicit.

scope and limits

formal statement (Lean)

  55noncomputable def extendByZero {N : ℕ} (u : GalerkinState N) : FourierState2D :=

proof body

Definition body.

  56  fun k =>
  57    -- Build a 2-vector coefficient from its two components.
  58    !₂[coeffAt u k ⟨0, by decide⟩, coeffAt u k ⟨1, by decide⟩]
  59
  60/-!
  61## Linearity of the zero-extension embedding
  62
  63We will eventually want to pass (linear) identities from Galerkin trajectories to limits.
  64For that, it is useful to record that `extendByZero` is a linear map.
  65-/
  66

used by (40)

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

… and 10 more

depends on (16)

Lean names referenced from this declaration's body.