Prove2Me

The asymmetry is the same for any two stiffnesses K1K_1, K2K_2

Proved
PinnedAsymmetry.asymmetry_indep_K

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

mathematical-physicstrigonometry

Let K1,K2,c,β,qK_1, K_2, c, \beta, q be real numbers, and let

ωK(q)=βcsin⁡q+(βcsin⁡q)2+K+2c (1−cos⁡q)\omega_K(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 with on-site stiffness KK. Then

ωK1(q)−ωK1(−q)=ωK2(q)−ωK2(−q).\omega_{K_1}(q) - \omega_{K_1}(-q) = \omega_{K_2}(q) - \omega_{K_2}(-q).

This is the statement in the mission's title: the propagation asymmetry is the same for every value of the on-site stiffness. It follows from the goal, whose right-hand side 2βcsin⁡q2\beta c \sin q contains no KK.

Preamble
import Mathlib
import Definitions.Def_PinnedAsymmetry_omega

open Real
Formal statement
namespace PinnedAsymmetry
theorem asymmetry_indep_K (K₁ K₂ c β q : ℝ) :
    omega K₁ c β q - omega K₁ c β (-q) = omega K₂ c β q - omega K₂ c β (-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)" (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

Definition used (omega). For real numbers K,c,β,qK, c, \beta, q, the statement uses the function

ω(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, with qq in radians. The square root is Mathlib's total real square root:

  • for x≥0x \ge 0, x\sqrt{x} is the usual non-negative square root;
  • for x<0x < 0, x\sqrt{x} is defined to be 00 and does not produce an error.

So whenever the radicand (βcsin⁡q)2+K+2c(1−cos⁡q)(\beta c \sin q)^2 + K + 2c(1-\cos q) is negative, the value is ω(K,c,β,q)=βcsin⁡q\omega(K,c,\beta,q) = \beta c \sin q. Nothing constrains KK, cc, β\beta or qq in the definition. Each of them can be any real number, including zero or a negative number.

Theorem (asymmetry_indep_K). Let K1,K2,c,β,qK_1, K_2, c, \beta, q be any five real numbers. There are no hypotheses:

  • K1K_1 and K2K_2 may be equal or different, and positive, zero or negative;
  • cc and β\beta may be positive, zero or negative;
  • qq is any real number.

The theorem asserts the equality

ω(K1,c,β,q)−ω(K1,c,β,−q)  =  ω(K2,c,β,q)−ω(K2,c,β,−q).\omega(K_1, c, \beta, q) - \omega(K_1, c, \beta, -q) \;=\; \omega(K_2, c, \beta, q) - \omega(K_2, c, \beta, -q).

Written out in full, with ⋅\sqrt{\cdot} meaning the truncated square root described above, the claim is

[βcsin⁡q+(βcsin⁡q)2+K1+2c(1−cos⁡q)]−[βcsin⁡(−q)+(βcsin⁡(−q))2+K1+2c(1−cos⁡(−q))]\Big[\beta c \sin q + \sqrt{(\beta c \sin q)^2 + K_1 + 2c(1-\cos q)}\Big] - \Big[\beta c \sin(-q) + \sqrt{(\beta c \sin(-q))^2 + K_1 + 2c(1-\cos(-q))}\Big] =[βcsin⁡q+(βcsin⁡q)2+K2+2c(1−cos⁡q)]−[βcsin⁡(−q)+(βcsin⁡(−q))2+K2+2c(1−cos⁡(−q))].= \Big[\beta c \sin q + \sqrt{(\beta c \sin q)^2 + K_2 + 2c(1-\cos q)}\Big] - \Big[\beta c \sin(-q) + \sqrt{(\beta c \sin(-q))^2 + K_2 + 2c(1-\cos(-q))}\Big].

In words, the difference between ω\omega at qq and at −q-q, with cc and β\beta fixed, is claimed to be the same for any two values of the parameter KK.

The claim covers the edge cases in which a radicand is negative, so that the corresponding square root is 00. It also covers q=0q = 0, where both sides are differences of equal terms. For reference, sin⁡(−q)=−sin⁡q\sin(-q) = -\sin q and cos⁡(−q)=cos⁡q\cos(-q) = \cos q, so for each KK the two radicands in a bracket pair are the same expression.

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