coeffAt
The definition extracts the j-th velocity component from a truncated 2D Galerkin state at Fourier mode k, returning zero when k falls outside the finite truncation set modes N. Researchers formalizing the passage from Galerkin approximations to continuum Fourier states cite this selector when building the zero-extension map and its linearity properties. The definition proceeds by a direct membership test on the finite mode set followed by a subtype cast or the constant zero.
claimLet $u$ be a Galerkin state truncated at level $N$, let $k$ be a 2D Fourier mode, and let $j$ index a velocity component. The extracted coefficient equals the value of $u$ at the corresponding index when $k$ belongs to the truncated mode set, and equals zero otherwise.
background
The ContinuumLimit2D module constructs a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to infinite Fourier coefficient states. A GalerkinState N is the Euclidean space of real coefficients indexed by the product of the finite mode set (modes N) and the two components Fin 2. Mode2 is the type of integer pairs (k1,k2), while modes N is the Finset of all such pairs with max(|k1|,|k2|) <= N.
proof idea
The definition performs a case split on membership of k in modes N. When the test succeeds it casts k to the subtype (modes N) and reads the corresponding entry from the Euclidean space u; otherwise it returns the real constant zero. No auxiliary lemmas are invoked beyond the membership predicate.
why it matters in Recognition Science
This selector supplies the basic access function for the zero-extension embedding extendByZero, which feeds the linearity lemmas coeffAt_add and coeffAt_smul together with the norm bound norm_extendByZero_le. It therefore occupies the first concrete step in the M5 milestone that makes the Galerkin-to-continuum dependency graph explicit. The construction keeps truncation predicates visible so that later milestones can replace analytic hypotheses with proofs.
scope and limits
- Does not prove convergence of any Galerkin sequence to a continuum solution.
- Does not encode the Navier-Stokes equations or convection terms.
- Does not incorporate Recognition Science constants or the phi-ladder.
- Does not address existence or uniqueness questions in the continuum limit.
formal statement (Lean)
46noncomputable def coeffAt {N : ℕ} (u : GalerkinState N) (k : Mode2) (j : Fin 2) : ℝ :=
proof body
Definition body.
47 if hk : k ∈ modes N then
48 -- `k` as an element of the finite index type `(modes N)`
49 let k' : (modes N) := ⟨k, hk⟩
50 u (k', j)
51 else
52 0
53
54/-- Extend a truncated Galerkin state by zero to a full Fourier coefficient state. -/