coeffBound
plain-language theorem explainer
coeffBound supplies a minimal IdentificationHypothesis for the 2D continuum limit by declaring that the limit Fourier trajectory satisfies the solution predicate precisely when its coefficients obey the uniform Galerkin bound B for every t ≥ 0 and every mode. Analysts constructing rigorous Galerkin-to-continuum passages for 2D Navier-Stokes on the torus would cite this as the first concrete, Lean-verified identification step. The definition is a one-line wrapper that invokes coeff_bound_of_uniformBounds to populate the isSolution field from the
Claim. Let $H$ be a UniformBoundsHypothesis supplying a family of Galerkin trajectories $u_N$ together with a uniform bound $B$. Let $HC$ be a ConvergenceHypothesis asserting pointwise modewise convergence of the zero-extended approximants to a limit trajectory $u$. Then coeffBound$(H,HC)$ is the IdentificationHypothesis whose solution predicate asserts that $u$ satisfies $||(u(t))_k|| ≤ B$ for all $t ≥ 0$ and all modes $k$.
background
UniformBoundsHypothesis packages a family of finite-dimensional Galerkin trajectories $u_N : ℕ → ℝ → GalerkinState N$ together with a single real $B ≥ 0$ such that $||u_N N t|| ≤ B$ for every truncation level $N$ and every $t ≥ 0$. ConvergenceHypothesis augments this with a candidate limit map $u : ℝ → FourierState2D$ and the statement that, for each fixed $t$ and mode $k$, the sequence of zero-extended coefficients converges to $(u t) k$ in the reals. IdentificationHypothesis then records an abstract solution concept IsSolution together with the claim that the limit $u$ meets it. The module ContinuumLimit2D (Milestone M5) assembles these objects to make the dependency graph of the Galerkin-to-continuum pipeline explicit while keeping analytic compactness and identification steps as named hypotheses rather than axioms.
proof idea
The definition is a one-line wrapper. It sets the IsSolution field of IdentificationHypothesis to the predicate that every coefficient of the limit trajectory lies inside the closed ball of radius $B$, then discharges the isSolution obligation by direct appeal to the already-proved theorem coeff_bound_of_uniformBounds (which itself follows from closedness of the closed ball under pointwise limits).
why it matters
This definition supplies the first concrete, checkable identification step inside the M5 pipeline that converts a family of Galerkin approximations into a candidate continuum Fourier trajectory. It sits immediately downstream of ConvergenceHypothesis and UniformBoundsHypothesis and is intended to be strengthened later when a concrete PDE solution concept replaces the present minimal bound predicate. No downstream declarations yet consume it; the declaration therefore functions as a scaffold placeholder whose parent theorems will appear once the full identification chain is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.