viscous_norm_bound_from_initial
The theorem establishes an a priori L2 bound for trajectories of the viscous Galerkin Navier-Stokes system on the torus. Analysts working on finite-mode truncations cite it to control coefficient growth before taking continuum limits. The argument invokes the discrete energy inequality and converts it to a norm bound by multiplying through by 2 and applying the square-root monotonicity of the norm on nonnegative reals.
claimLet $N$ be a natural number, let $ν ≥ 0$, let $B$ be a convection operator on the space of Galerkin states satisfying the energy-skew condition $⟨B(u,u),u⟩=0$, and let $u:ℝ→$Galerkin state space be a differentiable curve obeying the discrete Navier-Stokes equation $u'=νΔu−B(u,u)$. Then $‖u(t)‖≤‖u(0)‖$ for every $t≥0$.
background
The module builds a finite-dimensional Fourier-truncated model of 2D incompressible Navier-Stokes on the torus. GalerkinState is the Euclidean space of velocity coefficients indexed by the finite set of modes and two components. ConvectionOp abstracts the projected bilinear nonlinearity, while galerkinNSRHS assembles the right-hand side as the viscous Laplacian term minus the convection term. EnergySkewHypothesis encodes the single algebraic identity $⟨B(u,u),u⟩=0$ that guarantees energy conservation when viscosity vanishes. The upstream theorem viscous_energy_bound_from_initial supplies the corresponding bound on the discrete kinetic energy $E(u)=½‖u‖².
proof idea
The tactic proof opens by calling viscous_energy_bound_from_initial to obtain the energy inequality. It rewrites the result via the definition of discreteEnergy to reach ½‖u t‖² ≤ ½‖u 0‖². Multiplication by 2 produces the squared-norm comparison, after which le_of_sq_le_sq together with norm nonnegativity yields the final norm bound.
why it matters in Recognition Science
The result populates the uniform bound hypothesis required by UniformBoundsHypothesis in the continuum-limit module. It completes the viscous energy control begun by viscous_energy_bound_from_initial and supplies the basic a priori estimate that later compactness arguments in the Galerkin2D milestone rely upon. Within the classical bridge it furnishes the L2 control that must precede any passage to the continuum Navier-Stokes equations.
scope and limits
- Does not prove existence or uniqueness of Galerkin trajectories.
- Does not produce bounds uniform in the truncation level N.
- Does not treat the continuum limit or any compactness passage.
- Does not incorporate external forcing or non-periodic boundary conditions.
formal statement (Lean)
220theorem viscous_norm_bound_from_initial {N : ℕ} (ν : ℝ) (hν : 0 ≤ ν)
221 (B : ConvectionOp N) (HB : EnergySkewHypothesis B)
222 (u : ℝ → GalerkinState N)
223 (hu : ∀ t : ℝ, HasDerivAt u (galerkinNSRHS ν B (u t)) t) :
224 ∀ t ≥ 0, ‖u t‖ ≤ ‖u 0‖ := by
proof body
Tactic-mode proof.
225 intro t ht
226 have hE : discreteEnergy (u t) ≤ discreteEnergy (u 0) :=
227 viscous_energy_bound_from_initial (N := N) ν hν B HB u hu t ht
228 have hE' : (1 / 2 : ℝ) * ‖u t‖ ^ 2 ≤ (1 / 2 : ℝ) * ‖u 0‖ ^ 2 := by
229 simpa [discreteEnergy] using hE
230 -- Multiply both sides by `2` to cancel the `1/2`.
231 have hsq : ‖u t‖ ^ 2 ≤ ‖u 0‖ ^ 2 := by
232 have hmul := mul_le_mul_of_nonneg_left hE' (by norm_num : (0 : ℝ) ≤ 2)
233 -- `2 * (1/2) = 1`
234 simpa [mul_assoc] using hmul
235 -- Convert the square inequality to a norm inequality (norms are nonnegative).
236 exact le_of_sq_le_sq hsq (norm_nonneg (u 0))
237
238end IndisputableMonolith.ClassicalBridge.Fluids