The asymmetry is the same for any two stiffnesses $K_1$ , $K_2$

Proved

PinnedAsymmetryQ.asymmetry_indep_K

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

latticemathematical-physicstrigonometry

Let $q \ge 1$ , $K_1, K_2, c, \beta$ real and $k \in \mathbb{R}^q$ . Writing $\omega_K$ for the frequency with stiffness $K$ and $\bar k$ for the reversal along axis 0,

\omega_{K_1}(k) - \omega_{K_1}(\bar k) = \omega_{K_2}(k) - \omega_{K_2}(\bar k).

This is the stiffness-independence stated in the mission title.

Preamble

import Mathlib
import Definitions.Def_PinnedAsymmetryQ_omega

open Real BigOperators

Formal statement

namespace PinnedAsymmetryQ
theorem asymmetry_indep_K (q : ℕ) [NeZero q] (K₁ K₂ c β : ℝ) (k : Fin q → ℝ) :
    omega q K₁ c β k - omega q K₁ c β (flip0 q k)
      = omega q K₂ c β k - omega q K₂ c β (flip0 q k) := 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)" (stiffness cancels): 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

Theorem PinnedAsymmetryQ.asymmetry_indep_K. Let $q$ be a natural number with $q \neq 0$ (a standing typeclass assumption), so that the index set $\{0, 1, \dots, q-1\}$ is nonempty and contains the index $0$ . Let $K_1, K_2, c, \beta$ be arbitrary real numbers, and let $k = (k_0, k_1, \dots, k_{q-1}) \in \mathbb{R}^q$ be an arbitrary real vector indexed by $\{0, \dots, q-1\}$ . No other hypotheses are made: $K_1, K_2, c, \beta$ may be zero, negative or positive, and $k$ is unrestricted.

The statement uses two auxiliary definitions. For a real parameter $K$ (with $q, c, \beta$ as above), the function $\omega_K : \mathbb{R}^q \to \mathbb{R}$ is

\omega_K(k) \;=\; \beta c \sin(k_0) \;+\; \sqrt{\;(\beta c \sin k_0)^2 + K + 2c \sum_{a=0}^{q-1} \bigl(1 - \cos k_a\bigr)\;}\,,

where $\sqrt{\cdot}$ is Mathlib's total square root on $\mathbb{R}$ : it returns the usual nonnegative square root when its argument is $\ge 0$ , and returns $0$ whenever its argument is negative (so no condition is imposed ensuring the radicand is nonnegative; a negative radicand silently yields the value $0$ for the square-root term). The flip map $F : \mathbb{R}^q \to \mathbb{R}^q$ negates only the $0$ -th coordinate and leaves all others unchanged:

F(k)_0 = -k_0, \qquad F(k)_a = k_a \quad (a = 1, \dots, q-1).

(When $q = 1$ , $F(k) = (-k_0)$ and the sum in $\omega_K$ has the single term $1 - \cos k_0$ .)

The theorem asserts the equality of real numbers

\omega_{K_1}(k) - \omega_{K_1}\bigl(F(k)\bigr) \;=\; \omega_{K_2}(k) - \omega_{K_2}\bigl(F(k)\bigr),

for every $q \ge 1$ , all real $K_1, K_2, c, \beta$ and every $k \in \mathbb{R}^q$ ; that is, the difference $\omega_K(k) - \omega_K(F(k))$ takes the same value for any two choices of the parameter $K$ , with $q, c, \beta, k$ held fixed. Written out fully, the left side is

\Bigl[\beta c \sin k_0 + \sqrt{(\beta c \sin k_0)^2 + K_1 + 2c\textstyle\sum_{a}(1-\cos k_a)}\Bigr] - \Bigl[\beta c \sin(-k_0) + \sqrt{(\beta c \sin(-k_0))^2 + K_1 + 2c\bigl((1-\cos(-k_0)) + \textstyle\sum_{a\neq 0}(1-\cos k_a)\bigr)}\Bigr],

and the right side is the same expression with $K_1$ replaced by $K_2$ , each square root being interpreted as $0$ when its argument is negative.

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

The asymmetry is the same for any two stiffnesses K1K_1K1​, K2K_2K2​

The asymmetry is the same for any two stiffnesses $K_1$ , $K_2$