Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Metadata
slug: lee-kjoshanssen-2026-quantum-cerny-thue-morse
bibkey: lee2026quantumcerny
doi: null
url: https://arxiv.org/abs/2609.40154
triage: theorem
motivation_gids:
  - D5/S3/Quantum/QuantumChannels/QuantumCernyThueMorseRefutation.result

The Thue–Morse prefix 01101001 has quantum Černý complexity 3, not 2

Problem

Lee, Lee and Kjos-Hanssen, Quantum Černý complexity of binary words, arXiv:2609.40154v1, define the quantum Černý complexity as the least for which two quantum channels on density matrices and a start state make the unique shortest synchronizing word (Definition 1.1). Open problem 1 reads

(Thue–Morse prefix.) We conjecture ; the bound follows from Theorem~\ref{thm:kmp}.

Issue #13185 fixes the reading: channels and density matrices are the frozen QuantumChannel (Fin d) (Fin d) and DensityState (Fin d), letters act left to right, the reachable set is the set of images of the start state, and qc w = sInf {d | 1 ≤ d ∧ some instance of dimension d has w as its unique shortest synchronizing word}.

Motivation

The conjecture is the first item of the paper’s open problems and the test case for its question which words have . D5/S3/Quantum/QuantumChannels/QuantumCernyThueMorseRefutation.result proves that it fails.

Gap

Issue #13185 records the literature check: the paper has a single version; the authors’ Lean formalization proves only and leaves the conjecture open; no other source on quantum Černý complexity was found. not-found-in-searched-scope.

Route

  1. Linearization. For an instance let be the complex span of the differences of reachable states. A word synchronizes iff the linear map of its channel vanishes on ; both channels map into itself; the differences have trace zero, so for a qubit.
  2. Dimension lemma. For linear maps of a space of dimension at most 3 over any field, write for the map of the word . If , then one of , , , vanishes. The image of lies in that of , and equality would kill ; so $\operatorname{rank}M_{01}> \operatorname{rank}M_{01101}\ge1f_0M_{1101001}$ would vanish, so , hence . The image of lies in that of , and equality would kill ; so has rank 3, is injective, and .
  3. All four words are shorter than , so none can synchronize in a qubit instance where is the unique shortest synchronizing word. Hence no qubit instance exists, the set defining omits 2, and .

Falsifier

The proof would fail if a qubit instance had a difference space of dimension larger than 3, or if a vanishing word map on that space did not make the word synchronize.

Evidence

Numerical check (issue #13185): least-squares solutions of for random real pairs have some other word of length at most 8 with norm below in 4000 starts; positive controls with known (, , ) reach 0.157, 0.073, 0.052.

The canonical source is D5/S3/Quantum/QuantumChannels/QuantumCernyThueMorseRefutation.lean. Its public declarations are applyWord, reachable, Synchronizing, UniqueShortestSync, HasInstance, qc, thueMorsePrefix, claim, wordComp, mortal_thueMorse and result; channels and states are the frozen QuantumChannel and DensityState of D5/S3/Quantum/Foundation/FiniteStateChannel. The frozen module state has statement identity sha256:332066d32976fe43b4d932486582f8aff11487760096971ac14ea35547c4c5b3. The result declaration has statement identity sha256:1d759bb72185a8c08110b5869149d68f0cd2f72ef41a26cceaffa530c8886d76. The Freeze event is sha256:2103075b0f2102e23cbebd0493ebe987ad4e0dc65745108c5fbb2ce52e0d5f0e. Its project-level frozen prerequisite is the Freeze event of D5/S3/Quantum/Foundation/FiniteStateChannel (sha256:551ef7395f6a8461b4286652103c87fdc6c29b05f249630b04ea95ac06bbb10c). The proof uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.

Triage

Tier 1 external named conjecture (open problem 1 of a 2026 paper), preregistered in issue #13185 before any Lean. theorem; resolution refuted. The public theorem has proof_shape: content; its escape witness is the dimension lemma mortal_thueMorse. Admission basis open-problem-resolution; utility none.

What the refutation shows beyond the single word:

  • Value (proved in the paper and here). With the paper’s upper bound , the value is . The upper bound is proved in the paper and in the authors’ Lean files; it is not formalized here.
  • Mechanism (proved). A qubit gives a difference space of dimension at most 3. The prefix recurs at positions 4–5, and this recurrence, together with the first letter and the last letter , forces both letters to act bijectively or to make a shorter word synchronize.
  • Family (argument given here, not formalized). The same three steps apply to every word that starts with , ends with , and contains again at positions with and . With the map of the prefix ending at , and , equal images of and would make synchronize. A surjective would make synchronize. Equal images of and would make synchronize. An injective would make synchronize. So all such words have , and so do their images under exchanging the letters. Examples are , and ; numerically, least squares finds no qubit instance for these words (other-word norms , , ). For , where the second ends the word, it finds 0.0034.
  • Effect on the paper’s other questions.
    • Open problem 1 also asks whether all words with at least one alternation and no long constant power have . The word has both properties and , so the answer is no (proved here).
    • Open problem 3 remarks that for almost all would be consistent with the results. The family above contains, for random of length , a proportion tending to , and its letter-exchanged copy another . So at least a quarter of long words have , and almost all words having is false (by the family argument; not formalized).
    • The paper’s other results, the general bounds, and , are unaffected.
  • Open. The characterization of remains open.

ASSUMED-UNVERIFIED

The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent proof.