Foundation Lattice Isotropy Bound

The lattice bound

The foundation lattice isotropy bound is a structural constraint on a discrete lattice, the kind of grid used to model a periodic medium. It states that a certain expression for lattice dispersion, written as ω², is never negative and never exceeds 2. The bound follows from a basic fact about the cosine function: for any real number y, the value of 1 - cos(y) lies between 0 and 2. This is not a deep result in itself; it is a standard inequality from trigonometry.

What matters is what the inequality controls. In lattice dynamics, the square of the frequency ω² is often expressed as a sum of terms like 1 - cos(a·k), where a is the lattice spacing and k is a wavevector component. The bound ensures that this sum is non-negative, which means the squared frequency cannot be negative. A negative squared frequency would imply an imaginary frequency, a sign of instability or an unphysical mode. The bound therefore guarantees a basic stability property for the lattice's vibrational spectrum.

In Recognition Science, the framework models physical structure as emerging from a discrete record of events, and it uses a lattice to represent spatial structure. The module LatticeIsotropyBound.lean formalizes the bound in a machine-checked library of formal statements. It proves three statements: the non-negativity of 1 - cos(y), its upper bound of 2, and a three-dimensional version where the sum of three such terms, scaled by 2/a², is non-negative for positive lattice spacing a. The library records zero unproved assumptions and zero axioms, meaning the proof is complete within its system.

The practical consequence is a constraint on the lattice Laplacian spectrum, the set of allowed frequencies for waves on the grid. The bound limits how the dispersion relation can behave, ruling out negative squared frequencies. This is a small but load-bearing piece of the framework's larger claim that three spatial dimensions are forced by its axioms; the bound is one of the structural facts that makes the lattice model consistent.

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

theorem one_minus_cos_le_two (y : ℝ) : 1 - Real.cos y ≤ 2 :=
  by linarith [Real.neg_one_le_cos 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)])

def latticeIsotropyCert : LatticeIsotropyCert where
  dispersion_nonneg := one_minus_cos_nonneg
  dispersion_bounded := one_minus_cos_le_two
  lattice_3d_nonneg := lattice_3d_nonneg

What this page does not claim

The bound does not by itself prove that three spatial dimensions are necessary; it is one structural constraint among others. The bound does not state that all lattice vibrations are stable, only that squared frequencies are non-negative. The module does not derive the value of the lattice spacing a from first principles.

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: