ConvectionOp3
plain-language theorem explainer
ConvectionOp3 N defines the type of bilinear maps on the finite-dimensional space of Fourier velocity coefficients for the N-mode truncation of 3D Navier-Stokes. Researchers modeling discrete fluid dynamics cite it when setting up the nonlinearity for energy identities. The declaration is a direct type alias that identifies the operator space without additional structure or computation.
Claim. Let $B$ be an element of the function space $H_N to H_N to H_N$, where $H_N$ is the Euclidean space of real coefficients for velocity components indexed by the truncated Fourier modes on $T^3$ up to wavenumber $N$.
background
The module treats the 3D Navier-Stokes equations via spectral Galerkin truncation on the torus, restricting to Fourier modes in $[-N,N]^3$. GalerkinState3 N is the Euclidean space over the product of these modes with the three velocity components, serving as the finite-dimensional state space for the velocity field.
proof idea
This is a direct type abbreviation that sets ConvectionOp3 N equal to the space of bilinear maps from pairs of Galerkin states to Galerkin states. No lemmas or tactics are applied; the definition supplies the interface type used by galerkinNSRHS3 and EnergySkewHypothesis3.
why it matters
The type anchors the energy skew analysis for the Galerkin approximation. It supplies the parameter B in EnergySkewHypothesis3, whose skew condition is invoked to prove that the inviscid energy derivative vanishes and that viscous energy is nonincreasing. This supports the discrete energy identities in RS_NavierStokes_BKM.tex §4 and the connection to the sub-Kolmogorov framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.