nsDuhamelCoeffBound
nsDuhamelCoeffBound assembles an IdentificationHypothesis for the 2D Navier-Stokes continuum limit by pairing the inherited uniform bound on Fourier coefficients with a Duhamel-style remainder identity. Analysts working on rigorous passage from Galerkin truncations to weak solutions would cite it once pointwise convergence of the remainder terms is granted. The definition proceeds by direct construction of the IsSolution predicate, invoking the coefficient bound lemma and the nsDuhamel_of_forall constructor supplied by the convergence package.
claimLet $H$ be a uniform bounds hypothesis on a family of Galerkin trajectories $u_N$ with global bound $B$, and let $HC$ be the associated convergence hypothesis to a limit trajectory $u$. Given viscosity parameter $ν$, remainder families $D_N$ and $D$, pointwise convergence $D_N(t,k)→D(t,k)$ for each mode $k$, and the identity that each approximant satisfies $u_N(t,k)=e^{-ν|k|^2 t}u_N(0,k)+D_N(t,k)$ after zero extension, the pair $(H,HC)$ determines an IdentificationHypothesis asserting that $u$ satisfies the chosen 2D Navier-Stokes solution concept.
background
The module ContinuumLimit2D (Milestone M5) supplies a Lean-checkable pipeline shape for passing from finite-dimensional 2D Galerkin approximations on the torus to a continuum Fourier-state limit. It defines the relevant objects—an infinite Fourier coefficient state—and packages the analytic compactness and identification steps as explicit hypotheses rather than axioms or sorries, so that later milestones can replace them with proofs. FourierState2D is the type of maps from Mode2 to VelCoeff; extendByZero embeds a truncated GalerkinState N into this full state by zero-padding outside the truncation window. UniformBoundsHypothesis records a family of Galerkin trajectories uN together with a uniform bound B such that ||uN N t|| ≤ B for all N and t ≥ 0. ConvergenceHypothesis augments this with a candidate limit trajectory u and the assumption that the zero-extended coefficients converge pointwise to those of u. IdentificationHypothesis then packages an abstract solution predicate IsSolution together with the assertion that the limit satisfies it.
proof idea
The definition is a direct constructor. It sets the IsSolution field to the conjunction of two properties: the uniform coefficient bound, obtained by applying ConvergenceHypothesis.coeff_bound_of_uniformBounds to the supplied HC, and the IsNSDuhamelTraj predicate, obtained by applying ConvergenceHypothesis.nsDuhamel_of_forall to the convergence hypothesis, the viscosity ν, the remainder families D_N and D, and the two supplied hypotheses hD and hId. No further tactics are required beyond the two applications.
why it matters in Recognition Science
This definition closes the identification step inside the M5 pipeline for continuum limits of 2D fluids, making the dependency graph explicit so that later work can discharge the ConvergenceHypothesis via compactness. It feeds directly into downstream constructions that will instantiate the nonlinear remainder D as a concrete time-integrated forcing term. In the broader Recognition Science setting it supports the classical bridge by keeping the analytic hypotheses visible rather than hidden, thereby preserving the forcing-chain structure from T0 through the eight-tick octave while the fluid equations are recovered as a derived limit.
scope and limits
- Does not prove existence of the limit trajectory u.
- Does not instantiate the nonlinear remainder D as a specific integral operator.
- Does not establish convergence of the Duhamel integrals themselves.
- Does not address the three-dimensional case or boundary conditions.
- Does not discharge the ConvergenceHypothesis via any compactness argument.
formal statement (Lean)
1451def nsDuhamelCoeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1452 (D_N : ℕ → ℝ → FourierState2D) (D : ℝ → FourierState2D)
1453 (hD : ∀ t : ℝ, ∀ k : Mode2,
1454 Tendsto (fun N : ℕ => (D_N N t) k) atTop (nhds ((D t) k)))
1455 (hId :
1456 ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1457 (extendByZero (H.uN N t) k) =
1458 (heatFactor ν t k) • (extendByZero (H.uN N 0) k) + (D_N N t) k) :
1459 IdentificationHypothesis HC :=
proof body
Definition body.
1460 { IsSolution := fun u =>
1461 (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsNSDuhamelTraj ν D u
1462 isSolution := by
1463 refine ⟨?_, ?_⟩
1464 · intro t ht k
1465 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1466 · exact ConvergenceHypothesis.nsDuhamel_of_forall (HC := HC) (ν := ν) (D_N := D_N) (D := D) hD hId }
1467
1468/-- Identification constructor: coefficient bound + Duhamel remainder identity where the remainder is
1469defined as a **kernel integral** of a forcing term, and convergence of the kernel integrals is
1470packaged via `DuhamelKernelDominatedConvergenceAt`. -/
depends on (31)
-
H -
of -
coeff_bound_of_uniformBounds -
ConvergenceHypothesis -
DuhamelKernelDominatedConvergenceAt -
extendByZero -
FourierState2D -
heatFactor -
IdentificationHypothesis -
IsNSDuhamelTraj -
nsDuhamel_of_forall -
UniformBoundsHypothesis -
Mode2 -
kernel -
H -
isSolution -
isSolution -
via -
of -
identity -
is -
of -
as -
is -
of -
is -
kernel -
of -
is -
and