EnergySkewHypothesis
plain-language theorem explainer
EnergySkewHypothesis encodes the algebraic condition that a convection operator B on the truncated Galerkin space satisfies the inner product identity ⟨B(u,u), u⟩ = 0 for every state u. Researchers modeling finite-mode Navier-Stokes truncations cite it to obtain the inviscid energy conservation identity before taking continuum limits. The declaration is a direct structure definition that records this single skew-symmetry field.
Claim. Let $N$ be a natural number and let $B$ be a bilinear convection operator on the space of Galerkin states. The energy skew hypothesis asserts that the real inner product satisfies $⟨B(u,u), u⟩ = 0$ for every Galerkin state $u$.
background
The Galerkin2D module constructs a finite-dimensional Fourier-mode truncation of 2D incompressible Navier-Stokes on the torus. GalerkinState is the Euclidean space whose coordinates are the velocity coefficients for each retained mode and each of the two components. ConvectionOp is the abstract bilinear map that will later be replaced by explicit Fourier convolution plus Leray projection; its only required property at this stage is the skew-symmetry needed for energy balance.
proof idea
EnergySkewHypothesis is introduced as a structure definition whose single field directly states the required inner-product condition. No lemmas or tactics are invoked; the declaration itself supplies the interface used by all subsequent energy estimates.
why it matters
The hypothesis supplies the algebraic ingredient for the downstream theorem inviscid_energy_deriv_zero, which concludes that discrete energy is conserved when viscosity vanishes. It is also assumed in the viscous energy bounds viscous_energy_antitone and viscous_energy_bound_from_initial. Within the Recognition Science program it completes the basic energy identity required by milestone M1 of the ClassicalBridge before any continuum-limit arguments are attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.