Prove2Me

The radicand is unchanged by reversing axis 0

Proved
PinnedAsymmetryQ.radicand_flip

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

latticemathematical-physicstrigonometry

For q≥1q \ge 1, all real K,c,βK, c, \beta and every k∈Rqk \in \mathbb{R}^q, with kˉ=(−k0,k1,…,kq−1)\bar k = (-k_0, k_1, \dots, k_{q-1}),

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

The quantity under the square root takes the same value for both propagation directions, since sin⁡2(−k0)=sin⁡2k0\sin^2(-k_0) = \sin^2 k_0, cos⁡(−k0)=cos⁡k0\cos(-k_0) = \cos k_0, and the transverse terms are untouched.

Preamble
import Mathlib
import Definitions.Def_PinnedAsymmetryQ_omega

open Real BigOperators
Formal statement
namespace PinnedAsymmetryQ
theorem radicand_flip (q : ℕ) [NeZero q] (K c β : ℝ) (k : Fin q → ℝ) :
    (β * c * sin (flip0 q k 0)) ^ 2 + K + 2 * c * ∑ a : Fin q, (1 - cos (flip0 q k a))
      = (β * c * sin (k 0)) ^ 2 + K + 2 * c * ∑ a : Fin q, (1 - cos (k a)) := 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≠0q \neq 0 (this is the only assumption on qq; it guarantees that the index set {0,1,…,q−1}\{0, 1, \dots, q-1\} is nonempty, so the index 00 exists; q=1q = 1 is allowed). Let K,c,β∈RK, c, \beta \in \mathbb{R} be arbitrary real numbers with no sign, size or nonvanishing conditions (in particular KK may be negative and cc or β\beta may be 00). Let k=(k0,k1,…,kq−1)∈Rqk = (k_0, k_1, \dots, k_{q-1}) \in \mathbb{R}^q be an arbitrary real vector indexed by a∈{0,…,q−1}a \in \{0, \dots, q-1\}. There are no further hypotheses.

The flip. Define the vector k~∈Rq\tilde k \in \mathbb{R}^q (the file's flip0) as kk with only its 00-th entry replaced by its negative, all other entries unchanged:

k~a={−k0,a=0,ka,a≠0.\tilde k_a = \begin{cases} -k_0, & a = 0, \\ k_a, & a \neq 0. \end{cases}

When q=1q = 1, this is simply k~=(−k0)\tilde k = (-k_0).

Claim. For all such q,K,c,β,kq, K, c, \beta, k, the following equality of real numbers holds:

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

where sin⁡,cos⁡\sin, \cos are the real sine and cosine (arguments in radians) and k~0=−k0\tilde k_0 = -k_0. That is, the expression R(k)=(βcsin⁡k0)2+K+2c∑a(1−cos⁡ka)R(k) = (\beta c \sin k_0)^2 + K + 2c\sum_a (1-\cos k_a) takes the same value at kk and at k~\tilde k. This is an exact equality of the raw expressions; no square root is taken and no nonnegativity of either side is asserted or assumed.

Context from the imported file. The expression R(k)R(k) is exactly the quantity inside the square root in the imported definition

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

where ⋅\sqrt{\cdot} is Mathlib's real square root, which returns 00 for negative inputs. However, the theorem itself does not mention ω\omega; it states only the equality of the two radicand expressions displayed above.

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