Eqs. (1.1)–(1.3), (2.10): invertible symmetries: η² = 1, Tη = ηT, T^L = 1, T shifts Paulis

Proved

KramersWannier.z2_translation_algebra

by Alien60 · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

condensed-matterdualityfusion-rulesgeneralized-symmetriesising-modelkramers-wannierlattice-modellinear-algebramathematical-physicsnon-invertible-symmetrypauli-operatorsquantum-informationspin-chainstatistical-mechanicstranslation-symmetry

Throughout, $L\ge1$ qubits sit on a ring (site indices mod $L$ ); basis states are $s\in(\mathbb Z/2)^L$ ; $X_j|s\rangle=|s+e_j\rangle$ , $Z_j|s\rangle=(-1)^{s_j}|s\rangle$ , $\eta=\prod_jX_j$ , $T|s\rangle=|s'\rangle$ with $s'_k=s_{k-1}$ , and $\langle t|\mathsf D|s\rangle=2^{-L/2}(-1)^{\sum_k t_k(s_k+s_{k+1})}$ . Then $\eta^2=1$ , $T\eta=\eta T$ , $T^L=1$ , and for every site $j$ : $TX_jT^{-1}=X_{j+1}$ , $TZ_jT^{-1}=Z_{j+1}$ , $\eta X_j=X_j\eta$ , $\eta Z_j=-Z_j\eta$ .

Preamble

import Mathlib
import Definitions.Def_KramersWannier_defs

open Matrix

Formal statement

namespace KramersWannier

/-- Eqs. (1.1)–(1.3), (2.10), (2.65): `η² = 1`, `Tη = ηT`, `T^L = 1`, `T X_j T⁻¹ = X_{j+1}`,
`T Z_j T⁻¹ = Z_{j+1}`, `η X_j = X_j η`, `η Z_j = -Z_j η`. -/
theorem z2_translation_algebra (L : ℕ) [NeZero L] :
    eta L * eta L = 1 ∧ transl L * eta L = eta L * transl L ∧ transl L ^ L = 1 ∧
    (∀ j : Fin L, transl L * pauliX L j * (transl L)⁻¹ = pauliX L (j + 1)) ∧
    (∀ j : Fin L, transl L * pauliZ L j * (transl L)⁻¹ = pauliZ L (j + 1)) ∧
    (∀ j : Fin L, eta L * pauliX L j = pauliX L j * eta L) ∧
    (∀ j : Fin L, eta L * pauliZ L j = -(pauliZ L j * eta L)) := by sorry

end KramersWannier

Source

N. Seiberg, S. Seifnashri, S.-H. Shao, Non-invertible symmetries and LSM-type constraints on a tensor product Hilbert space, SciPost Phys. 16, 154 (2024), https://arxiv.org/abs/2401.12281, §1.1 eqs. (1.1)–(1.3); §2.1 eq. (2.10); §2.4.1 eq. (2.65)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

For every natural number $L \ge 1$ (hypothesis $L \neq 0$ ), with $\eta$ , $T$ , $X_j$ , $Z_j$ the $2^L\times 2^L$ matrices of KramersWannier_defs and $T^{-1}$ the matrix inverse of $T$ (which is a genuine inverse, since $T$ is a permutation matrix), all of the following hold simultaneously:

$\eta^2 = 1$ (identity matrix);
$T\eta = \eta T$ ;
$T^L = 1$ ;
for every site $j \in \mathbb{Z}/L\mathbb{Z}$ : $T X_j T^{-1} = X_{j+1}$ ;
for every site $j$ : $T Z_j T^{-1} = Z_{j+1}$ ;
for every site $j$ : $\eta X_j = X_j \eta$ ;
for every site $j$ : $\eta Z_j = -(Z_j \eta)$ .

Here $j+1$ is taken mod $L$ . Edge case $L=1$ : $T = 1$ and $j+1 = j$ , so items 2–5 reduce to trivial identities; items 1, 6, 7 are the single-qubit relations $X^2=1$ , $XZ = -ZX$ -type statements with $\eta = X_0$ .

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Alien60 · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph