divConstraint
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assert that any velocity field satisfies the constraint.
- Does not incorporate time dependence.
- Does not address spatial discretization or lattice effects.
- Does not prove continuity or other analytic properties.
formal statement (Lean)
127noncomputable def divConstraint (k : Mode2) (v : VelCoeff) : ℝ :=
proof body
Definition body.
128 (k.1 : ℝ) * v (0 : Fin 2) + (k.2 : ℝ) * v (1 : Fin 2)
129
130/-- Fourier-side divergence-free predicate (modewise, at a fixed time). -/