Passive forces symmetric (needs $L \ge 3$ )

Proved

PassivityTorus.symm_of_passive

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

latticelinear-algebramatrices

Let $L \ge 3$ , and let $W(x,a)$ be real $d\times d$ link matrices on the periodic lattice $(\mathbb{Z}/L\mathbb{Z})^q$ . If $P_W(v) = 0$ for every velocity field $v$ , then every link matrix is symmetric:

W(x,a)^{\mathsf T} = W(x,a) \qquad \text{for all sites } x \text{ and axes } a.

This is the "only if" direction of the goal. The hypothesis $L \ge 3$ is necessary: at $L = 2$ the forward and backward neighbours coincide, and a non-symmetric matrix on every link gives zero power.

Preamble

import Mathlib
import Definitions.Def_PassivityTorus_power

open Matrix BigOperators

Formal statement

namespace PassivityTorus
theorem symm_of_passive (q L d : ℕ) [NeZero L] (hL : 3 ≤ L)
    (W : Site q L → Fin q → Matrix (Fin d) (Fin d) ℝ)
    (h : ∀ 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) and correction 4 (at least 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

Setting. Let $q, L, d \in \mathbb{N}$ be natural numbers with $L \ge 3$ . (A separate typeclass assumption says $L \neq 0$ , which already follows from $L \ge 3$ .) 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 $\Lambda = (\mathbb{Z}/L\mathbb{Z})^q$ , with $L^q$ elements. Coordinates of a site live in $\{0,\dots,L-1\}$ with arithmetic taken modulo $L$ ; in particular the element " $-1$ " is $L-1$ , and adding $1$ to $L-1$ gives $0$ . For a site $x$ , a direction $a \in \{0,\dots,q-1\}$ and a step $s \in \mathbb{Z}/L\mathbb{Z}$ , the shift $x + s\,e_a$ is the site that agrees with $x$ in every coordinate except coordinate $a$ , which is replaced by $x_a + s \pmod L$ . Only the steps $s = 1$ and $s = -1 \equiv L-1$ are used below. Because $L \ge 3$ , the sites $x + e_a$ , $x - e_a$ and $x$ are pairwise distinct whenever $q \ge 1$ .

Data. $W$ is an arbitrary assignment $W_{x,a} \in \mathbb{R}^{d\times d}$ of a real $d \times d$ matrix to each site $x \in \Lambda$ and each direction $a \in \{0,\dots,q-1\}$ . No relation among different $W_{x,a}$ is assumed.

The functional. For a vector field $v : \Lambda \to \mathbb{R}^d$ (an arbitrary choice $v_x \in \mathbb{R}^d$ at every site), define

P_W(v) \;=\; \sum_{x \in \Lambda} \sum_{a=0}^{q-1} \Big\langle v_x,\; W_{x,a}\, v_{x+e_a} \;-\; W_{x-e_a,\,a}\, v_{x-e_a} \Big\rangle ,

where $\langle u, w\rangle = \sum_{i=1}^d u_i w_i$ is the standard dot product on $\mathbb{R}^d$ and $W_{x,a} v$ is the ordinary matrix–vector product. Note that the second term uses the matrix attached to the neighbouring site $x - e_a$ (in the same direction $a$ ), applied to the value of $v$ at $x - e_a$ .

Hypothesis. $P_W(v) = 0$ for every vector field $v : \Lambda \to \mathbb{R}^d$ .

Conclusion. For every site $x \in \Lambda$ and every direction $a \in \{0,\dots,q-1\}$ , the matrix $W_{x,a}$ is symmetric:

W_{x,a}^{\mathsf T} = W_{x,a}.

Degenerate cases. If $q = 0$ , there is exactly one site (the empty function), there are no directions, the inner sum is empty so $P_W \equiv 0$ and the hypothesis holds automatically, and the conclusion quantifies over an empty set of directions, so it holds vacuously. If $d = 0$ , every matrix is the empty $0\times 0$ matrix, $P_W \equiv 0$ , and every $W_{x,a}$ is trivially symmetric. The hypothesis is always satisfiable (e.g. by $W \equiv 0$ ), so the statement is not vacuous in general.

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 (needs L≥3L \ge 3L≥3)

Passive forces symmetric (needs $L \ge 3$ )