divConstraint_eq_zero_of_forall
plain-language theorem explainer
If every Galerkin approximant satisfies the Fourier divergence constraint at a fixed time and mode, the limiting Fourier coefficient satisfies it as well. Researchers passing spectral Galerkin schemes to continuum 2D Navier-Stokes solutions cite this when verifying that divergence-free properties survive the limit. The proof composes the continuous divergence map with the given modewise convergence and applies uniqueness of limits in the reals.
Claim. Let a family of Galerkin trajectories be uniformly bounded and converge modewise (after zero extension) to a limit trajectory $u$. Fix time $t$ and Fourier mode $k$. If the Fourier divergence $k_1 v_0 + k_2 v_1$ vanishes for every approximant coefficient vector $v$ at this $t,k$, then the same linear combination vanishes for the limit coefficient $u(t)_k$.
background
The module packages a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to a candidate continuum Fourier trajectory. UniformBoundsHypothesis supplies a family of truncated trajectories $u_N$ together with a uniform norm bound $B$ that holds for all truncation levels $N$ and all $t≥0$. ConvergenceHypothesis supplies the candidate limit $u$ and the assumption that the zero-extended Galerkin coefficients converge pointwise to those of $u$ at every mode. The Fourier divergence operator is the linear functional $k_1 v_0 + k_2 v_1$ on velocity coefficients; its continuity is recorded in the sibling lemma divConstraint_continuous.
proof idea
The tactic proof first obtains a convergent sequence of divergence values by composing the continuous map $v ↦ divConstraint k v$ with the modewise convergence hypothesis. It then rewrites the sequence as the constant zero sequence via the forall assumption and invokes tendsto_nhds_unique to conclude that the limit divergence must be zero.
why it matters
The result supplies the divergence-free half of the identification hypothesis used in divFreeCoeffBound and is invoked directly by divFree_of_forall to obtain IsDivergenceFreeTraj for the limit trajectory. It therefore closes one analytic step inside the M5 milestone that converts discrete Galerkin data into a continuum object while preserving the divergence constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.