divFreeCoeffBound
plain-language theorem explainer
This definition packages an IdentificationHypothesis for a limit Fourier trajectory from a uniform-bounds hypothesis on Galerkin approximants, a convergence hypothesis, and the assumption that every approximant satisfies the Fourier divergence constraint. Researchers formalizing the Galerkin-to-continuum passage for 2D incompressible flow would cite it to close the identification step in the M5 pipeline. The construction directly assembles the required IsSolution predicate by invoking the two derived facts coeff_bound_of_uniformBounds and div_
Claim. Given a uniform-bounds hypothesis $H$ on a family of Galerkin trajectories $u_N$ and a convergence hypothesis $HC$ to a limit trajectory $u$, together with the assumption that every approximant satisfies the Fourier divergence constraint, the limit trajectory satisfies the identification hypothesis whose solution predicate asserts that the trajectory is bounded by the uniform constant and divergence-free.
background
UniformBoundsHypothesis supplies a family of Galerkin trajectories $u_N$ together with a uniform bound $B$ that holds for all truncation levels $N$ and all $t≥0$. ConvergenceHypothesis supplies a candidate limit trajectory $u:ℝ→FourierState2D$ together with pointwise convergence of the zero-extended Galerkin coefficients. IdentificationHypothesis packages an abstract solution concept IsSolution together with a proof that the limit satisfies it. divConstraint is the real-valued Fourier-side divergence operator on a single mode; extendByZero embeds a truncated Galerkin state into the full Fourier state by zero-padding higher modes. The module ContinuumLimit2D defines a Lean-checkable pipeline shape that keeps the analytic compactness and identification steps explicit as hypotheses so that later milestones can replace them with proofs.
proof idea
One-line wrapper that constructs the IdentificationHypothesis record. It sets IsSolution to the conjunction of the uniform bound predicate and the IsDivergenceFreeTraj predicate. The bound component is obtained by applying coeff_bound_of_uniformBounds to HC. The divergence-free component is obtained by applying divConstraint_eq_zero_of_forall to HC and the supplied hDF assumption that every approximant satisfies the constraint.
why it matters
The definition supplies the concrete identification constructor required by the ContinuumLimit2D pipeline (Milestone M5) for passing from finite-dimensional Galerkin approximations to a continuum Fourier object. It directly implements the doc-comment claim that the coefficient bound follows from UniformBoundsHypothesis plus convergence while the divergence-free property follows from the approximant assumption. No downstream uses are recorded yet; the declaration therefore sits at the boundary between hypothesis and theorem in the classical-bridge fluid module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.