Prove2Me

ω(q)\omega(q) solves the dispersion relation

Proved
PinnedAsymmetry.omega_is_root

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

mathematical-physicstrigonometry

Let K,c,β,qK, c, \beta, q be real numbers with

(βcsin⁡q)2+K+2c (1−cos⁡q)≥0.\bigl(\beta c \sin q\bigr)^2 + K + 2c\,(1 - \cos q) \ge 0 .

Then the upper-branch frequency ω=ω(q)=βcsin⁡q+(βcsin⁡q)2+K+2c(1−cos⁡q)\omega = \omega(q) = \beta c \sin q + \sqrt{(\beta c \sin q)^2 + K + 2c(1-\cos q)} satisfies the dispersion relation

ω2−2βcsin⁡q  ω−(K+2c (1−cos⁡q))=0.\omega^2 - 2\beta c \sin q\;\omega - \bigl(K + 2c\,(1 - \cos q)\bigr) = 0 .

This ties the formula to the physics: it shows ω(q)\omega(q) is a genuine branch frequency of the model, so that the goal is a statement about the physical frequency rather than an arbitrary expression.

Preamble
import Mathlib
import Definitions.Def_PinnedAsymmetry_omega

open Real
Formal statement
namespace PinnedAsymmetry
theorem omega_is_root (K c β q : ℝ)
    (h : 0 ≤ (β * c * sin q) ^ 2 + K + 2 * c * (1 - cos q)) :
    (omega K c β q) ^ 2 - 2 * β * c * sin q * omega K c β q
      - (K + 2 * c * (1 - cos q)) = 0 := by sorry
end PinnedAsymmetry
Source
Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §7, Theorem 7.1: 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

PinnedAsymmetry.omega_is_root. Let K,c,β,qK, c, \beta, q be arbitrary real numbers. There are no other binders, no implicit arguments and no typeclass assumptions. sin⁡\sin and cos⁡\cos are the ordinary real sine and cosine, with qq read as an angle in radians. Write

b:=β csin⁡q,D:=K+2c (1−cos⁡q),Δ:=b2+D=(βcsin⁡q)2+K+2c(1−cos⁡q).b := \beta\, c \sin q, \qquad D := K + 2c\,(1 - \cos q), \qquad \Delta := b^2 + D = (\beta c \sin q)^2 + K + 2c(1-\cos q).

The imported definition ω(K,c,β,q)\omega(K,c,\beta,q) is total. It is defined for every real input as

ω(K,c,β,q)=βcsin⁡q+(βcsin⁡q)2+K+2c(1−cos⁡q)=b+Δ.\omega(K,c,\beta,q) = \beta c \sin q + \sqrt{(\beta c \sin q)^2 + K + 2c(1-\cos q)} = b + \sqrt{\Delta}.

Here ⋅\sqrt{\cdot} is Mathlib's real square root. For x≥0x \ge 0 it returns the unique non-negative real number yy with y2=xy^2 = x, which is the principal root. For every x<0x < 0 it returns the value 00. It never fails and never returns a complex value. So the definition always picks the "++" root, and when Δ<0\Delta < 0 it silently gives ω=b\omega = b.

The theorem takes one hypothesis:

Δ=(βcsin⁡q)2+K+2c(1−cos⁡q)  ≥  0(non-strict inequality).\Delta = (\beta c \sin q)^2 + K + 2c(1-\cos q) \;\ge\; 0 \quad \text{(non-strict inequality)}.

Under this hypothesis, Δ\sqrt{\Delta} is the genuine non-negative square root of Δ\Delta. The hypothesis is satisfiable, for example with K≥0K \ge 0 and c≥0c \ge 0, since 1−cos⁡q≥01 - \cos q \ge 0. It also holds for some negative KK or cc, provided the whole sum is non-negative. The theorem concludes the exact equality

ω2−2βcsin⁡q⋅ω−(K+2c(1−cos⁡q))=0,ω=ω(K,c,β,q).\omega^2 - 2\beta c \sin q \cdot \omega - \bigl(K + 2c(1-\cos q)\bigr) = 0, \qquad \omega = \omega(K,c,\beta,q).

In other words, ω\omega is a root of the quadratic x2−2b x−D=0x^2 - 2b\,x - D = 0 in xx. The statement says only that this particular value, b+Δb + \sqrt{\Delta}, is a root. It says nothing about the other root, b−Δb - \sqrt{\Delta}, and nothing about the sign of ω\omega or whether the root is unique. It makes no claim when Δ<0\Delta < 0, because the hypothesis excludes that case. Degenerate cases are included, for example c=0c = 0, or β=0\beta = 0, or sin⁡q=0\sin q = 0, where b=0b = 0 and ω=K+2c(1−cos⁡q)\omega = \sqrt{K + 2c(1-\cos q)}.

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