§1.1 (below eq. (1.4)): D is not invertible

Proved

KramersWannier.kw_not_invertible

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})}$ . $\mathsf D$ is not a unit of the matrix ring, and there is a nonzero vector $v$ with $\mathsf Dv=0$ .

Preamble

import Mathlib
import Definitions.Def_KramersWannier_defs

open Matrix

Formal statement

namespace KramersWannier

/-- §1.1, below eq. (1.4): `D` is not invertible; it has a nontrivial kernel. -/
theorem kw_not_invertible (L : ℕ) [NeZero L] :
    ¬ IsUnit (kwD L) ∧ ∃ v : Config L → ℂ, v ≠ 0 ∧ kwD L *ᵥ v = 0 := 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, text below eq. (1.4)

Read-back

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

For every $L \ge 1$ , with $D$ as in KramersWannier_defs:

$D$ is not a unit in the ring of $2^L\times 2^L$ complex matrices (it has no two-sided matrix inverse), and
there exists a vector $v \in \mathbb{C}^{\mathrm{Config}_L}$ (a complex-valued function on configurations), $v \neq 0$ , with $D v = 0$ (matrix–vector product, $(Dv)_t = \sum_s D_{t,s} v_s$ ).

Part 2 implies part 1 for square matrices, so the conjunction carries no more content than part 2.

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