divFreeCoeffBound
This definition constructs an IdentificationHypothesis for a candidate continuum limit trajectory u by asserting that u inherits uniform coefficient bounds from the Galerkin approximants and satisfies the Fourier-side divergence-free condition. Researchers formalizing the passage from finite-dimensional 2D Galerkin schemes to weak solutions of the Navier-Stokes equations on the torus would cite it when assembling the solution concept. The construction is a direct packaging step that invokes the derived bound theorem on uniform approximants and,
claimLet $H$ be a uniform-bounds hypothesis supplying a family of Galerkin trajectories $u_N$ with global bound $B$. Let $HC$ be a convergence hypothesis to a limit trajectory $u$. Assume that for every truncation level $N$, time $t$, and mode $k$ the Fourier divergence constraint holds: $k_1 v_0 + k_2 v_1 = 0$ where $v = $ extend-by-zero of the $N$-th approximant coefficient at $k$. Then the identification hypothesis for $HC$ is the structure whose solution predicate is the conjunction of the uniform bound on $u$ and the divergence-free trajectory property.
background
The module ContinuumLimit2D supplies the Lean-checkable pipeline shape for passing from finite Galerkin approximations to a continuum Fourier-state limit at milestone M5. UniformBoundsHypothesis packages a family of truncated trajectories $u_N$ together with a uniform norm bound $B$ that is independent of truncation level. ConvergenceHypothesis adds a candidate limit trajectory $u$ together with pointwise mode-by-mode convergence of the zero-extended Galerkin coefficients. IdentificationHypothesis is the abstract container that later receives a concrete solution concept; its IsSolution field records the predicate that the limit must satisfy.
proof idea
The definition constructs the IdentificationHypothesis record directly. It sets the IsSolution predicate to the conjunction of the uniform bound (for all $t$ and modes) and the IsDivergenceFreeTraj property. The isSolution field is proved by a two-line refinement: the bound clause is obtained by applying coeff_bound_of_uniformBounds to the convergence hypothesis, while the divergence-free clause is obtained by applying divConstraint_eq_zero_of_forall to the supplied assumption that every approximant satisfies the constraint.
why it matters in Recognition Science
The definition supplies the canonical constructor that turns uniform bounds plus per-approximant divergence-free data into the identification hypothesis required by the M5 pipeline. It therefore sits at the final identification step of the ClassicalBridge.Fluids.ContinuumLimit2D module, where hypotheses are kept explicit so that later milestones can replace them by concrete proofs. No downstream theorems yet depend on it, indicating that it is scaffolding for the eventual replacement of IdentificationHypothesis by a verified 2D Navier-Stokes solution concept.
scope and limits
- Does not derive the uniform bound $B$ from discrete energy or enstrophy estimates.
- Does not prove existence or convergence of the limit trajectory $u$.
- Does not verify the full Navier-Stokes equation, only the divergence-free condition.
- Does not address three-dimensional flows or non-periodic domains.
formal statement (Lean)
1412def divFreeCoeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1413 (hDF : ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2, divConstraint k ((extendByZero (H.uN N t)) k) = 0) :
1414 IdentificationHypothesis HC :=
proof body
Definition body.
1415 { IsSolution := fun u =>
1416 (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsDivergenceFreeTraj u
1417 isSolution := by
1418 refine ⟨?_, ?_⟩
1419 · intro t ht k
1420 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1421 · intro t k
1422 exact ConvergenceHypothesis.divConstraint_eq_zero_of_forall (HC := HC) (t := t) (k := k)
1423 (hDF := fun N => hDF N t k) }
1424
1425/-- Identification constructor: coefficient bound + (linear) Stokes/heat mild identity.
1426
1427The bound part is proved from `UniformBoundsHypothesis` + convergence.
1428The mild Stokes identity is proved from the extra assumption that it holds for every approximant. -/