one_minus_cos_nonneg
plain-language theorem explainer
The inequality 0 ≤ 1 - cos(y) for real y supplies the non-negativity of lattice dispersion in the Recognition Science foundation. It is cited to build the three-dimensional lattice Laplacian bound and the isotropy certificate. The proof is a one-line application of the standard cosine upper bound via linear arithmetic.
Claim. For every real number $y$, $0 ≤ 1 - cos y$.
background
The Lattice Isotropy Bound module records the key structural claim that lattice dispersion satisfies 0 ≤ ω². This follows from 1 - cos(y) ≥ 0, as stated in the module documentation. The same module records the companion upper bound 1 - cos(y) ≤ 2; together they constrain the spectrum of the lattice Laplacian. No additional upstream theorems are required beyond the library fact that cosine is at most one.
proof idea
The proof is a one-line wrapper that applies linarith to the library lemma Real.cos_le_one y, which states cos y ≤ 1 and rearranges directly to the target inequality.
why it matters
This result populates the dispersion_nonneg field inside latticeIsotropyCert and is invoked by lattice_dispersion_bounded and lattice_3d_nonneg. It supplies the lower bound half of the lattice dispersion estimate in Beltracchi Response §6. In the Recognition framework it anchors the non-negativity of the lattice model that supports the derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.