stokesMildCoeffBound
plain-language theorem explainer
stokesMildCoeffBound constructs an IdentificationHypothesis for the limit Fourier trajectory by combining the uniform coefficient bound inherited from Galerkin approximants with the assumption that each approximant obeys the linear mild Stokes evolution. Researchers formalizing the 2D Navier-Stokes continuum limit from finite truncations cite it when assembling the identification step of the M5 pipeline. The construction packages the bound from coeff_bound_of_uniformBounds together with the mild-trajectory constructor applied to the given hMild
Claim. Let $H$ be a uniform-bounds hypothesis supplying a family of Galerkin trajectories $u_N$ with global bound $B$, and let $HC$ be the corresponding convergence hypothesis to a limit trajectory $u$. For viscosity parameter $ν$, if every approximant satisfies the mild Stokes relation (after zero extension) $u_N(t,k) = e^{-ν|k|^2 t} u_N(0,k)$, then the limit $u$ satisfies the identification hypothesis: its coefficients remain bounded by $B$ for all $t≥0$ and it obeys the mild Stokes evolution.
background
In the ContinuumLimit2D module (Milestone M5) the goal is to shape a Lean-checkable passage from finite-dimensional Galerkin approximations to a continuum Fourier-state limit for 2D fluids on the torus. UniformBoundsHypothesis encodes a family of trajectories $u_N : ℕ → ℝ → GalerkinState N$ together with a uniform norm bound $B$ that holds for every truncation level and every time $t≥0$. ConvergenceHypothesis adds a candidate limit $u : ℝ → FourierState2D$ together with modewise convergence of the zero-extended Galerkin coefficients to those of $u$ (see the upstream result coeff_bound_of_uniformBounds). IdentificationHypothesis abstracts the target solution concept by requiring that the limit trajectory satisfies a chosen IsSolution predicate.
proof idea
The definition directly constructs the IdentificationHypothesis structure. Its IsSolution predicate is the conjunction of the coefficient bound (∀ t≥0, ∀ k, ‖(u t) k‖ ≤ B) and the IsStokesMildTraj property. The isSolution field is obtained by applying coeff_bound_of_uniformBounds to derive the bound from HC and by applying stokesMild_of_forall to the supplied hMild assumption on the approximants.
why it matters
This definition supplies one concrete way to discharge the IdentificationHypothesis inside the M5 pipeline, combining the inherited linear mild evolution with the uniform bound. It forms part of the Recognition Science bridge from discrete Galerkin structures to continuum limits without introducing axioms. No downstream uses are recorded yet; later milestones are expected to instantiate the nonlinear remainder term D_N inside the same identification structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.