Symmetric links are passive

Proved

PassivityRing.passive_of_symm

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

linear-algebramatrices

Let $N \ge 1$ and $d$ be natural numbers and let $W_0, \dots, W_{N-1}$ be real $d\times d$ matrices with $W_i^{\mathsf T} = W_i$ for every $i$ . Then for every choice of velocities $v_0, \dots, v_{N-1} \in \mathbb{R}^d$ (indices modulo $N$ ),

\sum_{i} v_i \cdot \bigl( W_i\, v_{i+1} - W_{i-1}\, v_{i-1} \bigr) = 0 .

This is the "if" direction of the goal, and it holds on rings of every size.

Preamble

import Mathlib
import Definitions.Def_PassivityRing_power

open Matrix BigOperators

Formal statement

namespace PassivityRing
theorem passive_of_symm (N d : ℕ) [NeZero N]
    (W : Fin N → Matrix (Fin d) (Fin d) ℝ) (hW : ∀ i, (W i)ᵀ = W i)
    (v : Fin N → (Fin d → ℝ)) : power N d W v = 0 := by sorry
end PassivityRing

Source

Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §6, Theorem 6.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)", Corrected Theorem 6.1(a): 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

Read-back of PassivityRing.passive_of_symm.

Data.

$N$ and $d$ are natural numbers. There is a standing assumption that $N \neq 0$ , so $N \ge 1$ . $d = 0$ is allowed.
The indices $i$ range over $\mathbb{Z}/N\mathbb{Z} = \{0, 1, \dots, N-1\}$ , which the code calls Fin N. On this index set, $+$ and $-$ are modular (wrap-around): $i+1$ means $(i+1) \bmod N$ , so $(N-1)+1 = 0$ . Likewise $i-1$ means $(i-1) \bmod N$ , so $0 - 1 = N-1$ . Nothing is truncated. The indices form a cyclic ring.
For each index $i$ , $W_i$ is a real $d \times d$ matrix.
For each index $i$ , $v_i \in \mathbb{R}^d$ is a real vector. The vectors $v_0, \dots, v_{N-1}$ are completely arbitrary.

Hypothesis. Every matrix is symmetric:

W_i^{\mathsf T} = W_i \qquad \text{for all } i \in \mathbb{Z}/N\mathbb{Z}.

There are no other hypotheses on $W$ or $v$ . The matrices need not be definite or invertible, and they need not relate to one another.

Definition expanded. The quantity "power" is defined as

P(W, v) \;=\; \sum_{i \in \mathbb{Z}/N\mathbb{Z}} v_i \cdot \bigl( W_i\, v_{i+1} \;-\; W_{i-1}\, v_{i-1} \bigr).

Here $\cdot$ is the plain real dot product on $\mathbb{R}^d$ : $a \cdot b = \sum_{k=1}^{d} a_k b_k$ .
$W v$ is the ordinary product of a matrix and a column vector.
$i+1$ and $i-1$ are taken modulo $N$ , as above.
In the second term, the matrix index and the vector index are both $i-1$ . That is, the term is $W_{i-1} v_{i-1}$ , not $W_i v_{i-1}$ .

Equivalently,

P(W, v) = \sum_{i} v_i^{\mathsf T} W_i\, v_{i+1} \;-\; \sum_{i} v_i^{\mathsf T} W_{i-1}\, v_{i-1}.

Conclusion. For every $N \ge 1$ , every $d$ , every family of symmetric real matrices $(W_i)$ and every family of vectors $(v_i)$ :

P(W, v) = 0.

Degenerate cases.

$N = 1$ . The only index is $0$ , and $0+1 = 0-1 = 0$ . The sum is the single term $v_0 \cdot (W_0 v_0 - W_0 v_0)$ .
$N = 2$ . Here $i+1 = i-1$ for both indices. Each term reads $v_i \cdot (W_i v_{i+1} - W_{i+1} v_{i+1})$ .
$d = 0$ . All vectors are empty and every dot product is $0$ .

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