extendByZero_add
plain-language theorem explainer
The zero-extension map from truncated Galerkin velocity states to full Fourier coefficient fields preserves vector addition. Researchers constructing the explicit embedding step in the 2D Galerkin-to-continuum pipeline cite this result when verifying linearity of the truncation operator. The proof is a direct term-mode reduction that applies functional and componentwise extensionality followed by simplification against the additivity of the coefficient extractor.
Claim. Let $E_N$ be the zero-extension operator sending a Galerkin state with $N$ modes to a full Fourier coefficient field in two dimensions. Then $E_N(u+v)=E_N(u)+E_N(v)$ for all Galerkin states $u,v$.
background
The ContinuumLimit2D module supplies the explicit objects needed for a Lean-checkable passage from finite Galerkin approximations to continuum Fourier states. GalerkinState N is the Euclidean space of real coefficients indexed by the truncated modes up to N together with the two velocity components. The noncomputable map extendByZero embeds such a state into the full FourierState2D by placing the extracted coefficients at the retained modes and zero elsewhere, using the auxiliary extractor coeffAt for each component.
proof idea
The proof is a one-line term-mode wrapper. It applies funext over modes, then ext over the two components, dispatches the finite cases, and simplifies using the definitions of extendByZero together with the upstream lemma coeffAt_add.
why it matters
This additivity is invoked directly to supply the map_add' field of extendByZeroLinear, which is then used in the differentiation result galerkinNS_hasDerivAt_extendByZero_mode. It therefore discharges one of the explicit linearity hypotheses required by the M5 milestone pipeline that converts truncated Galerkin states into continuum objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.