IsDivergenceFree
plain-language theorem explainer
Defines a predicate on Fourier coefficient states for 2D velocity fields that requires the divergence constraint to vanish at every mode. Researchers building incompressible flow models from Galerkin truncations to continuum Fourier states would cite this when enforcing the continuity equation in spectral space. The definition is a direct universal quantification over Mode2 using the divConstraint on each coefficient.
Claim. A Fourier state $u : Mode2 → VelCoeff$ satisfies the divergence-free condition when $∀ k ∈ ℤ×ℤ$, $k_1 · u(k)_0 + k_2 · u(k)_1 = 0$, where the left-hand side is the Fourier divergence for that mode.
background
The ContinuumLimit2D module (Milestone M5) constructs a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to an infinite Fourier coefficient state on the torus 𝕋². FourierState2D is the type Mode2 → VelCoeff, with Mode2 the integer pairs (k₁, k₂) indexing Fourier modes. The sibling definition divConstraint(k, v) returns the real number (k.1 : ℝ) * v(0) + (k.2 : ℝ) * v(1), giving the Fourier-side divergence for a single mode velocity coefficient.
proof idea
One-line definition that directly encodes the modewise condition: universal quantification over k : Mode2 requires divConstraint k (u k) = 0. No lemmas or tactics are applied; the body is the explicit predicate.
why it matters
This predicate supplies the incompressibility constraint inside the Fourier representation for the continuum-limit pipeline of 2D fluids. It supports the M5 milestone by giving an explicit, checkable condition on the infinite state obtained by zero-extension of Galerkin truncations. No downstream theorems currently depend on it, so it remains available for later integration into time-dependent or compactness arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.