Quantum Mechanics

Motivation

Kramers–Wannier duality was found in 1941 as a map between the high- and low-temperature phases of the two-dimensional Ising model (Kramers–Wannier 1941). In its quantum form it exchanges the transverse field $X_j$ and the nearest-neighbour coupling $Z_{j-1}Z_j$ of the transverse-field Ising chain, and it fixes the critical point. In conformal field theory it is implemented by a topological defect line (Fröhlich–Fuchs–Runkel–Schweigert 2004), the prototypical non-invertible symmetry: its fusion with itself is a sum of operators, not a single invertible one (Shao, TASI lectures 2023).

On a finite periodic chain the duality cannot be a unitary operator, because it maps the $\mathbb Z_2$-even sector to itself and annihilates the odd sector. Seiberg–Shao 2023 and Seiberg–Seifnashri–Shao 2024 wrote the exact lattice operator $\mathsf D$ on the tensor-product Hilbert space $(\mathbb C^2)^{\otimes L}$. They showed that its algebra closes only after the lattice translation is included: $\mathsf D^2=(1+\eta)T^{-1}$. This is a lattice relation that a fusion category does not describe, since the continuum fusion rule $\mathcal N^2=1+\eta$ appears only at low energy. The same identity drives the LSM-type constraint proved in that paper.

Timeline. 1941: Kramers and Wannier find the duality of the 2D Ising model. 2004: Fröhlich, Fuchs, Runkel and Schweigert realise it as a conformal defect. 2016: Aasen–Mong–Fendley construct the lattice defects. 2023–2024: Seiberg, Seifnashri and Shao find the exact operator algebra on the tensor-product Hilbert space, including the translation factor.

Setting

Fix $L\ge1$ qubits on a ring, with site indices in $\mathbb Z/L$ (Fin L with modular arithmetic). A computational-basis state is labelled by a configuration $s=(s_0,\dots,s_{L-1})\in(\mathbb Z/2)^L$ (Config L). Operators are complex $2^L\times2^L$ matrices indexed by configurations (Op L). Write $\operatorname{sgn}(a)=(-1)^a$.

• Pauli operators. $X_j|s\rangle=|s+e_j\rangle$ flips spin $j$ (pauliX), and $Z_j|s\rangle=(-1)^{s_j}|s\rangle$ (pauliZ).
• $\mathbb Z_2$ symmetry. $\eta=\prod_j X_j$ flips every spin (eta).
• Translation. $T|s\rangle=|s'\rangle$ with $s'_k=s_{k-1}$ (transl), so that $TX_jT^{-1}=X_{j+1}$.
• Kramers–Wannier operator (kwD):

$$\langle t|\,\mathsf D\,|s\rangle \;=\; 2^{-L/2}\,(-1)^{\sum_{k} t_k\,(s_k+s_{k+1})}.$$

This explicit formula is the definition used throughout. Relations (1.5) together with $\mathsf D\eta=\mathsf D$ determine $\mathsf D$ up to a scalar, and (1.4) fixes the scalar up to a sign. Every statement below is invariant under $\mathsf D\mapsto-\mathsf D$, so this is the operator of Seiberg–Seifnashri–Shao in that paper's normalisation (footnote 1). Its equality with their matrix-product presentation (2.64) is not formalised here.

Formalization targets

Goal: the non-invertible fusion rule (eqs. (1.4), (2.65), (F.18))

$$\mathsf D^2=(1+\eta)\,T^{-1}\qquad\text{for every }L\ge1 .$$

Milestones

1. Invertible algebra (eqs. (1.1)–(1.3), (2.10), (2.65)): $\eta^2=1$, $T\eta=\eta T$, $T^L=1$, $TX_jT^{-1}=X_{j+1}$, $TZ_jT^{-1}=Z_{j+1}$, $\eta X_j=X_j\eta$, $\eta Z_j=-Z_j\eta$.
2. Duality on $X$ (eq. (1.5)): $\mathsf D X_j=Z_{j-1}Z_j\,\mathsf D$.
3. Duality on $ZZ$ (eq. (1.5)): $\mathsf D Z_{j-1}Z_j=X_{j-1}\,\mathsf D$.
4. Absorbing $\eta$ (eqs. (1.4), (2.65)): $\mathsf D\eta=\eta\mathsf D=\mathsf D$.
5. Translation and adjoint (eq. (2.65), Table 1): $T\mathsf D=\mathsf DT$ and $\mathsf D^\dagger=\mathsf DT$.
6. Non-invertibility (§1.1): $\mathsf D$ is not a unit, and $\ker\mathsf D\neq0$.

Significance

The result. The goal identity is the defining relation of the lattice Kramers–Wannier symmetry. Together with milestones 4–5 it shows that $\mathsf D/\sqrt2$ restricted to the $\eta$-even sector squares to a translation, so $\mathsf D$ is a square root of $T^{-1}$ there. The paper uses this to derive its LSM-type constraint, and also to show that the lattice symmetry is not a fusion category, because the continuum rule $\mathcal N^2=1+\eta$ only emerges at low energy. Milestones 2–3 are the lattice Kramers–Wannier map on $\mathbb Z_2$-invariant operators, so $\mathsf D$ commutes with the critical Ising Hamiltonian $H=-\sum_j(Z_{j-1}Z_j+X_j)$.

Formalizing it. The identities are proved in the physics literature by tensor-network manipulations ((F.14)–(F.18)) and checked numerically, but none of this is machine-checked. This mission produces a reusable Lean setup for qubit chains: Pauli strings on $(\mathbb Z/2)^L$, $\mathbb Z_2$ and translation symmetries, and an exact non-invertible operator with its full operator algebra for every chain length. No mission on the platform or file in Mathlib currently formalizes a non-invertible lattice symmetry.

Difficulty

Each identity is easy to check for a fixed small $L$ by brute force. The content is that it holds for all $L$ at once, on a $2^L$-dimensional space. The difficulty is bookkeeping with periodic indices: sums over $(\mathbb Z/2)^L$ of characters $(-1)^{\langle t,\,\cdot\rangle}$, reindexing $k\mapsto k\pm1$ in Fin L (including $L=1$, where $k+1=k$, and $L=2$, where $k+1=k-1$), and the exact normalisation $2^{-L/2}$, so that the right-hand side carries no stray factor $2^L$. The goal also involves the matrix inverse $T^{-1}$, so a proof must establish that $T$ is invertible rather than rely on Lean's junk value.

Formalization scope

• Representation. Operators are Matrix (Fin L → ZMod 2) (Fin L → ZMod 2) ℂ; products are matrix products; $T^{-1}$ is Mathlib's matrix inverse (transl L)⁻¹; $\dagger$ is conjTranspose. Every theorem assumes [NeZero L], i.e. $L\ge1$.
• Conventions committed to. $Z_j=(-1)^{s_j}$ on basis states, translation to the right ($s'_k=s_{k-1}$), and $\mathsf D$ normalised by $2^{-L/2}$ as in eqs. (1.4)/(2.65). Other conventions (left translation, unnormalised $\mathsf D$) change the statements to $T$ instead of $T^{-1}$ or add a factor $2^L$; the conventions here reproduce the paper's equations verbatim.
• No trivialisation. kwD is an explicit formula, not a hypothesis. The goal fixes both sides completely, and milestone 1 pins the translation convention against eq. (2.10).
• Out of scope. The defect Hamiltonians, the MPO presentation (2.64) itself, the $\mathbb Z_2$- and duality-twisted operators of §§2.3.3–2.3.4, and the LSM constraint of §4.
• Reusable. Pauli operators, translation and $\eta$ on qubit chains; character-sum lemmas over $(\mathbb Z/2)^L$. Contributions of general Mathlib lemmas on Walsh–Hadamard-type sums are welcome.

Selected references

• H. A. Kramers, G. H. Wannier, Statistics of the Two-Dimensional Ferromagnet. Part I, Phys. Rev. 60, 252–262 (1941). doi:10.1103/PhysRev.60.252
• J. Fröhlich, J. Fuchs, I. Runkel, C. Schweigert, Kramers–Wannier duality from conformal defects, Phys. Rev. Lett. 93, 070601 (2004). arXiv:cond-mat/0404051
• D. Aasen, R. S. K. Mong, P. Fendley, Topological Defects on the Lattice I: The Ising model, J. Phys. A 49, 354001 (2016). arXiv:1601.07185
• N. Seiberg, S.-H. Shao, Majorana chain and Ising model – (non-invertible) translations, anomalies, and emanant symmetries, SciPost Phys. 16, 064 (2024). arXiv:2307.02534
• S.-H. Shao, What's Done Cannot Be Undone: TASI Lectures on Non-Invertible Symmetries (2023). arXiv:2308.00747
• 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). arXiv:2401.12281

Motivation

A known zero-energy vector does not by itself give a uniform positive gap above it. The Laughlin problem asks for a lower bound controlling every competing antisymmetric state. The pinned manuscript supplies the research context.

Setting

At N particles set Q=3(N−1). States are complex functions on finite configurations, with antisymmetry under exchanging particles. The energy is a sum of squared pair-annihilation amplitudes.

Formalization target

The selected goal is OAI.LaughlinGap.thm_main. Its central assertion is

$$\frac1{25}\operatorname{dist}(\psi,\mathbb C\Psi_{\rm L})^2\leq E(\psi).$$

The theorem states that there is a threshold N₀ ≥ 2 such that for every N ≥ N₀ and every antisymmetric complex-valued state ψ on N particles, each with local levels 0,…,Q where Q = 3(N−1), one has (1/25)·d(ψ)² ≤ E(ψ). Here a state assigns a complex number to each configuration a : Fin N → {0,…,Q}, and antisymmetric means that swapping the values at two distinct positions i and j negates ψ. The energy E(ψ) sums, over pairs i<j, over p = 0,…,2Q−2, and over configurations a with a_i = a_j = 0, the squared modulus of the pair amplitude, which is the sum over x,y of pairCoefficient(Q,p,x,y)·ψ(a with a_i replaced by x and a_j by y). The pair coefficient vanishes unless x+y = p+1, in which case it equals (x−y)/√2 times the square root of Q^{(x)}·Q^{(y)}·p! divided by Q·(2Q−2)^{(p)}·x!·y!, where m^{(k)} is the descending factorial. The Laughlin vector is built from the polynomial ∏{i<j}(x{i,0}x_{j,1} − x_{j,0}x_{i,1})³ in variables indexed by particle and a Boolean: its coefficient at the monomial with exponent a_i on x_{i,1} and Q−a_i on x_{i,0} is divided by ∏_i √C(Q,a_i). The quantity d(ψ)² is the infimum over complex c of the sum over configurations of |ψ(a) − c·Laughlin(a)|², the squared distance from ψ to the line spanned by the Laughlin vector, with no normalization of ψ assumed.

Significance and status

The selected goal has constant 1/25 and no normalization requirement on the state. The Fock-space inequality, the earlier 1/100 formulation and the planar endpoint are separate references; they retain their own representations and constants. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The bound must be uniform for all sufficiently large particle numbers and for every state, rather than a variational estimate on a selected excitation.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.Laughlin.mainTarget_proved (Open).
• OAI.LaughlinFock.thm_fock (Open).
• OAI.Laughlin.planar_gap (Open).

Selected references

• OpenAI, A Fock-space inequality and the Laughlin spectral gap, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.