laplacianCoeff3_inner_self_nonpos
plain-language theorem explainer
The lemma shows that for any finite-mode Galerkin state u in three dimensions the inner product of u with its spectral Laplacian is non-positive. Researchers on spectral methods for Navier-Stokes cite it to confirm dissipation from the viscous term in the truncated system. The proof rewrites the inner product as a sum over modes, factors each term as a non-positive wave-number factor times a non-negative square, and concludes via the sum rule for non-positive terms.
Claim. For any natural number $N$ and any Galerkin state $u$ (a vector in the Euclidean space over modes in $[-N,N]^3$ times three velocity components), the inner product satisfies $⟨u, Δu⟩_ℝ ≤ 0$, where the spectral Laplacian $Δu$ multiplies the coefficient at each wave vector $k$ by $-|k|^2$.
background
GalerkinState3 N is the Euclidean space of real coefficients indexed by the finite set modes3 N (all integer triples with coordinates in [-N,N]) crossed with the three velocity components. The operator laplacianCoeff3 applies the multiplier -kSq3(k) at each mode k, where kSq3(k) equals the squared Euclidean norm of the wave vector. This implements the Fourier symbol of the Laplacian on the three-torus under truncation to |k|∞ ≤ N.
proof idea
The tactic proof first rewrites the inner product via the definition of laplacianCoeff3 and the PiLp inner product, producing a sum over all mode-component pairs of u_kc · (-kSq3(kc.1) · u_kc). It then invokes Finset.sum_nonpos. For each summand it applies kSq3_nonneg to obtain -kSq3 ≤ 0, notes that u_kc squared is non-negative, rewrites the product by ring, and concludes non-positivity by mul_nonpos_of_nonpos_of_nonneg.
why it matters
The result is invoked directly by viscous_energy_nonpos3 to bound the viscous term ν⟨u,Δu⟩ ≤ 0 in the energy balance for the Galerkin system. It supplies the dissipation identity required in RS_NavierStokes_BKM.tex §4 for the three-dimensional spectral truncation. Within the Recognition Science framework it closes the discrete energy identity that connects to the eight-tick octave and the forcing of D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.