Optimal entanglement-assisted source coding under a balanced-difference promise
Julius A. Zeiss
quant-ph
Sep 14, 2026 · v1
math-ph
TL;DR
All lemmas, theorems, and corollaries on the balanced-difference source-coding bounds and quantum chromatic number are formalized and verified in Lean.
Abstract
Entanglement can reduce the communication required for coding tasks, but establishing the minimum achievable cost is essential to understanding its limits. We address this question in a zero-error source-coding task where Alice receives a word and Bob knows an unordered pair of candidates containing it. Alice does not know the pair and must enable Bob to identify her word without error using shared entanglement and one classical message. The candidates satisfy a balanced-difference promise: for words in $\mathbb{Z}_q^n$ with $n=q\ell$, each residue modulo $q$ occurs exactly $\ell$ times in their coordinatewise difference. For all integers $q\geq2$ and $\ell\geq1$, we prove that the task requires exactly $n$ messages when $(q-1)\ell$ is even and two messages when it is odd. These minima allow arbitrary finite-dimensional shared states independent of the inputs and arbitrary local measurements. In even parity, this establishes optimality of an existing entanglement-assisted protocol. In odd parity, an explicit deterministic protocol achieves the optimum of one bit without entanglement. Our proof combines Fourier analysis with a combinatorial counting argument to determine the smallest eigenvalue of the associated graphs. In even parity, this resolves the spectral assertion of Cao et al.'s Conjecture 6.3 for balanced cyclic generalized Hadamard graphs. Together with an explicit odd-parity bipartition, this determines the quantum chromatic number as $n$ in even parity and $2$ in odd parity, where the classical chromatic number is also $2$. All lemmas, theorems, and corollaries are formalized and verified in Lean.
Problem
In a zero-error entanglement-assisted source-coding task, Alice receives a word and Bob knows an unordered candidate pair containing it under a balanced-difference promise. The goal is to determine the minimum classical communication and whether entanglement helps.
Approach
The coding problem is recast as computing the least adjacency eigenvalue of balanced cyclic generalized Hadamard graphs. Fourier analysis diagonalizes these Cayley graphs, reducing the spectral bound to a combinatorial counting problem solved via a switching argument. An explicit bipartition handles the odd-parity case. All lemmas, theorems, and corollaries are formalized and verified in Lean.
Results
For all q≥2 and ℓ≥1, the task requires exactly n messages when (q−1)ℓ is even and two messages when odd. This proves optimality of the existing entanglement-assisted protocol in even parity and gives an entanglement-free optimal one-bit code in odd parity, determining quantum chromatic numbers of n and 2 respectively, and resolving the spectral part of Cao et al.'s Conjecture 6.3.