Prove2Me

ω(k)\omega(k) solves the qq-dimensional dispersion relation

Proved
PinnedAsymmetryQ.omega_is_root

by ShapeZero · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

latticemathematical-physicstrigonometry

Let q≥1q \ge 1, let K,c,βK, c, \beta be real, k∈Rqk \in \mathbb{R}^q, and suppose

(βcsin⁡k0)2+K+2c∑a(1−cos⁡ka)≥0.\bigl(\beta c \sin k_0\bigr)^2 + K + 2c \sum_{a} (1 - \cos k_a) \ge 0 .

Then ω=ω(k)\omega = \omega(k) satisfies

ω2−2βcsin⁡k0  ω−(K+2c∑a(1−cos⁡ka))=0,\omega^2 - 2\beta c \sin k_0\;\omega - \Bigl(K + 2c \sum_{a} (1 - \cos k_a)\Bigr) = 0,

so the formula is a genuine branch frequency of the qq-dimensional dispersion relation.

Preamble
import Mathlib
import Definitions.Def_PinnedAsymmetryQ_omega

open Real BigOperators
Formal statement
namespace PinnedAsymmetryQ
theorem omega_is_root (q : ℕ) [NeZero q] (K c β : ℝ) (k : Fin q → ℝ)
    (h : 0 ≤ (β * c * sin (k 0)) ^ 2 + K + 2 * c * ∑ a : Fin q, (1 - cos (k a))) :
    (omega q K c β k) ^ 2 - 2 * β * c * sin (k 0) * omega q K c β k
      - (K + 2 * c * ∑ a : Fin q, (1 - cos (k a))) = 0 := by sorry
end PinnedAsymmetryQ
Source
Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §7, Theorem 7.1 (extended to q axes): https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ShapeZero_C1_Formal_Proofs.pdf ; corrected in "Errata — C1 Formal Proofs (Sections 3 and 6)", "Related: the pinned asymmetry (Section 7)": https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ERRATUM_Theorem_6.1.md
Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. Let qq be a natural number with q≥1q \ge 1 (the only typeclass assumption, "q≠0q \neq 0"). Let K,c,βK, c, \beta be arbitrary real numbers (no sign or nonzero restrictions; each may be negative or zero), and let k=(k0,k1,…,kq−1)k = (k_0, k_1, \dots, k_{q-1}) be an arbitrary vector of real numbers indexed by {0,1,…,q−1}\{0, 1, \dots, q-1\}. Here k0k_0 is the entry at index 00, which exists because q≥1q \ge 1; sin⁡\sin and cos⁡\cos are the ordinary real sine and cosine (arguments in radians). Write

S  =  K+2c∑a=0q−1(1−cos⁡ka),b  =  β c sin⁡k0,D  =  b2+S=(βcsin⁡k0)2+K+2c∑a=0q−1(1−cos⁡ka).S \;=\; K + 2c\sum_{a=0}^{q-1}\bigl(1 - \cos k_a\bigr), \qquad b \;=\; \beta\, c\, \sin k_0, \qquad D \;=\; b^2 + S = (\beta c \sin k_0)^2 + K + 2c\sum_{a=0}^{q-1}\bigl(1-\cos k_a\bigr).

The defined quantity. The imported definition ω(q,K,c,β,k)\omega(q, K, c, \beta, k) is the real number

ω  =  βcsin⁡k0  +  D,\omega \;=\; \beta c \sin k_0 \;+\; \sqrt{D},

where ⋅\sqrt{\cdot} is Mathlib's total real square root: for D≥0D \ge 0 it is the unique nonnegative rr with r2=Dr^2 = D, and for D<0D < 0 it returns the junk value 00 (so for D<0D<0 the definition would give ω=βcsin⁡k0\omega = \beta c \sin k_0). The same definition file also defines an auxiliary map flip0\mathrm{flip0} (replacing k0k_0 by −k0-k_0 and leaving the other entries unchanged), but it does not occur in this statement.

Hypothesis. The single hypothesis is

D  =  (βcsin⁡k0)2+K+2c∑a=0q−1(1−cos⁡ka)  ≥  0,D \;=\; (\beta c \sin k_0)^2 + K + 2c\sum_{a=0}^{q-1}\bigl(1-\cos k_a\bigr) \;\ge\; 0,

i.e. exactly the argument of the square root is nonnegative, so the junk branch D<0D<0 is excluded. The hypothesis is satisfiable (e.g. c=0c = 0, K≥0K \ge 0), and is not automatic: e.g. c=0c = 0, K<0K < 0 violates it. No other constraints are imposed on K,c,β,kK, c, \beta, k.

Conclusion. Under these assumptions, the statement asserts the exact equality

ω2  −  2 βcsin⁡k0  ω  −  (K+2c∑a=0q−1(1−cos⁡ka))  =  0,\omega^2 \;-\; 2\,\beta c \sin k_0\;\omega \;-\; \Bigl(K + 2c\sum_{a=0}^{q-1}\bigl(1-\cos k_a\bigr)\Bigr) \;=\; 0,

that is, ω\omega is a root of the real quadratic x2−2bx−S=0x^2 - 2bx - S = 0. The statement asserts only that ω\omega satisfies this equation; it says nothing about the other root b−Db - \sqrt{D}, about which root ω\omega is (beyond what the definition gives), about uniqueness, or about the sign of ω\omega.

Degenerate cases included. The case q=1q = 1 is included (the sum has the single term 1−cos⁡k01 - \cos k_0). The case c=0c = 0 is included, where b=0b = 0, D=KD = K, and the hypothesis reduces to K≥0K \ge 0 with ω=K\omega = \sqrt{K}. The case β=0\beta = 0 or sin⁡k0=0\sin k_0 = 0 is included, where b=0b = 0 and ω=S\omega = \sqrt{S}. Negative cc and negative KK are allowed provided D≥0D \ge 0.

Human review

  • Endorsed by Shuze Chen · Sep 24, 2026

    Confirmed by the moderator at approval.

  • Endorsed by ShapeZero · Sep 24, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph