IndisputableMonolith.Foundation.LatticeIsotropyBound

   1import Mathlib
   2
   3/-!
   4# Lattice Isotropy Bound — Beltracchi Response §6
   5
   6Key structural bound: lattice dispersion is non-negative (0 ≤ ω²).
   7This follows from 1 - cos(y) ≥ 0.
   8
   9Also: 1 - cos(y) ≤ 2 (bounded above).
  10
  11Together these constrain the lattice Laplacian spectrum.
  12
  13Lean status: 0 sorry, 0 axiom.
  14-/
  15
  16namespace IndisputableMonolith.Foundation.LatticeIsotropyBound
  17
  18theorem one_minus_cos_nonneg (y : ℝ) : 0 ≤ 1 - Real.cos y :=
  19  by linarith [Real.cos_le_one y]
  20
  21theorem one_minus_cos_le_two (y : ℝ) : 1 - Real.cos y ≤ 2 :=
  22  by linarith [Real.neg_one_le_cos y]
  23
  24theorem lattice_dispersion_bounded (y : ℝ) :
  25    0 ≤ 1 - Real.cos y ∧ 1 - Real.cos y ≤ 2 :=
  26  ⟨one_minus_cos_nonneg y, one_minus_cos_le_two y⟩
  27
  28theorem lattice_3d_nonneg (a k1 k2 k3 : ℝ) (ha : 0 < a) :
  29    0 ≤ (2 / a ^ 2) * ((1 - Real.cos (a * k1)) +
  30                        (1 - Real.cos (a * k2)) +
  31                        (1 - Real.cos (a * k3))) :=
  32  mul_nonneg (by positivity)
  33    (by linarith [one_minus_cos_nonneg (a * k1), one_minus_cos_nonneg (a * k2),
  34                  one_minus_cos_nonneg (a * k3)])
  35
  36structure LatticeIsotropyCert where
  37  dispersion_nonneg : ∀ y : ℝ, 0 ≤ 1 - Real.cos y
  38  dispersion_bounded : ∀ y : ℝ, 1 - Real.cos y ≤ 2
  39  lattice_3d_nonneg : ∀ (a k1 k2 k3 : ℝ), 0 < a →
  40    0 ≤ (2 / a ^ 2) * ((1 - Real.cos (a * k1)) + (1 - Real.cos (a * k2)) + (1 - Real.cos (a * k3)))
  41
  42def latticeIsotropyCert : LatticeIsotropyCert where
  43  dispersion_nonneg := one_minus_cos_nonneg
  44  dispersion_bounded := one_minus_cos_le_two
  45  lattice_3d_nonneg := lattice_3d_nonneg
  46
  47end IndisputableMonolith.Foundation.LatticeIsotropyBound
  48