RSNS2DPipelineHypothesis
plain-language theorem explainer
RSNS2DPipelineHypothesis packages uniform bounds on a family of Galerkin trajectories, their convergence to a limit Fourier trajectory on the torus, and identification of that limit as satisfying an abstract 2D Navier-Stokes solution concept. Researchers working on the Recognition Science classical bridge to fluids would cite this structure as the single top-level assumption needed to reach global regularity in two dimensions. The declaration is a plain record definition with three fields and no proof obligations.
Claim. Let $H_b$ be a uniform-in-$N$ bound on Galerkin trajectories $u_N(t)$ with global constant $B$. Let $H_c$ assert existence of a limit trajectory $u(t)$ in full Fourier space together with modewise convergence of the zero-extended coefficients. Let $H_i$ assert that this limit satisfies a chosen abstract solution concept for the 2D Navier-Stokes equations. Then the pipeline hypothesis is the record $(H_b, H_c, H_i)$.
background
The module states the top-level composition for the 2D pipeline: Galerkin2D approximations plus LNAL semantics plus one-step simulation plus CPM instantiation plus continuum-limit packaging yield an abstract continuum solution. UniformBoundsHypothesis supplies a family of discrete trajectories $u_N : N : ℕ → ℝ → GalerkinState N$ together with a single global bound $B ≥ 0$. ConvergenceHypothesis (given those bounds) supplies a candidate limit $u : ℝ → FourierState2D$ (where FourierState2D is the space of all mode-to-coefficient maps) and asserts pointwise Tendsto convergence of the extended Galerkin coefficients. IdentificationHypothesis then asserts that the limit trajectory satisfies a chosen solution concept IsSolution.
proof idea
The declaration is a record definition that simply assembles the three component hypotheses; no tactics or lemmas are applied. Each field directly references the corresponding structure from the ContinuumLimit2D module, with the convergence field depending on the bounds field and the identification field depending on the convergence field.
why it matters
This structure is the sole hypothesis passed to the downstream theorem rs_implies_global_regularity_2d, which extracts the existence of the limit Fourier trajectory together with its convergence property. It completes the architectural composition described in the module doc-comment for Milestone M6, making the full dependency graph from Galerkin2D through CPM2D explicit without introducing sorry or axiom. The construction sits inside the Recognition Science classical bridge and prepares the ground for later concrete bounds derived from energy/enstrophy inequalities and CPM coercivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.