IsDivergenceFreeTraj
plain-language theorem explainer
The predicate requires that a map u from real time to full Fourier coefficient states on the 2-torus has vanishing Fourier divergence at every mode and every instant. It is cited by limit-passage arguments that transfer the divergence-free property from Galerkin approximants to the continuum object. The definition is a direct universal quantification over times and modes of the modewise linear constraint.
Claim. A function $u : ℝ → (ℤ² → ℝ²)$ satisfies the divergence-free trajectory condition when $∀ t ∈ ℝ, ∀ k = (k₁, k₂) ∈ ℤ², k₁ u(t,k)₁ + k₂ u(t,k)₂ = 0$.
background
The ContinuumLimit2D module constructs a Lean-checkable pipeline from finite Galerkin truncations of 2D flows on the torus to an infinite Fourier object. FourierState2D is the type of all maps from 2D Fourier modes (integer pairs) to velocity coefficient pairs. divConstraint extracts the Fourier divergence of one coefficient vector at mode k as the real number k₁ v_x + k₂ v_y.
proof idea
The declaration is a definition that directly encodes the universal statement that divConstraint vanishes for every time slice and every mode. No lemmas or tactics are invoked; the body is the primitive predicate itself.
why it matters
The predicate is used by divFree_of_forall to pass the divergence-free property to the limiting trajectory under modewise convergence, by divFreeCoeffBound to build the identification hypothesis, and by rs_implies_global_regularity_2d_divFreeCoeffBound to obtain the regularity conclusion without a separate identification object. It supplies the analytic step that closes the continuum-limit pipeline in the 2D classical bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.