Metadata
slug: klimov-2023-w-state-ti-mps-bond-dimension
bibkey: klimov2023wstate
doi: 10.48550/arXiv.2306.16456
url: https://arxiv.org/abs/2306.16456v2
triage: theorem
motivation_gids:
- D5/S3/Quantum/SpinChains/WStateTIMPSBondDimension.result
The minimal translation-invariant MPS bond dimension of the W-state
Problem
P. Klimov, R. Sengupta and J. Biamonte, On Translation-Invariant Matrix Product States and advances in MPS representations of the -state, arXiv:2306.16456v2, Section 3, conjecture after their Theorem 1:
These experiments lead us to conjecture that the representation obtained in Theorem \ref{W state representation} could be optimal both in terms of asymptotics and the constant factor or in other words it is impossible to come up with a TI MPS representation with PBC with bond dimension smaller than for the -state of order .
A TI MPS representation with PBC of bond dimension of the normalized -state of order is a pair of complex matrices , with when exactly one is and otherwise (Section 2). Problem 4 of Section 4 asks whether , and the table of Section 4 lists .
Motivation
The -state is translation invariant, but a translation-invariant MPS
with periodic boundary conditions needs a bond dimension that grows with
: the known lower bound is for every
, and Theorem 1 of the paper gives the upper bound
. The conjecture says that this upper bound is exact.
The frozen declaration
D5/S3/Quantum/SpinChains/WStateTIMPSBondDimension.result refutes it.
Gap
Issue #12026 classifies the conjecture as Tier 1 and records the bounded literature check before any Lean. It found:
- arXiv v2 is the latest version, with no journal version;
- the five citing works listed by Semantic Scholar (arXiv:2408.04729, 2408.13033, 2410.19541, 2412.19635, 2503.16327) give no representation below ; 2410.19541 calls the minimal TI MPS an open question, and 2503.16327 cites the paper as evidence for ;
- arXiv:1809.08185, arXiv:2108.00031 and quant-ph/0608197 give only border bond dimension, lower bounds and the representation.
These are orchestrator-reported literature readings,
not-found-in-searched-scope; they do not establish exhaustive worldwide
novelty or exclude an independent answer.
Route
- Take the matrices and , with the matrix units, and write .
- , and is for even and otherwise.
- A word with letters has trace , where the cyclic gaps between consecutive letters add up to .
- For the gap is and the trace is . For all gaps even and at least needs , so , and then the gaps add up to , which is odd: the trace is . For , .
- So . In Lean the 128 word traces of the integer matrices are computed by the kernel and the factor is pulled out of each word.
Falsifier
The kernel-checked result excludes the bound
for , hence the conjecture, the answer “yes” to Problem 4, and the
table entry . Changing the definition of a representation (the
normalization , the cyclic trace, or the order of the matrix
product) would change the question.
Evidence
Exact SymPy arithmetic over all 128 words and an independent NumPy computation give the traces above (0 failures). The same matrices give 10 and 17 failures for and , and perturbing one entry by gives 7–21 failures. As a positive control, the paper’s Theorem 1 construction for passes the same checker (issue #12026).
The canonical source is
D5/S3/Quantum/SpinChains/WStateTIMPSBondDimension.lean. Its public
declarations are IsWStateTIMPS, claim and result. The frozen module
state has statement identity sha256:fd1e75a90d7c9c176ed83ca1295f07558a4caf391781f06e1d7c9f3c285e68c0. The result declaration has
statement identity sha256:8debb2e851e522c233797783f07fc7d6b5e8597be4fe6289c23b239431fd636d. The Freeze event is sha256:ac8c966e2d620df874db853c6f0de88ba4ae76757fabf4a4c4bc2f531cbbf038. It has
no project-level frozen prerequisites (pinned Mathlib only). The proof uses
only the standard axioms propext, Classical.choice and Quot.sound; no
sorry, native_decide, or new axiom.
Triage
Tier 1 published conjecture; resolution Refuted by
D5/S3/Quantum/SpinChains/WStateTIMPSBondDimension.result.
proof_shape: bind-only (evaluation at an explicit pair of matrices);
admission_basis: open-problem-resolution (issue #12026). Utility
certified-instance, refuting claim.
What the refutation shows
- Proved in this module: the normalized -state of order has a translation-invariant MPS representation with periodic boundary conditions of bond dimension .
- Where the conjecture fails: in the proof of Theorem 1, vanishes for and is nonzero for (display (d1), l. 373–379), and a word of weight is killed only by its shortest cyclic gap, which is below (l. 407). That mechanism needs of order . The witness keeps the paper’s shape of a scaled matrix unit ( a multiple of a matrix unit: in the paper, here) but takes a periodic : the entry is nonzero only on an arithmetic progression of lengths, and the words of weight are killed by parity instead of by short gaps.
- Computed, not formalized (orchestrator): with a multiple of and a nonnegative integer , exact traces over all words give , and , against , , . An exhaustive search over matrices with this finds no representation for . This restricted search does not settle the table entries and ; they are open here.
- Model derivation, not checked in Lean (GPT Pro seat): for and , the -cycle on the vertices with the extra edge , and a multiple of , give . A word of weight would need , hence , against . So along this subsequence, and the “asymptotics” part of the conjecture fails along it. The orchestrator recomputed () over all words. Whether for all is open here.
- Unchanged: Theorem 1 (the upper bound ), the lower bound , the paper’s general constructions and its algorithm for do not depend on the conjecture. The paper’s question whether , and its question whether is monotone, remain open here.
ASSUMED-UNVERIFIED
The bounded literature check does not establish worldwide priority or absence of an independent counterexample. The Lean kernel verifies the encoded statement and its axiom closure; correspondence to the external paper, including the reading of the cases display as the definition of a representation and the hypothesis as a weakening, is checked by reading the source and the definitions.