dispersion
plain-language theorem explainer
dispersion aggregates the three single-axis lattice contributions into the full 3D cubic-lattice Laplacian eigenvalue in momentum space. Researchers modeling emergent Lorentz symmetry from discrete lattices or deriving continuum limits in field theory would cite it when establishing isotropy at long wavelengths. The definition is a direct sum of the axis_dispersion formula over the Fin 3 components of k.
Claim. $ω(a, k) := ∑_{i=1}^3 (2/a²)(1 − cos(a k_i))$ for lattice spacing $a$ and wave-vector components $k = (k_1, k_2, k_3)$.
background
The module derives rotationally invariant continuum physics from a cubic lattice by showing that the leading-order dispersion matches the isotropic Laplacian eigenvalue |k|². axis_dispersion supplies the single-axis building block: (2/a²)(1 − cos(a k)). dispersion simply sums this quantity over the three coordinate directions, yielding the full lattice-Laplacian eigenvalue in three dimensions. The module context is the resolution of Beltracchi §8: a physical cubic ledger must not induce a preferred frame, so the continuum limit must recover boost-and-rotation symmetry at long wavelengths.
proof idea
One-line wrapper that applies axis_dispersion to each component of the Fin 3 vector k and sums the results.
why it matters
This definition supplies the concrete 3D dispersion object used by dispersion_upper_bound_by_isotropic and dispersion_nonneg, which in turn certify that the cubic lattice recovers the rotationally invariant |k|² at leading order. It feeds downstream results including noble_gas_bp_full_ordering, polarizabilityProxy, and the CPM2D bridge and hypothesisNormSq constructions in fluid models. The construction directly supports the T8 step (D = 3) and the RCL-based emergence of Lorentz symmetry in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.