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
- 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.
- 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 .
- 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.