Upper-branch frequency $\omega(q)$ on a uniform gyroscopic ring

Definition

PinnedAsymmetry_omega

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

mathematical-physicstrigonometry

Fix real numbers $K$ (on-site stiffness), $c$ (neighbour coupling), $\beta$ (gyroscopic strength) and a wavenumber $q$ . The upper-branch frequency of a wave with wavenumber $q$ on a uniform ring is

\omega(q) = \beta c \sin q + \sqrt{\bigl(\beta c \sin q\bigr)^2 + K + 2c\,(1 - \cos q)} .

When the quantity under the square root is non-negative, $\omega(q)$ is a root of the dispersion relation $\omega^2 - 2\beta c \sin q\,\omega - (K + 2c(1-\cos q)) = 0$ (milestone M1).

Formalization Note The square root is Real.sqrt, which returns $0$ on negative inputs; no sign conditions are placed on $K, c, \beta, q$ .

Definition code

import Mathlib

open Real

namespace PinnedAsymmetry

/-- Upper-branch frequency on a uniform ring: stiffness K, neighbour coupling c,
gyroscopic strength β, wavenumber q. -/
noncomputable def omega (K c β q : ℝ) : ℝ :=
  β * c * sin q + Real.sqrt ((β * c * sin q) ^ 2 + K + 2 * c * (1 - cos q))

end PinnedAsymmetry

Source

Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §7, Theorem 7.1 (dispersion relation): 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

Definition PinnedAsymmetry.omega. This defines a real-valued function $\omega$ of four real arguments $K, c, \beta, q \in \mathbb{R}$ , in that order. Nothing restricts the arguments: $K$ , $c$ and $\beta$ can be any real numbers, including zero and negative values, and $q$ is any real number used as an angle in radians inside the real sine and cosine. Write

A \;=\; \beta\, c\, \sin q, \qquad R \;=\; A^2 + K + 2c\,(1 - \cos q).

The definition is

\omega(K, c, \beta, q) \;=\; A + \operatorname{sqrt}(R) \;=\; \beta c \sin q \;+\; \operatorname{sqrt}\!\Big( (\beta c \sin q)^2 + K + 2c\,(1-\cos q) \Big).

Here $\operatorname{sqrt}$ is Mathlib's total real square root. For $x > 0$ it returns the unique nonnegative $y$ with $y^2 = x$ . For every $x \le 0$ it returns exactly $0$ , with no error and no complex value. Its output is always $\ge 0$ . Only the " $+$ " branch of the root appears. Nothing in the definition selects a " $-$ " branch, and there is no division.

Edge cases the definition allows:

The radicand is at most zero. This happens when $R \le 0$ . Since $A^2 \ge 0$ and $1 - \cos q \ge 0$ , $R$ can be negative only if $K < 0$ , or if $c < 0$ with $\cos q \ne 1$ . In that case the square root silently becomes $0$ and $\omega(K,c,\beta,q) = \beta c \sin q$ .
The sign of $\omega$ . If $K + 2c(1-\cos q) \ge 0$ , then $\operatorname{sqrt}(R) \ge |A|$ , so $\omega \ge 0$ . If $K + 2c(1-\cos q) < 0$ and $A < 0$ , then $\omega$ is negative.
Special values.
- When $q$ is a multiple of $2\pi$ , $\sin q = 0$ and $\cos q = 1$ , so $\omega = \operatorname{sqrt}(K)$ . This equals $\sqrt{K}$ when $K \ge 0$ and $0$ when $K < 0$ .
- When $\beta = 0$ or $c = 0$ , $A = 0$ , so $\omega = \operatorname{sqrt}\big(K + 2c(1-\cos q)\big)$ .
- When $c = 0$ , this reduces further to $\omega = \operatorname{sqrt}(K)$ for every $\beta$ and $q$ .

The declaration is marked noncomputable. It is only a definition and asserts no property of $\omega$ .

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

Upper-branch frequency ω(q)\omega(q)ω(q) on a uniform gyroscopic ring

Upper-branch frequency $\omega(q)$ on a uniform gyroscopic ring