Foundation Lattice Isotropy Bound One Minus Cos Le Two

The bounded step

The cosine function oscillates between -1 and 1. Subtract its value from 1, and the result measures how far the angle has swung from zero: at zero it is 0, at a quarter turn it is 1, and at a half turn it reaches 2. The quantity 1 - cos(y) therefore never falls below 0 and never rises above 2. That second bound, the upper ceiling of 2, is the content of the declaration one_minus_cos_le_two.

In the Recognition Science framework, which treats physical structure as the record of discrete recognition events, this bound constrains the lattice Laplacian, the standard discrete version of the curvature operator. The framework's machine-checked library of formal theorems proves both the lower bound (0 ≤ 1 - cos(y)) and the upper bound (1 - cos(y) ≤ 2) for every real number y. Together they confine the lattice dispersion, the spread of allowed energy-like values, to the interval [0, 2]. A separate theorem assembles these into a certificate that the three-dimensional lattice Laplacian stays non-negative when the lattice spacing is positive.

The declaration does not claim that any particular physical lattice exists, nor that the bound is tight. It does not say that the cosine's range is the reason for three spatial dimensions; that forcing chain lives elsewhere in the framework and depends on additional structure. What the bound establishes is narrower and fully general: for any real angle, the quantity 1 - cos(y) cannot exceed 2. That is a fact about elementary trigonometry, verified with zero axioms beyond the standard logical ones, and it is the load-bearing ceiling for the framework's lattice spectrum.

The practical consequence is that the framework's lattice model has a finite band of allowed dispersion values. A reader can now see why the framework's lattice calculations stay bounded without invoking any physical measurement: the ceiling is a theorem about the cosine function itself.

theorem one_minus_cos_le_two (y : ℝ) : 1 - Real.cos y ≤ 2 :=
  by linarith [Real.neg_one_le_cos y]

theorem one_minus_cos_nonneg (y : ℝ) : 0 ≤ 1 - Real.cos y :=
  by linarith [Real.cos_le_one 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 bound does not prove that any physical lattice exists. The bound does not by itself force three spatial dimensions; that requires the separate linking chain. The bound does not say the cosine's range is the reason for the framework's constants.

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: