Zero net power $\iff$ every link coupling is symmetric (rings of $N \ge 3$ sites)

Proved

PassivityRing.passive_iff_symm

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

linear-algebramatrices

Let $N \ge 3$ and $d$ be natural numbers. On a ring of $N$ sites (indices modulo $N$ ), each site carries a velocity $v_i \in \mathbb{R}^d$ and each link carries a real $d\times d$ matrix $W_i$ . The total power of the coupling is

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

Then

\bigl( P_W(v) = 0 \ \text{for every } v \bigr) \iff \bigl( W_i^{\mathsf T} = W_i \ \text{for every } i \bigr).

So a per-link neighbour coupling on a ring of at least three sites does no net work for every motion exactly when every link matrix is symmetric. The ring-size condition is necessary, and the statement does not assert that the coupling commutes with any complex structure.

Preamble

import Mathlib
import Definitions.Def_PassivityRing_power

open Matrix BigOperators

Formal statement

namespace PassivityRing
theorem passive_iff_symm (N d : ℕ) [NeZero N] (hN : 3 ≤ N)
    (W : Fin N → Matrix (Fin d) (Fin d) ℝ) :
    (∀ 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): 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.passive_iff_symm.

Setting and binders.

$N$ and $d$ are natural numbers.
$N \neq 0$ is assumed as a typeclass condition. The hypothesis $3 \le N$ is also assumed, which already implies $N \neq 0$ .
$d$ has no constraint. In particular, $d = 0$ is allowed, and then every matrix and vector is empty.
$W = (W_0, \dots, W_{N-1})$ is an arbitrary family of $N$ real $d \times d$ matrices, one for each index $i \in \mathbb{Z}/N\mathbb{Z}$ .

Indices run over $\{0, 1, \dots, N-1\}$ , and all index arithmetic is modular (cyclic), taken mod $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$ . Subtraction wraps around. It does not truncate at $0$ .

Because $N \ge 3$ , the constant $1$ really is $1$ , and for every $i$ the indices $i-1$ , $i$ , $i+1$ are three distinct positions on a cycle of length $N$ .

The "power" (definition expanded inline). Take a configuration $v = (v_0, \dots, v_{N-1})$ , where each $v_i \in \mathbb{R}^d$ . The quantity $P_W(v) \in \mathbb{R}$ is

P_W(v) \;=\; \sum_{i=0}^{N-1} v_i^{\mathsf T}\big( W_i\, v_{i+1} \;-\; W_{i-1}\, v_{i-1} \big),

with indices mod $N$ . Here:

$W_i\, v_{i+1}$ is the ordinary matrix–vector product.
$x^{\mathsf T} y = \sum_{k=1}^{d} x_k y_k$ is the standard dot product on $\mathbb{R}^d$ .

Assertion. The following two statements are equivalent (a biconditional):

\Big(\forall\, v \in (\mathbb{R}^d)^N:\; P_W(v) = 0\Big) \iff \Big(\forall\, i \in \{0,\dots,N-1\}:\; W_i^{\mathsf T} = W_i\Big).

The left side says that $P_W$ vanishes identically on all real configurations $v$ , with no restriction on $v$ .
The right side says that every matrix $W_i$ is symmetric.

Edge case. When $d = 0$ , both sides hold trivially: every sum over $k$ is empty and every $0 \times 0$ matrix is symmetric.

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

Zero net power ⟺ \iff⟺ every link coupling is symmetric (rings of N≥3N \ge 3N≥3 sites)

Zero net power $\iff$ every link coupling is symmetric (rings of $N \ge 3$ sites)