Zero net power $\iff$ every link coupling is symmetric, on a $q$ -dimensional lattice ( $L \ge 3$ )

Proved

PassivityTorus.passive_iff_symm

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

latticelinear-algebramatrices

Let $q$ and $d$ be natural numbers and $L \ge 3$ . On the periodic cubic lattice $(\mathbb{Z}/L\mathbb{Z})^q$ , let each link $(x,a)$ carry a real $d\times d$ matrix $W(x,a)$ , with total power

P_W(v) = \sum_{x} \sum_{a=0}^{q-1} v(x) \cdot \Bigl( W(x,a)\, v(x+e_a) - W(x-e_a,a)\, v(x-e_a) \Bigr).

Then

\bigl( P_W(v) = 0 \ \text{for every } v \bigr) \iff \bigl( W(x,a)^{\mathsf T} = W(x,a) \ \text{for every } x, a \bigr).

A per-link neighbour coupling on a lattice of any dimension does no net work for every motion exactly when every link matrix is symmetric. It does not assert that the coupling commutes with any complex structure.

Preamble

import Mathlib
import Definitions.Def_PassivityTorus_power

open Matrix BigOperators

Formal statement

namespace PassivityTorus
theorem passive_iff_symm (q L d : ℕ) [NeZero L] (hL : 3 ≤ L)
    (W : Site q L → Fin q → Matrix (Fin d) (Fin d) ℝ) :
    (∀ v : Site q L → (Fin d → ℝ), power q L d W v = 0)
      ↔ ∀ x a, (W x a)ᵀ = W x a := 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. Assume $L \neq 0$ (a typeclass assumption), and also assume $L \ge 3$ (an explicit hypothesis, which already implies $L \neq 0$ ). A site is a function $x : \{0,\dots,q-1\} \to \mathbb{Z}/L\mathbb{Z}$ , so the set of sites is the discrete torus $(\mathbb{Z}/L\mathbb{Z})^q$ , which has $L^q$ elements. For a site $x$ and a direction $a \in \{0,\dots,q-1\}$ , write $e_a$ for the $a$ -th unit vector. The shifted site $x \pm e_a$ is $x$ with only its $a$ -th coordinate changed, to $x_a \pm 1$ taken modulo $L$ . Addition wraps around: $L-1$ goes to $0$ . For $-1$ , the code adds the residue $L-1$ , so $0$ goes to $L-1$ . All other coordinates stay the same. Let

W : (\mathbb{Z}/L\mathbb{Z})^q \times \{0,\dots,q-1\} \to \mathbb{R}^{d\times d}

be an arbitrary assignment of a real $d \times d$ matrix $W_{x,a}$ to every site $x$ and direction $a$ . No further conditions are placed on $W$ .

The quantity $P_W(v)$ ("power"). For any function $v : (\mathbb{Z}/L\mathbb{Z})^q \to \mathbb{R}^d$ (arbitrary, and possibly zero), define

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

Here $u^\top w = \sum_{i} u_i w_i$ is the ordinary dot product on $\mathbb{R}^d$ , and $W_{x,a} v(\cdot)$ is the ordinary matrix–vector product. The second term uses the matrix at the neighbouring site $x-e_a$ , again with direction $a$ , not the matrix at $x$ .

Assertion. For every $q, L, d$ and $W$ as above (with $L \ge 3$ ):

\Big(\forall\, v : (\mathbb{Z}/L\mathbb{Z})^q \to \mathbb{R}^d,\;\; P_W(v) = 0\Big) \iff \Big(\forall\, x \in (\mathbb{Z}/L\mathbb{Z})^q,\ \forall\, a \in \{0,\dots,q-1\},\;\; W_{x,a}^{\top} = W_{x,a}\Big).

In words, $P_W$ vanishes for every vector field $v$ exactly when every matrix $W_{x,a}$ is symmetric. The statement is a biconditional, so it claims both directions.

Degenerate cases.

If $q = 0$ , there is exactly one site (the empty function) and no directions. The inner sum is then empty, so $P_W(v) = 0$ for every $v$ , and the right-hand side holds vacuously. Both sides are true.
If $d = 0$ , all vectors and matrices are empty, so both sides are trivially true.
The cases $L = 1$ and $L = 2$ (where $x + e_a = x - e_a$ or $x \pm e_a = x$ ) are excluded by the hypothesis $L \ge 3$ . When $L \ge 3$ , the three sites $x - e_a$ , $x$ , $x + e_a$ are distinct.

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, on a qqq-dimensional lattice (L≥3L \ge 3L≥3)

Zero net power $\iff$ every link coupling is symmetric, on a $q$ -dimensional lattice ( $L \ge 3$ )