LatticeIsotropyCert
plain-language theorem explainer
LatticeIsotropyCert packages the elementary bounds 1 - cos y ≥ 0, 1 - cos y ≤ 2, and their three-dimensional lattice sum into a single record. A researcher modeling discrete spacetime or lattice regularizations would cite it to guarantee that the dispersion relation remains non-negative for real wave-vectors. The declaration is a direct record constructor that assembles three already-proved trigonometric inequalities without further reasoning.
Claim. A structure certifying lattice dispersion bounds: for every real $y$, $0 ≤ 1 - cos y ≤ 2$, and for every $a > 0$ and reals $k_1,k_2,k_3$, $0 ≤ (2/a^2) [(1 - cos(a k_1)) + (1 - cos(a k_2)) + (1 - cos(a k_3))]$.
background
The Lattice Isotropy Bound module establishes structural control on the cubic-lattice dispersion relation ω² = (2/a²) Σ (1 - cos(a k_i)). Non-negativity follows from the elementary inequality 1 - cos y ≥ 0, which holds because cosine is concave and reaches its maximum at zero. The module also records the trivial upper bound 1 - cos y ≤ 2. Upstream, the theorem lattice_3d_nonneg proves the summed three-dimensional case by applying the one-dimensional bound componentwise and scaling by the positive prefactor 2/a². The imported result dispersion_nonneg from LorentzEmergence performs the identical summation over Fin 3 axes.
proof idea
The structure is populated by direct field assignment inside the record constructor. The field dispersion_nonneg receives the theorem one_minus_cos_nonneg, dispersion_bounded receives one_minus_cos_le_two, and lattice_3d_nonneg receives the already-established lattice_3d_nonneg theorem. No tactics or reductions occur beyond the record syntax itself.
why it matters
The certificate is consumed by the downstream definition latticeIsotropyCert, which supplies the packaged bounds to any later argument that needs a non-negative, bounded lattice Laplacian spectrum. It directly implements the module claim that lattice dispersion is non-negative (0 ≤ ω²) and bounded above, thereby constraining the discrete spectrum before continuous limits are taken. In the Recognition Science setting this supplies the trigonometric foundation required prior to invoking the phi-ladder mass formula or the eight-tick octave that forces D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.