coeff_bound_of_uniformBounds
plain-language theorem explainer
If Galerkin approximants satisfy a uniform bound B in the discrete norm for all truncation levels N and times t ≥ 0, then the modewise limits of their zero-extended coefficients satisfy the same bound. Researchers constructing continuum limits from Galerkin approximations in 2D fluids would cite this result to establish the identification hypothesis. The argument proceeds by showing each approximant coefficient lies in the closed ball of radius B, passing to the limit via closedness of that ball under the given pointwise convergence.
Claim. Let $H$ be a uniform bounds hypothesis for a family of Galerkin trajectories $u_N$ with bound $B$, and let $HC$ be a convergence hypothesis from those approximants to a limit trajectory $u$. Then for all $t ≥ 0$ and all modes $k$, $‖(u(t))_k‖ ≤ B$.
background
In the ContinuumLimit2D module the pipeline from finite Galerkin approximations to a continuum Fourier state is formalized by packaging analytic steps as explicit hypotheses. UniformBoundsHypothesis packages a family of Galerkin trajectories uN together with a uniform bound B such that for all N and t ≥ 0 the discrete norm satisfies ‖uN N t‖ ≤ B; this would arise in a full proof from energy estimates or compactness arguments. ConvergenceHypothesis assumes a candidate limit u : ℝ → FourierState2D together with modewise convergence of the zero-extended approximants: for each t and k, the sequence (extendByZero (H.uN N t)) k tends to (u t) k as N → ∞.
proof idea
The proof fixes t ≥ 0 and mode k, then shows that for every N the extended coefficient (extendByZero (H.uN N t)) k lies in the closed ball of radius B centered at zero. This follows from norm_extendByZero_le combined with the uniform bound H.bound N t ht. The set of points in the closed ball is closed, so the limit under the assumed convergence HC.converges t k must also lie in the ball. Extracting the distance from the membership statement yields the desired norm bound.
why it matters
This theorem supplies the coefficient bound component of the IdentificationHypothesis used by coeffBound, divFreeCoeffBound, nsDuhamelCoeffBound and their variants; those constructors in turn feed the existence statement continuum_limit_exists. It therefore closes one concrete step in the M5 milestone pipeline that turns Galerkin approximants into a continuum limit object. Within the Recognition Science framework the result sits inside the ClassicalBridge layer that bridges discrete algebraic structures to continuum fluid models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.