isotropic_envelope_rotation_invariant
plain-language theorem explainer
The theorem establishes that for any two wavevectors of equal magnitude squared the cubic-lattice dispersion is bounded above by the same rotationally invariant continuum Laplacian eigenvalue. Researchers constructing continuum limits from discrete lattices cite it to confirm absence of leading-order rotational anisotropy. The proof is a one-line wrapper that rewrites the equal-magnitude hypothesis and invokes the dispersion upper bound lemma.
Claim. Let $a>0$. For $k,k' : Fin 3 → ℝ$ with $∑_{i=1}^3 k_i^2 = ∑_{i=1}^3 k'_i^2$, the lattice dispersion satisfies $∑_{i=1}^3 (2/a^2)(1 - cos(a k_i)) ≤ ∑_{i=1}^3 k'_i^2$.
background
The module derives Lorentz emergence from a cubic ledger to address Beltracchi §8 on preferred frames. Core definitions are axis_dispersion(a,k) = (2/a²)(1 - cos(a k)) for a single axis and continuum_isotropic(k) = ∑_{i=1}^3 k_i² for the rotationally invariant continuum eigenvalue; the full dispersion is the sum of the three axis terms. The local setting uses the momentum-space cubic Laplacian bounded above by the isotropic |k|² via the Taylor inequality 1 - cos(x) ≤ x²/2. Upstream, dispersion_upper_bound_by_isotropic supplies the single-vector upper bound that this theorem extends to equal-magnitude pairs.
proof idea
The proof is a one-line wrapper. It rewrites the hypothesis continuum_isotropic k = continuum_isotropic k' into the target inequality, then applies the lemma dispersion_upper_bound_by_isotropic a ha k.
why it matters
This populates the envelope_isotropic slot of lorentzEmergenceCert, the structure that certifies emergence of rotationally invariant physics. It fills the module step showing the cubic lattice introduces no rotational anisotropy at leading order, directly supporting the continuum limit in which D = 3 yields isotropic dispersion. In the Recognition framework it closes one link in the chain from discrete ledger to continuum Lorentz symmetry without preferred directions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.