divConstraint
plain-language theorem explainer
The divConstraint function encodes the Fourier-space divergence constraint for a single 2D mode and its velocity coefficient vector as their dot product. Researchers establishing rigorous passage from Galerkin truncations to continuum Fourier states in incompressible flow would cite this definition when showing that divergence-free conditions survive the limit. It is realized as a direct linear combination with no auxiliary lemmas.
Claim. For a Fourier mode $k = (k_1, k_2) = (k_1, k_2) ∈ ℤ²$ and velocity coefficient vector $v = (v_1, v_2) ∈ ℝ²$, the divergence constraint is given by $k_1 v_1 + k_2 v_2$.
background
The ContinuumLimit2D module defines objects for a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to a continuum Fourier state, packaging analytic compactness steps as explicit hypotheses. A Mode2 is a pair of integers representing a 2D Fourier wavevector. A VelCoeff is the two-component real vector of Fourier velocity amplitudes at that mode.
proof idea
The definition is a direct one-line expression that casts the integer mode components to reals, multiplies each by the corresponding velocity component, and sums the results.
why it matters
This definition supplies the primitive for the Fourier-side divergence-free predicates IsDivergenceFree and IsDivergenceFreeTraj. It is invoked in divConstraint_eq_zero_of_forall and divFree_of_forall, which establish that the constraint passes to the continuum limit under uniform bounds and convergence hypotheses. It thereby supports the classical bridge to fluid equations by making the incompressibility condition explicit in the Fourier basis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.