divFreeCoeffBound
plain-language theorem explainer
The definition constructs an IdentificationHypothesis for a limit Fourier trajectory by inheriting a uniform coefficient bound from Galerkin approximants and preserving the Fourier divergence constraint under pointwise convergence. Researchers formalizing the continuum limit of 2D Navier-Stokes Galerkin schemes would cite it to close the identification step from discrete to continuum objects. It is realized as a record definition that applies the coefficient bound lemma and the divergence preservation lemma inside the solution predicate.
Claim. Let $H$ be a uniform bounds hypothesis on a family of Galerkin trajectories and $HC$ the associated convergence hypothesis to a limit trajectory $u$. If every approximant satisfies the Fourier divergence constraint at each mode and time, then the limit satisfies the identification hypothesis: $u$ is bounded by the uniform constant and divergence-free.
background
The module ContinuumLimit2D defines a Lean-checkable pipeline shape for passing from finite-dimensional 2D Galerkin approximations to a continuum Fourier limit object, keeping analytic compactness and identification steps as explicit hypotheses rather than axioms. UniformBoundsHypothesis packages a family of Galerkin trajectories $uN$ together with a global bound $B$ such that each approximant stays inside the ball of radius $B$. ConvergenceHypothesis supplies a candidate limit trajectory $u$ together with pointwise mode-by-mode convergence of the zero-extended Galerkin coefficients. IdentificationHypothesis then asserts that this limit satisfies a chosen solution concept, here instantiated as boundedness plus the Fourier divergence-free condition.
proof idea
The definition builds the IdentificationHypothesis record directly. IsSolution is set to the conjunction of the uniform bound predicate and IsDivergenceFreeTraj. The isSolution field is proved by a two-step refinement: the bound direction invokes coeff_bound_of_uniformBounds on the convergence hypothesis, while the divergence direction invokes divConstraint_eq_zero_of_forall on the supplied approximant constraint hDF.
why it matters
This definition supplies the concrete constructor for the identification step inside the M5 milestone of the continuum-limit pipeline. It depends on the two derived facts coeff_bound_of_uniformBounds and divConstraint_eq_zero_of_forall that sit inside the ConvergenceHypothesis namespace. The construction keeps the classical bridge explicit so that later milestones can replace the hypotheses with proofs; it does not yet connect to the core Recognition Science forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.