ConvergenceHypothesis
plain-language theorem explainer
A structure packaging a candidate continuum Fourier trajectory u together with its modewise convergence from zero-extended Galerkin approximants under a uniform bound hypothesis H. Researchers closing the compactness step in the Recognition Science fluid pipeline cite it when moving from finite truncations to the infinite coefficient state. The declaration is a plain structure definition whose fields directly record the limit map and the Tendsto condition at each mode.
Claim. Let $H$ be a UniformBoundsHypothesis supplying Galerkin trajectories $u_N$ and a uniform bound $B$. A ConvergenceHypothesis for $H$ consists of a trajectory $u : ℝ → (Mode2 → VelCoeff)$ such that for every time $t$ and mode $k$, the sequence of zero-extended coefficients extendByZero$(u_N(N,t))_k$ converges to $u(t)_k$ as $N → ∞$.
background
The ContinuumLimit2D module at milestone M5 defines objects for passing from finite-dimensional 2D Galerkin approximations to a continuum Fourier limit while keeping analytic steps explicit as hypotheses. UniformBoundsHypothesis records a family of truncated trajectories $u_N : ℕ → ℝ →$ GalerkinState N together with a global bound $B$ that holds uniformly in $N$ and for all $t ≥ 0$. FourierState2D is the type of all mode-indexed velocity coefficients on the torus; extendByZero lifts each truncated state into this space by zeroing coefficients outside the truncation window.
proof idea
The declaration is a structure definition. It introduces the field u for the candidate limit trajectory and the field converges that asserts pointwise Tendsto convergence of the extended Galerkin coefficients to the limit coefficients.
why it matters
ConvergenceHypothesis supplies the central hypothesis used by coeffBound and divFreeCoeffBound to build IdentificationHypothesis, which is required by the existence theorem continuum_limit_exists. It encodes the compactness step that closes the passage from Galerkin truncations to the continuum Fourier state in two dimensions, consistent with the module's goal of making the dependency graph explicit for later replacement of hypotheses by proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.