divConstraint
plain-language theorem explainer
The Fourier divergence constraint for a single 2D mode k and velocity coefficient v equals the dot product of the wavevector with the velocity vector. Workers on the 2D Galerkin-to-continuum limit pipeline cite it when enforcing incompressibility modewise before passing to the limit object. It is introduced by a direct algebraic definition with no lemmas.
Claim. For a Fourier mode $(k_1,k_2)∈ℤ²$ and velocity coefficient vector $v=(v_1,v_2)∈ℝ²$, the divergence constraint is the scalar $k_1 v_1 + k_2 v_2$.
background
The ContinuumLimit2D module constructs a Lean-checkable pipeline from finite 2D Galerkin truncations to an infinite Fourier coefficient state, keeping all analytic steps as explicit hypotheses. Mode2 is the type of a 2D Fourier mode (k₁,k₂). VelCoeff is the type of a velocity Fourier coefficient, an element of EuclideanSpace ℝ (Fin 2). The upstream divergence definition from DiscreteNSOperator supplies the corresponding discrete operator on a lattice; the present expression is its Fourier-space counterpart for a single mode.
proof idea
Direct definition. The body is the explicit linear combination (k.1 : ℝ) * v 0 + (k.2 : ℝ) * v 1 with no tactic steps or lemmas applied.
why it matters
This supplies the primitive expression for the Fourier-side divergence-free predicate. It is invoked to define IsDivergenceFree and IsDivergenceFreeTraj, which are then used in divFreeCoeffBound and the regularity theorem rs_implies_global_regularity_2d_divFreeCoeffBound. It therefore occupies the incompressibility slot inside the M5 continuum-limit pipeline. In the Recognition framework it closes one link in the bridge from discrete Navier-Stokes operators to continuum objects while leaving compactness and identification steps as named hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.