Pauli operators, Z2 symmetry, translation and the Kramers-Wannier operator on a periodic qubit chain

Definition

KramersWannier_defs

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

For $L$ qubits on a ring: basis labels Config L $=(\mathbb Z/2)^L$ , operators Op L (complex matrices indexed by configurations), the sign sgn $a\mapsto(-1)^a$ , Pauli operators pauliX j (flip spin $j$ ) and pauliZ j (diagonal $(-1)^{s_j}$ ), the $\mathbb Z_2$ symmetry eta $=\prod_jX_j$ (flip all spins), the translation transl ( $T|s\rangle=|s'\rangle$ , $s'_k=s_{k-1}$ , indices mod $L$ ), and the Kramers-Wannier operator kwD with $\langle t|\mathsf D|s\rangle=2^{-L/2}(-1)^{\sum_k t_k(s_k+s_{k+1})}$ .

Definition code

import Mathlib

/-!
# The Kramers–Wannier operator on a periodic qubit chain (Seiberg–Seifnashri–Shao 2024)

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), arXiv:2401.12281, §1.1 and §2.

A chain of `L` qubits with periodic boundary conditions (site `j` and site `j + L` are identified,
realised by modular arithmetic in `Fin L`). The Hilbert space `(ℂ²)^{⊗L}` is identified with
functions on the computational (`Z`-eigen)basis `Config L = Fin L → ZMod 2`, where `s j = 0`
means `Z_j = +1` and `s j = 1` means `Z_j = -1`. Operators are complex matrices indexed by
`Config L`.

* `pauliX j`, `pauliZ j`: the Pauli operators on site `j` (`X_j` flips `s j`, `Z_j = (-1)^{s j}`);
* `eta`: the `ℤ₂` symmetry `η = ∏_j X_j` (flips every spin), eq. (1.2);
* `transl`: the lattice translation `T`, with `T X_j T⁻¹ = X_{j+1}`, `T Z_j T⁻¹ = Z_{j+1}`,
  eqs. (1.1), (2.10); in the basis, `T |s⟩ = |s'⟩` with `s'_{k} = s_{k-1}`;
* `kwD`: the Kramers–Wannier operator `D` with matrix elements
  `⟨t| D |s⟩ = 2^{-L/2} (-1)^{∑_k t_k (s_k + s_{k+1})}`.
  This explicit formula is taken as the definition; it is the operator satisfying (1.4)–(1.5) and
  (2.65) in the paper's normalisation (footnote 1). Its equality with the matrix-product presentation
  (2.64) is not part of this development.
-/

namespace KramersWannier

/-- Computational-basis labels of `L` qubits: `s j ∈ ZMod 2` is the `Z_j` eigenvalue `(-1)^{s j}`. -/
abbrev Config (L : ℕ) := Fin L → ZMod 2

/-- The sign `(-1)^a` for `a ∈ ZMod 2`. -/
def sgn (a : ZMod 2) : ℂ := if a = 0 then 1 else -1

/-- Operators on `(ℂ²)^{⊗L}`, as matrices in the computational basis. -/
abbrev Op (L : ℕ) := Matrix (Config L) (Config L) ℂ

variable (L : ℕ)

/-- Pauli `X_j`: flips the spin on site `j`, `X_j |s⟩ = |s + e_j⟩`. -/
def pauliX (j : Fin L) : Op L := fun t s => if t = s + Pi.single j 1 then 1 else 0

/-- Pauli `Z_j`: diagonal, `Z_j |s⟩ = (-1)^{s j} |s⟩`. -/
def pauliZ (j : Fin L) : Op L := Matrix.diagonal fun s => sgn (s j)

/-- The `ℤ₂` symmetry operator `η = ∏_j X_j` (eq. (1.2)): flips every spin. -/
def eta : Op L := fun t s => if t = s + 1 then 1 else 0

/-- Lattice translation `T` (eqs. (1.1), (2.10): `T X_j T⁻¹ = X_{j+1}`):
`T |s⟩ = |s'⟩` with `s'_k = s_{k-1}`, indices mod `L`. -/
def transl [NeZero L] : Op L := fun u s => if u = (fun k => s (k - 1)) then 1 else 0

/-- The non-invertible Kramers–Wannier operator `D` (eqs. (1.4), (1.5), (2.64)):
`⟨t| D |s⟩ = 2^{-L/2} (-1)^{∑_k t_k (s_k + s_{k+1})}`, indices mod `L`. -/
noncomputable def kwD [NeZero L] : Op L :=
  fun t s => ((Real.sqrt 2 : ℂ)⁻¹) ^ L * sgn (∑ k, t k * (s k + s (k + 1)))

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.5), §2.1 eq. (2.10), §2.4.1 eqs. (2.64)-(2.65), footnote 1

Read-back

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

Throughout, $L$ is a natural number and $\mathbb{Z}_2 = \mathbb{Z}/2\mathbb{Z}$ . Site indices live in $\mathbb{Z}/L\mathbb{Z}$ (i.e. $\{0,\dots,L-1\}$ with addition and subtraction taken mod $L$ ; in particular $k+1$ and $k-1$ wrap around). The definitions below do not themselves assume $L \ge 1$ , except transl and kwD, which require $L \neq 0$ .

Configurations. $\mathrm{Config}_L$ is the set of all functions $s : \mathbb{Z}/L\mathbb{Z} \to \mathbb{Z}_2$ (there are $2^L$ of them). It is an additive group under pointwise addition; $e_j$ denotes the configuration that is $1$ at site $j$ and $0$ elsewhere, and $\mathbf{1}$ the constant configuration $1$ .

Sign. For $a \in \mathbb{Z}_2$ , $\operatorname{sgn}(a) \in \mathbb{C}$ is $1$ if $a = 0$ and $-1$ if $a = 1$ , i.e. $\operatorname{sgn}(a) = (-1)^a$ ; it satisfies $\operatorname{sgn}(a+b) = \operatorname{sgn}(a)\operatorname{sgn}(b)$ .

Operators. An "operator" is simply a complex $2^L \times 2^L$ matrix $M$ whose rows and columns are indexed by $\mathrm{Config}_L$ ; $M_{t,s}$ is the entry in row $t$ , column $s$ (read as $\langle t|M|s\rangle$ ). Products are ordinary matrix products, acting on column vectors. No tensor-product structure is used; all operators are defined by their matrix entries:

Pauli X at site $j$ : $(X_j)_{t,s} = 1$ if $t = s + e_j$ , else $0$ . So $X_j$ is the permutation matrix sending basis vector $|s\rangle$ to $|s+e_j\rangle$ .
Pauli Z at site $j$ : the diagonal matrix with $(Z_j)_{s,s} = (-1)^{s_j}$ .
$\eta$ : $\eta_{t,s} = 1$ if $t = s + \mathbf{1}$ (every spin flipped), else $0$ .
Translation $T$ (requires $L \neq 0$ ): $T_{u,s} = 1$ if $u_k = s_{k-1}$ for all $k$ (indices mod $L$ ), else $0$ . So $T|s\rangle = |s'\rangle$ with $s'_k = s_{k-1}$ ; for $L = 1$ , $T$ is the identity matrix.
Kramers–Wannier operator $D$ (requires $L \neq 0$ ):

D_{t,s} = \Big(\tfrac{1}{\sqrt 2}\Big)^{L}\,(-1)^{\sum_{k \in \mathbb{Z}/L\mathbb{Z}} t_k\,(s_k + s_{k+1})},

where the exponent is computed in $\mathbb{Z}_2$ and $s_{k+1}$ wraps mod $L$ . All entries are real, of absolute value $2^{-L/2}$ . Edge case $L = 1$ : $s_0 + s_{0+1} = 2s_0 = 0$ , so $D = \tfrac{1}{\sqrt2}\begin{pmatrix}1&1\1&1\end{pmatrix}$ .

The docstrings attribute these to a specific paper (equation numbers, normalisation, "closed form of the matrix-product operator of eq. (2.64)"); the code contains only the explicit formulas above, with no matrix-product-operator construction, so that identification is a claim not represented in the code.

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