Symmetric links are passive

Proved

PassivityTorus.passive_of_symm

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

latticelinear-algebramatrices

Let $W(x,a)$ be real $d\times d$ link matrices on the periodic lattice $(\mathbb{Z}/L\mathbb{Z})^q$ with $L \ge 1$ , and suppose every one is symmetric, $W(x,a)^{\mathsf T} = W(x,a)$ . Then for every velocity field $v$ ,

P_W(v) = 0 .

This is the "if" direction of the goal, valid for every lattice size.

Preamble

import Mathlib
import Definitions.Def_PassivityTorus_power

open Matrix BigOperators

Formal statement

namespace PassivityTorus
theorem passive_of_symm (q L d : ℕ) [NeZero L]
    (W : Site q L → Fin q → Matrix (Fin d) (Fin d) ℝ) (hW : ∀ x a, (W x a)ᵀ = W x a)
    (v : Site q L → (Fin d → ℝ)) : power q L d W v = 0 := by sorry
end PassivityTorus

Source

Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §6, Theorem 6.1 (extended to a q-dimensional periodic lattice): 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

Setting. Let $q, L, d$ be natural numbers, with the standing assumption $L \neq 0$ (so $L \ge 1$ ). There are no other restrictions: $q = 0$ and $d = 0$ are allowed. A site is any function $x : \{0,\dots,q-1\} \to \mathbb{Z}/L\mathbb{Z}$ , which is a point of the discrete torus $(\mathbb{Z}/L\mathbb{Z})^q$ . Write $x_a$ for its $a$ -th coordinate. The shift of $x$ in direction $a \in \{0,\dots,q-1\}$ by $s \in \mathbb{Z}/L\mathbb{Z}$ is the site that agrees with $x$ in every coordinate except $a$ , where the value becomes $x_a + s$ computed modulo $L$ :

(\operatorname{shift}(x,a,s))_b = \begin{cases} x_a + s \pmod L & b = a,\\ x_b & b \neq a.\end{cases}

We write $x + e_a := \operatorname{shift}(x,a,1)$ and $x - e_a := \operatorname{shift}(x,a,-1)$ . Here $-1$ means the residue $L-1$ , so $x - e_a$ changes coordinate $a$ to $x_a + (L-1) \equiv x_a - 1 \pmod L$ . Both shifts wrap around periodically. When $L = 1$ , the only residue is $0$ , so $1 = -1 = 0$ and $x \pm e_a = x$ .

Data. The statement takes:

a family of real $d \times d$ matrices $W_{x,a}$ , one for each site $x$ and each direction $a \in \{0,\dots,q-1\}$ ;
a vector field $v$ that assigns to each site $x$ a vector $v(x) \in \mathbb{R}^d$ . Nothing is assumed about $v$ .

Definition of power. The power of $(W, v)$ is the real number

P(W,v) \;=\; \sum_{x \in (\mathbb{Z}/L)^q} \;\sum_{a=0}^{q-1} \; v(x) \cdot \Big( W_{x,a}\, v(x+e_a) \;-\; W_{x-e_a,\,a}\, v(x-e_a) \Big).

Here $\cdot$ is the standard dot product $\sum_{i=1}^d u_i w_i$ on $\mathbb{R}^d$ , and $W\,u$ is the ordinary matrix–vector product. The outer sum runs over all $L^q$ sites, and the inner sum runs over all $q$ directions. The matrix in the second term is indexed by the shifted site $x - e_a$ and the same direction $a$ .

Hypothesis. Every matrix in the family is symmetric:

W_{x,a}^{\mathsf T} = W_{x,a} \quad\text{for all sites } x \text{ and all directions } a.

Assertion. For all $q, L, d$ with $L \ge 1$ , every symmetric family $W$ as above, and every vector field $v : (\mathbb{Z}/L)^q \to \mathbb{R}^d$ ,

P(W,v) = 0.

Degenerate cases included by the quantifiers.

$q = 0$ : there is exactly one site (the empty function), and the direction sum is empty, so $P = 0$ regardless of $W$ and $v$ .
$d = 0$ : every vector and every dot product is zero, so $P = 0$ .
$L = 1$ : there is exactly one site, and $x \pm e_a = x$ . Each summand is $v(x)\cdot(W_{x,a} - W_{x,a})\,v(x) = 0$ , so $P = 0$ even without symmetry.
$L = 2$ : the residues satisfy $1 = -1$ , so $x + e_a = x - e_a$ .

The symmetry hypothesis can always be satisfied, for example by $W \equiv 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