lorentzEmergenceCert
plain-language theorem explainer
The definition assembles a certificate showing that cubic-lattice dispersion is bounded above by the rotationally invariant continuum value |k|² for a > 0 and k in R³, with the bound depending only on |k|, the dispersion nonnegative, and a quantitative sandwich on the axis contribution. Lattice regularizers and emergent-spacetime modelers would cite it when checking that a discrete ledger yields isotropic leading-order physics. The construction directly invokes four sibling lemmas that supply the upper bound, nonnegativity, envelope invariance,
Claim. For lattice spacing $a > 0$ and wave vector $k = (k_1, k_2, k_3) ∈ ℝ³ the lattice dispersion satisfies dispersion$(a,k) ≤ |k|²$, the upper bound depends only on $|k|$, dispersion$(a,k) ≥ 0$, and the single-axis dispersion obeys the sandwich $0 ≤ k_i² - $axis dispersion$(a,k_i) ≤ k_i²$.
background
The module addresses Beltracchi's §8 concern that a cubic ledger would select a preferred frame. The lattice Laplacian in momentum space yields dispersion proportional to Σ_i (1 - cos(a k_i)). The continuum isotropic value is the rotationally invariant |k|². Axis dispersion isolates the contribution of one coordinate. The Taylor bound 1 - x²/2 ≤ cos(x) implies each axis term is at most k_i², so the sum is at most |k|². MODULE_DOC states: 'The cubic lattice does not induce a preferred frame in the continuum limit. The continuum limit of the lattice Laplacian is the isotropic (hence Lorentz-invariant in D+1) continuum Laplacian.'
proof idea
The definition is a structure constructor for LorentzEmergenceCert. It supplies the upper_bound field by the lemma dispersion_upper_bound_by_isotropic, the nonneg field by dispersion_nonneg, the envelope_isotropic field by isotropic_envelope_rotation_invariant, and the sandwich field by axis_dispersion_sandwich. No further tactics are required.
why it matters
The certificate supplies the concrete statement that residual anisotropy is a UV effect vanishing at long wavelengths, thereby closing the leading-order argument for emergent rotational invariance on the cubic lattice. It fills the physical reading section of the module that directly answers Beltracchi §8. In the Recognition framework it supports the emergence of D = 3 with Lorentz-compatible dispersion from the simplicial ledger (T8). The module notes that rigorous encoding of the O(a² |k|²) Symanzik correction remains a future extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.