Passive forces symmetric (rings of $N \ge 3$ sites)

Proved

PassivityRing.symm_of_passive

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

linear-algebramatrices

Let $N \ge 3$ and $d$ be natural numbers and let $W_0, \dots, W_{N-1}$ be real $d\times d$ matrices. Suppose that 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 .

Then every link matrix is symmetric: $W_i^{\mathsf T} = W_i$ for all $i$ .

This is the "only if" direction of the goal. The hypothesis $N \ge 3$ is necessary: on rings of $1$ or $2$ sites there are non-symmetric link matrices with zero power for every motion.

Preamble

import Mathlib
import Definitions.Def_PassivityRing_power

open Matrix BigOperators

Formal statement

namespace PassivityRing
theorem symm_of_passive (N d : ℕ) [NeZero N] (hN : 3 ≤ N)
    (W : Fin N → Matrix (Fin d) (Fin d) ℝ)
    (h : ∀ v : Fin N → (Fin d → ℝ), power N d W v = 0) :
    ∀ i, (W i)ᵀ = W i := 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) and correction 4 (ring of ≥ 3 sites): 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 PassivityRing.symm_of_passive.

Parameters.

$N$ and $d$ are natural numbers.
$N$ is assumed nonzero (a typeclass assumption), and there is also the explicit hypothesis $N \ge 3$ .
The dimension $d$ is unrestricted. It may be $0$ , in which case every matrix is the empty $0\times 0$ matrix and the conclusion holds trivially.
$W = (W_0, W_1, \dots, W_{N-1})$ is an arbitrary family of $N$ real $d\times d$ matrices, indexed by $\mathbb{Z}/N\mathbb{Z}$ (Lean's Fin N). No symmetry, sign, invertibility or other condition is placed on the $W_i$ .

Index arithmetic. All index arithmetic is on $\mathbb{Z}/N\mathbb{Z}$ , so it is cyclic, taken modulo $N$ :

$i+1$ means $(i+1) \bmod N$ , so $(N-1)+1 = 0$ .
$i-1$ means $(i-1) \bmod N$ , so $0-1 = N-1$ .

The indices therefore form a ring $0 \to 1 \to \cdots \to N-1 \to 0$ . Nothing truncates at the ends.

The "power" functional (expanded definition). For a configuration $v = (v_0,\dots,v_{N-1})$ , with each $v_i \in \mathbb{R}^d$ , the value is

P_W(v) \;=\; \sum_{i=0}^{N-1} v_i \cdot \bigl( W_i\, v_{i+1} \;-\; W_{i-1}\, v_{i-1} \bigr),

where:

$\cdot$ is the standard Euclidean dot product on $\mathbb{R}^d$ ;
$W_i v_{i+1}$ is the ordinary matrix–vector product;
the indices $i\pm 1$ are taken modulo $N$ as above.

Put differently, $P_W(v) = \sum_i \bigl( v_i^{\mathsf T} W_i v_{i+1} - v_i^{\mathsf T} W_{i-1} v_{i-1} \bigr)$ , a real number.

Hypothesis. The functional vanishes identically: for every configuration $v \in (\mathbb{R}^d)^N$ ,

P_W(v) = 0 .

Conclusion. Every matrix in the family is symmetric:

\forall\, i \in \mathbb{Z}/N\mathbb{Z}:\quad W_i^{\mathsf T} = W_i .

Summary of the whole statement. Take any $N \ge 3$ , any $d \ge 0$ , and any family of real $d\times d$ matrices $W_0,\dots,W_{N-1}$ on a cyclic ring of $N$ sites. If the quantity $\sum_i v_i\cdot(W_i v_{i+1} - W_{i-1} v_{i-1})$ , with cyclic indices, equals zero for all choices of vectors $v_0,\dots,v_{N-1}\in\mathbb{R}^d$ , then every $W_i$ equals its own transpose.

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

Passive forces symmetric (rings of N≥3N \ge 3N≥3 sites)

Passive forces symmetric (rings of $N \ge 3$ sites)