one_minus_cos_le_two
plain-language theorem explainer
The inequality 1 - cos y ≤ 2 holds for every real y. Lattice isotropy proofs cite it to upper-bound the dispersion relation in the Recognition Science foundation. The proof is a one-line linarith reduction from the standard bound cos y ≥ -1.
Claim. For all real numbers $y$, $1 - cos y ≤ 2$.
background
The Lattice Isotropy Bound module supplies the upper bound on 1 - cos y to complement the non-negativity result. Together they ensure lattice dispersion satisfies 0 ≤ 1 - cos y ≤ 2, which constrains the spectrum of the discrete Laplacian. The module follows the requirements of Beltracchi Response §6 for a non-negative and bounded dispersion relation.
proof idea
The tactic linarith is applied directly to the hypothesis Real.neg_one_le_cos y, which states cos y ≥ -1 and rearranges algebraically to the target inequality.
why it matters
The result feeds lattice_dispersion_bounded, which constructs the pair of bounds, and then populates latticeIsotropyCert. It supplies one of the two dispersion constraints required for the lattice isotropy certificate in the foundation layer, consistent with the D = 3 and eight-tick octave structure of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.