VelCoeff3
plain-language theorem explainer
The three-dimensional Euclidean space over the reals serves as the coefficient space for velocity modes in the spectral Galerkin truncation of the Navier-Stokes equations on the three-torus. Researchers constructing finite-mode fluid approximations would reference this type when building the discrete velocity field. The declaration is a direct type abbreviation with no additional structure or proof obligations.
Claim. The space of velocity coefficients is the Euclidean space $mathbb{R}^3$.
background
The module develops a three-dimensional spectral Galerkin truncation for the Navier-Stokes equations as an extension of the two-dimensional case. Fourier modes are restricted to the cube $[-N,N]^3$ on the torus $T^3$. The velocity coefficient type supplies the underlying vector space for these mode coefficients. The module establishes the energy-skew property of the nonlinearity and the dissipative character of the Laplacian term.
proof idea
The declaration is a one-line type abbreviation that directly identifies the velocity coefficient type with the standard three-dimensional Euclidean space over the reals.
why it matters
This type definition supplies the finite-dimensional space required for the Galerkin approximation in three dimensions within the Recognition Science treatment of Navier-Stokes. It supports the energy identity and enstrophy bounds referenced in RS_NavierStokes_BKM.tex section 4. The abbreviation enables the spectral setting that connects to the discrete sub-Kolmogorov framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.