IsStokesMildTraj
plain-language theorem explainer
IsStokesMildTraj encodes the explicit mild solution of the linear Stokes equation on the 2D torus by requiring that every Fourier mode coefficient at time t equals its initial value multiplied by the heat decay factor exp(-ν |k|^2 t). Researchers formalizing the continuum limit of Galerkin approximations for 2D incompressible flow cite this predicate when passing linear evolution from finite truncations to the full Fourier state. The definition consists of a direct universal quantification over t ≥ 0 and all modes that records the closed-form,
Claim. A trajectory $u : [0,∞) → (ℤ² → VelCoeff)$ satisfies the mild Stokes condition for viscosity ν when $u(t,k) = e^{-ν |k|^2 t} · u(0,k)$ for every $t ≥ 0$ and every mode $k ∈ ℤ²$.
background
The ContinuumLimit2D module constructs an explicit Lean pipeline from finite Galerkin truncations to a continuum Fourier object at milestone M5. FourierState2D is the type of all functions from Mode2 (ℤ × ℤ) to velocity coefficients, obtained by extending truncated states by zero outside the truncation window. heatFactor(ν,t,k) is defined as Real.exp(-ν · |k|^2 · t), the exact multiplier solving the decoupled linear heat equation on each mode. The module keeps analytic compactness steps as named hypotheses rather than axioms so that later milestones can discharge them.
proof idea
The declaration is a direct definition whose body is the universal statement ∀ t ≥ 0, ∀ k : Mode2, (u t) k = (heatFactor ν t k) • (u 0) k. No lemmas or tactics are invoked; the predicate simply records the closed-form solution of the linear system.
why it matters
IsStokesMildTraj supplies the linear building block for IsNSDuhamelTraj (the Duhamel remainder form) and for the differential form derived in stokesODE. It is invoked inside the identification constructors stokesMildCoeffBound and the regularity theorems rs_implies_global_regularity_2d_stokesMildCoeffBound and rs_implies_global_regularity_2d_stokesODECoeffBound, which link the Recognition Science forcing chain to classical 2D Navier-Stokes regularity questions. The predicate therefore closes one step in the explicit-dependence graph that replaces truncation hypotheses with proved limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.