axis_dispersion
plain-language theorem explainer
The single-axis dispersion relation for the cubic-lattice Laplacian is defined by (2/a²)(1 - cos(a k)). Lattice field theorists and discrete-to-continuum analysts cite it when deriving bounds that recover the isotropic |k|² envelope. The definition is a direct one-line transcription of the standard one-dimensional finite-difference eigenvalue.
Claim. The single-axis dispersion relation is defined by $ω(a,k) := (2/a^2)(1 - cos(a k))$ for real lattice spacing $a$ and wave number $k$.
background
This module shows how a cubic ledger can yield rotationally invariant continuum physics, answering Beltracchi §8. The lattice Laplacian decomposes axis-by-axis: the full three-dimensional dispersion is the sum over the three coordinate directions of the single-axis term. The rotationally invariant continuum Laplacian eigenvalue is the squared Euclidean norm |k|². The upstream definition dispersion(a, k) := ∑_{i:Fin 3} axis_dispersion a (k i) assembles the three independent axis contributions.
proof idea
One-line definition that directly encodes the trigonometric expression for the one-dimensional lattice dispersion along a single axis.
why it matters
This supplies the primitive building block for every bound proved in the module. It is unfolded inside axis_dispersion_nonneg, axis_dispersion_upper_bound, axis_dispersion_sandwich, and dispersion_upper_bound_by_isotropic, which together establish the LorentzEmergenceCert: dispersion ≤ |k|² (rotationally invariant envelope), dispersion ≥ 0, and envelope depends only on |k|. The construction therefore closes the leading-order gap between the cubic ledger and continuum Lorentz symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.