coeffAt_smul
plain-language theorem explainer
The lemma shows that coefficient extraction from a Galerkin state commutes with scalar multiplication. Researchers building the 2D continuum limit pipeline cite it to confirm linearity of the mode embedding before compactness steps. The proof splits on membership of the mode in the truncation set and simplifies using the coefficient definition.
Claim. For scalar $c$, Galerkin state $u$ truncated at level $N$, Fourier mode $k$, and component index $j$, the extracted coefficient satisfies $coeffAt(c·u,k,j)=c·coeffAt(u,k,j)$.
background
The ContinuumLimit2D module outlines a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to a continuum limit object, defining coefficient states and embeddings while leaving analytic compactness steps as explicit hypotheses. coeffAt extracts the velocity component at a given mode, returning zero when the mode lies outside the finite truncation set. GalerkinState is the Euclidean space of coefficients over the product of the mode set and the two components; Mode2 denotes integer pairs for 2D Fourier modes; modes N collects those with max norm at most N.
proof idea
The term proof invokes classical logic then cases on whether mode k belongs to modes N. Each branch applies simp to the definition of coeffAt, which itself branches on the same membership test, and the equality follows immediately.
why it matters
It supports extendByZero_smul, which shows zero-extension preserves scalar multiplication. This advances the M5 milestone by making the dependency graph explicit for the passage from Galerkin states to continuum objects. Within the Recognition framework it secures linearity at the coefficient extraction step prior to any identification or compactness arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.