dispersion_nonneg
plain-language theorem explainer
The theorem establishes non-negativity of the three-dimensional lattice dispersion for any positive spacing a. Researchers working on discrete-to-continuum limits or lattice isotropy bounds would cite it to confirm the quadratic form from the cubic ledger is positive semi-definite. The proof is a one-line wrapper that unfolds the sum and reduces each axis term to the single-axis non-negativity lemma.
Claim. For every real number $a > 0$ and every wave vector $k : [3] → ℝ$, the lattice dispersion $D(a,k) := ∑_{i=0}^2 (2/a²)(1 − cos(a k_i))$ satisfies $D(a,k) ≥ 0$.
background
In the LorentzEmergence module the cubic lattice Laplacian in momentum space is represented by the dispersion relation, defined as the sum of three independent axis contributions. Each axis term is axis_dispersion a k := (2/a²)(1 − cos(a k)), which is non-negative because cos x ≤ 1 for all real x. The full dispersion therefore inherits non-negativity once the sum is shown to be non-negative termwise. This local setting is part of the argument that the leading-order continuum limit recovers the rotationally invariant Laplacian eigenvalue |k|² while higher-order lattice corrections vanish.
proof idea
The term proof first unfolds the definition of dispersion to expose the Finset sum over the three axes. It then applies Finset.sum_nonneg, reducing the claim to non-negativity on each component. Each component is discharged directly by the upstream theorem axis_dispersion_nonneg a (k i) ha, which itself rests on Real.cos_le_one.
why it matters
The result supplies the nonnegativity clause inside lorentzEmergenceCert, which certifies recovery of Lorentz-invariant physics from the cubic ledger in the continuum limit. It also populates LatticeIsotropyCert. Within the Recognition framework it closes a prerequisite step for the T8 forcing to D = 3 by guaranteeing that the spatial dispersion operator is positive semi-definite before matching to the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.