Prove2Me

The radicand is the same at qq and −q-q

Proved
PinnedAsymmetry.radicand_even

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

mathematical-physicstrigonometry

For all real K,c,β,qK, c, \beta, q,

(βcsin⁡(−q))2+K+2c (1−cos⁡(−q))=(βcsin⁡q)2+K+2c (1−cos⁡q).\bigl(\beta c \sin(-q)\bigr)^2 + K + 2c\,\bigl(1 - \cos(-q)\bigr) = \bigl(\beta c \sin q\bigr)^2 + K + 2c\,\bigl(1 - \cos q\bigr).

The quantity under the square root in ω(q)\omega(q) takes the same value in both propagation directions. This is why the stiffness KK cancels from the asymmetry.

Preamble
import Mathlib

open Real
Formal statement
namespace PinnedAsymmetry
theorem radicand_even (K c β q : ℝ) :
    (β * c * sin (-q)) ^ 2 + K + 2 * c * (1 - cos (-q))
      = (β * c * sin q) ^ 2 + K + 2 * c * (1 - cos 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)": 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

PinnedAsymmetry.radicand_even. Let K,c,β,qK, c, \beta, q be any four real numbers. There are no hypotheses. No sign, nonzero, or range conditions are imposed on any of them. The values K=0K = 0, c=0c = 0, β=0\beta = 0, negative values, and every real qq (read as an angle in radians, of any size) are all included. The statement asserts the identity

(β c sin⁡(−q))2+K+2c(1−cos⁡(−q))  =  (β c sin⁡q)2+K+2c(1−cos⁡q).\bigl(\beta\, c\, \sin(-q)\bigr)^2 + K + 2c\bigl(1 - \cos(-q)\bigr) \;=\; \bigl(\beta\, c\, \sin q\bigr)^2 + K + 2c\bigl(1 - \cos q\bigr).

Here sin⁡\sin and cos⁡\cos are the usual real sine and cosine. The expression on each side is a plain real-number sum. It is not placed under a square root or any other operation, and nothing is claimed about its sign. So the statement says only this: the real-valued expression f(q)=(βcsin⁡q)2+K+2c(1−cos⁡q)f(q) = (\beta c \sin q)^2 + K + 2c(1 - \cos q) takes the same value at −q-q as at qq, for all real K,c,β,qK, c, \beta, q. In other words, ff is an even function of qq for every choice of the parameters K,c,βK, c, \beta.

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