discreteEnergy
discreteEnergy supplies the discrete kinetic energy for a Galerkin state u as half its squared Euclidean norm on the coefficient space. Researchers deriving energy conservation or dissipation in truncated 2D Navier-Stokes models within Recognition Science cite this definition when establishing algebraic identities for the inviscid and viscous cases. The definition is a direct one-line expression using the built-in norm on EuclideanSpace.
claimLet $N$ be a natural number and let $u$ be a Galerkin state consisting of real velocity coefficients indexed by the truncated modes and two components. The discrete energy is $E(u) := (1/2) ||u||^2$, where $||·||$ is the Euclidean norm on the coefficient space.
background
The Galerkin2D module builds a finite-dimensional Fourier-truncated model for 2D incompressible Navier-Stokes on the torus, with the explicit goal of obtaining a concrete discrete state space and the basic algebraic energy identity for the inviscid case. GalerkinState N is the EuclideanSpace ℝ over the product of the mode set and Fin 2, so that inner products and norms are immediately available for energy calculations. The module isolates the single algebraic property of the convection operator needed for energy conservation, namely that the inner product of B(u,u) with u vanishes.
proof idea
This is a one-line wrapper that directly applies the squared-norm expression on the EuclideanSpace type for the Galerkin coefficients. No lemmas beyond the standard norm definition are invoked.
why it matters in Recognition Science
This definition supplies the energy functional used in every energy estimate in the module. It appears directly in inviscid_energy_deriv_zero to obtain conservation under the EnergySkewHypothesis, and in viscous_energy_antitone together with viscous_energy_bound_from_initial to obtain monotonicity and initial-data bounds for positive viscosity. The construction completes the basic energy identity step of Milestone M1 and supplies the discrete counterpart to continuum kinetic energy, consistent with the Recognition Science forcing chain that derives classical physics from the J-uniqueness and eight-tick structures.
scope and limits
- Does not prove existence or uniqueness of solutions to the discrete dynamical system.
- Does not address the continuum limit as the truncation parameter N tends to infinity.
- Does not include external forcing or non-periodic boundary conditions.
- Does not extend to three-dimensional or compressible flows.
Lean usage
theorem energy_nonnegative {N : ℕ} (u : GalerkinState N) : discreteEnergy u ≥ 0 := by unfold discreteEnergy; positivityformal statement (Lean)
90noncomputable def discreteEnergy {N : ℕ} (u : GalerkinState N) : ℝ :=
proof body
Definition body.
91 (1 / 2 : ℝ) * ‖u‖ ^ 2
92
93/-- Algebraic hypothesis capturing the skew-symmetry of the Galerkin nonlinearity in L²:
94\( \langle B(u,u), u \rangle = 0 \). -/