All missions

Why election control is studied

An election is run by someone — a chair, a committee, an organiser — who can shape it without touching a single ballot: by deciding which candidates appear, which voters are registered, or how the electorate is split into bodies that pre-select nominees. Bartholdi, Tovey and Trick (1992) proposed to measure how well a voting rule protects itself against such manipulation by the computational difficulty of finding a successful manipulation: a rule for which the chair's problem is NP-complete is resistant, one for which it is solvable in polynomial time is vulnerable. They studied constructive control, where the chair wants a given candidate to become the unique winner.

Hemaspaandra, Hemaspaandra and Rothe (arXiv:cs/0507027, Artificial Intelligence 171, 2007) introduced destructive control: the chair wants a despised candidate not to be the unique winner ("anyone but him"). They classified plurality, Condorcet and approval voting under seven control types in both settings. This mission formalizes the last of their main results, Theorem 3.6, on control by partition of voters.

Timeline:

• 1992: Bartholdi, Tovey and Trick define constructive control and its complexity for plurality and Condorcet; for partition of voters they use a model in which ties in subcommittees are forbidden.
• 2005–2007: Hemaspaandra, Hemaspaandra and Rothe add destructive control, approval voting, and the two tie-handling models below.
• 2026: version v5 of the paper adds Appendix A, a corrected proof of the TP case of Theorem 4.21.

Setting

An election has candidates $C=\{0,\dots,m-1\}$ and voters $V=\{0,\dots,n-1\}$, each casting a ballot. For plurality and Condorcet voting a ballot is a strict ranking of $C$; for approval voting it is the set of candidates the voter approves of. The election $(D,U)$, with candidates $D\subseteq C$ and voters $U\subseteq V$, reads each ballot through the preferences it induces on $D$. Its winner set $W(D,U)$ is:

• plurality: the candidates of $D$ ranked first among $D$ by a maximum number of voters of $U$;
• Condorcet: the $x\in D$ that beat every other $y\in D$ in the pairwise election, $\#\{v\in U: x\succ_v y\}>\#\{v\in U: y\succ_v x\}$ (at most one candidate; possibly none);
• approval: the candidates of $D$ approved by a maximum number of voters of $U$.

In control by partition of voters the chair splits $V$ into two subcommittees $V_1$ and $V_2=V\setminus V_1$ (either may be empty). Each subcommittee holds the subelection $(C,V_i)$ and nominates candidates. Under Ties-Promote (TP) it nominates all its winners; under Ties-Eliminate (TE) it nominates its winner if there is exactly one and nobody otherwise. The two-stage election then is

$$\mathrm{twoStage}(V_1)=W\bigl(N(V_1)\cup N(V_2),\,V\bigr),$$

the nominees running against each other before all voters. Given $(C,c,V)$, the constructive problem asks whether some partition gives $\mathrm{twoStage}(V_1)=\{c\}$, the destructive problem whether some partition gives $\mathrm{twoStage}(V_1)\neq\{c\}$.

Definition 3.1 of the paper: a rule is susceptible to a control type if in some election the chair can change $c$ from not being the unique winner to being it (constructive), or from being the unique winner to not being it (destructive). It is vulnerable if it is susceptible and the problem's language is in P; certifiably-vulnerable if it is susceptible and a successful partition can be computed in polynomial time; resistant if it is susceptible and the language is NP-complete.

Formalization targets

Goal: Theorem 3.6

With Hitting Set and Exact Cover by Three-Sets NP-complete (the two facts the paper takes from Garey and Johnson),

$$\begin{aligned} &\text{approval: resistant (CC, TE and TP);\ vulnerable and certifiably-vulnerable (DC, TE and TP);}\\ &\text{plurality: vulnerable and certifiably-vulnerable (CC and DC, TE);\ resistant (CC and DC, TP);}\\ &\text{Condorcet: vulnerable and certifiably-vulnerable (DC).} \end{aligned}$$

Nine clauses, each including its susceptibility part.

Milestones

1. Susceptibility witnesses: Examples 4.9, 4.10, 4.11, 4.16, 4.17.
2. Polynomial-time algorithms: Theorems 4.18 and 4.19 (plurality, TE), 4.20 (Condorcet), 4.21 (approval, destructive, TE and TP).
3. Plurality TP hardness: Claims 4.29 and 4.30 on Construction 4.28; Theorem 4.39 (Restricted Hitting Set is NP-complete); Claims 4.40 and 4.41; Corollary 4.42.
4. Approval constructive hardness: Theorems 4.45 (TP) and 4.46 (TE), by reduction from X3C.

Significance

Theorem 3.6 is where the tie-handling model changes the classification: plurality is vulnerable under TE and resistant under TP, for both constructive and destructive control. Under TE at most one candidate leaves each subcommittee; under TP any set of tied candidates may advance. The theorem also shows that approval and Condorcet, which resist constructive control by partition of voters, are vulnerable to its destructive form. Results of this kind underlie the comparison tables of the later control literature (Faliszewski, Hemaspaandra and Hemaspaandra, Control and bribery in voting, 2016).

The paper's proofs are combinatorial algorithms and many-one reductions, stated informally. No part of the paper has been machine-checked. A formal development produces:

• the elections, winner sets on candidate subsets, and the two-stage election, in a form reusable for the other control types of the paper (adding, deleting and partitioning candidates or voters);
• verified polynomial-time algorithms on Cook's Turing-machine model. Several of the printed algorithms have gaps, including the TP case of Theorem 4.21 that the authors corrected in v5, so a checked version settles their correctness;
• verified reductions from Hitting Set and X3C.

Difficulty

The algorithmic clauses need more than correctness of a decision procedure: membership in P and polynomial-time computability are statements about a one-tape Turing machine reading binary codes. An algorithm described by "for each candidate d, check …" has to be compiled to that model, and its running time bounded, which no existing library on the platform does for elections.

The plurality TE algorithms are case analyses: who can be nominated by each part, and how many first-place votes each candidate must surrender. The cases where $c$ has no first-place vote, or where a subcommittee is empty, are exactly where the printed algorithms slip. The approval TP destructive algorithm was wrong as first published.

For the hardness clauses the reductions must be shown correct for every instance. Claim 4.41 needs an arithmetic padding condition, which is why the paper first proves Restricted Hitting Set NP-complete (Theorem 4.39) and then reduces from it. NP membership, which the paper calls obvious, still has to be proved in the checking-relation form of NP.

Formalization scope

• Candidates are Fin m and voters Fin n, both possibly empty. A profile is Fin n → Ballot m, so the multiset of ballots is a list (one ballot per voter, as the paper assumes on p. 4).
• A ranking is Equiv.Perm (Fin m), read as the position of each candidate. An approval ballot is a Finset.
• Winner sets are computed on a candidate subset with the induced preferences. Every election with an empty candidate set has no winner, and an empty subcommittee ties all candidates at score zero.
• A partition is V₁ : Finset (Fin n) and its complement.
• Unique winner means the winner set equals {c}; an empty winner set is a destructive success.
• P, NP-completeness and polynomial-time computability are the published CookPvsNP notions. Instance codes are lists of binary numbers over the published alphabet BSym: $m, n, c$, then the ballots.
• A certificate function must return the code of a partition that works on every yes-instance and the fixed token "control impossible" (encNats [0]) on every no-instance.
• Construction 4.28 is a predicate satisfied by every profile of the stated shape, whatever the "arbitrary" orders.
• The only hypotheses are NP-completeness of Hitting Set (p. 24) and of X3C (p. 28), exactly as the paper states them. Both are true (Garey–Johnson SP8, SP2).

None of these is a trivializing reading. "In P" is a Turing-machine statement, not a Decidable instance. Every vulnerable or resistant clause carries its susceptibility part. A certifiable-vulnerability witness must output a successful partition, which is more than deciding the language.

Welcome contributions: proofs of the examples (finite computations), of Claims 4.29–4.41 (counting arguments), of NP membership of the control languages, and Turing-machine implementations of election-scoring primitives, which later missions can reuse.

Selected references

• E. Hemaspaandra, L. A. Hemaspaandra, J. Rothe, Anyone but Him: The Complexity of Precluding an Alternative, Artificial Intelligence 171(5–6):255–285, 2007; arXiv:cs/0507027v5, 2026. https://arxiv.org/abs/cs/0507027 — DOI https://doi.org/10.1016/j.artint.2007.01.005
• J. Bartholdi III, C. Tovey, M. Trick, How hard is it to control an election?, Mathematical and Computer Modelling 16(8–9):27–40, 1992. https://doi.org/10.1016/0895-7177(92)90085-Y
• M. Garey, D. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• S. Cook, The P versus NP problem, Clay Mathematics Institute problem description. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf
• P. Faliszewski, E. Hemaspaandra, L. A. Hemaspaandra, Control and bribery in voting, in Handbook of Computational Social Choice, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781107446984.008

Motivation

A density operator $\rho$ on $\mathbb C^d$ describes a quantum system completely, but it cannot be read off a single copy: it has to be estimated from many identically prepared copies. Its spectrum $r_1 \ge \dots \ge r_d \ge 0$, $\sum_\alpha r_\alpha = 1$, is the part of $\rho$ that does not depend on a basis. It determines the entropy and purity of the state and the amount of entanglement it carries when it is the reduced state of a pure state.

Keyl and Werner (arXiv:quant-ph/0102027, Phys. Rev. A 64, 052311, 2001) proposed measuring $N$ copies with the projections of the Schur–Weyl decomposition of $(\mathbb C^d)^{\otimes N}$ and reporting the normalized Young frame $Y/N$. They stated that this estimator is consistent and that its error probabilities decay exponentially, with rate the classical relative entropy of the estimate with respect to the true spectrum. The same measurement, now called weak Schur sampling, became the basic primitive of later spectrum, entropy and state tomography algorithms (Keyl, arXiv:quant-ph/0412053; O'Donnell and Wright, arXiv:1508.01907).

Timeline:

• 1990. Duffield (Proc. Amer. Math. Soc. 109, 1990) proves large-deviation properties of tensor powers of group representations, which covers the maximally mixed state $\rho = d^{-1}\mathbb 1$.
• 2001. Keyl and Werner state the theorem for every $\rho$, with a proof sketch that extends Duffield's computation.
• 2006. Keyl (arXiv:quant-ph/0412053) gives a full large-deviation analysis of the full-state estimator built on this measurement.

Setting

Fix $d \ge 1$ and $N \ge 1$. A Young frame $Y$ with $N$ boxes and at most $d$ rows is a sequence of row lengths $Y_1 \ge Y_2 \ge \dots \ge Y_d \ge 0$ with $\sum_\alpha Y_\alpha = N$.

The permutation $p$ of $N$ points acts on $(\mathbb C^d)^{\otimes N}$ by permuting the tensor factors, $S_p\,\psi_1\otimes\dots\otimes\psi_N = \psi_{p^{-1}1}\otimes\dots\otimes\psi_{p^{-1}N}$. Each $d\times d$ matrix $X$ acts by $X^{\otimes N}$. Grouping the irreducible components of the permutation action by type gives orthogonal projections $P_Y$, one for each Young frame, onto the summands $\mathcal R_Y \otimes \mathcal S_Y$. Here $\mathcal S_Y$ is the Specht module of the symmetric group, and $\mathcal R_Y$ is the Schur module carrying an irreducible representation $\pi_Y$ of $GL(d,\mathbb C)$. The character of $\pi_Y$ is $\chi_Y(\rho) = \operatorname{tr}\pi_Y(\rho)$.

The set of possible spectra is the closed ordered simplex

$$\Sigma = \{ s \in \mathbb R^d : s_1 \ge \dots \ge s_d \ge 0,\ \textstyle\sum_j s_j = 1 \}.$$

The estimator reports $Y/N \in \Sigma$. Its outcome law on $\rho^{\otimes N}$ is

$$K_N(\Delta) = \operatorname{tr}\big(E_N(\Delta)\,\rho^{\otimes N}\big), \qquad E_N(\Delta) = \sum_{Y:\ Y/N\in\Delta} P_Y .$$

The rate function is the relative entropy

$$I(s) = \sum_j s_j(\ln s_j - \ln r_j) \in [0,\infty],$$

with $0\ln 0 = 0$, and with $I(s) = +\infty$ when $s_j > 0 = r_j$ for some $j$. A set $\Delta \subseteq \Sigma$ has small boundary if its interior is dense in its closure, both taken in the topology of $\Sigma$.

Formalization targets

Goal: the Theorem of §II

For every density matrix $\rho$ on $\mathbb C^d$ with spectrum $r \in \Sigma$:

1. Asymptotic exactness. For every $f$ continuous on $\Sigma$,

$$\lim_{N\to\infty}\sum_Y f\big(Y/N\big)\operatorname{tr}(\rho^{\otimes N}P_Y) = f(r).$$

2. Error estimate. If $\rho$ is non-singular, then for every $\Delta\subseteq\Sigma$ with small boundary,

$$\lim_{N\to\infty}\frac1N\ln K_N(\Delta) = -\inf_{s\in\Delta}I(s).$$

3. Large-deviation bounds. For every $\rho$ and every $\Delta\subseteq\Sigma$, with interior and closure relative to $\Sigma$,

$$-\inf_{\operatorname{int}\Delta} I \le \liminf_N \frac1N\ln K_N(\Delta) \le \limsup_N\frac1N\ln K_N(\Delta) \le -\inf_{\operatorname{cl}\Delta} I.$$

Three printed slips are corrected in this statement:

• The printed (12) lacks the minus sign; the paper's own (11) has it.
• The printed (5)–(6) define $\Sigma$ with strict inequalities, which excludes $Y/N$ for $Y = (N,0,\dots,0)$.
• (12) fails for some singular $\rho$: there $\frac1N\ln K_N(\Delta)$ can oscillate between $-\infty$ and a finite value. Item 3 keeps the paper's "for every $\rho$".

Milestones (the steps of §III)

• the properties of the $P_Y$ from (2)–(4), including the trace form $\operatorname{tr}(S_pP_Y) = \dim\mathcal R_Y\,\hat\chi_Y(p)$ of (4) on the summand;
• the trace formula $\operatorname{tr}(\rho^{\otimes N}P_Y) = \chi_Y(\rho)\dim\mathcal S_Y$, (17);
• the weight expansion of $\chi_Y$ as the Schur polynomial $s_Y(r)$, (20);
• the highest-weight property of $Y$;
• the sandwich $r^Y \le \chi_Y(\rho) \le \dim(\mathcal R_Y)\,r^Y$, (21);
• the bound $\dim\mathcal R_Y \le (N+1)^{d(d-1)/2}$;
• the limit $\frac1N\ln\sum_Y \operatorname{tr}(\rho^{\otimes N}P_Y)e^{\eta\cdot Y} \to \ln\sum_\alpha r_\alpha e^{\eta_\alpha}$ for decreasing $\eta$, (22)–(25);
• the Legendre identity $I(s) = \sup_\eta(\eta\cdot s - \ln\sum_\alpha r_\alpha e^{\eta_\alpha})$;
• $I \ge 0$ on $\Sigma$, with $I(s) = 0$ only for $s = r$.

Significance

The theorem makes measuring the Young frame a consistent estimator of the spectrum, with an explicit exponential error rate. For a ball $B$ around $r$, the probability that $Y/N$ falls outside $B$ is $e^{-N(\inf_{\Sigma\setminus B}I + o(1))}$. This is the classical Cramér rate for the empirical distribution of $N$ samples from $r$, even though no classical samples from $r$ are ever produced. The same Schur–Weyl measurement underlies sample-optimal spectrum and state estimation, the quantum empirical-distribution analogues of Sanov's theorem, and universal entanglement concentration.

The paper gives a proof sketch. Its final step needs the scaled cumulant generating function outside the ordered cone and the regularity required by the Gärtner–Ellis theorem, and the authors leave this to an extension of Duffield's work. No machine-checked proof of the theorem or of any of its steps exists. Formalizing it also adds to the published Schur–Weyl layer (QAlgorithms.Schur.isotypicProjector, schurModule, schurPolynomial) its first theorems: projection identities, the trace formula, the Schur polynomial character formula and the Weyl dimension bound. Other missions built on weak Schur sampling can reuse these.

Difficulty

The obvious argument runs through a classical reduction: diagonalize $\rho$, observe that $K_N$ depends only on $r$, and apply Sanov's theorem. This fails. $\operatorname{tr}(\rho^{\otimes N}P_Y) = \dim\mathcal S_Y\, s_Y(r)$ is not a multinomial law: the frame $Y$ is not the type of a sequence of independent samples from $r$. The authors remark that there seems to be no direct reduction to the i.i.d. setting.

The exponential rate has to be extracted from $s_Y(r)$ instead. This is a sum over exponentially many semistandard fillings, weighted by multiplicities, and it must be controlled uniformly over all frames. The paper's computation of the cumulant generating function covers only decreasing $\eta$, while the Gärtner–Ellis theorem needs it on all of $\mathbb R^d$ with regularity. For singular $\rho$, $I$ is infinite on most of $\Sigma$ and the limit (12) can genuinely fail to exist, so only the two-sided bounds survive.

Formalization scope

Lean conventions fixed by the statements:

• States are Matrix (Fin d) (Fin d) ℂ satisfying QAlgorithms.IsDensityMatrix (positive semidefinite, trace one), and $\rho^{\otimes N}$ is QAlgorithms.piKron N ρ.
• Young frames are QAlgorithms.Schur.Partition d N.
• $P_Y$ is the published isotypicProjector, defined from the permutation action alone. None of its properties is assumed; they are milestone 1.
• Rows and coordinates are indexed by Fin d, and Lean's index $0$ is the paper's index $1$.
• $\Sigma$ is the closed ordered simplex.
• $r$ is tied to $\rho$ by $\rho = U\operatorname{diag}(r)U^*$ with $U$ unitary and $r\in\Sigma$.
• $\frac1N\ln K_N(\Delta)$ is computed in EReal with $\ln 0 = -\infty$ (ENNReal.log), so an event of probability zero has rate $-\infty$, not $0$.
• $I$ is EReal-valued, equal to $+\infty$ where $s$ charges a zero of $r$.
• Interiors and closures are taken in the subspace topology of $\Sigma$. The interior of a subset of $\Sigma$ taken in $\mathbb R^d$ is empty, and that reading would make item 2 vacuous; the relative topology rules it out.
• $\Delta$ ranges over all subsets of $\Sigma$, since $K_N$ is a finite sum.
• Nothing in the goal is a free parameter pinned by hypotheses: $K_N$ is the Born probability of the actual $\rho^{\otimes N}$, and $r$ is the spectrum of $\rho$.

A complete development needs:

• the basic representation theory of the published Schur–Weyl modules;
• the character identity $\chi_Y = s_Y$;
• the Weyl dimension formula or a direct bound;
• the Gärtner–Ellis theorem, or a direct Laplace-method argument on the finite set of frames;
• the Gibbs variational formula for the relative entropy.

The Schur–Weyl facts and the Gärtner–Ellis theorem are reusable well beyond this mission. Contributions of any of these as separate theorems are welcome.

Selected references

• M. Keyl and R. F. Werner, Estimating the spectrum of a density operator, Phys. Rev. A 64, 052311 (2001). arXiv:quant-ph/0102027
• N. G. Duffield, A large deviation principle for the reduction of product representations, Proc. Amer. Math. Soc. 109, 503–515 (1990). https://www.ams.org/journals/proc/1990-109-02/
• M. Keyl, Quantum state estimation and large deviations, Rev. Math. Phys. 18, 19–60 (2006). arXiv:quant-ph/0412053
• R. O'Donnell and J. Wright, Efficient quantum tomography, STOC 2016. arXiv:1508.01907
• R. S. Ellis, Entropy, Large Deviations, and Statistical Mechanics, Springer, Grundlehren 271 (1985).

Motivation

Online platforms rank products, and the ranking is learned from clicks. Click farms and bots exploit this: fake users click on a product so that the platform promotes it. Golrezaei, Manshadi, Schneider and Sekar (arXiv:2009.05138, Operations Research 71(4), 2023) study how to learn a ranking when an unknown number of users are fake and cannot be told apart from real ones. They show that a standard optimistic learner (UCB) can be pushed to regret linear in $T$ by $O(\log^2 T)$ fake users (their Theorem 1), and they give two robust algorithms: FAR, which needs the number $F$ of fake users, and FORC (Fake-Oblivious Ranking with Cross-learning), which does not. The multi-level idea behind FORC comes from corruption-robust bandits (Lykouris, Mirrokni, Paes Leme, STOC 2018). The ranking setting makes it harder, because which products a customer examines is itself random.

Setting

A platform shows $n$ products to $T$ users in turn. Product $i$ has an unknown click probability $\mu_i\in[0,1]$, indexed so that

$$\mu_1>\mu_2>\dots>\mu_n,$$

and $\Delta_{j,i}=\mu_j-\mu_i$. A ranking $\pi$ puts product $\pi(j)$ at position $j$.

A real customer follows a cascade. She examines positions $1,2,\dots$ in turn and clicks the product at position $j$ with probability $\mu_{\pi(j)}$, which ends her visit. If she does not click, she leaves with an unknown exit probability $q_j\in[0,1]$, or moves on to position $j+1$. After position $n$ she always leaves. The platform observes $c_t$: the last examined position and whether its product was clicked.

A fake entity controls the fake users. Its adaptive policy $\mathbf P$ maps the history $\mathcal H_{t-1}=\{(\pi_s,f_s,c_s)\}_{s<t}$ (past rankings, fake indicators and observations) to a probability distribution over this round's user. The user is either real, or fake and clicking any chosen product, or fake and clicking nothing and leaving at any chosen position. The fakeness budget $F$ says that at most $F$ rounds are fake on every realization. The platform never learns which users were fake. Only real clicks count:

$$\mathrm{Reg}_T=\sup_{\mathbf P}\Big\{\mathbb E\Big[\sum_{t=1}^T\mathcal C_{r,t}(\pi^\star)\Big]-\mathbb E\Big[\sum_{t=1}^T\mathcal C_{r,t}(\pi_t)\Big]\Big\},$$

where $\mathcal C_{r,t}=1$ when the user of round $t$ is real and clicks, and $\pi^\star(i)=i$ is the optimal ranking.

FORC runs $L=\lceil\log_2T\rceil$ levels. In each round it samples level $\ell$ with probability $2^{-\ell}$ (level $1$ takes the remaining mass). Each level keeps feedback counts and a product-ordering graph $G^{(\ell)}$, whose edge $(i,j)$ records that product $j$ is believed better than $i$. The displayed ranking is $\mathrm{GraphRankSelect}(\eta^{(\ell_t)},G)$. It fills the positions in order, each time with a product that has no outgoing edge into the remaining set, preferring the one with the fewest observations. Samples propagate upward, with weight $2^{-\ell}$ at level $\ell$ (cross-learning). Edges propagate downward, and a graph that acquires a cycle is eliminated.

Formalization targets

Goal: Theorem 3

There is an absolute constant $C$ such that, for all $n\ge1$, $T\ge2$, $F\ge0$, every instance, every policy within budget $F$, and every resolution of FORC's unspecified choices,

$$\mathrm{Reg}_T(\mathrm{FORC})\le C\,\big(n^2F+\log T\big)\sum_{j=1}^n\sum_{i=j+1}^n\frac{\log(nT)}{\Delta_{j,i}}.$$

This is the paper's $O(\cdot)$ statement (16), with the constant made explicit and uniform.

Milestones, in the order the proof uses them

1. Lemma 1 (regret decomposition): for any algorithm, regret $\le F+\sum_t\sum_{j<i}\Delta_{j,i}\Pr[\mathcal A_{r,t}(\pi_t(j)=i)]$.
2. Lemma 11: one level $\ell\ge\log_2F$ is exposed to at most $\log(2L/\delta)+3$ fake users with probability at least $1-\delta/(2L)$.
3. Lemma 5: with probability at least $1-\delta/2$, every level $\ell\ge\log_2F$ is exposed to at most $\log(2L/\delta)+3$ fake users, with $\delta=1/(n^3T)$.
4. Lemma 13: a Hoeffding bound $2e^{-2\varepsilon^2\hat\eta}$ for the cross-learned weighted mean.
5. Lemma 6: the good event $\mathcal G$ (accurate estimates at the high levels, few fake users there) has probability at least $1-\delta$.
6. Lemma 15: on $\mathcal G$, the graphs of levels $\ell\ge\lceil\log_2F\rceil$ never hold an incorrect edge, and they hold the correct edge between $i$ and $j$ once both products have $\gamma_{j,i}=64\log(4nT/\delta)/\Delta_{j,i}^2$ cross-learned samples.
7. Lemma 9: the loss off $\mathcal G$ is at most $1/n^2$.

Significance

Theorem 3 says that a platform that does not know how many of its users are fake loses only $O((n^2F+\log T)\log T)$ real clicks against the best fixed ranking (for fixed $n$ and gaps bounded below). The obvious algorithms lose $\Omega(T)$. It extends multi-layer corruption robustness from multi-armed bandits to a combinatorial feedback model in which the observed coordinates are themselves random and depend on the ranking.

Formalizing it gives:

• a machine-checked cascade click model with exit probabilities and an adaptive adversary;
• a reusable regret decomposition for rankings (Lemma 1);
• a per-level corruption bound for randomized level sampling (Lemmas 5 and 11);
• a fully specified FORC.

None of these results is formalized anywhere, to our knowledge. The theorem is proved in the paper, so the remaining work is a formal proof of the known argument. The planning check of that argument found slips in constants of auxiliary lemmas (Lemmas 7, 8, 10) but nothing affecting the $O(\cdot)$ statement.

Difficulty

The levels at or above $\ell^\star=\lceil\log_2F\rceil$ are the easy part. They see $O(\log\log T)$ fake users, so their confidence windows absorb the corruption and their graphs stay correct (Lemmas 5, 6, 15).

The levels below $\ell^\star$ are the hard part. They are sampled more often and can be corrupted arbitrarily. The obvious argument would bound the misplacements at each low level separately, and that fails: a corrupted low level can keep a bad product on top for as long as it is not eliminated. The paper's Lemma 10 controls these levels only through the interaction of the two cross-learning directions. It runs an induction over products with a change of measure between levels, and that step is where the factor $n^2F$ comes from.

The adversary is adaptive and sees all past rankings. The bound fails if the adversary could see the current round's level.

Formalization scope

• Model. Products, positions, levels and rounds are Fin n, Fin n, Fin L and Fin T, all 0-based. Lean level $k$ is paper level $\ell=k+1$, so the condition $\ell\ge\lceil\log_2F\rceil$ becomes $F\le2^{k+1}$.
• Probabilities. Every space is finite, so expectations are finite sums over trajectories $\mathtt{Fin}\ T\to\mathtt{Step}$. Each trajectory is weighted by the level probabilities, the policy's PMF and the cascade law. No measure theory is used except in Lemma 13.
• Adversary. The policy is a function of the past history only. It never sees the current ranking or level.
• Algorithms. A general algorithm (Lemma 1) draws an internal label with history-dependent weights and ranks as a function of its own past. It never sees the fake indicators.
• Committed conventions. $L=\lceil\log_2T\rceil$, $\delta=1/(n^3T)$, natural logarithms. Rewards are averages of clicks, which reads Step 8's denominator $\eta+1$ as $\eta$. FORC's tie-breaking, its "arbitrary ranking" and its fallback when no level qualifies are arbitrary functions of its past, and every statement holds for all of them.
• Added hypotheses. $T\ge2$ is added to the goal, because at $T=1$ the right-hand side is $0$ while the regret can be positive. $n\ge1$ is added because $\delta$ is undefined at $n=0$.
• Ruled out. FORC's definition takes no $F$, $\mu$ or $q$. The adversary is randomized and adaptive rather than oblivious. The customer law and the level weights are probability distributions (checked in a sorry-free sanity file). $C$ is quantified before every other variable. Trivializing variants of the goal are therefore excluded.
• Out of scope. Theorem 1 (UCB's linear regret), Theorem 2 (FAR, with $F$ known), Lemmas 7, 8, 10, 16–18 (printed constants rest on non-integer counts), and the numerical study of §7.
• Infrastructure. A complete development needs a Freedman/Bernstein inequality for bounded martingale differences (Lemma 12, cited from Beygelzimer et al. 2011). It also needs the conditional form of Hoeffding behind Lemma 6, and a coupling of the finite trajectory law with independent sample sequences. These pieces are reusable for any cascade or corruption-robust bandit formalization. Proofs of the milestones, and of Lemmas 7, 8 and 10 in any faithful form, are welcome.

Selected references

• N. Golrezaei, V. Manshadi, J. Schneider, S. Sekar, Learning Product Rankings Robust to Fake Users, Operations Research 71(4), 2023; arXiv:2009.05138v1 (2020). https://arxiv.org/abs/2009.05138
• T. Lykouris, V. Mirrokni, R. Paes Leme, Stochastic Bandits Robust to Adversarial Corruptions, STOC 2018. https://arxiv.org/abs/1803.09353
• A. Beygelzimer, J. Langford, L. Li, L. Reyzin, R. Schapire, Contextual Bandit Algorithms with Supervised Learning Guarantees, AISTATS 2011. https://arxiv.org/abs/1002.4058
• N. Craswell, O. Zoeter, M. Taylor, B. Ramsey, An Experimental Comparison of Click Position-Bias Models, WSDM 2008. https://doi.org/10.1145/1341531.1341545
• B. Kveton, C. Szepesvári, Z. Wen, A. Ashkan, Cascading Bandits: Learning to Rank in the Cascade Model, ICML 2015. https://arxiv.org/abs/1502.02763

Motivation

The n-Queens problem, placing $n$ mutually non-attacking queens on an $n\times n$ chessboard, is a standard benchmark in constraint programming and artificial intelligence. As a decision problem it is trivial: a solution exists for every $n$ other than $2$ and $3$ and can be written down in closed form, and the input $\langle n\rangle$ has only $\log n$ bits. This has repeatedly led to criticism of its use as a benchmark.

The variant n-Queens Completion, posed in 1850, asks whether a board on which some queens are already placed can be completed to a full solution. Gent, Jefferson and Nightingale (JAIR 2017) show that this variant is genuinely hard: deciding it is NP-complete and counting its completions is #P-complete. This gives benchmark designers a version of the puzzle with a provable hardness guarantee, and it makes the n-Queens literature (Pólya's modular construction, Rivin–Zabih exchanges) a source of reduction gadgets.

Timeline:

• Pólya: the product construction of n-Queens solutions from modular ones (as stated by Bell and Stevens 2009, Thm. 6).
• 1992: Rivin and Zabih's exchange lemma for queens using the same lines (Thm. 2.4).
• 1996: Creignou and Hermann classify the complexity of counting generalized satisfiability; #P-completeness of Monotone 1-in-3-SAT is a corollary.
• 2014: Porschen, Schmidt, Speckenmeyer and Wotzlaw (Lemma 4): 1-in-3-SAT with positive literals, distinct variables per clause and at most three occurrences per variable is NP-complete.
• 2017: Gent, Jefferson and Nightingale: n-Queens Completion is NP-complete and #P-complete (Theorem 37).

Setting

A queen is a pair $q=(\alpha,\beta)$ of non-negative integers, its column and row. Its sum-diagonal is $\alpha+\beta$ and its difference-diagonal is the integer $\alpha-\beta$. It fits on board size $n$ if $\max(\alpha,\beta)<n$. Two distinct queens attack each other if they share a column, a row, a sum-diagonal or a difference-diagonal. A solution to the $n$-Queens problem ($n\ge1$) is a set of $n$ queens that fit on board size $n$, no two attacking.

An instance of n-Queens Completion (Problem 2) is a pair $\langle n,P\rangle$: a board size $n\ge1$ and a set $P$ of queens that fit on board size $n$, no two in the same row or column. $P$ may contain two queens on a common diagonal; such an instance simply has no solution. A completion is an $n$-Queens solution $S$ with $P\subseteq S$.

The proof passes through four intermediate problems. In Problem 3 the extra queens must use prescribed columns $C$ and rows $R$. In Problem 4 (Excluded Diagonals) sets $D^-$, $D^+$ of difference- and sum-diagonals are forbidden. Problem 5 is a family of Problem 4 instances that interact only through their sum-diagonals. Problem 6 is Restricted 1-in-3-SAT: clauses of three distinct positive variables, every variable in at most three clauses, and an assignment must make exactly one variable of every clause true.

Complexity is measured on the published CookLevin machine model: a language is a set of binary strings, CookLevin.NPComplete is NP-completeness under polynomial-time many-one reductions, and a function $f$ from strings to $\mathbb N$ is in #P if it counts the accepted certificates of an NP verifier. Every instance is coded with its board size in unary, as the paper assumes (p. 820). $\mathrm{NQC}$ is the language of codes of instances that have a completion, and $\#\mathrm{NQC}(x)$ is the number of completions of the instance coded by $x$.

Formalization targets

Goal: Theorem 37

$$\mathrm{NQC}\ \text{is NP-complete}\qquad\text{and}\qquad \#\mathrm{NQC}\ \text{is \#P-complete}.$$

Here #P-completeness means membership in #P together with hardness under parsimonious reductions: polynomial-time maps $R$ with $f(x)=\#\mathrm{NQC}(R(x))$ for every string $x$. The statement is unconditional.

Milestones

• Theorem 4: Restricted 1-in-3-SAT is NP-complete and #P-complete.
• Theorem 36, with Lemmas 33–35: variable and clause gadgets give a parsimonious reduction from Restricted 1-in-3-SAT to Problem 5.
• Theorem 23, with Lemmas 9, 21, 22: laying the gadgets out along one long diagonal reduces Problem 5 to Problem 4.
• Theorem 19, with Lemmas 17, 18: blocker queens outside the board reduce Problem 4 to Problem 3.
• Theorem 13, with Lemmas 11, 12: a 19-queens frame filled with modular solutions reduces Problem 3 to n-Queens Completion.
• Supporting results: Pólya's Theorem 2, Observation 6 on $Q_{19}$, Lemma 7 on $A_n$, $B_n$, the Rivin–Zabih Lemma 8, Lemma 25 and Observation 29, and Lemma 30.

Each reduction theorem states both halves of "parsimonious": the paper's construction preserves the number of solutions instance by instance, and a polynomial-time map on codes implements it.

Significance

The result. Theorem 37 shows that the hardness of n-Queens Completion is not an artefact of a particular solver. The same chain shows that Excluded Diagonals and Blocked n-Queens are NP- and #P-complete (Corollary 38), and Corollary 15 (from Lemma 12) shows that every non-attacking set of queens occurs inside some full solution of a larger board. Because the reductions are parsimonious, they also transfer counting hardness: counting completions exactly is as hard as #SAT.

Formalizing it. The result is proved on paper; no part of it is machine-checked. The mission adds the platform's first #P layer (#P, parsimonious reductions, #P-completeness) on top of the published CookLevin NP framework, and the first chessboard objects. Four printed slips are corrected, each with a counterexample: Lemma 8 needs $|P_1|=|P|$; Problem 3 needs $C,R\subseteq\{0,\dots,n-1\}$ (Theorem 13 fails otherwise); Definition 20's $D^+$ overshoots $2n-2$; Definition 20 is undefined for the empty family.

Difficulty

The obvious argument fails in two places.

First, each reduction is a bijection between solution sets whose correctness depends on exhaustive diagonal bookkeeping: that the 19-queens frame and the embedded modular solutions leave exactly the intended squares free, that the blockers of Definition 16 rule out exactly the chosen diagonals, and that gadgets on a long diagonal interact only through sum-diagonals. Each is a case analysis over many families of squares, with integer arithmetic on both diagonals.

Second, Theorem 4 is cited, not proved, for its hard part. A proof from scratch needs #P-hardness of a 1-in-3-SAT variant, i.e. a parsimonious version of the Cook–Levin theorem. The published CookLevin.sat_npComplete gives the decision half only, and many standard reductions from SAT are not parsimonious. In addition, every map must be shown polynomial-time on the CookLevin machine model, which the paper asserts "by inspection".

Formalization scope

Lean conventions:

• a queen is ℕ × ℕ (column, row), the difference-diagonal is computed in ℤ, and sets of queens are Finset (ℕ × ℕ);
• board sizes are $n\ge1$, and an instance of Problem 3 (hence of Problems 4 and 5) has $C,R\subseteq\{0,\dots,n-1\}$;
• a Problem 5 instance is a List of Problem 4 instances, and its sum-diagonal condition applies to distinct indices;
• a Problem 6 instance is a duplicate-free list of three-element clauses over natural-number variables, the list order being the clause order and variables ordered increasingly, and a solution is the set of true variables;
• codes write every number in unary and list a set without repetition; strings that code no valid instance are no-instances with count $0$;
• counts are Set.ncard of solution sets, which are finite.

The constructions (Definitions 10, 16, 20, 24, 26–28, 31) are transcribed as defs, never chosen by Classical.choice. Each reduction theorem fixes its output to the code of the paper's construction.

Trivializing formalizations are ruled out explicitly:

• the problems are List Bool languages, not Prop-valued predicates;
• #P membership requires the verifier's polynomial length bound, without which ncard of an infinite set is $0$;
• parsimonious reductions must be CookLevin.IsPolyTimeComputable;
• counts are of solutions, not of codes;
• the board size is unary;
• the goal assumes no hardness hypothesis.

Infrastructure that is reusable beyond this mission: the #P definitions and their closure under composition of parsimonious reductions, and polynomial-time computability of list and arithmetic manipulations on unary codes, for which the published WordRAM simulation (CookLevin.ramPolyTime_to_tm_poly, CookLevin.polyTimeComputable_comp) is the intended route. A parsimonious Cook–Levin theorem would serve every future #P-completeness result. Contributions are welcome on any milestone; the gadget lemmas (33–35) and the arithmetic facts (Lemma 9, Observations 6 and 29, Lemma 30) are self-contained and decidable on finite data.

Selected references

• I. P. Gent, C. Jefferson, P. Nightingale, Complexity of n-Queens Completion, Journal of Artificial Intelligence Research 59 (2017) 815–848. https://doi.org/10.1613/jair.5512
• J. Bell, B. Stevens, A survey of known results and research areas for n-queens, Discrete Mathematics 309(1) (2009) 1–31.
• I. Rivin, R. Zabih, A dynamic programming solution to the n-queens problem, Information Processing Letters 41(5) (1992) 253–256.
• N. Creignou, M. Hermann, Complexity of generalized satisfiability counting problems, Information and Computation 125(1) (1996) 1–12.
• S. Porschen, T. Schmidt, E. Speckenmeyer, A. Wotzlaw, XSAT and NAE-SAT of linear CNF classes, Discrete Applied Mathematics 167 (2014) 1–14.
• C. H. Papadimitriou, Computational Complexity, Addison-Wesley, 1994, Chapter 18.

Why maximal output norms matter

A quantum channel can carry classical information at a rate given by its Holevo capacity $C_1$ for one use. If a sender may encode messages in states that are entangled across $m$ uses, the capacity per use could in principle exceed $C_1$, and the ultimate classical capacity then requires a limit $m\to\infty$ (Holevo; Schumacher–Westmoreland). Whether this regularization is ever needed is the additivity question of quantum Shannon theory. It is equivalent to the additivity of the minimum output entropy of the channel (Shor 2004).

Amosov, Holevo and Werner proposed a stronger property (AHW 2000): the maximal output $z$-norm of a channel is multiplicative,

$$\nu_z(\mathcal M^{\otimes m})=[\nu_z(\mathcal M)]^m .$$

Through the Rényi entropies $S_z(\rho)=-\ln\operatorname{Tr}[\rho^z]/(z-1)$ this is the same as additivity of the minimum output Rényi entropy of order $z$, and multiplicativity for $z$ arbitrarily close to $1$ would give the additivity of the Holevo capacity.

Timeline. In 2004 Giovannetti, Lloyd, Maccone, Shapiro and Yen computed $\nu_k$ for one use of the classical-noise channel at integer $k$ (arXiv:quant-ph/0404037). In the same year Giovannetti and Lloyd proved multiplicativity for $m$ uses of that channel at every integer $k$ (arXiv:quant-ph/0403075), the result of this mission. In 2009 Hayden and Winter disproved multiplicativity for general channels at $z>1$ (arXiv:0807.4753), and Hastings disproved additivity of the minimum output entropy in general (arXiv:0809.3972). For bosonic Gaussian channels the question was settled positively by Giovannetti, Holevo and García-Patrón (arXiv:1312.2251) and Mari, Giovannetti and Holevo (arXiv:1312.3545). The integer-order case for the classical-noise channel predates these and has a self-contained Gaussian-integral proof.

The channel and the norms

One use of the channel is a single bosonic mode with annihilation operator $a$ and Fock basis $|0\rangle,|1\rangle,\dots$. The displacement operator is $D(\mu)=\exp(\mu a^\dagger-\mu^*a)$ for $\mu\in\mathbb C$. For a noise parameter $n\ge0$, the classical-noise channel displaces the input by a random amount:

$$\mathcal N_n(\rho)=\int d^2\mu\;P_n(\mu)\,D(\mu)\rho D^\dagger(\mu),\qquad P_n(\mu)=\frac{e^{-|\mu|^2/n}}{\pi n},$$

with $d^2\mu=d\,\mathrm{Re}\,\mu\,d\,\mathrm{Im}\,\mu$; at $n=0$ the law is the point mass at $0$ and the channel is the identity.

For $m$ uses the Hilbert space is $\mathcal H^{\otimes m}=\ell^2(\mathbb N^m)$, with basis $|u\rangle$, $u\in\mathbb N^m$. With $\vec\mu\in\mathbb C^m$ and $D(\vec\mu)=D_1(\mu_1)\cdots D_m(\mu_m)$,

$$\mathcal N_n^{\otimes m}(\rho)=\int d^2\vec\mu\;P_n(\vec\mu)\,D(\vec\mu)\,\rho\,D^\dagger(\vec\mu),\qquad P_n(\vec\mu)=\frac{e^{-|\vec\mu|^2/n}}{(\pi n)^m},$$

for every density operator $\rho$ of the $m$ modes, including states entangled across uses.

For $z\ge1$ the $z$-norm is $\|A\|_z=(\operatorname{Tr}|A|^z)^{1/z}$ and the maximal output $z$-norm is

$$\nu_z(\mathcal N_n^{\otimes m})=\sup_\rho\big\|\mathcal N_n^{\otimes m}(\rho)\big\|_z ,$$

the supremum over all density operators of the $m$ uses. A coherent product is $|\alpha_1\rangle\otimes\cdots\otimes|\alpha_m\rangle$, with $\langle p|\alpha\rangle=e^{-|\alpha|^2/2}\alpha^p/\sqrt{p!}$.

Formalization targets

Goal: Eq. (11)

For all $n\ge0$, all $m$ and every integer $k\ge1$,

$$\nu_k(\mathcal N_n^{\otimes m})=\left[\frac{1}{(n+1)^k-n^k}\right]^{m/k},$$

and every coherent product attains this value. Since the single-use value is $[(n+1)^k-n^k]^{-1/k}$, this is multiplicativity at every integer order.

Milestones

1. Eq. (10), for $m$-fold coherent products and every real $z\ge1$: $\|\mathcal N_n^{\otimes m}(\rho_{\vec\alpha})\|_z=[(n+1)^z-n^z]^{-m/z}$.
2. Part one (Sec. I A): every input is dominated by a pure input, so $\nu_z$ is a supremum over pure states.
3. Eqs. (16)–(17): for $\rho=|\psi\rangle\langle\psi|$, $\operatorname{Tr}\{[\mathcal N_n^{\otimes m}(\rho)]^k\}$ is the Gaussian average of $\prod_s\langle\psi|D^\dagger(\vec\mu_s)D(\vec\mu_{s+1})|\psi\rangle$.
4. Eq. (A1): the Weyl relation $D^\dagger(\vec\mu)D(\vec\nu)=D(\vec\nu-\vec\mu)\,e^{(\vec\nu\cdot\vec\mu^\dagger-\vec\mu\cdot\vec\nu^\dagger)/2}$.
5. Eq. (A12) (= (33)): $\int d^2\nu\,\frac{e^{-d|\nu|^2/|e|^2}}{\pi n|e|^2}\langle p|D(-\nu)|q\rangle=\frac{2/n}{2d+|e|^2}\big(\frac{2d-|e|^2}{2d+|e|^2}\big)^p\delta_{pq}$ for $\mathrm{Re}\,d>0$, $e\ne0$.
6. Eq. (34), last identity: $(1/n^k)/\det[C+G^\dagger G/2]=1/((n+1)^k-n^k)$ for the circulant matrices of (26)–(28).
7. Eq. (22) with $\lambda_0$ of (34): $|\langle\phi|\Theta|\phi\rangle|\le[(n+1)^k-n^k]^{-m}\|\phi\|^2$ on the $k$-copy space.
8. Eq. (12): $\operatorname{Tr}\{[\mathcal N_n^{\otimes m}(\rho)]^k\}\le[(n+1)^k-n^k]^{-m}$ for every input $\rho$.

Significance

The identity shows that, for the classical-noise channel, entangled inputs never increase the maximal output $k$-norm: the optimum over $m$ uses is attained by unentangled coherent products. Equivalently, the minimum output Rényi entropy of every integer order $k\ge2$ is additive for $\mathcal N_n$. It was one of the first proofs of the Amosov–Holevo–Werner property for an infinite-dimensional channel, and through the decomposition of Sec. II of the paper it extends to the non-circular classical channels and to the attenuator and amplifier channels with thermal noise.

The paper result is proved; no machine-checked proof exists. A formalization produces Fock-coefficient models of multi-mode displacements and of a Gaussian channel acting on entangled inputs, a Schatten-norm interface on $\ell^2$, the multi-mode Weyl relation, and the Gaussian-average identity (A12), all reusable for other bosonic channels.

Difficulty

The lower bound is a computation on coherent inputs. The upper bound must hold for every input of $m$ modes, entangled across uses, without any energy constraint, in an infinite-dimensional space. Bounding each use separately does not work: the $k$-th moment of the output is not a product over uses when the input is entangled. The obstruction is removed only after rewriting the moment as an expectation value of an operator on $k$ copies of the $m$-mode space and controlling its spectrum, which needs exact Gaussian integrals of displacement matrix elements and an explicit circulant determinant. On the formal side, the traces, functional-calculus powers and series of infinite-dimensional trace-class operators each need their own convergence arguments.

Formalization scope

• Fock coordinates are occupation strings Fin m → ℕ; operators are coefficient arrays Matrix (Fin m → ℕ) (Fin m → ℕ) ℂ with $X_{uv}=\langle u|X|v\rangle$; the Hilbert space is lp (fun _ => ℂ) 2. $\ell^2(\mathbb N)^{\otimes m}=\ell^2(\mathbb N^m)$ replaces the Hilbert tensor product, which Mathlib lacks.
• Density operators, rank-one arrays and the single-mode displacement and coherent coefficients come from two published platform definition modules (Dependency50.P33, Dependency50.P39).
• $\mathcal N_n^{\otimes m}$ is the integral (14) acting on every coefficient array; it is never defined through its values on product or coherent inputs. It is the multi-mode, coefficient-level counterpart of the platform's single-mode operator Claimed50.P39.displacementNoiseChannel, which cannot act on entangled inputs.
• The noise law is $\mathcal N(0,n/2)\otimes\mathcal N(0,n/2)$ in $(\mathrm{Re}\,\mu,\mathrm{Im}\,\mu)$; at $n=0$ it is the Dirac mass, so all statements hold for every $n\ge0$. Only (A12) and (34), whose formulas divide by $n$, assume $n>0$.
• $\|A\|_z=(\sum_u\langle u|(A^\dagger A)^{z/2}|u\rangle)^{1/z}$ through the continuous functional calculus; traces, norms and $\nu_z$ take values in $[0,\infty]$, so no supremum has a junk real value.
• $k$ ranges over all integers $k\ge1$ and $z$ over all reals $z\ge1$; the abstract's "greater than two" is not a hypothesis.

A supremum over product, Gaussian or finite-photon inputs, or a channel defined only on coherent states, would make the goal a different and much weaker theorem; $\nu_k$ here ranges over all density operators of the $m$ modes.

Contributions welcome: the multi-mode Weyl relation and Gaussian integrals of displacement matrix elements, a trace-class and Schatten-norm library on $\ell^2$ of a countable index, and the spectral argument for the operator $\Theta$.

Selected references

• V. Giovannetti, S. Lloyd, Additivity properties of a Gaussian channel, Phys. Rev. A 69, 062307 (2004); arXiv:quant-ph/0403075v3. https://arxiv.org/abs/quant-ph/0403075
• V. Giovannetti, S. Lloyd, L. Maccone, J. H. Shapiro, B. J. Yen, Minimum Rényi and Wehrl entropies at the output of bosonic channels, Phys. Rev. A 70, 022328 (2004); arXiv:quant-ph/0404037. https://arxiv.org/abs/quant-ph/0404037
• P. W. Shor, Equivalence of additivity questions in quantum information theory, Commun. Math. Phys. 246, 453 (2004); arXiv:quant-ph/0305035. https://arxiv.org/abs/quant-ph/0305035
• G. G. Amosov, A. S. Holevo, R. F. Werner, On some additivity problems in quantum information theory, Problems of Information Transmission 36, 305 (2000); arXiv:math-ph/0003002. https://arxiv.org/abs/math-ph/0003002
• P. Hayden, A. Winter, Counterexamples to the maximal p-norm multiplicativity conjecture for all p > 1, Commun. Math. Phys. 284, 263 (2008); arXiv:0807.4753. https://arxiv.org/abs/0807.4753
• M. B. Hastings, Superadditivity of communication capacity using entangled inputs, Nature Physics 5, 255 (2009); arXiv:0809.3972. https://arxiv.org/abs/0809.3972
• V. Giovannetti, A. S. Holevo, R. García-Patrón, A solution of Gaussian optimizer conjecture, Commun. Math. Phys. 334, 1553 (2015); arXiv:1312.2251. https://arxiv.org/abs/1312.2251
• A. Mari, V. Giovannetti, A. S. Holevo, Quantum state majorization at the output of bosonic Gaussian channels, Nature Communications 5, 3826 (2014); arXiv:1312.3545. https://arxiv.org/abs/1312.3545

Motivation

A binary linear code is used on a noisy channel by transmitting codewords and correcting the errors at the receiver. If $H$ is a parity-check matrix of the code and $y$ is the received word, the receiver computes the syndrome $s = yH$ and must find a minimum-weight error pattern $z$ with $zH = s$. A second basic question is whether a code has a codeword of a given weight, which governs its error-correcting ability. For a general code the best known algorithms for both tasks search an exponentially large set.

Berlekamp, McEliece and van Tilborg (IEEE Trans. Inform. Theory 24(3), 1978) showed that both tasks, in their decision form, are NP-complete. The result is the standard explanation of why no efficient general decoder is expected, and it is the hardness assumption behind code-based public-key cryptography (the McEliece cryptosystem, proposed by McEliece in the same year, and its descendants).

Timeline. Karp (1972) listed THREE-DIMENSIONAL MATCHING among 21 NP-complete problems. Berlekamp, McEliece and van Tilborg (1978) reduced it to COSET WEIGHTS and to SUBSPACE WEIGHTS. They left open whether the minimum-distance version ("weight $\le w$" in SUBSPACE WEIGHTS) is NP-complete; Vardy proved it in 1997 (IEEE Trans. Inform. Theory 43(6)).

Setting

All vectors and matrices have entries in $\mathrm{GF}(2)$, and $x$ is a row vector: $xA$ is computed modulo 2, with $x$ indexed by the rows of $A$. The Hamming weight $|x|$ is the number of nonzero entries of $x$.

• COSET WEIGHTS. Input: a binary $m \times n$ matrix $A$, a binary vector $y$ of length $n$ and a nonnegative integer $w$. Property: there is $x$ with $|x| \le w$ and $xA = y$.
• SUBSPACE WEIGHTS. Input: a binary $m \times n$ matrix $A$ and a nonnegative integer $w$. Property: there is $x$ with $|x| = w$ and $xA = 0$.
• THREE-DIMENSIONAL MATCHING (3DM). Input: a finite set $T$ and a set $U \subseteq T \times T \times T$ of triples. Property: there is $W \subseteq U$ with $|W| = |T|$ in which no two triples agree in any coordinate.

A decision problem is presented to a machine through a fixed binary encoding of its instances. It is in NP if the encodings of its yes-instances form a language with a polynomial-time verifier and polynomially long certificates. It is NP-hard if every language in NP reduces to it by a polynomial-time computable many-one reduction, a map from strings to instances that preserves the answer. It is NP-complete if both hold.

The triple incidence matrix $B$ of $U$ has one row per triple. With $|T| = n$ and $T = \{0, \dots, n-1\}$, the row of $(a, b, c)$ has a $1$ in columns $a$, $n + b$ and $2n + c$ and zeros elsewhere. For SUBSPACE WEIGHTS the paper builds, with $t = |U|$, the $(3nt + 3n + t) \times (3nt + 3n)$ matrix $A$. Its top $t$ rows are $B$ followed by $3n$ copies of the $t \times t$ identity matrix $I_t$, and its lower $3nt + 3n$ rows form the identity matrix $I_{3n(t+1)}$.

Formalization targets

Goal

$$\text{COSET WEIGHTS and SUBSPACE WEIGHTS are both in NP and both NP-hard.}$$

Formally: NPCompleteFor encodeCoset CosetWeightsYes ∧ NPCompleteFor encodeSubspace SubspaceWeightsYes, with no hypotheses. This is the paper's abstract and the two conclusions of Section III.

Milestones

1. 3DM is NP-hard (Karp's problem 17), referenced from the published PricingWithTips.threeDM_np_hard.
2. A polynomial-time many-one reduction from 3DM makes any encoded problem NP-hard.
3. COSET WEIGHTS is in NP. SUBSPACE WEIGHTS is in NP.
4. $U$ has a matching iff some $|T|$ rows of $B$ have mod 2 sum $11\cdots1$.
5. $U$ has a matching iff $(B,\ 11\cdots1,\ |T|)$ is a yes-instance of COSET WEIGHTS, and this instance is computed in polynomial time.
6. Every $x$ with $xA = 0$ satisfies $|x_1| = |y| + 3n|x_0|$ and $|x| = |y| + (3n+1)|x_0|$, where $x_0$ is the first $t$ coordinates of $x$, $x_1$ the remaining $3n(t + 1)$, and $y = x_0 B$.
7. $|x_0|$ is the quotient and $|y|$ the remainder of $|x|$ divided by $3n + 1$. In particular, $|x| = 3n^2 + 4n$ forces $|x_0| = n$ and $|y| = 3n$.
8. $U$ has a matching iff $(A,\ 3n^2 + 4n)$ is a yes-instance of SUBSPACE WEIGHTS, and this instance is computed in polynomial time.

Milestone 7 corrects the paper's wording. Read in order, "they are the remainder and quotient" makes $|x_0|$ the remainder, which is false: $n = 1$, $U = \{(1,1,1)\}$ and $x$ the all-ones vector give $|x| = 7 = 1 \cdot 4 + 3$ with $|x_0| = 1$ and $|y| = 3$. The paper's next sentence uses the correct order.

Significance

The result. NP-completeness of COSET WEIGHTS means that maximum-likelihood decoding of a general binary linear code on the binary symmetric channel is as hard as any problem in NP. Efficient decoders must therefore use structure: algebraic codes, low-density parity checks, list or iterative decoding. NP-completeness of SUBSPACE WEIGHTS shows the same for deciding whether a code has a word of a given weight, and so for computing weight distributions. Code-based cryptography cites these results to support its security assumptions. Later hardness results in coding theory (minimum distance, approximate decoding, decoding with preprocessing) build on the same reduction pattern.

Formalizing it. The result has been proved since 1978, but no machine-checked proof of it exists on this platform. What is published nearby is the NP-hardness of 3DM, in the TM2 framework this mission uses, and the NP-hardness of a gap promise version of binary syndrome decoding (the GapCVP development). The gap result is in a different machine framework, does not include NP membership, and does not cover SUBSPACE WEIGHTS. This mission adds:

• the two problems with honest encodings;
• their membership in NP, which needs polynomial-time verifiers built as Mathlib TM2 machines;
• both reductions, including the weight-counting argument behind the SUBSPACE reduction;
• a general transfer lemma for NP-hardness along polynomial-time reductions from 3DM, reusable for any further reduction from 3DM in this framework.

Difficulty

The combinatorics is short. The work lies elsewhere.

• Machine-level complexity. Mathlib states composition of polynomial-time TM2 computations only as proof_wanted. Transferring NP-hardness along a reduction therefore requires composing two TM2 machines with a polynomial time bound. The NP verifiers and the two reduction maps (building $B$ and the large matrix $A$ from the 3DM table, writing $w$ in binary) must be built as concrete multi-stack machines with step counts. A proof that only shows the maps are computable, or computable by some unspecified algorithm, does not prove these statements.
• The SUBSPACE direction "weight $3n^2+4n$ ⇒ matching". A codeword of the right weight need not visibly come from a set of triples. The weight identity and the quotient–remainder argument force $|x_0| = n$ and $x_0 B = 11\cdots1$. Since every row of $B$ has weight 3, $n$ rows summing to a vector of weight $3n$ must have disjoint supports, and disjoint supports mean a matching.
• $\le$ against $=$. COSET WEIGHTS asks for weight at most $|T|$, while a matching uses exactly $|T|$ rows. Closing the gap uses the same row-weight count.

Formalization scope

• Instances. COSET instances are CosetInstance $\langle m, n, A, y, w \rangle$ and SUBSPACE instances are SubspaceInstance $\langle m, n, A, w \rangle$, with A : Matrix (Fin m) (Fin n) (ZMod 2). $xA$ is Matrix.vecMul x A, and the Hamming weight is hammingNorm.
• Encodings. encodeCoset and encodeSubspace write $m$ and $n$ in unary, then the entries bit by bit, then $w$ in binary with a self-delimiting marker code. Unary dimensions keep the certificate length $m$ polynomial in the input length. Binary $w$ is the stricter choice for membership and changes nothing for hardness, since the reductions output $w = n$ and $w = 3n^2 + 4n$.
• 3DM. 3DM is the published PricingWithTips.ThreeDMInstance $\langle n, \mathrm{edge} \rangle$, with $T$ = Fin n and $U$ = the true entries of the table. Its yes-predicate ThreeDMYes assigns each first coordinate a pair of second and third coordinates, using no second and no third coordinate twice and only triples of $U$. The definition is imported from a market model (PricingWithTips_Model), but only its matching part, the structure Allocation, is used; nothing about markets enters. The triples are listed lexicographically, which fixes the row order of $B$.
• NP. Membership in NP is the published PricingWithTips.PolynomiallyVerifiable. NP-hardness, NPHardFor, is the published NPHardMarketPredicate generalized from 3DM instances to any encoded instance type. Reductions are many-one maps computed by Turing.TM2ComputableInPolyTime from the input string to the encoding of the produced instance.
• Ruled out. A reduction given only as a function with an "iff" is not a reduction; any problem reduces to any nontrivial problem that way. Every reduction here carries a polynomial-time TM2 machine.
• Degenerate instances are kept. With $T = \emptyset$ all three problems answer yes (SUBSPACE with $w = 0$). With $U = \emptyset$ and $n > 0$ all answer no. Both cases, and the paper's Example 1, were checked by decide on the definitions.
• Not formalized. Concluding Remarks 1)–3): full column rank, generator-matrix versions, and the minimum-distance conjecture. Also not formalized is the Section III remark relating the decision problem to finding a minimum-weight solution.
• Contributions welcome. A general composition lemma for TM2ComputableInPolyTime, and TM2 machines for matrix arithmetic over $\mathrm{GF}(2)$, are reusable well beyond this mission.

Selected references

• E. R. Berlekamp, R. J. McEliece, H. C. A. van Tilborg, On the inherent intractability of certain coding problems, IEEE Trans. Inform. Theory 24(3):384–386, 1978. https://doi.org/10.1109/TIT.1978.1055873
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, pp. 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979.
• A. Vardy, The intractability of computing the minimum distance of a code, IEEE Trans. Inform. Theory 43(6):1757–1766, 1997. https://doi.org/10.1109/18.641542
• R. J. McEliece, A public-key cryptosystem based on algebraic coding theory, DSN Progress Report 42-44, 1978.

Motivation

A quantum channel has many capacities, one for each kind of information sent and each auxiliary resource allowed: classical bits or qubits, with or without shared entanglement, with or without a free classical side channel. Comparing these capacities is how quantum Shannon theory locates the value of each resource. Some comparisons look as if they should be trivially ordered. A qubit can carry a classical bit, so one might expect the capacity for quantum information never to exceed the capacity for classical information.

Bennett, Devetak, Shor and Smolin (arXiv:quant-ph/0406086, 2004) show that this expectation fails once classical communication is free. They construct retrocorrectable channels, whose noise can be undone after the fact by combining a classical output of the channel with a reference system entangled with one of its inputs, and they show that for these channels the quantum capacity assisted by two-way classical communication, $Q_2$, exceeds the unassisted one-shot Holevo capacity, $C_H$. The one-shot Holevo capacity was the standard single-letter quantity for classical communication at the time (Holevo 1998; Schumacher and Westmoreland 1997). This mission formalizes that headline for the paper's smallest example, the qubit channel $R_{2,2}$.

Setting

The standard retrocorrectable channel $R_{c,d}$ (Fig. 1, p. 2) has a control input in $\mathbb C^c$, a data input in $\mathbb C^d$, a data output in $\mathbb C^d$, and a classical control output. At each use the channel draws, independently,

1. a basis $B=\{w_1,\dots,w_c\}$ of $\mathbb C^c$, the columns of a Haar-random unitary $W\in U(c)$, and
2. unitaries $U_1,\dots,U_c\in U(d)$, each Haar-random.

It measures the control input in the basis $B$, obtaining $j$; applies $U_j$ to the data; emits the data and the classical flag $k=(B,U_1,\dots,U_c)$; and keeps $j$ hidden. For a fixed flag, an input operator $X$ on $\mathbb C^c\otimes\mathbb C^d$ is mapped to

$$\mathcal N_k(X)=\sum_{j=1}^{c}U_j\,\operatorname{Tr}_c\!\big[(|w_j\rangle\langle w_j|\otimes I)X\big]\,U_j^\dagger .$$

The paper's example is $S=R_{2,2}$.

The one-shot Holevo capacity $C_H$ is the supremum, over finite input ensembles $\{p_x,\rho_x\}$ of density matrices on the full input, of the entropy of the average output minus the average output entropy, in bits. The flag is part of the output, but it is independent of the input, so this equals the flag average

$$\chi(\{p_x,\rho_x\})=\mathbb E_k\Big[S\Big(\sum_xp_x\mathcal N_k(\rho_x)\Big)-\sum_xp_xS(\mathcal N_k(\rho_x))\Big].$$

The two-way assisted quantum capacity $Q_2$ is the supremum of rates $R$ such that, for every $\eta>0$ and all large $n$, Alice can send $m\ge Rn$ qubits to Bob with fidelity at least $1-\eta$ on every pure message, using the channel exactly $n$ times interleaved with unlimited local operations and free classical communication in both directions, and no prior entanglement. Each use's flag becomes known after that use.

Formalization targets

Goal: the separation

$$C_H(R_{2,2})\ <\ Q_2(R_{2,2}).$$

This is the abstract's claim for the paper's witness. It fixes no constant, so it is the most stable form of the result.

Milestones

1. Echo effect (§3, p. 3). On the maximally entangled state of a reference and the control, measuring the reference in the basis $B^T$ and the control in $B$ yields equal outcomes, with probability $\delta_{ij}/c$ for the pair $(i,j)$.
2. Fig. 2 (p. 3). One use of $S$ with two-way classical communication implements a noiseless qubit channel: the output equals the input on every one-qubit state.
3. First bullet of §3 (p. 3): $Q_2(R_{2,2})\ge 1$.
4. Eq. (1) (p. 2):

$$C_H(R_{2,2})=1+\frac{\pi^2/18-5/6}{\ln 2}=0.5888 .$$

Significance

The result. The separation shows that free two-way classical communication can raise a channel's quantum capacity above its unassisted one-shot classical capacity. No ordering of the form "quantum ≤ classical" can therefore hold across assistance models without qualification. The paper uses the same family of channels to separate feedback-assisted classical capacity from $C_H$, and it places these examples in a ladder of inequalities among the assisted capacities (§5, Fig. 5). The retrocorrectable channel is a reusable counterexample: its noise is invisible to either party alone and removable by both together.

Formalizing it. The result has a complete informal argument in the paper: eq. (1) is stated with its reduction by symmetry, and the protocol of Fig. 2 is explicit. To our knowledge it has no machine-checked proof. The formal development adds three things: a definition of an operational two-way assisted capacity for channels with a continuous classical output; an exact evaluation of a one-shot Holevo capacity that requires an optimization over all input ensembles, entangled and mixed ones included; and a verified echo-effect identity that is reusable for transpose-trick protocols.

Difficulty

The two sides of the inequality are hard for different reasons.

On the $Q_2$ side, Fig. 2 makes the lower bound look immediate, but it must be carried out inside an operational model. Such a model has adaptive instruments, public outcomes, a fresh Haar-distributed flag at each use, and a protocol output that is a measure-theoretic average over the flags. Achievability then requires codes for every large block length.

On the $C_H$ side, the paper's evaluation rests on a symmetry claim: the optimum is attained by a uniform data ensemble with a fixed control input. Proving this means showing that no ensemble does better, including ensembles that entangle control and data. The obvious bound fixes one flag and maximizes, but this fails, because for a fixed flag the channel can be nearly noiseless. The bound must use the average over the Haar flag of the minimum output entropy, and that average is a two-dimensional integral over the overlaps $|\langle w_1|\psi\rangle|^2$ and $|\langle\phi|U_1^\dagger U_2|\phi\rangle|^2$. Its closed form, $5/6-\pi^2/18$ nats, has to be computed exactly.

Formalization scope

Lean conventions:

• The flag is a pair (W, U) with W : Matrix.unitaryGroup (Fin c) ℂ (the basis $B$ is its columns, whose phases are also revealed; they are independent of the input and change no capacity) and U : Fin c → Matrix.unitaryGroup (Fin d) ℂ.
• The flag law is the product of the published normalized Haar measures QAlgorithms.Schur.unitaryHaar. The paper's "random" is read as independent Haar, the reading under which eq. (1) holds.
• Inputs are indexed (control, data), 0-based.
• Entropies are in bits (QAlgorithms.vnEntropy).
• $C_H$ is an iSup in ℝ≥0∞ of a lower Lebesgue integral over the flag. $Q_2$ is an sSup in ℝ≥0∞ of achievable rates, defined through an inductive predicate of adaptive protocols with an exact count of channel uses.
• $B^T$ is the basis of transposed projectors $(|w_j\rangle\langle w_j|)^T$.

Trivializing formalizations are ruled out:

• The flag-averaged channel $\rho\mapsto\mathbb E_k\mathcal N_k(\rho)$, or any model that discards the flag, has $C_H=0$ and $Q_2=0$.
• A non-Haar flag law, a point mass for instance, makes the data channel noiseless and the goal false.
• Restricting $C_H$ to product, pure or fixed-control inputs would assume the paper's symmetry claim instead of proving it.

None of these is used: the flag is conditioned on in both capacities, the law is Haar, and ensembles range over all density matrices on $\mathbb C^2\otimes\mathbb C^2$.

Needed infrastructure: Haar integration of polynomial and entropy functionals over $U(2)$; continuity and concavity of von Neumann entropy; Bochner integration of matrix-valued maps; and the composition and repetition of adaptive protocols. Contributions toward any of these, and toward the general-$c,d$ statements of the paper, are welcome.

Selected references

• C. H. Bennett, I. Devetak, P. W. Shor, J. A. Smolin, Inequalities and separations among assisted capacities of quantum channels, arXiv:quant-ph/0406086v1, 2004. https://arxiv.org/abs/quant-ph/0406086
• A. S. Holevo, The capacity of the quantum channel with general signal states, IEEE Trans. Inf. Theory 44(1), 269–273, 1998. https://doi.org/10.1109/18.651037
• B. Schumacher, M. D. Westmoreland, Sending classical information via noisy quantum channels, Phys. Rev. A 56, 131, 1997. https://doi.org/10.1103/PhysRevA.56.131
• C. H. Bennett, D. P. DiVincenzo, J. A. Smolin, Capacities of quantum erasure channels, Phys. Rev. Lett. 78, 3217, 1997. https://arxiv.org/abs/quant-ph/9701015