lattice_dispersion_bounded
plain-language theorem explainer
The theorem establishes that for any real y the quantity 1 minus cosine y lies between zero and two. Lattice modelers in Recognition Science cite the bound to guarantee that lattice dispersion remains non-negative and finite. The proof is a direct term pairing of the two elementary cosine inequalities already proved in the same module.
Claim. For every real number $y$, $0 ≤ 1 - cos y$ and $1 - cos y ≤ 2$.
background
The Lattice Isotropy Bound module records the structural fact that lattice dispersion satisfies 0 ≤ ω² because 1 - cos(y) ≥ 0, together with the upper bound 1 - cos(y) ≤ 2. These two inequalities jointly constrain the spectrum of the lattice Laplacian. The local setting is the Beltracchi Response §6, whose purpose is to secure isotropy properties for the lattice model in Recognition Science.
proof idea
The proof is a one-line term wrapper that applies the sibling lemmas one_minus_cos_nonneg and one_minus_cos_le_two to assemble the required conjunction.
why it matters
This result supplies the elementary bounds that keep the lattice Laplacian spectrum non-negative and bounded, a prerequisite for the isotropy certification in three dimensions. It directly supports the downstream construction of lattice_3d_nonneg and LatticeIsotropyCert. Within the Recognition framework the bound contributes to the forcing chain that fixes D = 3 by ensuring the lattice dispersion relation remains well-behaved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.