UniformBoundsHypothesis
plain-language theorem explainer
The uniform bounds hypothesis collects a family of Galerkin trajectories u_N together with a single nonnegative real B such that the norm of each u_N(t) stays at most B for every truncation level N and every t at least zero. Analysts working on the 2D Navier-Stokes continuum limit cite this record to guarantee uniform control on the approximants before compactness arguments are applied. Its viscous constructor obtains the bound by chaining the dissipative energy estimate from initial data through the skew-symmetry of the convection operator.
Claim. A structure consisting of a family of maps $u_N : [0,∞) → V_N$ (where $V_N$ is the Galerkin state space at truncation level $N$), a nonnegative real $B$, and the assertion that $‖u_N(t)‖ ≤ B$ for all $N ∈ ℕ$ and $t ≥ 0$. The associated constructor builds the structure from a viscous right-hand side, an energy-skew hypothesis on the convection operator, and a uniform initial bound.
background
The ContinuumLimit2D module (Milestone M5) defines a Lean-checkable pipeline shape for passing from finite-dimensional 2D Galerkin approximations to a continuum limit object. It introduces the infinite Fourier coefficient state, the zero-extension map extendByZero that embeds truncated coefficients into the full space, and packages analytic steps such as compactness as explicit hypotheses rather than axioms. GalerkinState N denotes the finite-dimensional space of Fourier modes up to level N; ConvectionOp N is the abstract projected nonlinearity; EnergySkewHypothesis asserts that the inner product of B(u,u) with u vanishes, which encodes energy conservation for the inviscid case; and galerkinNSRHS is the right-hand side νΔu − B(u,u).
proof idea
The ofViscous constructor assembles the record by setting the trajectory family and bound directly from the inputs. It then verifies the uniform bound field by applying the viscous norm bound lemma to each trajectory (which compares the norm at time t to the initial norm via dissipation) and composing the result with the supplied initial bound hypothesis via transitivity.
why it matters
This supplies the uniform boundedness input required by ConvergenceHypothesis, by coeff_bound_of_uniformBounds, and by the theorem continuum_limit_exists that asserts existence of a limit Fourier trajectory with modewise convergence of the approximants. It also feeds the identification hypothesis coeffBound that defines what it means for the limit to be a solution. In the Recognition Science classical bridge this closes the discrete-to-continuum step for 2D fluids by ensuring controlled trajectories before weak compactness is invoked, consistent with the overall pipeline from finite Galerkin systems to the continuum object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.