Stepping back then forward returns to the start

Proved

PassivityTorus.shift_back_forward

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

latticelinear-algebramatrices

For every site $x$ of the periodic lattice $(\mathbb{Z}/L\mathbb{Z})^q$ (with $L \ge 1$ ) and every axis $a$ ,

(x - e_a) + e_a = x .

One step back along axis $a$ followed by one step forward returns to the original site. This is the fact that makes the one-step shift a bijection of the lattice, which is needed to reindex the power sum.

Preamble

import Mathlib
import Definitions.Def_PassivityTorus_power

open Matrix BigOperators

Formal statement

namespace PassivityTorus
theorem shift_back_forward {q L : ℕ} [NeZero L] (x : Site q L) (a : Fin q) :
    shift (shift x a (-1)) a 1 = x := 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$ and $L$ be natural numbers, with the standing assumption $L \neq 0$ (so $L \ge 1$ ); $q$ is unrestricted and may be $0$ . Write $\mathbb{Z}_L = \{0, 1, \dots, L-1\}$ for the integers modulo $L$ , where addition and negation wrap around modulo $L$ . A site is a function $x : \{0, \dots, q-1\} \to \mathbb{Z}_L$ , i.e. a point $x = (x_0, \dots, x_{q-1})$ of the discrete torus $(\mathbb{Z}_L)^q$ .

The shift operation. For a site $x$ , a direction $a \in \{0, \dots, q-1\}$ and a step $s \in \mathbb{Z}_L$ , the shifted site $\sigma_a^s(x)$ is obtained from $x$ by replacing only coordinate $a$ with $x_a + s \pmod L$ and leaving every other coordinate unchanged:

\bigl(\sigma_a^s(x)\bigr)_b = \begin{cases} x_a + s \pmod L, & b = a,\\ x_b, & b \neq a. \end{cases}

Here the step $-1$ means the additive inverse of $1$ in $\mathbb{Z}_L$ , i.e. the residue $L-1$ (so adding it is subtracting $1$ modulo $L$ , with $0 - 1 = L-1$ ); the step $1$ means the residue $1 \bmod L$ . In the degenerate case $L = 1$ , both $1$ and $-1$ equal $0$ , and every shift is the identity.

Statement. For all $q, L$ with $L \neq 0$ , every site $x \in (\mathbb{Z}_L)^q$ , and every direction $a \in \{0, \dots, q-1\}$ :

\sigma_a^{1}\bigl(\sigma_a^{-1}(x)\bigr) = x,

as an equality of functions $\{0,\dots,q-1\} \to \mathbb{Z}_L$ (i.e. in every coordinate). Concretely: first moving coordinate $a$ back by one step modulo $L$ (to $x_a - 1 \bmod L$ ), and then moving the coordinate $a$ of the resulting site forward by one step modulo $L$ , returns exactly the original site $x$ ; all coordinates other than $a$ are untouched by both steps. When $q = 0$ there is no direction $a$ , so the statement holds vacuously; the definition file's other declaration (power) is not used in this statement.

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