coeffBound
This definition builds an IdentificationHypothesis for the 2D continuum limit by declaring that the limit Fourier trajectory satisfies the solution predicate precisely when its coefficients remain bounded by the uniform Galerkin bound B for all t ≥ 0. Analysts constructing rigorous Galerkin-to-continuum passages for 2D Navier-Stokes on the torus would cite it as the minimal provable identification step. The construction is a direct one-line wrapper that invokes the coefficient bound theorem obtained from uniform bounds plus modewise convergence
claimGiven a uniform bounds hypothesis $H$ supplying Galerkin trajectories $u_N$ with global bound $B$ and a convergence hypothesis $HC$ producing limit trajectory $u$, the identification hypothesis asserts that $u$ satisfies the solution concept defined by the predicate $IsSolution(u) := (∀ t ≥ 0, ∀ k ∈ ℤ², ‖(u t)_k‖ ≤ B)$.
background
The ContinuumLimit2D module sets up 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 $u_N$ together with a uniform bound $B$ that holds for all truncation levels $N$ and all $t ≥ 0$; the bound is expected to arise from discrete energy or enstrophy estimates. ConvergenceHypothesis supplies a candidate limit trajectory $u$ together with pointwise mode-by-mode convergence of the zero-extended Galerkin coefficients to those of $u$. IdentificationHypothesis then abstracts the target solution concept as a predicate $IsSolution$ on trajectories together with a proof that the limit satisfies it.
proof idea
One-line wrapper that applies ConvergenceHypothesis.coeff_bound_of_uniformBounds to establish the coefficient bound inside the IdentificationHypothesis. The wrapper directly sets the IsSolution field to the predicate ∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B and obtains the required isSolution proof by specializing the upstream bound theorem at each fixed t and mode.
why it matters in Recognition Science
This definition supplies the first concrete identification step inside the M5 milestone pipeline for the classical bridge to fluids. It demonstrates that uniform bounds plus modewise convergence already deliver a basic boundedness property without further analytic input, serving as a minimal placeholder that later milestones can strengthen by replacing the abstract IsSolution predicate with a full PDE verification. The module documentation notes that the dependency graph is kept explicit precisely so that such hypotheses can be discharged progressively.
scope and limits
- Does not derive the uniform bound B from energy or enstrophy estimates.
- Does not verify that the limit satisfies the Navier-Stokes equation.
- Does not establish existence of the limit trajectory itself.
- Does not address three-dimensional or non-periodic domains.
formal statement (Lean)
1400def coeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) :
1401 IdentificationHypothesis HC :=
proof body
Definition body.
1402 { IsSolution := fun u => ∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B
1403 isSolution := by
1404 intro t ht k
1405 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k) }
1406
1407/-- Identification constructor: coefficient bound + divergence-free (Fourier-side).
1408
1409The coefficient bound part is proved from `UniformBoundsHypothesis` + convergence.
1410The divergence-free part is proved from the extra assumption that *each approximant* is divergence-free.
1411-/