Quadratic, never linear. The lattice clears every Lorentz bound.
On the recognition lattice the dispersion relation is the cos-Laplacian the Lean library carries
(Foundation/SimplicialLedger/LorentzEmergence.lean, 0 sorry):
ω² = (2/a²) Σi [1 − cos(kia)]. Lean proves the dispersion is
bounded by the rotationally invariant continuum envelope |k|², which is Lorentz symmetry emerging at leading
order. At finite spacing every mode runs slightly slow, with deficit δ ≈ (ka)²/8:
quadratic in energy over the Planck scale, never linear. This script computes the exact velocities, expands the
correction order by order, and scores the quadratic MODEL estimate against published Lorentz-violation bounds
from gamma-ray timing, clock comparison, and neutrino experiments. It clears all five with 10¹² to
10²⁰ of room.
Exact ω(k) and velocities
Exact lattice dispersion, its Taylor series in a² (each term printed separately), group velocity, phase velocity, and the fractional correction to the continuum. The default probe k = 0.1 gives |vg − c|/c = 1.25×10⁻³, exactly the leading (ka)²/8 law, and subluminal: on this lattice vg = cos(ka/2) on-axis, always ≤ c.
No linear Lorentz violation
Any detection of linear O(E/EP) Lorentz violation falsifies this formulation outright. That is the sharpest kill condition on this page.
What is proved vs modeled
THEOREM (0 sorry, LorentzEmergence.lean): the lattice dispersion is non-negative, bounded above
by |k|², and its continuum envelope is rotationally invariant. DEF/MODEL
(LorentzViolationBoundFromRS.lean): the violation order is 2. The coefficient 1/8 and the
a = Planck length identification are modeling choices in this script. A correction this page owes you: an
earlier version claimed massless modes travel at exactly c by a "no-dispersion theorem"; no such theorem
exists in the library, and the lattice itself says photons run one part in 10³⁶ slow at Fermi-LAT
energies.
The lattice correction, measured
Group-velocity deficit |vg/c − 1| against wavenumber, computed from the exact cos dispersion (the same formula the script runs, and the same one the Lean proves theorems about). On log-log axes the low-k regime is a clean slope-2 line: the correction is quadratic, never linear. Physical particles live at the far left of this plot; the deficit reaches 1 at k = π, the Brillouin-zone edge, ~10¹⁹ GeV, where the lattice wave stands still.
RS vs experimental bounds
| Experiment | Sector | E (GeV) | Expt bound | RS MODEL prediction | Margin |
|---|---|---|---|---|---|
| Fermi-LAT GRB 090510 | massless | 31 | 1e−20 | 8.06e−37 | 10¹⁶ |
| MAGIC Mrk 501 | massless | 1200 | 3e−19 | 1.21e−33 | 10¹⁴ |
| Hughes-Drever (e−) | massive | 5.1e−4 | 1e−25 | 2.19e−46 | 10²⁰ |
| IceCube (ν) | massive | 100 | 1e−23 | 8.39e−36 | 10¹² |
| Clock comparison (p) | massive | 0.938 | 1e−27 | 7.38e−40 | 10¹² |
Run it yourself
$ python3 lattice_dispersion.py --bounds --- RS vs Experimental Lorentz Violation Bounds --- Fermi-LAT GRB 090510 (photon) massless 8.06e-37 YES MAGIC Mrk 501 (photon) massless 1.21e-33 YES Hughes-Drever (electron) massive 2.19e-46 YES IceCube (neutrino) massive 8.39e-36 YES Clock comparison (proton) massive 7.38e-40 YES Any detection of LINEAR Lorentz violation O(E/E_P) falsifies this lattice picture. $ python3 lattice_dispersion.py --scan # 20-point sweep to the Brillouin-zone edge
Mixed tier, stated exactly. THEOREM (Lean, 0 sorry): the cos-Laplacian dispersion is
non-negative, bounded by the rotationally invariant envelope |k|²
(LorentzEmergence.lean). DEF/MODEL: the violation order is 2
(LorentzViolationBoundFromRS.lean, a bare definition, not a physics theorem), the coefficient
1/8, the lattice-spacing = Planck-length identification, and applying one scalar dispersion to all particle
sectors. MEASURED: the five-bound comparison. A correction this page owes you: an earlier version used a cosh
dispersion (superluminal, not the Lean form) and claimed photons travel at exactly c by a "no-dispersion
theorem" that does not exist in the library; both are now fixed to mirror the Lean. The predictions sit 12 to
20 orders of magnitude below current sensitivity, so today's table is a consistency check, not a
discrimination. The falsifier that bites is linear LV: one confirmed O(E/EP) detection at any energy
kills the formulation.