lattice_3d_nonneg
plain-language theorem explainer
lattice_3d_nonneg establishes non-negativity of the scaled three-dimensional lattice dispersion (2/a²) times the sum of (1 - cos(a k_i)) terms. Lattice modelers cite it to certify that the discrete Laplacian spectrum remains non-negative. The proof is a term-mode one-liner that multiplies the positivity of the prefactor by the sum of three instances of the bound 1 - cos(y) ≥ 0.
Claim. For all real numbers $a, k_1, k_2, k_3$ with $a > 0$, $0 ≤ (2/a²) [(1 - cos(a k_1)) + (1 - cos(a k_2)) + (1 - cos(a k_3))]$.
background
The Lattice Isotropy Bound module supplies the structural inequalities for lattice dispersion in the Beltracchi Response §6. Its central claim is that lattice dispersion satisfies 0 ≤ ω², which follows from the elementary inequality 1 - cos(y) ≥ 0 for real y. A companion result gives the matching upper bound 1 - cos(y) ≤ 2, jointly constraining the spectrum of the discrete Laplacian.
proof idea
The proof is a term-mode one-liner. It applies mul_nonneg to the positivity of 2/a² and to a linarith closure that invokes one_minus_cos_nonneg on each of the three arguments ak1, ak2, a*k3.
why it matters
This theorem supplies the three-dimensional non-negativity clause required by the LatticeIsotropyCert structure, which packages the dispersion bounds for downstream certification. It directly implements the key structural bound 0 ≤ ω² stated in the module documentation for the Beltracchi Response §6. Within the lattice isotropy package it ensures the discrete model remains consistent with the non-negative spectrum demanded by the underlying constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.