continuum_limit_exists
The declaration establishes that uniform bounds on a family of 2D Galerkin trajectories, together with a convergence hypothesis supplying a limit Fourier trajectory and an identification hypothesis confirming it solves the target PDE, produce an explicit continuum solution whose coefficients inherit the uniform bound. Researchers working on the 2D Navier-Stokes regularity problem via Galerkin approximation would cite this as the capstone step that packages the limit object. The proof is a direct term-mode construction that selects the candidate
claimLet $H$ be a uniform bounds hypothesis on Galerkin trajectories $u_N$ with global bound $B$. Let $HC$ be a convergence hypothesis providing a limit trajectory $u : ℝ →$ (Fourier state) together with mode-by-mode convergence of the zero-extended approximants. Let $HI$ be an identification hypothesis asserting that $u$ satisfies the chosen solution concept. Then there exists a trajectory $u$ such that the approximants converge pointwise to $u(t)$, $u$ satisfies the solution property, and $‖u(t)_k‖ ≤ B$ for all $t ≥ 0$ and modes $k$.
background
The module ContinuumLimit2D implements milestone M5: a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to a continuum Fourier limit on the torus. It introduces three hypothesis structures. UniformBoundsHypothesis packages a family of Galerkin trajectories $u_N : ℕ → ℝ →$ GalerkinState N together with a uniform bound $B$ such that $‖u_N(t)‖ ≤ B$ for all $N$ and $t ≥ 0$. ConvergenceHypothesis supplies a candidate limit $u : ℝ →$ FourierState2D (where FourierState2D ≔ Mode2 → VelCoeff) and the pointwise convergence statement that the zero-extended Galerkin coefficients tend to $u(t)_k$. IdentificationHypothesis asserts an abstract solution concept IsSolution : (ℝ → FourierState2D) → Prop together with the claim that the limit satisfies it. The local theoretical setting keeps analytic compactness and identification steps as explicit hypotheses so later milestones can replace them with proofs. An upstream result used here is coeff_bound_of_uniformBounds, which states that if the approximants are uniformly bounded then the limit coefficients inherit the same bound by closedness of the closed ball.
proof idea
The proof is a term-mode refinement that constructs the witness as the triple consisting of the candidate limit $u$ supplied by the convergence hypothesis, the convergence property itself, the solution property taken directly from the identification hypothesis, and the uniform bound obtained by applying coeff_bound_of_uniformBounds to the convergence data.
why it matters in Recognition Science
This theorem is the central milestone (M5) of the ContinuumLimit2D module, packaging the existence of the continuum limit object. It is used by rs_implies_global_regularity_2d in Regularity2D, which composes the full RS-to-regularity bridge pipeline and concludes the existence of a limit Fourier trajectory satisfying the regularity claim. The result fills the final analytic step in the 2D Navier-Stokes regularity argument within the Recognition Science framework, where the classical bridge connects discrete Galerkin dynamics to the continuum PDE. It touches the open question of discharging the abstract identification hypothesis with a concrete verification of the Navier-Stokes solution concept.
scope and limits
- Does not establish the uniform bounds hypothesis from energy estimates.
- Does not prove the convergence of the Galerkin approximations.
- Does not instantiate the concrete solution concept inside the identification hypothesis.
- Does not extend to three spatial dimensions.
- Does not address the forcing term or viscosity parameters explicitly.
formal statement (Lean)
1621theorem continuum_limit_exists
1622 (H : UniformBoundsHypothesis)
1623 (HC : ConvergenceHypothesis H)
1624 (HI : IdentificationHypothesis HC) :
1625 ∃ u : ℝ → FourierState2D,
1626 (∀ t : ℝ, ∀ k : Mode2, Tendsto (fun N : ℕ => (extendByZero (H.uN N t)) k) atTop (𝓝 ((u t) k)))
1627 ∧ HI.IsSolution u
1628 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) := by
proof body
Term-mode proof.
1629 refine ⟨HC.u, HC.converges, ?_, ?_⟩
1630 · simpa using HI.isSolution
1631 · intro t ht k
1632 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1633
1634end ContinuumLimit2D
1635
1636end IndisputableMonolith.ClassicalBridge.Fluids