Power identity: $P = \sum_i v_i \cdot (W_i - W_i^{\mathsf T})\, v_{i+1}$

Proved

PassivityRing.power_eq

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

linear-algebramatrices

Let $N \ge 1$ and $d$ be natural numbers, let $W_0, \dots, W_{N-1}$ be real $d\times d$ matrices and $v_0, \dots, v_{N-1} \in \mathbb{R}^d$ , with indices modulo $N$ . Then the total power satisfies

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

The identity holds for every ring size, with no condition on the link matrices. It rewrites the power so that each link contributes only through its antisymmetric part.

Preamble

import Mathlib
import Definitions.Def_PassivityRing_power

open Matrix BigOperators

Formal statement

namespace PassivityRing
theorem power_eq (N d : ℕ) [NeZero N]
    (W : Fin N → Matrix (Fin d) (Fin d) ℝ) (v : Fin N → (Fin d → ℝ)) :
    power N d W v = ∑ i : Fin N, v i ⬝ᵥ ((W i - (W i)ᵀ) *ᵥ v (i + 1)) := 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) (power identity): 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.power_eq. Fix natural numbers $N$ and $d$ , with $N \ge 1$ (this is the only hypothesis). $d = 0$ is allowed. Let the indices $i$ range over $\mathbb{Z}/N\mathbb{Z} = \{0, 1, \dots, N-1\}$ . On these indices, $i+1$ and $i-1$ are taken modulo $N$ , so the indices wrap around a cycle:

(N-1) + 1 = 0, \qquad 0 - 1 = N-1 .

When $N = 1$ the only index is $0$ , and $i+1 = i-1 = i = 0$ .

The theorem holds for every choice of the following data, with no further conditions such as symmetry, invertibility or positivity:

a family of real $d \times d$ matrices $W_0, \dots, W_{N-1}$ ;
a family of real vectors $v_0, \dots, v_{N-1} \in \mathbb{R}^d$ .

For a matrix $A$ and a vector $x$ , $A x$ is the ordinary matrix–vector product $(Ax)_k = \sum_{l} A_{kl} x_l$ . For two vectors, $x \cdot y = \sum_{k=1}^{d} x_k y_k$ is the ordinary dot product. $W_i^{\mathsf T}$ is the transpose of $W_i$ .

The quantity "power" $P(W, v)$ is defined as a sum over all $N$ cyclic indices:

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).

Both the matrix and the vector in the second term use the cyclically previous index $i-1$ . The first term uses the matrix at index $i$ and the vector at the cyclically next index $i+1$ .

The theorem asserts the identity

\sum_{i \in \mathbb{Z}/N\mathbb{Z}} v_i \cdot \bigl( W_i\, v_{i+1} - W_{i-1}\, v_{i-1} \bigr) \;=\; \sum_{i \in \mathbb{Z}/N\mathbb{Z}} v_i \cdot \bigl( (W_i - W_i^{\mathsf T})\, v_{i+1} \bigr),

with all index arithmetic taken modulo $N$ .

Edge cases the statement covers:

$N = 1$ : every shift is trivial. The left side is $v_0 \cdot (W_0 v_0 - W_0 v_0) = 0$ . The right side is $v_0 \cdot ((W_0 - W_0^{\mathsf T}) v_0)$ .
$N = 2$ : $i+1$ and $i-1$ are the same index, so both terms of the definition involve the other vector.
$d = 0$ : all vectors are empty and both sides are the empty sum $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

Power identity: P=∑ivi⋅(Wi−WiT) vi+1P = \sum_i v_i \cdot (W_i - W_i^{\mathsf T})\, v_{i+1}P=∑i​vi​⋅(Wi​−WiT​)vi+1​

Power identity: $P = \sum_i v_i \cdot (W_i - W_i^{\mathsf T})\, v_{i+1}$