rs_implies_global_regularity_2d
plain-language theorem explainer
The declaration shows that a Recognition Science pipeline hypothesis for 2D fluids implies existence of a global regular Fourier trajectory satisfying the packaged solution concept. Researchers composing discrete-to-continuum bridges in the classical fluids setting would cite it as the M6 capstone. The proof is a one-line wrapper that applies the upstream continuum limit existence theorem to the three packaged sub-hypotheses.
Claim. Let $H$ be a structure containing uniform bounds on a Galerkin family, a convergence hypothesis to a limit Fourier trajectory, and an identification hypothesis that the limit satisfies a chosen solution concept. Then there exists a map $u : ℝ →$ (Mode2 → VelCoeff) such that the zero-extended Galerkin coefficients converge pointwise in each mode to the components of $u(t)$, the trajectory $u$ satisfies the identification property, and all coefficients remain bounded by the uniform bound $B$ for all $t ≥ 0$.
background
The module supplies the top-level composition theorem for the 2D pipeline: Galerkin2D (M1) + LNAL encoding (M2) + one-step simulation (M3) + CPM instantiation (M4) + continuum limit packaging (M5) yields an abstract continuum solution. RSNS2DPipelineHypothesis is the structure that packages three sub-hypotheses: UniformBoundsHypothesis (uniform-in-N bounds for the Galerkin family), ConvergenceHypothesis (convergence to a limit Fourier trajectory), and IdentificationHypothesis (the limit satisfies a chosen solution concept for 2D Navier–Stokes on the torus). Upstream, continuum_limit_exists states that given UniformBoundsHypothesis, ConvergenceHypothesis, and IdentificationHypothesis, there exists a limit trajectory $u$ with the required pointwise convergence in Fourier modes.
proof idea
The proof is a one-line wrapper that applies continuum_limit_exists to the three fields H.Hbounds, H.Hconv, and H.Hid extracted from the pipeline hypothesis. The simpa tactic discharges the goal by direct substitution of these components into the upstream theorem.
why it matters
This theorem completes the 2D regularity pipeline by composing the lower milestones without axioms or sorrys, realizing the abstract global regularity claim stated in the module doc-comment. It fills the M6 architectural slot in the classical bridge and positions the framework for concrete PDE applications. No downstream uses are recorded yet; the open question it touches is making the identification hypothesis concrete rather than abstract.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.