Foundation Lattice Isotropy Bound Lattice Dispersion Bounded

The lattice dispersion bound

The declaration lattice_dispersion_bounded establishes a simple but fundamental inequality about the cosine function: for any real number y, the quantity 1 - cos(y) is always between 0 and 2, inclusive. This is a basic fact of trigonometry, since the cosine of any angle lies between -1 and 1, so subtracting it from 1 gives a result between 0 and 2. The declaration proves this in a machine-checked library of formal theorems, meaning the proof has been verified step by step by a computer.

The bound matters because it constrains the dispersion relation, the mathematical rule that connects a wave's frequency to its wavelength, in lattice models. In such models, a discrete grid of points replaces continuous space, and the dispersion relation determines which frequencies are physically allowed. The inequality 0 ≤ 1 - cos(y) ≤ 2 ensures that the dispersion is non-negative and bounded above. A related theorem extends this to three dimensions: for a lattice with spacing a, the sum of three such terms, each multiplied by 2/a², is also non-negative. This guarantees that the lattice Laplacian, a discrete version of the second derivative, has a spectrum that is bounded below.

In Recognition Science, this bound appears as part of a structural argument about isotropy, the property of being the same in all directions. The framework models physical space as a discrete lattice, and the bound on the dispersion relation is a necessary condition for that lattice to behave isotropically at large scales. The declaration does not claim that the lattice is actually isotropic, nor does it prove that any particular physical system obeys this dispersion relation. It establishes only the mathematical inequality, which is a prerequisite for further analysis.

The practical consequence is that any lattice model that respects this bound has a well-defined ground state energy, since the dispersion cannot become negative. This is a necessary condition for the model to be physically sensible, but it is far from sufficient. The bound is a tool, not a conclusion.

theorem lattice_dispersion_bounded (y : ℝ) :
    0 ≤ 1 - Real.cos y ∧ 1 - Real.cos y ≤ 2 :=
  ⟨one_minus_cos_nonneg y, one_minus_cos_le_two y⟩

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)])

What this page does not claim

The lattice is actually isotropic, only that a necessary bound holds. Any particular physical system obeys this dispersion relation. The bound is sufficient for a well-defined ground state, only necessary.

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: