Eq. (1.5a): Kramers–Wannier on the field: D X_j = Z_{j-1} Z_j D

Proved

KramersWannier.kw_intertwines_X

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})}$ . For every site $j$ , $\mathsf D X_j=Z_{j-1}Z_j\,\mathsf D$ .

Preamble

import Mathlib
import Definitions.Def_KramersWannier_defs

open Matrix

Formal statement

namespace KramersWannier

/-- Eq. (1.5), first line: `D X_j = Z_{j-1} Z_j D` (indices mod `L`). -/
theorem kw_intertwines_X (L : ℕ) [NeZero L] (j : Fin L) :
    kwD L * pauliX L j = pauliZ L (j - 1) * pauliZ L j * kwD 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 eq. (1.5), first line

Read-back

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

For every $L \ge 1$ and every site $j \in \mathbb{Z}/L\mathbb{Z}$ ,

D\,X_j = Z_{j-1}\,Z_j\,D,

as $2^L\times 2^L$ matrix identities, with $D$ , $X_j$ , $Z_j$ as in KramersWannier_defs and $j-1$ taken mod $L$ . Entrywise this says $D_{t,\,s+e_j} = (-1)^{t_{j-1}+t_j} D_{t,s}$ for all $t,s$ .

Edge case $L=1$ : $j-1 = j$ , so $Z_{j-1}Z_j = Z_j^2 = 1$ and the statement becomes $D X_0 = D$ . For $L=2$ , $j-1 = j+1$ .

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