EnergySkewHypothesis3
plain-language theorem explainer
EnergySkewHypothesis3 packages the algebraic requirement that a bilinear convection operator B on the finite-dimensional Galerkin space satisfies the inner-product identity ⟨B(u,u), u⟩ = 0 for every velocity state u. Spectral analysts working on truncated Navier-Stokes systems cite it to obtain exact energy conservation in the inviscid case and controlled dissipation when viscosity is present. The declaration is simply a structure definition that names this single skew condition as a reusable Prop.
Claim. Let $B$ be a bilinear map from pairs of Galerkin velocity fields (real vectors indexed by the finite set of wave-vectors in $[-N,N]^3$ together with three components) to velocity fields. The energy-skew hypothesis asserts that the real inner product satisfies $⟨B(u,u),u⟩_ℝ=0$ for every such field $u$.
background
GalerkinState3 N is the Euclidean space of real vectors whose indices run over the Cartesian product of the finite mode set modes3 N with Fin 3; it therefore represents divergence-free velocity fields truncated to Fourier modes with |k_i|≤N on the 3-torus. ConvectionOp3 N is the type of bilinear operators that encode the projected nonlinear term of the Navier-Stokes equations inside this finite-dimensional space. The module documentation states that the central energy identity of the 3D Galerkin truncation is precisely the skew-symmetry ⟨B(u,u),u⟩=0, which is listed as the second key result after Fourier-mode truncation on T³.
proof idea
The declaration is a bare structure definition whose single field is the universally quantified inner-product condition. No lemmas or tactics are invoked; the structure simply bundles the skew property so that it can be passed as a named hypothesis to later energy estimates.
why it matters
The hypothesis supplies the algebraic ingredient that makes the Galerkin nonlinearity energy-preserving, and is therefore assumed in every downstream energy theorem: inviscid_energy_deriv_zero3, viscous_energy_antitone3, viscous_energy_bound3, viscous_energy_deriv3, viscous_energy_nonpos3 and viscous_norm_bound3. It directly implements the energy-identity claim of the module (RS_NavierStokes_BKM.tex §4) and thereby supports the discrete sub-Kolmogorov framework inside Recognition Science by guaranteeing that the truncated convection term neither creates nor destroys kinetic energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.