axis_dispersion_upper_bound
plain-language theorem explainer
The single-axis lattice dispersion satisfies (2/a²)(1 − cos(a k)) ≤ k² for a > 0. Lattice regularization studies and derivations of continuum limits from discrete structures cite this to confirm the leading-order match to the isotropic Laplacian eigenvalue. The proof unfolds the definition, applies the elementary bound 1 − y²/2 ≤ cos y, and rearranges algebraically.
Claim. For a > 0, (2/a²)(1 − cos(a k)) ≤ k².
background
The LorentzEmergence module derives rotationally invariant continuum physics from a cubic lattice Laplacian to address preferred-frame concerns. The single-axis dispersion is defined as (2/a²)(1 − cos(a k)). This rests on the structural conditions established by the from theorem in PrimitiveDistinction, which extracts four substantive conditions plus definitional facts from seven axioms. The module uses the standard Taylor inequality 1 − x²/2 ≤ cos x to bound each axis contribution.
proof idea
Unfolds the axis_dispersion definition, applies Real.one_sub_sq_div_two_le_cos to obtain 1 − cos(ak) ≤ (ak)²/2, uses linarith to rearrange, multiplies through by the positive factor 2/a² via mul_le_mul_of_nonneg_left, and simplifies the right-hand side to k² by field_simp.
why it matters
This bound feeds axis_dispersion_sandwich, which produces the sandwich 0 ≤ k² − axis_dispersion ≤ k², and dispersion_upper_bound_by_isotropic, which lifts the result to the full lattice dispersion ≤ continuum_isotropic. It supplies the key step showing the cubic ledger recovers the rotationally invariant |k|² at leading order, consistent with the eight-tick octave and D = 3 in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.