LorentzEmergenceCert
plain-language theorem explainer
The LorentzEmergenceCert structure certifies that cubic-lattice dispersion is bounded above by the isotropic continuum Laplacian, remains nonnegative, and possesses a rotationally invariant upper envelope. Researchers deriving continuum limits from discrete lattices cite it to confirm that leading-order dispersion matches the rotationally invariant form required for Lorentz emergence. The structure is assembled directly from four prior lemmas that establish the individual bounds.
Claim. Let $a > 0$ and let $k : Fin 3 → ℝ$. Define the lattice dispersion by $ω(a, k) = ∑_{i=1}^3 (2/a²)(1 − cos(a k_i))$ and the isotropic continuum Laplacian by $Δ(k) = ∑_{i=1}^3 k_i²$. The certificate asserts $ω(a, k) ≤ Δ(k)$, $ω(a, k) ≥ 0$, that $Δ(k) = Δ(k')$ implies $ω(a, k) ≤ Δ(k')$, and the axis sandwich $0 ≤ k² − (2/a²)(1 − cos(a k)) ≤ k²$.
background
The module addresses Beltracchi §8 by showing how a cubic lattice can yield rotationally invariant continuum physics. Key definitions from the module are axis_dispersion(a, k) = (2/a²)(1 − cos(a k)), the single-axis contribution to the lattice Laplacian; dispersion(a, k) = sum of axis_dispersion over the three axes; and continuum_isotropic(k) = sum k_i², the rotationally invariant continuum eigenvalue. The module doc states that the lattice Laplacian in momentum space is −(2/a²) sum (1 − cos(a k_i)) and that the Taylor bound 1 − x²/2 ≤ cos(x) produces the upper bound by |k|².
proof idea
The structure is a one-line wrapper that applies four lemmas: dispersion_upper_bound_by_isotropic supplies the upper bound, dispersion_nonneg supplies non-negativity, isotropic_envelope_rotation_invariant supplies the envelope invariance, and axis_dispersion_sandwich supplies the axis sandwich inequality.
why it matters
This certificate is the master statement that lattice dispersion is bounded by and approaches the isotropic continuum form, directly answering Beltracchi §8 at the level of the lattice Laplacian. It is instantiated in lorentzEmergenceCert, which supplies the concrete proofs. In the Recognition framework it supports the continuum limit in which lattice artifacts vanish, consistent with emergence of rotationally invariant physics at large scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.