The propagation asymmetry $\omega(k) - \omega(\bar k) = 2\beta c \sin k_0$ on a $q$-dimensional lattice

Theorem PinnedAsymmetryQ.asymmetry. Fix a natural number $q$ with $q \neq 0$ (the only hypothesis; it guarantees that the index set $\{0, 1, \dots, q-1\}$ is nonempty and contains $0$; the case $q = 1$, where $0$ is the only index, is included). Fix arbitrary real numbers $K$, $c$, $\beta$ (no sign, nonzero or other conditions: $K$ may be negative, and $c$ or $\beta$ may be zero or negative). Fix an arbitrary real vector $k = (k_0, k_1, \dots, k_{q-1}) \in \mathbb{R}^q$, indexed by $a \in \{0, \dots, q-1\}$, with no conditions on its entries (they are not reduced modulo $2\pi$ or restricted in any way).

The function $\omega$ used in the statement is defined, for such $q, K, c, \beta, k$, by

where $\sqrt{\cdot}$ is Mathlib's real square root: for $x \ge 0$ it is the usual non-negative square root, and for $x < 0$ it returns $0$ (no error, no complex value). So whenever the radicand is negative, $\omega(k) = \beta c \sin k_0$. The sum runs over all $q$ indices, including $a = 0$.

The operation $\mathrm{flip}_0$ takes the vector $k$ and replaces only its $0$-th entry by its negative, leaving all other entries unchanged:

(When $q = 1$, $\mathrm{flip}_0(k) = (-k_0)$.) Thus, written out,

with the same convention for the square root of a negative number.

The theorem asserts that, for every such $q$, $K$, $c$, $\beta$ and $k$, the following exact equality of real numbers holds:

Here $\sin$ and $\cos$ are the real sine and cosine. There are no further hypotheses; the equality is claimed for all parameter values, including those where the radicands are negative (square roots then equal $0$) and degenerate values such as $c = 0$, $\beta = 0$, or $k_0 \in \pi\mathbb{Z}$, where the right-hand side is $0$.