Eqs. (1.4), (2.65): fusion rule D² = (1 + η) T⁻¹

Proved

KramersWannier.kw_fusion

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 $L\ge1$ : $\mathsf D^2=(1+\eta)\,T^{-1}$ .

Preamble

import Mathlib
import Definitions.Def_KramersWannier_defs

open Matrix

Formal statement

namespace KramersWannier

/-- Eqs. (1.4), (2.65), (F.18): the non-invertible fusion rule `D² = (1 + η) T⁻¹`. -/
theorem kw_fusion (L : ℕ) [NeZero L] :
    kwD L * kwD L = (1 + eta L) * (transl 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.4); §2.4.1 eq. (2.65); App. F eq. (F.18)

Read-back

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

For every $L \ge 1$ , with $D$ , $\eta$ , $T$ as in KramersWannier_defs and $T^{-1}$ the matrix inverse of the permutation matrix $T$ (a genuine inverse; $T^{-1}|s\rangle = |s''\rangle$ with $s''_k = s_{k+1}$ ),

D^2 = (1 + \eta)\,T^{-1},

where $1$ is the identity matrix. Entrywise the right side has $(t,s)$ -entry $1$ if $t = s''$ or $t = s'' + \mathbf{1}$ , and $0$ otherwise (these two cases are distinct since $L \ge 1$ ). Edge case $L = 1$ : $T = 1$ and the statement reads $D^2 = 1 + \eta = \begin{pmatrix}1&1\1&1\end{pmatrix}$ .

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