axis_dispersion_sandwich
plain-language theorem explainer
The axis dispersion along one lattice direction satisfies the sandwich 0 ≤ k² − D(a,k) ≤ k² for a > 0. Lattice regularization theorists deriving continuum limits would cite it to confirm that the leading term recovers the isotropic Laplacian eigenvalue without directional bias. The proof is a direct term-mode wrapper that pairs the non-negativity lemma with the upper-bound lemma via linarith.
Claim. For real numbers $a > 0$ and $k$, let $D(a,k)$ denote the single-axis lattice dispersion. Then $0 ≤ k^2 - D(a,k) ≤ k^2$.
background
This theorem belongs to the LorentzEmergence module, which shows how a cubic lattice yields rotationally invariant continuum physics and thereby addresses Beltracchi §8. The local setting begins from the lattice Laplacian Δ_lattice φ(x) = (1/a²) Σ_i [φ(x + a e_i) + φ(x − a e_i) − 2 φ(x)], whose Fourier symbol is −(2/a²) Σ_i [1 − cos(a k_i)]. The axis_dispersion function isolates the contribution of one coordinate: proportional to (1 − cos(a k))/a². Module documentation states that the leading-order dispersion is rotation invariant, which is the content of 'no preferred frame at continuum scales'. The result relies on the upstream lemmas axis_dispersion_upper_bound (from 1 − cos(y) ≤ y²/2) and axis_dispersion_nonneg (from 0 ≤ 1 − cos(y)).
proof idea
The proof is a term-mode wrapper. It opens a pair of goals with refine ⟨?, ?⟩ and discharges the first by linarith applied to axis_dispersion_upper_bound a k ha, then discharges the second by linarith applied to axis_dispersion_nonneg a k ha.
why it matters
The declaration supplies the sandwich component required by the downstream master certificate lorentzEmergenceCert, which packages upper bound, non-negativity, isotropy, and this sandwich into a single structure. It completes the lattice-Laplacian step that shows the continuum limit recovers |k|² without preferred directions, directly answering Beltracchi §8. Within the Recognition Science framework it supports the emergence of isotropic D = 3 physics from the phi-forced eight-tick lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.