latticeIsotropyCert
plain-language theorem explainer
A certificate is supplied showing that dispersion on a three-dimensional lattice is non-negative and bounded above by a constant. Lattice modelers working on discrete spacetime or Laplacian spectra cite this when establishing isotropy constraints. The definition assembles three trigonometric inequalities into the required structure without additional hypotheses.
Claim. The structure requires: for all real $y$, $0$ ≤ $1 - cos y$; for all real $y$, $1 - cos y$ ≤ $2$; and for $a > 0$ and real $k_1,k_2,k_3$, $0$ ≤ $(2/a^2) [(1 - cos(a k_1)) + (1 - cos(a k_2)) + (1 - cos(a k_3))]$. This definition witnesses the three properties by direct substitution of the corresponding inequalities.
background
The Lattice Isotropy Bound module supplies structural bounds ensuring lattice dispersion satisfies $0$ ≤ ω². The module documentation states that non-negativity follows from $1 - cos y$ ≥ $0$, with an additional upper bound $1 - cos y$ ≤ $2$ that together constrain the lattice Laplacian spectrum in three dimensions (Beltracchi Response §6).
proof idea
This is a definition that constructs the required structure by assigning each field to an existing lemma: the non-negativity field to the theorem proving $0$ ≤ $1 - cos y$, the boundedness field to the theorem proving $1 - cos y$ ≤ $2$, and the three-dimensional field to the theorem that sums the three axis contributions under positivity.
why it matters
The definition completes the isotropy certificate in the foundation layer and supplies the non-negativity component used by dispersion results in the simplicial ledger. It directly implements the lattice bound stated in Beltracchi Response §6 and aligns with the framework derivation of three spatial dimensions. No open questions remain as every component is already proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.