Foundation Lattice Isotropy Bound Lattice 3d Nonneg

The lattice bound

In solid-state physics, a lattice is a repeating grid of atoms or sites, and the lattice Laplacian is the standard way to measure how a quantity at one site differs from its neighbors. For a one-dimensional chain, the energy of a mode with wave number k is proportional to 1 - cos(k), a term that is always between 0 and 2. The lower bound means no mode has negative energy; the upper bound caps how much energy a mode can carry.

The same logic extends to three dimensions. If a lattice has spacing a and wave numbers k1, k2, k3 along the three axes, the total dispersion is the sum (2 / a²) times [(1 - cos(a k1)) + (1 - cos(a k2)) + (1 - cos(a k3))]. Because each cosine term is at most 1, each bracket is non-negative, so the whole sum is non-negative. That is exactly what the declaration lattice_3d_nonneg states: for any positive spacing a and any real wave numbers, the three-dimensional lattice dispersion is greater than or equal to zero.

This result is proved in the framework's machine-checked library of formal theorems, with no unproved assumptions. The proof is a direct application of the fact that cos(y) ≤ 1 for every real y, so 1 - cos(y) ≥ 0. The declaration also bundles this into a certificate structure that records the non-negativity and boundedness of the dispersion for all dimensions.

What the declaration does not claim is broader physical content. It does not assert that any particular lattice is stable, that waves propagate without loss, or that three dimensions are forced by this inequality alone. It is a mathematical bound on a specific expression, not a statement about the origin of spatial dimensions. The result is a tool: it guarantees that a basic lattice model never produces negative energy, which is a necessary sanity check for any further analysis.

theorem lattice_3d_nonneg (a k1 k2 k3 : ℝ) (ha : 0 < a) :
    0 ≤ (2 / a ^ 2) * ((1 - Real.cos (a * k1)) +
                        (1 - Real.cos (a * k2)) +
                        (1 - Real.cos (a * k3))) :=
  mul_nonneg (by positivity)
    (by linarith [one_minus_cos_nonneg (a * k1), one_minus_cos_nonneg (a * k2),
                  one_minus_cos_nonneg (a * k3)])

theorem one_minus_cos_nonneg (y : ℝ) : 0 ≤ 1 - Real.cos y :=
  by linarith [Real.cos_le_one y]

structure LatticeIsotropyCert where
  dispersion_nonneg : ∀ y : ℝ, 0 ≤ 1 - Real.cos y
  dispersion_bounded : ∀ y : ℝ, 1 - Real.cos y ≤ 2
  lattice_3d_nonneg : ∀ (a k1 k2 k3 : ℝ), 0 < a →
    0 ≤ (2 / a ^ 2) * ((1 - Real.cos (a * k1)) + (1 - Real.cos (a * k2)) + (1 - Real.cos (a * k3)))

What this page does not claim

This declaration does not prove that any lattice is dynamically stable. It does not claim that three dimensions are forced by this inequality alone. It does not address wave propagation, damping, or any time-dependent behavior.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/LatticeIsotropyBound.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: