IsStokesODETraj
IsStokesODETraj defines the modewise differential form of the linear Stokes equation on Fourier coefficients for 2D velocity fields on the torus. Analysts working on continuum limits of Galerkin schemes or regularity questions for Navier-Stokes cite this predicate when moving from mild to strong formulations. The definition directly encodes the required derivative condition via HasDerivWithinAt on each coefficient trajectory restricted to t ≥ 0.
claimLet ν ∈ ℝ be viscosity and let u : ℝ → (ℤ × ℤ → VelCoeff) be a trajectory of Fourier states. The predicate holds precisely when, for every t ≥ 0 and every mode k ∈ ℤ × ℤ, the map s ↦ u(s)(k) admits derivative −(ν |k|²) u(t)(k) at s = t, where the derivative is taken within the half-line [0, ∞).
background
The module ContinuumLimit2D supplies a Lean-checkable pipeline shape for extracting continuum objects from finite 2D Galerkin truncations. FourierState2D is the type of all sequences of velocity coefficients indexed by Mode2 = ℤ × ℤ; kSq returns the squared wavenumber |k|² that appears in the Fourier Laplacian. The local setting keeps all compactness and identification steps as explicit hypotheses so that later milestones can replace them with proofs.
proof idea
As a definition the body is the predicate itself: universal quantification over t ≥ 0 and k : Mode2 of the HasDerivWithinAt statement for the coefficient map, with the expected linear right-hand side built from ν and kSq. No lemmas or tactics are invoked.
why it matters in Recognition Science
The predicate is applied by the theorem stokesODE, which converts the mild trajectory assumption into the differential form, and by rs_implies_global_regularity_2d_stokesODECoeffBound, which lifts coefficient bounds from the mild to the differential setting. It supplies the analytic identification step inside the 2D fluid bridge of the Recognition framework, keeping the linear evolution separate from nonlinear terms until later milestones.
scope and limits
- Does not assert existence or uniqueness of any trajectory.
- Does not include the nonlinear convective term.
- Does not encode convergence of Galerkin approximations.
- Does not specify initial data or external forcing.
formal statement (Lean)
175def IsStokesODETraj (ν : ℝ) (u : ℝ → FourierState2D) : Prop :=
proof body
Definition body.
176 ∀ t ≥ 0, ∀ k : Mode2,
177 HasDerivWithinAt (fun s : ℝ => (u s) k) (-(ν * kSq k) • (u t) k) (Set.Ici (0 : ℝ)) t
178
179/-!
180## First nonlinear (Duhamel-style) identification: heat evolution + remainder
181
182To start introducing the nonlinear Navier–Stokes term without committing to the full analytic
183infrastructure (time integrals, dominated convergence, etc.), we use a *Duhamel-like remainder*
184term `D(t,k)`:
185
186`u(t,k) = heatFactor(ν,t,k) • u(0,k) + D(t,k)`.
187
188In a future milestone, `D` will be instantiated as the time-integrated nonlinear forcing.
189For now, this already gives a useful “nonlinear-shaped” identity that can be passed to the limit
190under modewise convergence, provided the remainders also converge modewise.
191-/
192
193/-- Duhamel-style (nonlinear) remainder form: `u = heatFactor • u0 + D` (modewise, for `t ≥ 0`). -/