axis_dispersion_nonneg
plain-language theorem explainer
The single-axis dispersion of the cubic lattice Laplacian is non-negative whenever the lattice spacing is positive. Workers on discrete-to-continuum limits cite it to guarantee that the quadratic form remains positive semi-definite before taking the isotropic bound. The argument is a direct algebraic reduction: unfold the definition, factor out the positive prefactor 2/a², and invoke cos ≤ 1.
Claim. For every positive real number $a$ and every real number $k$, the quantity $(2/a^2)(1 - cos(a k))$ is non-negative.
background
The module shows how a cubic lattice ledger can recover rotationally invariant continuum physics. The single-axis dispersion is defined by unfolding to (2/a²)(1 - cos(a k)). The full three-dimensional dispersion is the sum of three such terms over the coordinate axes. The local setting is the standard Taylor bound 1 - x²/2 ≤ cos(x), which supplies both the upper envelope by |k|² and the non-negativity used here.
proof idea
Unfold the definition of axis_dispersion. Apply mul_nonneg to the manifestly positive factor 2/a² (obtained via div_nonneg from 0 ≤ 2 and a² ≥ 0) and the term (1 - cos(a k)). The second factor is non-negative by linarith with the Mathlib fact Real.cos_le_one.
why it matters
It supplies the non-negativity half of the sandwich bounds that appear in axis_dispersion_sandwich and is summed to obtain dispersion_nonneg. These two results together establish that the lattice dispersion lies between 0 and the rotationally invariant continuum Laplacian eigenvalue, which is the key step toward Lorentz emergence from the cubic ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.