dispersion_upper_bound_by_isotropic
plain-language theorem explainer
Lattice dispersion on a cubic grid with spacing a > 0 is bounded above by the isotropic continuum Laplacian eigenvalue sum k_i² for any wave vector k in three dimensions. Researchers deriving continuum limits from discrete lattices or verifying emergent Lorentz invariance cite this when confirming the absence of leading-order anisotropy. The argument proceeds by unfolding the sum definitions and applying the componentwise axis upper bound via Finset.sum_le_sum.
Claim. For $a > 0$ and $k : Fin 3 → ℝ$, the lattice dispersion $∑_{i=1}^3 (2/a²)(1 − cos(a k_i)) ≤ ∑_{i=1}^3 k_i²$.
background
The LorentzEmergence module shows how a cubic ledger recovers rotationally invariant physics. Dispersion is the sum over the three axes of axis_dispersion a (k_i), with each axis term equal to (2/a²)(1 − cos(a k_i)). Continuum_isotropic is defined as the sum of k_i squared, the eigenvalue of the continuum Laplacian. Axis_dispersion_upper_bound establishes the single-axis bound (2/a²)(1 − cos(a k)) ≤ k² using the inequality 1 − y²/2 ≤ cos y. This bound ensures the lattice dispersion never exceeds the isotropic continuum value, providing the foundation for proving rotational symmetry of the envelope.
proof idea
Unfold dispersion and continuum_isotropic to expose the sums, then invoke Finset.sum_le_sum. The resulting goal reduces to showing axis_dispersion a (k i) ≤ (k i)² for each i, which is discharged directly by axis_dispersion_upper_bound a (k i) ha.
why it matters
It is invoked by isotropic_envelope_rotation_invariant to prove that equal-magnitude wave vectors share the same upper envelope, and by lorentzEmergenceCert to assemble the full emergence certificate. The module doc states this as the first proof item addressing Beltracchi §8 on preferred frames in cubic lattices. Within Recognition Science it supports the forcing chain step to D = 3 spatial dimensions by ensuring isotropy at leading order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.