Prove2Me

The propagation asymmetry ω(q)−ω(−q)=2βcsin⁡q\omega(q) - \omega(-q) = 2\beta c \sin q is independent of KK

Proved
PinnedAsymmetry.asymmetry

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

mathematical-physicstrigonometry

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

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

be the upper-branch frequency on a uniform ring. Then

ω(q)−ω(−q)=2βcsin⁡q.\omega(q) - \omega(-q) = 2\beta c \sin q .

The difference between the two propagation directions contains no KK: the asymmetry is pinned, even though each frequency depends on the on-site stiffness. The statement concerns the linear asymmetry on a uniform lattice only.

Preamble
import Mathlib
import Definitions.Def_PinnedAsymmetry_omega

open Real
Formal statement
namespace PinnedAsymmetry
theorem asymmetry (K c β q : ℝ) :
    omega K c β q - omega K c β (-q) = 2 * β * c * sin q := 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

Auxiliary function ω\omega. For real numbers K,c,β,qK, c, \beta, q, the definition sets

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

Here sin⁡\sin and cos⁡\cos are the real sine and cosine, and qq is in radians. The square root is the real square root extended to all of R\mathbb{R}. For radicand x≥0x \ge 0 it returns the nonnegative root x\sqrt{x}. For radicand x<0x < 0 it returns 00 and gives no error. So whenever (βcsin⁡q)2+K+2c(1−cos⁡q)<0(\beta c \sin q)^2 + K + 2c(1-\cos q) < 0, which can happen for example when KK is negative enough, ω(K,c,β,q)\omega(K,c,\beta,q) is just βcsin⁡q\beta c \sin q. No sign, positivity or range conditions are placed on any of K,c,β,qK, c, \beta, q.

Theorem (PinnedAsymmetry.asymmetry). For every choice of four real numbers K,c,β,q∈RK, c, \beta, q \in \mathbb{R}, with no hypotheses at all, the following equation holds:

ω(K,c,β,q)  −  ω(K,c,β,−q)  =  2 β c sin⁡q.\omega(K,c,\beta,q) \;-\; \omega(K,c,\beta,-q) \;=\; 2\,\beta\, c\,\sin q .

Written out with the definition in place, the claim is:

[βcsin⁡q+(βcsin⁡q)2+K+2c(1−cos⁡q)]  −  [βcsin⁡(−q)+(βcsin⁡(−q))2+K+2c(1−cos⁡(−q))]  =  2βcsin⁡q,\Big[\beta c \sin q + \sqrt{(\beta c \sin q)^2 + K + 2c(1-\cos q)}\Big] \;-\; \Big[\beta c \sin(-q) + \sqrt{(\beta c \sin(-q))^2 + K + 2c(1-\cos(-q))}\Big] \;=\; 2\beta c \sin q,

In this equation each ⋅\sqrt{\cdot} follows the convention above: it gives 00 for a negative radicand. The statement is an unconditional equality of real numbers. It is quantified over all real KK (including negative values and zero), all real cc (including c≤0c \le 0), all real β\beta (including β=0\beta = 0) and all real qq (not limited to any interval). In the last case, β=0\beta = 0 or c=0c = 0, the right-hand side is 00.

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