coeffAt_add
plain-language theorem explainer
The additivity property for coefficient extraction from summed Galerkin states in truncated 2D Fourier representations holds for any truncation level N. Researchers passing finite Galerkin approximations to continuum Fourier states cite this when confirming that the zero-extension embedding is linear. The proof splits on membership of the queried mode in the finite truncation set and simplifies directly from the extraction definition.
Claim. Let $N$ be a natural number. For Galerkin states $u,v$ (coefficients on modes up to $N$), a mode $k=(k_1,k_2)$, and component index $j$, the extraction map satisfies $c(u+v,k,j)=c(u,k,j)+c(v,k,j)$, where $c$ returns the stored value if $k$ lies in the truncation window and zero otherwise.
background
The module ContinuumLimit2D constructs a Lean-checked pipeline from finite Galerkin truncations of 2D velocity fields on the torus to an infinite Fourier coefficient state. GalerkinState N is the Euclidean space of real coefficients indexed by the finite set of modes (pairs of integers with max-norm at most N) times the two velocity components. The extraction function coeffAt returns the stored coefficient when the mode belongs to that finite set and zero otherwise, thereby embedding the truncated state into the full FourierState2D (functions from all modes to 2-vectors). This extraction is the basic building block for the zero-extension map whose linearity properties are recorded in the same file.
proof idea
The term proof opens classical logic, performs case distinction on whether the mode k belongs to the finite set modes N, and applies simplification in each branch using the definition of coeffAt (which branches on the same membership test). No external lemmas beyond the definition and the case split are required.
why it matters
The result is invoked directly by the downstream lemma extendByZero_add, which establishes that zero-extension preserves addition and is therefore a linear map from GalerkinState N into FourierState2D. This linearity step is required before any compactness or identification arguments can pass identities from the discrete Galerkin trajectories to the continuum limit object. Within the Recognition Science classical bridge it supplies the algebraic foundation for the M5 pipeline that converts truncated approximations into objects suitable for later analytic limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.