VelCoeff
VelCoeff is the type of real 2-vectors that serve as Fourier velocity coefficients for each truncated mode in the 2D Galerkin model. Researchers deriving discrete energy identities or passing to continuum limits in Navier-Stokes approximations cite this as the basic coefficient space. The declaration is a direct one-line type abbreviation with no proof obligations.
claimThe space of velocity Fourier coefficients is the Euclidean space $E^2$ over the reals, where each element is a pair $(û_1, û_2)$.
background
The Galerkin2D module constructs a finite-dimensional Fourier-mode truncation of 2D incompressible Navier-Stokes on the torus. Modes are indexed by a finite Finset, and each mode carries a velocity coefficient whose type is VelCoeff. The module's design isolates the algebraic property needed for inviscid energy conservation while remaining executable for later analytic work on continuum limits.
proof idea
One-line type abbreviation that directly sets VelCoeff equal to EuclideanSpace ℝ (Fin 2), using the standard two-component indexing for the velocity vector at each mode.
why it matters in Recognition Science
VelCoeff supplies the coefficient type used throughout the discrete fluid model, appearing in downstream statements such as divConstraint (Fourier-side divergence), coeff_bound_of_uniformBounds (uniform bounds under convergence), and duhamelKernelDominatedConvergenceAt_of_forcing. It realizes the M1 milestone of a concrete state space before continuum analysis, consistent with the Recognition Science forcing chain and self-similar fixed-point structure.
scope and limits
- Does not enforce the divergence-free condition on individual coefficients.
- Does not fix the truncation level or the set of active modes.
- Does not incorporate time evolution or the convection operator.
- Does not define any specific norm beyond the inherited Euclidean structure.
formal statement (Lean)
56abbrev VelCoeff : Type := EuclideanSpace ℝ (Fin 2)
proof body
Definition body.
57
58/-- The Galerkin state: velocity coefficients for each truncated mode and each component. -/
used by (15)
-
aestronglyMeasurable_galerkinForcing_mode_of_continuous -
coeff_bound_of_uniformBounds -
divConstraint -
divConstraint_continuous -
divConstraint_eq_zero_of_forall -
duhamelKernelDominatedConvergenceAt_of_forcing -
duhamelRemainderOfGalerkin_integratingFactor -
duhamelRemainderOfGalerkin_kernel -
FourierState2D -
galerkinNS_hasDerivAt_duhamelRemainder_mode -
hasDerivAt_extendByZero_apply -
nsDuhamel_of_forall -
nsDuhamel_of_forall_kernelIntegral_of_forcing -
stokesMild_of_forall -
stokesODE