Why count copies of a quantum state

A mixed state of a $D$-dimensional quantum system is a $D\times D$ positive semidefinite matrix $\rho$ of trace $1$. Writing $\rho$ down takes about $D^2$ real numbers, and $D$ is exponential in the number of qubits, so learning $\rho$ in full is expensive. Holevo's theorem and the random access code bounds of Ambainis, Nayak, Ta-Shma and Vazirani say that an $n$-qubit state carries far fewer usable classical bits than its $2^n$ amplitudes suggest. Shadow tomography, introduced by S. Aaronson (arXiv:1711.01053), makes this quantitative: given $M$ known two-outcome measurements $E_1,\dots,E_M$, how many copies of an unknown $\rho$ are needed to estimate every acceptance probability $\operatorname{Tr}(E_i\rho)$ to within $\varepsilon$?

Aaronson shows that $\widetilde O(\log^4 M\cdot\log D/\varepsilon^4)$ copies suffice, polylogarithmic in $M$ and $D$. The question this mission addresses is the converse: how many copies are necessary. Section 6 of the paper proves two lower bounds. Theorem 16 gives $\Omega(\min\{D,\log M\}/\varepsilon^2)$ even when $\rho$ and the $E_i$ are diagonal (a classical distribution). Theorem 19, the goal here, strengthens the dimension term to $D^2$ for genuinely quantum states.

Timeline:

• 2016: full tomography of a $D$-dimensional state to trace-distance accuracy $\varepsilon$ needs $\Theta(D^2/\varepsilon^2)$ copies up to logarithmic factors, with upper and lower bounds by O'Donnell and Wright (arXiv:1508.01907) and Haah, Harrow, Ji, Wu and Yu (arXiv:1508.01797).
• 2017–2018: Aaronson poses shadow tomography (Problem 1), proves the polylogarithmic upper bound (Theorem 2), and proves the lower bounds of Theorems 16 and 19.
• 2020 onward: classical shadows (Huang, Kueng and Preskill, arXiv:2002.08953) and later shadow-tomography algorithms study the same estimation task with other measurement models and improved upper bounds.

Setting

Fix a dimension $D$. A two-outcome measurement is a $D\times D$ Hermitian matrix $E$ with $0\preceq E\preceq I$; it accepts $\rho$ with probability $\operatorname{Tr}(E\rho)$. The tensor power $\rho^{\otimes k}$ is the $D^k\times D^k$ matrix of $k$ independent copies. A strategy using $k$ copies is a measurement of $\rho^{\otimes k}$ with finitely many outcomes $\omega\in\Omega$, given by positive semidefinite matrices $\Pi_\omega$ with $\sum_\omega\Pi_\omega = I$, together with outputs $b(\omega)=(b_1(\omega),\dots,b_M(\omega))$. It succeeds on $\rho$ when, with probability at least $2/3$ over $\omega$, $|b_i(\omega)-\operatorname{Tr}(E_i\rho)|\le\varepsilon$ for every $i\in[M]$.

The proof works with these further objects, all defined in the mission:

• an orthogonal projection $\mathbb P$ onto an $N/2$-dimensional subspace of $\mathbb C^N$ (Hermitian, idempotent, trace $N/2$);
• $\rho_{\mathbb P} := \tfrac2N\mathbb P$, the maximally mixed state on that subspace;
• $\sigma_{\mathbb P,\varepsilon} := (1-6\varepsilon)\,\mathbb I/N + 6\varepsilon\,\rho_{\mathbb P}$;
• the von Neumann entropy in bits, $S(\rho) = -\sum_x\lambda_x\log_2\lambda_x$ over the eigenvalues of $\rho$;
• for states $\sigma_1,\dots,\sigma_K$ and $\zeta := \tfrac1K\sum_i\sigma_i^{\otimes T}$, the quantum mutual information with the classical index, $I(\zeta;i) := S(\zeta) - \tfrac1K\sum_i S(\sigma_i^{\otimes T})$.

Formalization targets

Goal: Theorem 19 (p. 23)

There are a universal constant $c>0$ and a threshold $N_0$ such that for all $D\ge N_0$, all $M$ with $\log_2 M\ge N_0^2$ and all $0<\varepsilon\le\tfrac16$, some measurements $E_1,\dots,E_M$ on $\mathbb C^D$ force every strategy that succeeds on every mixed state to use

$$k \;\ge\; c\,\frac{\min\{D^2,\ \log_2 M\}}{\varepsilon^2}$$

copies. The goal fixes only the shape $\Omega(\min\{D^2,\log M\}/\varepsilon^2)$, not a constant, so a sharper constant does not invalidate it.

Milestones (pp. 23–24)

The milestones follow the proof, which sets $N:=\lfloor\min\{D,\sqrt{\log_2 M}\}\rfloor$ and $K:=\lfloor c^{N^2}\rfloor$:

1. Eq. (2): for some $c\in(1,2)$ and all large even $N$ there are $K$ projections $\mathbb P_i$ of rank $N/2$ with $|\operatorname{Tr}(\mathbb P_i\rho_j)-\tfrac12|\le\tfrac1{12}$ for all $i\ne j$.
2. $\operatorname{Tr}(\mathbb P_i\sigma_i) = \tfrac12+3\varepsilon$.
3. $|\operatorname{Tr}(\mathbb P_j\sigma_i)-\tfrac12| = 6\varepsilon|\operatorname{Tr}(\mathbb P_j\rho_i)-\tfrac12|\le\tfrac\varepsilon2$ for $i\neq j$.
4. The exact entropy $S(\sigma_i) = \log_2 N - [1-h(\tfrac12+3\varepsilon)]$, with $h$ the binary entropy, and the bound $S(\sigma_i)\ge\log_2 N - C\varepsilon^2$.
5. $I(\zeta;i)\le T(\log_2 N - S(\sigma_i))$ when all $\sigma_i$ have equal entropy.

Significance

Theorem 19 shows that the $\log M$ dependence of shadow tomography cannot be removed, and that for $M\ge 2^{D^2}$ shadow tomography is as hard as full tomography: as $M$ grows the bound becomes the $\Omega(D^2/\varepsilon^2)$ tomography lower bound, which it therefore contains. Compared with the classical Theorem 16, it shows that quantum states need quadratically more copies in the dimension term. The $1/\varepsilon^2$ factor matches the upper bound of Proposition 20 for the decision version, so the $\varepsilon$-dependence of the lower bound is tight in that setting.

The results are proved in the paper; none of them has a machine-checked proof that we know of. Formalizing the argument requires von Neumann entropy and its additivity on tensor products, the bound $S\le\log_2(\text{dimension})$, a Holevo-plus-Fano step that turns successful estimation into mutual information, and the existence of many nearly orthogonal half-dimensional subspaces. Each is reusable well beyond this mission.

Difficulty

The obvious attempt adapts the classical argument of Theorem 16, which hides $K$ subsets of $[N]$ in a biased distribution. Quantum states allow $\exp(\Omega(N^2))$ hidden subspaces instead of $\exp(\Omega(N))$ subsets, which is where $D^2$ comes from, but two steps change character. First, the hiding family must be shown to exist: Eq. (2) is a concentration statement for random subspaces, and the lemma the paper cites for it (Lemma 18) is misstated, as explained below. Second, the information bound must be carried out for quantum states: the step "learning $i$ from $\zeta$ requires $I(\zeta;i)\ge\log_2 K$" needs Holevo's bound and Fano's inequality, adjusted for success probability $2/3$ rather than certainty.

Formalization scope

Matrices are Matrix n n ℂ over a finite index type; the goal uses $n=\texttt{Fin } D$. Conventions committed to:

• A mixed state is the published WildeQIT.IsDensityOperator (positive semidefinite, trace $1$), reused as a reference item.
• A strategy is a finite-outcome POVM on $\rho^{\otimes k}$, indexed by Fin k → Fin D, with deterministic outputs $b(\omega)\in\mathbb R^M$; classical randomness can be absorbed into the outcome set.
• Probabilities and traces are real parts of complex traces. Entropies use $\log_2$; Lean's $\log_2 0 = 0$ gives $0\log 0=0$, and vnEntropy returns $0$ on non-Hermitian matrices, which no statement uses.
• Added to the goal: the threshold $N_0$ on $D$ and $\sqrt{\log_2 M}$ (for $D=1$, $k=0$ succeeds) and $\varepsilon\le\tfrac16$ (for $\varepsilon\ge\tfrac12$, the output $b_i=\tfrac12$ succeeds with $k=0$). Problem 1's $b_i\in[0,1]$ is dropped, an equivalent statement under clipping.
• The measurements are chosen before the strategy (for every strategy, the same $E$), which is the meaning of a lower bound.

A trivializing formalization is ruled out: the goal does not mention $N$, $K$, $\mathbb P_i$, $\sigma_i$ or $\zeta$, the success condition quantifies over all mixed states rather than a vacuous class, and the measurements are fixed before the strategy.

Not drafted:

• Lemma 18 (pp. 22–23) is false as printed. Since $\mathbb E_S[\rho_S] = \mathbb I/N$, $\operatorname{Tr}(\mathbb P_T\rho_S)$ concentrates at $1/2$, not $1/4$. The proof needs only Eq. (2), which is centred correctly and is a milestone.
• Eq. (2) is stated as existence, not as "probability $1-o(1)$ over Haar-random subspaces", because Mathlib has no Haar measure on the unitary group or the Grassmannian; existence is what the proof uses.
• "$I(\zeta;i)$ must be at least $\log_2 K$" is not drafted: as stated it is imprecise for success probability $2/3$, and the correct Holevo–Fano form is left to the solver.
• The final combination $I(\zeta;i)=O(T\varepsilon^2)$, $T=\Omega(N^2/\varepsilon^2)$ is the goal's last step.

Contributions welcome: proofs of the milestones; a Haar-measure version of Eq. (2); von Neumann entropy infrastructure (additivity, the dimension bound, concavity); Holevo's bound and Fano's inequality for finite-dimensional states.

Selected references

• S. Aaronson, Shadow Tomography of Quantum States, arXiv:1711.01053v2, 2018; STOC 2018. https://arxiv.org/abs/1711.01053
• P. Hayden, D. Leung, A. Winter, Aspects of generic entanglement, Comm. Math. Phys. 265, 2006. https://arxiv.org/abs/quant-ph/0407049
• R. O'Donnell, J. Wright, Efficient quantum tomography, STOC 2016. https://arxiv.org/abs/1508.01907
• J. Haah, A. W. Harrow, Z. Ji, X. Wu, N. Yu, Sample-optimal tomography of quantum states, IEEE Trans. Inf. Theory 63, 2017. https://arxiv.org/abs/1508.01797
• A. Ambainis, A. Nayak, A. Ta-Shma, U. Vazirani, Dense quantum coding and quantum finite automata, J. ACM 49, 2002. https://arxiv.org/abs/quant-ph/9804043
• H.-Y. Huang, R. Kueng, J. Preskill, Predicting many properties of a quantum system from very few measurements, Nature Physics 16, 2020. https://arxiv.org/abs/2002.08953

Motivation

The k-server problem (Manasse, McGeoch and Sleator, 1990) is the central problem of online computation: $k$ servers sit on points of a metric space, requests arrive one at a time at points of the space, and each request must be served by moving a server to it, at a cost equal to the distance travelled. An online algorithm decides without knowing future requests; its quality is its competitive ratio, the worst-case ratio between its cost and the cost of an optimal offline schedule. Paging (caching) is the special case of a uniform metric, and weighted paging the case of a weighted star.

Timeline of the upper bounds for general metrics:

• 1990: Manasse, McGeoch and Sleator prove that every deterministic algorithm has ratio at least $k$ and conjecture that $k$ is achievable.
• 1991: Fiat, Rabani and Ravid give the first ratio depending on $k$ only (exponential in $k$).
• 1995: Koutsoupias and Papadimitriou prove that the work function algorithm is $(2k-1)$-competitive.
• For randomized algorithms against an oblivious adversary, the conjectured answer is $O(\log k)$, achieved for paging (Fiat et al., 1991), but until 2011 nothing better than the deterministic $2k-1$ was known for general metrics, even when the ratio may depend on the number of points $n$.
• 2011: Bansal, Buchbinder, Mądry and Naor give the first polylogarithmic bound, $O(\log^2 k\log^3 n\log\log n)$ (arXiv:1110.1580; J. ACM 62(5), 2015, DOI 10.1145/2783434), the result of this mission.

Setting

Let $(M,\mathrm{dist})$ be a finite metric space with $n$ points and $k$ a number of servers. A configuration $C:\{1,\dots,k\}\to M$ places server $i$ at $C(i)$. A deterministic online algorithm maps each prefix of the request sequence to a configuration that has a server at the last request; its cost on a sequence $\rho$ is the total distance travelled. $\mathrm{OPT}(C_0,\rho)$ is the least cost of any schedule serving $\rho$ from the initial configuration $C_0$. A randomized algorithm is a probability distribution over deterministic online algorithms, all starting at $C_0$; it is $c$-competitive if there is a constant $a$ such that its expected cost on every request sequence $\rho$ is at most $c\cdot\mathrm{OPT}(C_0,\rho)+a$.

The paper works with three auxiliary objects. A σ-HST is a rooted tree whose leaves are the points, in which all edges from a node to its children have one common length, equal to $1/\sigma$ times the length of the edge above that node; the distance between two leaves is the length of the tree path. A weighted σ-HST only requires that the edge above a non-root internal node be at least $\sigma$ times each edge below it. In the fractional k-server problem on a tree, the state is a vector $x$ of server probabilities on the leaves with $0\le x_i\le1$ and $\sum_i x_i=k$, a request at leaf $i$ forces $x_i=1$, and moving from $x$ to $x'$ costs $\sum_v W(v)\,|x'_v-x_v|$, where $x_v$ is the mass below node $v$ and $W(v)$ the length of the edge above $v$. In the allocation problem on a weighted star with weights $w_i$, requests carry a location $i^t$, a monotone cost vector $h^t(0)\ge\dots\ge h^t(k)\ge0$ (the cost of serving with $j$ servers there) and a server quota $\kappa(t)\le k$.

Formalization targets

Goal: Theorem 1

There is a universal constant $C>0$ such that for all $k\ge2$, every metric space $M$ with $n\ge3$ points and every initial configuration $C_0$, some randomized online algorithm starting at $C_0$ is

$$C\,\log^2 k\,\log^3 n\,\log\log n\text{-competitive.}$$

Milestones

In the order the proof uses them:

1. Claim 15: the fix-stage inequality behind the allocation algorithm's analysis.
2. Theorem 5: for every $0<\varepsilon\le1$, a fractional allocation algorithm whose hit cost is at most $(1+\varepsilon)(\mathrm{Opt}+w_{\max}g(\kappa))+a$ and whose movement cost is at most $O(\log(k/\varepsilon))(\mathrm{Opt}+w_{\max}g(\kappa))+a$, where $g(\kappa)=\sum_t|\kappa(t)-\kappa(t-1)|$.
3. Theorem 6: given such allocation algorithms, an $O(\ell\log(k\ell))$-competitive fractional k-server algorithm on every weighted σ-HST of depth $\ell$ with $\sigma=\Omega(\ell\log(k\ell))$.
4. Theorem 8: every σ-HST with $n$ leaves becomes a weighted σ-HST of depth $O(\log n)$ on the same leaves, with distances distorted by at most $2\sigma/(\sigma-1)$.
5. Lemma 25 and Theorem 24: on a σ-HST with $\sigma>5$, randomized states consistent with a changing fractional state can be maintained online at cost $O(c_t)$ per step.
6. Theorem 7: on a σ-HST with $\sigma>5$, a $c$-competitive fractional algorithm yields an $O(c)$-competitive randomized one.

Significance

The theorem broke the exponential gap between the $\Omega(\log k)$ lower bound and the $2k-1$ upper bound for randomized k-server, and showed that randomization helps on every finite metric, not only on uniform or specially structured ones. Its two-level method (a fractional algorithm on trees driven by per-node allocation problems, followed by an online rounding) became the template for later work, including the $O(\log^2 k)$ bound on HSTs of Bubeck, Cohen, Lee, Lee and Mądry (STOC 2018) and Lee's $O(\log^6 k)$ bound on general metrics (FOCS 2018).

The result is proved, in this paper. As far as is known it has no machine-checked proof. Formalizing it means formalizing the analysis of an online algorithm driven by a continuous-time process, a potential-function argument with exact constants, a tree contraction with a distortion bound, and an online randomized rounding against a transportation cost. The allocation, HST and rounding statements are reusable for other online problems on trees (metrical task systems, weighted paging).

Difficulty

For a deterministic or randomized algorithm on a tree, the natural recursion splits the servers of each node among its children. Coté, Meyerson and Poplawski showed that this works if each node solves an allocation problem with a strong guarantee: hit cost within a factor $1+\varepsilon$ of optimal. Integral allocation algorithms cannot achieve this; the integrality gap example of the paper (p. 8) gives a factor $\Omega(k)$. The fractional relaxation avoids the gap, but then the rounding step must keep a randomized state consistent with a fractional state at constant-factor cost, and the HSTs obtained from general metrics have depth growing with the aspect ratio, which a depth-dependent ratio cannot afford. Each of the three reductions (allocation to fractional k-server, deep HST to shallow weighted HST, fractional to randomized) loses only polylogarithmic or constant factors, and the main theorem needs all three at once.

Formalization scope

The k-server model, randomized algorithms and competitiveness are the published definitions KServer_model and KServer_randomized; competitiveness carries an additive constant fixed before the request sequence. Trees are finite rooted trees with a parent map, a depth function and positive edge lengths; points of the k-server problem are the leaves, and the theorems take an arbitrary finite metric space together with a bijection to the leaves and the hypothesis that the distance equals the tree distance. Fractional k-server states have exactly $k$ units of mass, each leaf at most $1$, and fractional algorithms are measured against the integral offline optimum. The allocation optimum is the integral optimum; cost vectors are finite, non-negative and non-increasing; the diameter of the star is $w_{\max}=\max_i w_i$. The cost of changing a randomized state is the transportation cost over couplings, with minimum-matching cost between configurations. Every $O(\cdot)$ is an explicit constant quantified before the instance, except that in Theorems 7 and 24 and Lemma 25 it may depend on $\sigma$.

Formalizations that make the targets trivial are excluded: the fractional state must place a full server on every request and stay in $[0,1]$, the benchmark is the integral optimum (not the algorithm's own or the fractional cost), and no constant may depend on $k$, $n$, the metric or the tree, since otherwise Theorem 1 would follow from the $2k-1$ bound.

The proof of Theorem 1 also uses the embedding of Fakcharoenphol, Rao and Talwar [18] of a finite metric into a distribution over σ-HSTs with expected distortion $O(\sigma\log_\sigma n)$. It is an external ingredient, not a result of this paper, and is not a milestone; contributions formalizing it (or Bartal's earlier embedding) are welcome, as are formalizations of the integral optimum's properties on trees (Lemmas 21–22 of the paper), which are not stated here.

Selected references

• N. Bansal, N. Buchbinder, A. Mądry, J. Naor, A Polylogarithmic-Competitive Algorithm for the k-Server Problem, arXiv:1110.1580v1, 2011; J. ACM 62(5), 2015. https://arxiv.org/abs/1110.1580, https://doi.org/10.1145/2783434
• M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
• E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42(5), 1995. https://doi.org/10.1145/210118.210128
• A. Fiat, R. Karp, M. Luby, L. McGeoch, D. Sleator, N. Young, Competitive paging algorithms, J. Algorithms 12, 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• J. Fakcharoenphol, S. Rao, K. Talwar, A tight bound on approximating arbitrary metrics by tree metrics, J. Comput. Syst. Sci. 69(3), 2004. https://doi.org/10.1016/j.jcss.2004.04.011
• A. Coté, A. Meyerson, L. Poplawski, Randomized k-server on hierarchical binary trees, STOC 2008. https://doi.org/10.1145/1374376.1374474

Motivation

Project scheduling with cumulative resources models production and logistics projects in which activities fill and empty storage: an activity withdraws material from an inventory when it starts and deposits its output when it completes, and every inventory must stay between a safety stock and a storage capacity. Neumann, Schwindt and Zimmermann treat this model in §2.12 of Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2) and use it in their process-industry applications.

Before any optimization, a scheduler must know whether a feasible schedule exists at all. Theorem 2.12.1 of the book answers the complexity of this question: it is NP-complete, and it stays NP-complete when the project network has no cycles. The contrast with renewable resources (machines, workers) is the point of the theorem: with renewable resources, the feasibility problem is NP-complete as well (Theorem 2.3.13, after Bartusch, Möhring and Radermacher, 1988), but an acyclic network always admits a feasible schedule when every requirement is within capacity.

The mission also collects the two other reductions the book proves in full: Proposition 2.5.4 (recognizing whether an activity lies in some minimal delaying alternative, the branching object of the book's branch-and-bound procedures, is NP-complete) and Proposition 3.4.2 (maximizing weighted start-time deviations, a resource-levelling objective, is NP-hard without any resource constraints).

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$; activity $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has a duration $p_i\in\mathbb N$, with $p_0=p_{n+1}=0$. The project network $N$ has arc set $E$; an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$ on the start times. A schedule is a real vector $S=(S_i)_{i\in V}$ with $S_0=0$ and $S_i\ge0$; it is time-feasible if it meets every temporal constraint.

Cumulative resources $k\in\mathcal R^\gamma$ carry integer demands $r_{ik}$: $r_{ik}<0$ depletes $-r_{ik}$ units at the start $S_i$, $r_{ik}>0$ replenishes $r_{ik}$ units at the completion $S_i+p_i$, and $r_{0k}$ is the initial stock. The inventory at time $t$ is

$$r_k(S,t)=\sum_{i:\ r_{ik}<0,\ S_i\le t} r_{ik}+\sum_{i:\ r_{ik}>0,\ S_i+p_i\le t} r_{ik}.$$

With safety stock $\underline R_k$ and storage capacity $\overline R_k$ (integers, $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$ by (2.12.1)), $S$ is feasible if it is time-feasible and $\underline R_k\le r_k(S,t)\le\overline R_k$ for every $k$ and every $t\ge0$. The decision problem of $PSc|temp|C_{\max}$ asks whether a feasible schedule exists.

For renewable resources $k\in\mathcal R$ with capacities $R_k$ and requirements $r_{ik}\in\mathbb N$, a set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$. A delaying alternative for $F$ is a set $B\subseteq F$ such that $F\setminus B$ is not forbidden; it is minimal if no proper subset of $B$ is one.

In $PS\infty|temp,\bar d|f$ there are no resources, schedules must also satisfy $S_{n+1}\le\bar d$, and the objective here is $f(S)=-\sum_{i\in V}\sum_{j>i}w_{ij}|S_j-S_i|$ with weights $w_{ij}\ge0$.

NP and NP-completeness are taken in the sense of Cook's Turing-machine formulation, with instances written in binary.

Formalization targets

Goal: Theorem 2.12.1

Assuming PARTITION is NP-complete,

$$L=\{\text{codes of instances of }PSc|temp|C_{\max}\text{ with a feasible schedule}\}\ \text{ and }\ L_{\mathrm{acyc}}=L\cap\{N\text{ acyclic}\}$$

are both NP-complete.

Milestones

1. Membership (proof of Theorem 2.12.1): $L\in\mathrm{NP}$ and $L_{\mathrm{acyc}}\in\mathrm{NP}$.
2. Reduction correctness (proof of Theorem 2.12.1): for sizes $s(1),\dots,s(\nu)$ with even sum, the project with $r_0=r_{n+1}=-\sum s(i)/2$, $r_i=s(i)$, $\underline R=\overline R=0$, $d^{\min}_{0,n+1}=1$ has an acyclic network, and it has a feasible schedule iff the sizes split into two parts of equal sum.
3. Polynomial transformation: $\mathrm{PARTITION}\le_p L_{\mathrm{acyc}}$.
4. Proof of Proposition 2.5.4, one resource: for $j^*\in B\subseteq F$, $B$ is a minimal delaying alternative iff $R-\min_{j\in B}r_j<\sum_{i\in F\setminus B}r_i\le R$.
5. Proof of Proposition 2.5.4, with $r_{j^*}=1$: a minimal delaying alternative contains $j^*$ iff some $A\subseteq F\setminus\{j^*\}$ has $\sum_{i\in A}r_i=R$.
6. Proposition 2.5.4: assuming SUBSET SUM is NP-complete, deciding whether some minimal delaying alternative for a forbidden set $F$ contains $j^*\in F$ is NP-complete.
7. Proof of Proposition 3.4.2: a graph has a cut of at least $M$ edges iff the constructed instance has a schedule with $S_i\in\{0,1\}$ and $\sum_{i<j}w_{ij}|S_j-S_i|\ge M$.
8. Proposition 3.4.2: assuming SIMPLE MAX CUT is NP-complete, the decision version of $PS\infty|temp,\bar d|-\sum\sum w_{ij}|S_j-S_i|$ is NP-hard.

The goal follows from milestones 1 and 3 together with the transfer of NP-completeness along $\le_p$ (on the platform as CookPvsNP.npComplete_of_polyReducible).

Significance

The result. Theorem 2.12.1 explains why the book's methods for cumulative resources enumerate precedence relations between depleting and replenishing activities (minimal surplus and shortage sets, Theorem 2.12.4) instead of relying on a constructive feasibility test: unless P = NP, no polynomial algorithm decides feasibility, even for acyclic networks, where the renewable-resource case is trivial. Proposition 2.5.4 does the same for the branching scheme of §2.5, and Proposition 3.4.2 places the resource-levelling objectives of Chapter 3 among the hard ones.

Formalizing it. The three results are proved in the book, as short reductions whose delicate steps are left implicit: the polynomial size of a certificate for real-valued schedules, the handling of instances outside the construction (odd sums, empty index sets, oversized items), and the passage from an optimization problem to its decision version. None of the three reductions is machine-checked anywhere known. The mission states them against a single Turing-machine model and a single binary encoding, reusing the published definitions CookPvsNP_defs, so that the reductions compose with the Cook–Levin development already on the platform.

Difficulty

The mathematical content of the reductions is short; the difficulty is in the complexity-theoretic layer. Two steps resist the obvious argument.

First, NP membership. The book's certificate is a schedule, and a schedule is a real vector: it is not a string. A verifier needs a finite certificate of polynomial length, and it is not immediate that a feasible instance has a feasible schedule with small rational (or integer) start times, since the inventory constraints involve strict orderings between event times.

Second, polynomial-time computability in a concrete Turing-machine model. The transformation must compute, on a one-tape machine, binary codes of sums and halves of the input sizes, an arc list of quadratic length, and must map malformed strings to fixed no-instances. Informal "clearly polynomial" arguments have to become explicit machine constructions or a reusable library of closure properties.

Formalization scope

The Lean development fixes the following conventions.

• Activities are Fin (n + 2), with the completion Fin.last (n + 1); resources are Fin m. Start times are real.
• The inventory constraints hold for every $t\ge0$, not only for $0\le t\le\bar d$ as (2.12.2) is printed; the book's proofs use this reading.
• Real activities may have duration $0$ in $PSc|temp|C_{\max}$: the reduction of Theorem 2.12.1 uses only such activities.
• Instances are coded as lists of integers written in binary over the alphabet $\{0,1,-,\#\}$; arc weights are listed for every ordered pair of activities together with an arc indicator. Well-formedness (standing assumptions such as $n\ge1$, $p_0=p_{n+1}=0$, no loops, (2.12.1), $r_{ik}\le R_k$) is part of each language.
• "Acyclic" means the nodes admit a numbering increasing along every arc.
• The NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT (Karp, 1972) enters as a hypothesis of the corresponding theorem; these are not results of the book.
• Proposition 3.4.2 is stated for the decision version of the optimization problem, with natural-number weights and threshold.

A trivializing formalization is ruled out: the languages contain only codes of well-formed instances, the encoding is injective, and the hypotheses on the source problems are true theorems, so the goal cannot hold vacuously or by a degenerate encoding.

A complete development needs closure properties of polynomial-time computable functions in Cook's model (composition, binary arithmetic, list manipulation), transitivity of $\le_p$, and a small-certificate lemma for systems of difference constraints with strict and non-strict inequalities. These are reusable for every NP-hardness proof stated in the same framework. Contributions to any of them, to the instance-level milestones 2, 4, 5 and 7, or to the NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT in this model, are welcome.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. doi:10.1007/978-3-540-24800-2
• M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16, 1988.
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972. doi:10.1007/978-1-4684-2001-2_9
• S. Cook, The P versus NP Problem, Clay Mathematics Institute problem description. claymath.org

Motivation

Max $k$-cover is the basic coverage problem of combinatorial optimization. The input is a collection of subsets of a finite ground set and a number $k$; the task is to choose $k$ subsets that together cover as many points as possible. It models facility and sensor placement, the selection of a small committee or feature set representing a population, and budgeted versions of set cover. It is also the prototype of maximizing a monotone submodular function under a cardinality constraint.

The greedy algorithm covers at least a $1-1/e\approx 0.632$ fraction of the optimum. This bound goes back to Hochbaum and Pathria and, for general submodular functions, to Nemhauser, Wolsey and Fisher (1978). For two decades it was not known whether a polynomial-time algorithm could do better. Uriel Feige answered the question in A Threshold of ln n for Approximating Set Cover (J. ACM 45(4), 1998, pp. 634–652, doi:10.1145/285055.285059), Section 5. His Theorem 5.3 (p. 648) states: "For any $\epsilon > 0$, max $k$-cover cannot be approximated in polynomial time within a ratio of $(1 - 1/e + \epsilon)$, unless $P = NP$." Together with the greedy bound, it makes $1-1/e$ the exact approximation threshold of max $k$-cover.

Timeline:

• 1978: Nemhauser, Wolsey and Fisher prove the greedy $1-1/e$ bound for monotone submodular maximization.
• 1992: Arora, Lund, Motwani, Sudan and Szegedy prove the PCP theorem. With Papadimitriou–Yannakakis (1991) it gives Theorem 2.1.1 of the paper: MAX 3SAT-B has a constant gap unless P = NP.
• 1994: Lund and Yannakakis introduce partition-system reductions from multi-prover proof systems to set cover.
• 1995: Raz proves the parallel repetition theorem (Theorem 2.2.2 of the paper).
• 1998: Feige proves the ln n threshold for set cover (the subject of mission I of this series) and the $1-1/e$ threshold for max $k$-cover.

Setting

An instance consists of $n$ points $\{0,\dots,n-1\}$, a list of subsets $S_1,\dots,S_s$ of the points, and a number $k$. Its value $\mathrm{opt}$ is the largest number of points covered by at most $k$ of the sets. Instances are written over a three-letter alphabet:

• $n$ in unary;
• each set as its characteristic bit-vector;
• $k$ in unary.

Following p. 648, a polynomial-time algorithm approximates max $k$-cover within a ratio $\delta$ if on every input it outputs a number $v$ with

$$\delta\cdot\mathrm{opt}\le v\le\mathrm{opt}.$$

The algorithm need not name the sets. This is the non-constructive notion of approximation.

The proof is a reduction from the MAX 3SAT-5 problem. A 3CNF-5 formula has exactly three literals per clause, over three distinct variables, and every variable occurs in exactly five clauses. The reduction goes through a $k$-prover proof system for such a formula $\varphi$ with $M$ clauses:

• The verifier picks $\ell$ clauses at random, and a distinguished variable in each; there are $R=(3M)^\ell$ random strings $r$.
• Each prover $P_i$ is attached to a code word of length $\ell$ and weight $\ell/2$; distinct words are at Hamming distance at least $\ell/3$.
• On coordinate $j$, prover $P_i$ receives the clause if its bit is 1, and the distinguished variable if its bit is 0.
• Answers are satisfying assignments of the received clauses and bits for the received variables.
• Two provers are consistent if they assign the same values to the distinguished variables. The verifier weakly accepts if some pair of distinct provers is consistent, and strongly accepts if every pair is.

The max $k'$-cover instance of §5 attaches to every random string $r$ a copy $B_r$ of the explicit partition system. Its points are the vectors in $\{0,\dots,k-1\}^L$ with $L=2^\ell$, so $m=k^L$. Its $L$ partitions are labelled by the $\ell$-bit strings, and each splits the points by the value of one coordinate. There are $N=mR$ points in all. For each prover $i$, question $q$ and answer $a$, the set $S_{(q,a,i)}$ collects, for every $r$ on which $P_i$ receives $q$, the $i$th part of the partition of $B_r$ labelled by the values that $a$ gives to the distinguished variables of $r$. The budget is $k'=kQ$, where $Q$ is the number of questions a single prover can receive.

Formalization targets

Goal: Theorem 5.3

$$\forall\varepsilon>0:\quad \text{max } k\text{-cover is approximable within } 1-\tfrac1e+\varepsilon \ \Longrightarrow\ \mathrm{P}=\mathrm{NP},$$

conditional on the two cited results below. The ratio is left free (any $\varepsilon>0$), so the goal records the shape of the threshold and not a particular constant.

Milestones

• Proposition 2.1.2 (p. 640): for some $\varepsilon>0$ it is NP-hard to distinguish satisfiable 3CNF-5 formulas from those in which at most a $(1-\varepsilon)$-fraction of the clauses can be satisfied simultaneously.
• Lemma 2.3.1 (p. 643): a satisfiable $\varphi$ admits a strategy that always strongly accepts; on a far-from-satisfiable $\varphi$ the weak acceptance probability is at most $k^2\,2^{-c\ell}$.
• Coverage of the explicit partition system (p. 649): $j$ subsets from pairwise different partitions cover exactly $(1-(1-1/k)^j)m$ points.
• Proposition 5.4 (p. 649): if at most $kQ$ sets cover a $(1-1/e+\varepsilon)$-fraction of the points, then at least an $\varepsilon/3$-fraction of the random strings are good. Here $r$ is good if $w_r\le3k/\varepsilon$ sets meet $B_r$ and two of them from different provers lie in the same partition.
• Decoding (p. 649): such a covering yields a strategy that weakly accepts with probability at least $(\varepsilon/3)(\varepsilon/3k)^2$.
• Gap (p. 649): a satisfiable formula gives a cover of all $N$ points by $kQ$ sets. If at most a $(1-\varepsilon')$-fraction of the clauses are satisfiable, $kQ$ sets cover at most $(1-1/e+g(k))N$ points, where $g(k)\to0$, for all large $\ell$.
• Proposition 5.1 (p. 647): every greedy run covers at least $(1-1/e)\,\mathrm{opt}$ points.

Significance

The result closes the approximability of max $k$-cover: the greedy algorithm cannot be beaten by any constant unless P = NP. Consequences:

• Submodular maximization. Coverage functions are monotone submodular, so the bound transfers to monotone submodular maximization under a cardinality constraint, whenever the function is given in a form that encodes a coverage instance.
• Other problems. Hardness results for facility location, budgeted allocation, and welfare maximization with coverage valuations reduce from it.
• The reduction itself. The $\ell$-fold $k$-prover system combined with a partition system that is exactly countable is the template for later $1-1/e$ hardness proofs.

Status: the theorem has been proved since 1998. It has not been formalized; neither the reduction nor the underlying proof systems exist in Mathlib or on this platform. This mission produces:

• a machine-checked reduction from MAX 3SAT-5 to max $k$-cover;
• an exact counting lemma for product partition systems;
• the averaging and concavity argument of Proposition 5.4;
• a formal statement of the greedy bound for coverage.

The cited PCP-based gap (Theorem 2.1.1) and parallel repetition (Theorem 2.2.2) remain hypotheses. They are separate, much larger formalization projects.

Difficulty

The obvious argument uses the soundness of the proof system directly: a large cover should force consistent answers. It fails because a cover may spend many sets on a few random strings and cover them completely, while covering the rest partially without any two sets from the same partition. What saves the argument is exact counting. For sets from pairwise different partitions, coverage is exactly $h(j)=(1-(1-1/k)^j)m$, a concave function of the number $j$ of sets used. Since the sets meet a random string $k$ times on average, Jensen's inequality caps the total coverage of such "unstructured" strings at about $(1-(1-1/k)^k)$, which tends to $1-1/e$. A further obstacle is that the reduction must run in polynomial time. The paper therefore takes $\ell$ and $k$ constant (unlike the set-cover reduction, where $\ell=\Theta(\log\log n)$), and the soundness bound $k^2 2^{-c\ell}$ must beat $(\varepsilon/3)(\varepsilon/3k)^2$ at a constant $\ell$. The quantifier order ($k$ large first, then $\ell$ large) is part of the difficulty.

A second obstacle is the machine model. The goal is a statement about polynomial-time Turing machines, so the reduction and the decision procedure built from a hypothetical approximation algorithm must be compiled into Cook's one-tape machines.

Formalization scope

• Machine model. CookPvsNP_defs (a published platform definition): one-tape Turing machines, $\mathrm{P}$, $\mathrm{NP}$, polynomial-time computable functions, CNF formulas and their encoding. "P = NP" is P Bool = NP Bool, the form in which CookPvsNP.P_ne_NP states the open problem.
• Cited results as hypotheses. Theorem 2.1.1 enters as Thm211. Raz's theorem enters as RazRepetition, its consequence stated on p. 642: the $\ell$-fold clause–variable game on a far-from-satisfiable 3CNF-5 formula has acceptance probability at most $2^{-c\ell}$. This is weaker than Raz's general theorem, so the conditional statement is stronger. No hypothesis about max $k$-cover is assumed.
• Approximation. The value form above, with no size threshold. For $\varepsilon>1/e$ the ratio exceeds one and the hypothesis is unsatisfiable on any instance with $\mathrm{opt}>0$; those values are vacuous, as in the paper.
• $\mathrm{opt}$. Taken over at most $k$ sets. This agrees with the paper's "exactly $k$" whenever $k\le s$.
• Probability and counting. Probabilities are uniform counts over the $(3M)^\ell$ random strings. Fractions in lower-bound statements are written as counts compared with multiples of $R$.
• Canonical answers. The type of answers is restricted to satisfying assignments of the received clauses, following the paper's "without loss of generality" (p. 643). All indices are 0-based.
• Partition system. The §4 construction is defined for any partition system with $\ell$-bit partition labels and instantiated with the explicit product system. Its $L=2^\ell$ coordinates are the $\ell$-bit strings themselves.
• Not formalized. The running time of the greedy algorithm, and the constructive variant (Proposition 5.2), which belongs to the set-cover mission.

A trivializing formalization is ruled out: every cited input is a named, satisfiable proposition about 3CNF formulas or the two-prover game, never about max $k$-cover, and the approximation hypothesis is satisfiable for ratios up to $1$.

Needed infrastructure, reusable beyond this mission:

• composition and simulation lemmas for Cook's machines;
• the uniformity of the verifier's questions on 3CNF-5 formulas;
• concavity of $j\mapsto 1-(1-1/k)^j$;
• $(1-1/k)^k\to 1/e$ bounds.

Contributions to any of these, or to either cited theorem, are welcome.

Selected references

• U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4) (1998) 634–652. https://doi.org/10.1145/285055.285059
• R. Raz, A parallel repetition theorem, SIAM J. Comput. 27(3) (1998) 763–803 (STOC 1995). https://doi.org/10.1137/S0097539795280895
• S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3) (1998) 501–555. https://doi.org/10.1145/278298.278306
• C. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3) (1991) 425–440. https://doi.org/10.1016/0022-0000(91)90023-X
• C. Lund, M. Yannakakis, On the hardness of approximating minimization problems, J. ACM 41(5) (1994) 960–981. https://doi.org/10.1145/185675.306789
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions—I, Math. Programming 14 (1978) 265–294. https://doi.org/10.1007/BF01588971
• S. Cook, The P versus NP problem, Clay Mathematics Institute. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

Set cover is the problem of covering a finite ground set with as few members of a given family of subsets as possible. It models facility location, crew scheduling, test-suite minimization and many other selection problems in operations research, and it is one of the canonical NP-hard problems. The greedy algorithm, which repeatedly picks the subset covering the most uncovered points, finds a cover at most about $\ln n$ times larger than the optimum on an instance with $n$ points (Johnson 1974; Lovász 1975; Chvátal 1979). Whether any efficient algorithm does substantially better was open for two decades.

Timeline of the lower bounds:

• 1992. The PCP theorem (Arora, Lund, Motwani, Sudan, Szegedy) implies that set cover cannot be approximated within some constant $1+\varepsilon$ unless P = NP.
• 1994. Lund and Yannakakis showed that set cover cannot be approximated within $\tfrac14\log_2 n$ unless $\mathrm{NP}\subseteq\mathrm{TIME}(n^{O(\mathrm{polylog}\, n)})$, and within $\tfrac12\log_2 n\approx 0.72\ln n$ under a randomized assumption.
• 1998. Feige showed that for every $\varepsilon>0$, set cover cannot be approximated within $(1-\varepsilon)\ln n$ unless $\mathrm{NP}\subseteq\mathrm{TIME}(n^{O(\log\log n)})$ (J. ACM 45(4), 634–652). This matches the greedy bound up to lower-order terms.
• 2014. Dinur and Steurer replaced the assumption by P ≠ NP (STOC 2014).

This mission formalizes Feige's theorem, the result that fixed $\ln n$ as the threshold.

Setting

An instance consists of $n$ points $\{0,\dots,n-1\}$ and a list of subsets $S_1,\dots,S_s$. A cover is a set of indices whose subsets together contain every point. The instance is coverable if every point lies in some $S_i$. It is written as a string: $n$ in unary, then each subset as its characteristic vector.

A deterministic polynomial-time algorithm approximates set cover within $\rho(n)$ if, for some threshold $n_0$ and every coverable instance with $n \ge n_0$ points, the value $v$ it outputs satisfies $\mathrm{OPT}\le v\le\rho(n)\cdot\mathrm{OPT}$, where $\mathrm{OPT}$ is the size of a smallest cover.

$\mathrm{TIME}(n^{O(\log\log n)})$ is the class of languages that a deterministic one-tape Turing machine decides within $|w|^{c(\log_2\log_2|w|+1)}+c$ steps, for some constant $c$. Machines, $\mathrm{P}$ and $\mathrm{NP}$ are those of the published definition CookPvsNP_defs.

The proof passes through three objects, each defined in the mission:

1. 3CNF-5 formulas: CNF formulas in which every clause has three literals on distinct variables and every variable occurs in exactly five clauses.
2. The $k$-prover proof system of §2.3. A verifier picks $\ell$ random clauses and a distinguished variable in each. Each prover, according to its code word, receives some of these clauses and the distinguished variables of the others. Under the weak acceptance predicate, some two provers give consistent answers on the distinguished variables. Under the strong acceptance predicate, all provers do.
3. Partition systems $B(m,L,k,d)$ (Definition 3.1). These are $L$ partitions of $m$ points, each into $k$ parts, such that covering the points with parts taken from pairwise different partitions needs at least $d$ parts.

Formalization targets

Goal: Theorem 4.4

$$\exists\,\varepsilon>0:\ \text{set cover is approximable within }(1-\varepsilon)\ln n\ \Longrightarrow\ \mathrm{NP}\subseteq\mathrm{TIME}\big(n^{O(\log\log n)}\big).$$

The statement fixes no constant beyond $\varepsilon$. The parameters $k$, $\ell$ and $m$ of the reduction are choices made inside the proof. The goal carries three cited results as hypotheses: Theorem 2.1.1 (MAX 3SAT-B gap), the consequence of Raz's parallel repetition theorem for the clause–variable game, and the Naor–Schulman–Srinivasan construction of partition systems.

Milestones, in the order the proof uses them

1. Proposition 2.1.2: MAX 3SAT-5 is gap NP-hard.
2. Proposition 2.2.1: the one-round clause–variable game has value $1-\varepsilon/3$.
3. Lemma 2.3.1: the $k$-prover system is complete with strong acceptance and has soundness $k^2 2^{-c\ell}$ for weak acceptance.
4. Lemma 3.2: partition systems with $d=(1-2/k)k\ln m$ exist.
5. Propositions 4.2 and 4.3: a cover with $(1-\delta)kQ\ln m$ subsets yields a prover strategy that is weakly accepted with probability at least $2\delta/(k\ln m)^2$.
6. Lemma 4.1: the gap between $kQ$ and $(1-2f(k))kQ\ln m$.

Significance

The result. Combined with the greedy algorithm, Theorem 4.4 shows that $\ln n$ is the approximation threshold of set cover under a mild complexity assumption. Set cover reduces approximation-preservingly to many covering problems, so the threshold transfers to them. Examples are dominating set, several facility-location and group Steiner problems, and hitting-set formulations used in scheduling and testing. The $k$-prover system with two acceptance predicates and the partition-system gadget became standard tools for later hardness-of-approximation proofs.

Formalizing it. The theorem is proved and has been strengthened (Dinur–Steurer 2014), but no machine-checked proof of any $\Omega(\log n)$ inapproximability of set cover is known. This mission contributes:

• a Lean model of multi-prover proof systems with uniform-count probabilities;
• partition systems and their probabilistic existence proof;
• a gap-preserving reduction whose running time is analysed on Turing machines, not merely asserted.

Difficulty

• The ratio comes from two gaps at once. One is a gap in acceptance probability. The other is a gap between strong and weak acceptance. A reduction from a two-prover system, as in Lund–Yannakakis, loses a constant factor because a cheating cover can use two parts of the same partition. Feige's analysis must turn every small cover into a strategy under which some pair of provers is consistent (Proposition 4.3), and this averaging argument has to lose only a factor $(k\ln m)^2$.
• Parameters interlock. $\ell=\Theta(\log\log n)$ must make $k^2 2^{-c\ell}$ smaller than $2\delta/(k\ln m)^2$ while keeping the instance of size $n^{O(\log\log n)}$. The time bound must hold for a one-tape machine, including the deterministic partition-system construction.
• Encoding. The reduction must be computed by an explicit machine on string encodings. Showing that a "clearly polynomial" construction meets the time bound on such a machine is substantial work.

Formalization scope

• Cited results as hypotheses. Theorem 2.1.1, Raz's theorem and the Naor et al. construction are not proved in the mission; each is a named proposition (Thm211, RazRepetition, NaorPartitionSystems) and a hypothesis of the goal.
  • RazRepetition is only the consequence of Raz's theorem that the paper uses (p. 642): a $2^{-c\ell}$ error bound for the repeated clause–variable game on 3CNF-5 formulas far from satisfiable.
  • NaorPartitionSystems relaxes "time linear in $m$" to polynomial time and renders "$L$ polynomial in $d$" as $L\le\lfloor\log_2 m\rfloor^a$. Both relaxations weaken the hypothesis.
• Approximation in value form. The algorithm outputs a number $v$ with $\mathrm{OPT}\le v\le\rho(n)\mathrm{OPT}$, and only on coverable instances with $n\ge n_0$. Any algorithm that outputs a cover yields such a value, so this hypothesis is weaker than the paper's. The guard $n\ge n_0$ is needed because $(1-\varepsilon)\ln n<1$ for small $n$.
• Machine model. The machines are Cook's deterministic one-tape machines. Multi-tape simulation costs a quadratic factor, which the class absorbs.
• Probabilities are uniform counts over the $(5n)^\ell$ random strings. Strategies are deterministic. Answers are canonical (satisfying on clause coordinates), as the paper assumes without loss of generality.
• Not formalized. Randomized classes (ZTIME) are not defined here, so the following are omitted: the last sentence of Lemma 3.2, Proposition 6.1, and the randomized variants.
• Ruling out a trivial formalization. The gap notion requires far-from-satisfiable formulas to have at least one clause. Otherwise the empty formula would be both a yes-instance and a no-instance, and Theorem 2.1.1 would hold trivially.
• Infrastructure and reuse. The shared layer can serve other PCP-based hardness proofs: 3CNF-5 formulas, the $k$-prover system, partition systems, and the gap-NP-hardness notion. Welcome contributions include:
  • time bounds for list and table manipulations on one-tape machines;
  • a Hadamard-code construction satisfying the weight and distance conditions;
  • the union-bound and averaging lemmas behind Lemma 2.3.1 and Proposition 4.2.

Selected references

• U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4), 634–652, 1998. https://doi.org/10.1145/285055.285059
• C. Lund, M. Yannakakis, On the hardness of approximating minimization problems, J. ACM 41(5), 960–981, 1994. https://doi.org/10.1145/185675.306789
• R. Raz, A parallel repetition theorem, SIAM J. Comput. 27(3), 763–803, 1998 (STOC 1995). https://doi.org/10.1137/S0097539795280895
• M. Naor, L. J. Schulman, A. Srinivasan, Splitters and near-optimal derandomization, FOCS 1995, 182–191. https://doi.org/10.1109/SFCS.1995.492475
• S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3), 501–555, 1998. https://doi.org/10.1145/278298.278306
• C. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. Syst. Sci. 43(3), 425–440, 1991. https://doi.org/10.1016/0022-0000(91)90023-X
• V. Chvátal, A greedy heuristic for the set-covering problem, Math. Oper. Res. 4(3), 233–235, 1979. https://doi.org/10.1287/moor.4.3.233
• I. Dinur, D. Steurer, Analytical approach to parallel repetition, STOC 2014, 624–633. https://doi.org/10.1145/2591796.2591884

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models table formatting, the placement of program segments on pages, and the allocation of files to disc tracks, and it is NP-complete, so exact solutions require search in general. Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3 (1974)) therefore studied four simple placement heuristics and bounded how far each can be from the optimum in the worst case. Their paper is one of the founding results of the worst-case analysis of approximation algorithms.

This mission concerns the two decreasing heuristics, which sort the items from largest to smallest before placing them. For them the paper proves that at most $\tfrac{11}{9}$ of the optimum, plus an additive constant, is ever used, and that the factor $\tfrac{11}{9}$ cannot be improved.

Timeline.

• 1973: D. S. Johnson's MIT thesis proves $FFD(L)\le \tfrac{11}{9}L^*+4$; the argument exceeds 75 pages.
• 1974: Johnson, Demers, Ullman, Garey and Graham publish the bound for FFD and BFD, with a complete proof of the reduction from BFD to FFD and an outline of the FFD argument.
• 1985: B. S. Baker gives a shorter proof of $FFD(L)\le\tfrac{11}{9}L^*+3$ (J. Algorithms 6).
• 1991: M. Yue publishes a proof of $FFD(L)\le\tfrac{11}{9}L^*+1$.
• 2007: G. Dósa determines the tight additive constant, $FFD(L)\le\tfrac{11}{9}L^*+\tfrac{6}{9}$ (ESCAPE 2007, LNCS 4614).

Setting

A list is a finite sequence $L=(a_1,a_2,\dots,a_n)$ of real numbers in $(0,1]$; values may repeat. A bin has capacity $1$; its level is the sum of the numbers placed in it. The optimum $L^*$ is the least number of bins into which the elements of $L$ can be distributed so that no bin has level exceeding $1$.

The bins $B_1,B_2,\dots$ start empty and the elements are placed one at a time, in list order.

• First-Fit (FF) places $a_i$ into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$.
• Best-Fit (BF) places $a_i$ into a bin whose level $\beta$ satisfies $\beta\le 1-a_i$ and is as large as possible, the one of least index among ties.
• First-Fit Decreasing (FFD) and Best-Fit Decreasing (BFD) first arrange $L$ into nonincreasing order and then apply FF, respectively BF.

$FFD(L)$ and $BFD(L)$ are the numbers of bins that receive at least one element.

Two auxiliary notions from the paper's proof also appear among the milestones. The position $(j,k)$ of an element in a packing means that it is the $k$-th element placed into bin $j$. The weight $W(X)$ of a collection of elements is defined through $k$-pieces, the elements in $(\tfrac1{k+1},\tfrac1k]$. Each element has the weight $w_1(x)=\lfloor 1/x\rfloor^{-1}$. A pair $(x,y)$ with $x$ a $k$-piece and $kx+y\le1$ has the discounted weight $w_2(x,y)=w_1(x)+\tfrac{k-1}{k}w_1(y)$, and any other pair has $w_1(x)+w_1(y)$. $W(X)$ is the least total weight over all ways of grouping $X$ into singletons and pairs.

Formalization targets

Goal: Theorem 3.2

For every list $L$,

$$FFD(L)\le \frac{11}{9}L^*+4\qquad\text{and}\qquad BFD(L)\le\frac{11}{9}L^*+4 .$$

The constants are the paper's. Both halves are part of the goal.

Milestones, in the order the argument uses them

1. Lemma 3.3. If $FFD(L)>rL^*+d$ with $r,d\ge1$, the list $L'$ keeping only the elements exceeding $(r-1)/r$ also has $FFD(L')>rL'^*+d$; the same for BFD. With $r=\tfrac{11}{9}$ this reduces the goal to lists in $(\tfrac2{11},1]$.
2. Claims 3.4.5 and 3.4.6, two steps of the proof of Theorem 3.4 that concern only the FFD packing $PF$ and the BFD run. On $[\tfrac16,1]$, BFD places every element exceeding $\tfrac13$ exactly where FFD does. Among the remaining positions of $PF$, the lexicographic order of positions respects the order of the sorted list.
3. Theorem 3.4. If $L\subseteq[\tfrac16,1]$, then $BFD(L)\le FFD(L)$. This transfers the bound from FFD to BFD on $(\tfrac2{11},1]$.
4. Lemma 4.2. For every integer $N\ge4$ and $L\subseteq(\tfrac1N,\tfrac12]$,

$$W(L)\ge FFD(L)-N+2 .$$

5. The reduced assertion (Section 4, p. 314). If $L\subseteq(\tfrac2{11},1]$, then

$$FFD(L)\le\frac{11}{9}L^*+4 .$$

6. Theorem 3.1, the matching lower bound: for each $k\ge1$ there is a list with $L^*=k$ and $FFD(L)=BFD(L)>\tfrac{11}{9}L^*-2$.

Significance

The bound makes FFD and BFD, which run in $O(n\log n)$ time, the reference heuristics for off-line bin packing. The $\tfrac{11}{9}$ bound and its proof technique of weighting functions were the model for the analysis of many later packing and scheduling heuristics. Theorem 3.1 shows that the factor is exact, so together with the goal it determines $\lim_{k\to\infty}R_{FFD}(k)=\lim_{k\to\infty}R_{BFD}(k)=\tfrac{11}{9}$, where $R_A(k)$ is the largest ratio $A(L)/L^*$ over lists with $L^*=k$.

The result is proved, but the source proves it only in part. The paper gives complete proofs of Lemma 3.3, Theorem 3.4 and Theorem 3.1. For the reduced assertion it gives only an outline, whose central inequalities involve maps the paper never defines, and it refers to the thesis for the details. Lemma 4.2 is proved in the paper through two claims. A formal proof of the goal must therefore either formalize one of the later complete proofs (Baker 1985, Yue 1991, Dósa 2007) or reconstruct the thesis argument. No machine-checked proof of the $\tfrac{11}{9}$ bound is present in Mathlib or on the platform.

Difficulty

The obvious approach, used for First-Fit in Section 2 of the same paper, assigns each element a weight depending only on its size, so that every bin of the algorithm's packing weighs at least $1$ and every bin of an optimal packing weighs at most the target ratio. For FFD no weighting of single elements works at ratio $\tfrac{11}{9}$. Summing $w_1$ over the elements overcharges the FFD packing: a set of elements fitting into one bin can carry total $w_1$-weight well above $\tfrac{11}{9}$. The paper's remedy is a weight defined on pairs, $W(X)$, which discounts elements that could share a bin with a larger one. Even with $W$, the bins of FFD whose largest element exceeds $\tfrac12$ do not fit the scheme. Handling them requires a case analysis that the paper only sketches and that runs to more than 75 pages in the thesis.

The BFD half cannot be obtained by bounding BFD by FFD in general: there are lists with $BFD(L)=\tfrac{10}{9}FFD(L)$. Theorem 3.4 works only because Lemma 3.3 first removes all elements below $\tfrac2{11}$.

Formalization scope

Lists are L : List ℝ with the predicate IsList L ($0<a\le1$ for every element), assumed by every statement. $L^*$ is optBins L, the least b : ℕ admitting a map from the items to Fin b with every bin sum at most $1$. A run keeps the nonempty bins as a List (List ℝ) in index order and opens a new bin at the end exactly when no nonempty bin fits, which matches the paper's "least $j$" over infinitely many empty bins. The fit test is non-strict. FFD and BFD are FF and BF applied to sortDesc L, a stable merge sort into nonincreasing order. They are defined for every list, so the goal is stated for arbitrary, unsorted $L$. Positions are $0$-based pairs (bin, place in bin) read off the run.

$W$ sorts its argument into nonincreasing order, so index is the position in that order. It then minimizes over involutions of the positions, which encode the partitions into one- and two-element sets. Weights are real-valued; the paper's use of rationals is incidental. The range hypotheses are exactly the paper's: $[\tfrac16,1]$ is closed in Theorem 3.4, $(\tfrac2{11},1]$ is open at $\tfrac2{11}$, and Lemma 4.2 has $\tfrac1N<a\le\tfrac12$.

A weakened goal, such as $FFD(L)\le\tfrac{11}{9}L^*+c$ with a larger $c$, a bound for sorted lists only, or the FFD half alone, is a different theorem and does not close the mission. Claims 3.4.1–3.4.4 and 3.4.7 and the inequalities $(*)$, $(**)$ of the outline are not stated: they concern the paper's step-by-step construction and the undefined maps $f$, $g$.

A complete development needs basic lemmas about FF and BF runs (levels stay at most $1$, a new bin opens only when nothing fits, runs on prefixes). It also needs invariance of FFD and BFD under permutations of equal elements, the monotonicity of $L^*$ under deletion, and $L^*\ge\sum_i a_i$. These are reusable in the other missions of this series. Proofs of individual milestones, alternative complete proofs of the goal, and sharper additive constants are all welcome.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, Ph.D. thesis, Massachusetts Institute of Technology, 1973 (reference [8] of the paper above).
• B. S. Baker, A new proof for the first-fit decreasing bin-packing algorithm, Journal of Algorithms 6(1):49–70, 1985. https://doi.org/10.1016/0196-6774(85)90018-5
• M. Yue, A simple proof of the inequality FFD(L) ≤ 11/9 OPT(L) + 1, ∀L, for the FFD bin-packing algorithm, Acta Mathematicae Applicatae Sinica 7(4):321–331, 1991.
• G. Dósa, The tight bound of first fit decreasing bin-packing algorithm is FFD(I) ≤ 11/9 OPT(I) + 6/9, ESCAPE 2007, LNCS 4614:1–11, 2007. https://doi.org/10.1007/978-3-540-74450-4_1

Motivation

Given a real matrix $A=(a_{ij})\in\mathbb R^{m\times n}$, consider maximizing the bilinear form $\sum_{i,j}a_{ij}x_iy_j$ over sign vectors $x\in\{\pm1\}^m$, $y\in\{\pm1\}^n$. This discrete optimum, written $\mathrm{OPT}(A)$, is closely tied to the cut norm of a matrix and is NP-hard to compute. Relaxing each sign to a unit vector and each product to an inner product gives the semidefinite value $\mathrm{SDP}(A)$, computable in polynomial time. Grothendieck's inequality (Grothendieck, 1953) states that the relaxation overshoots by at most a universal factor: there is a finite $K$, independent of $A$, of $m,n$, and of the dimension of the vectors, with $\mathrm{SDP}(A)\le K\cdot\mathrm{OPT}(A)$ for every $A$. The Grothendieck constant $K_G$ is the least such $K$ — equivalently, the worst-case integrality gap of the canonical semidefinite relaxation of this bilinear problem.

The constant is not a curiosity of one optimization problem. It originated in functional analysis, where it is central to the geometry of Banach spaces and to harmonic analysis; it governs the approximation ratio available for cut norms; and, in quantum information, it measures the maximal advantage of quantum over classical correlations in Bell-type experiments. Its exact value has been open since 1953.

A timeline of the bounds:

• 1953, Grothendieck. Existence of a finite $K$, together with the lower bound $K_G\ge\pi/2=1.5707\ldots$
• 1977, Krivine. $K_G\le\pi/\bigl(2\log(1+\sqrt2)\bigr)=1.7822\ldots$, obtained by analyzing hyperplane rounding, and conjectured to be optimal.
• 1984/1991, Davie and Reeds (independently). $K_G\ge1.6769\ldots$, from an explicit high-dimensional Gaussian hard instance.
• 2011, Braverman–Makarychev–Makarychev–Naor. Krivine's conjecture is false: $K_G<\pi/(2\log(1+\sqrt2))$ strictly, with no quantitative gap.
• 2014, Naor–Regev. Mixtures of Krivine schemes are asymptotically optimal: rounding schemes of this one family approach the true value of $K_G$.
• 2026, Heilman; Jones–Malavolta. The first improvements on Davie–Reeds, by $10^{-26}$ and $10^{-12}$ respectively; and the first explicit numerical improvements on Krivine's bound, of order $10^{-5}$ (Heilman; Li–Saha–Xue et al.).
• 2026, Saha–Li–Xue–Chaudhuri–Klivans–Kothari–Meka. The bounds this mission targets:

$$\frac{6\pi}{11}\ \le\ K_G\ \le\ \frac{\pi}{2\log(1+\sqrt2)}-3.47\times10^{-4},$$

i.e. $1.7135\ldots\le K_G\le1.7818\ldots$, which fixes the tenths digit of $K_G$ at $7$.

Setting

Fix $m,n\in\mathbb N$ and $A\in\mathbb R^{m\times n}$.

$$\mathrm{OPT}(A):=\max_{x\in\{\pm1\}^m,\;y\in\{\pm1\}^n}\sum_{i,j}a_{ij}x_iy_j,\qquad \mathrm{SDP}(A):=\sup_{d\in\mathbb N}\ \sup_{u_i,v_j\in S^{d-1}}\sum_{i,j}a_{ij}\langle u_i,v_j\rangle .$$

Here $u_1,\dots,u_m$ and $v_1,\dots,v_n$ are unit vectors of a common but arbitrary finite dimension $d$. Since a sign is a unit vector in dimension one, $\mathrm{OPT}(A)\le\mathrm{SDP}(A)$. Call $K$ a Grothendieck bound if $\mathrm{SDP}(A)\le K\cdot\mathrm{OPT}(A)$ for every $m$, $n$ and $A$, and set $K_G:=\inf\{K: K\text{ is a Grothendieck bound}\}$.

Upper bounds on $K_G$ come from rounding algorithms. A Krivine scheme of dimension $k$ is a pair of partitions of $\mathbb R^k$ into a $+1$ region and a $-1$ region, encoded by measurable odd functions $f,g:\mathbb R^k\to\{\pm1\}$: the algorithm maps each SDP vector to a Gaussian point in $\mathbb R^k$, correlated according to the inner products, and reads off the label of the region the point lands in. Taking $f=g=\operatorname{sgn}(z_1)$ recovers random hyperplane rounding. The quality of a scheme is carried by its normalized correlation function

$$H(t):=\frac{\pi}{2}\,\mathbb E\bigl[f(X)g(Y)\bigr],$$

where $X,Y$ are standard Gaussian vectors in $\mathbb R^k$ with $\mathbb E[X_iY_i]=t$ for every coordinate $i$. For the half-space partition $H(t)=\arcsin t$, whose analysis gives Krivine's bound. Writing the odd expansion $H(t)=b_1t+b_3t^3+\cdots$, the hyperplane scheme sits at $(b_1,b_3)=(1,\tfrac16)$.

Formalization targets

Goal

$$\frac{6\pi}{11}\ \le\ K_G\ \le\ \frac{\pi}{2\log(1+\sqrt2)}-3.47\times10^{-4}$$

This is the two-sided bound the source paper states as the outcome of its Theorems 2.1 and 2.2. It is the weakest statement that carries both of the paper's contributions at once; each side is also a milestone in its own right, so partial progress is recorded even if only one direction closes.

Milestones

The milestone list runs from the classical background to the two new bounds: $\mathrm{OPT}\le\mathrm{SDP}$; the existence of a finite Grothendieck bound; $K_G\ge\pi/2$; Krivine's $K_G\le\pi/(2\log(1+\sqrt2))$; the affine coefficient constraint $b_3\ge2b_1-\tfrac{11}{6}$ valid for every Krivine scheme (Theorem 2.2, equation (1)); the transfer of a member of the affine family into a lower bound on $K_G$ (Appendix A); the lower bound $K_G\ge6\pi/11$ (Theorem 2.2); and the cubic–quintic upper bound (Theorem 2.1).

Significance

The two target bounds narrow an interval that had been essentially static for four decades: before 2026 the state of the art was $1.6769\ldots\le K_G\le1.7822\ldots$, wide enough that the tenths digit was unknown. The lower bound is also methodologically new. Every previous lower bound was obtained by exhibiting a hard instance; this one instead proves a ceiling on the performance of every rounding scheme in the Krivine family and converts that ceiling, through the Naor–Regev optimality theorem, into a bound on the constant. The affine constraint $b_3\ge2b_1-\tfrac{11}{6}$ is the transportable core of that argument: being affine in the coefficients, it survives mixing schemes and passing to limits, which is exactly what the reduction to $K_G$ requires.

On the formalization side, nothing here is machine-checked today. The upper bound (Theorem 2.1) is certified by interval arithmetic in the companion paper, and the lower bound's central one-dimensional inequality likewise rests on a computer-assisted certificate; reproducing either inside Lean means building a rigorous numeric layer on top of the analytic argument. Ahead of that, the mission needs a formal definition of $K_G$ itself and of the Krivine-scheme apparatus, neither of which exists in Mathlib — these are reusable well beyond this mission, since Grothendieck's inequality feeds cut-norm approximation and Bell-inequality bounds. Contributions of intermediate lemmas about $\mathrm{OPT}$, $\mathrm{SDP}$, Gaussian correlation identities, and Hermite expansions are welcome even when the headline bounds stay open.

Difficulty

The obvious route to a lower bound is to write down a matrix and compute. That route is what Davie and Reeds exhausted; improving it has produced gains of order $10^{-12}$ at best, because the hard instances are high-dimensional Gaussian objects whose $\mathrm{OPT}$ is itself hard to bound tightly. The route taken here avoids instances entirely, and its difficulty lies elsewhere: a constraint on a single scheme is worthless unless it survives averaging over schemes and passing to limits of schemes of growing dimension, since only then does the Naor–Regev optimality theorem convert it into a statement about $K_G$. Constraints that are nonlinear in the scheme do not survive that passage, which is why the target inequality is affine in $(b_1,b_3)$. For the upper bound, the difficulty is that the improvement is genuinely asymptotic: it comes from a limit of schemes of growing dimension rather than any fixed low-dimensional partition, and the final margin of $3.47\times10^{-4}$ is certified numerically rather than in closed form.

Formalization scope

$\mathrm{OPT}(A)$ and $\mathrm{SDP}(A)$ are defined as suprema of explicitly described sets of reals, over matrices indexed by Fin m and Fin n with real entries; the sign vectors are real-valued functions constrained to take the values $1$ and $-1$, and the relaxation quantifies over unit vectors of EuclideanSpace ℝ (Fin d) for an existentially quantified $d$, so no dimension bound is built in. The empty-index cases $m=0$ or $n=0$ are included and give value $0$ on both sides. $K_G$ is the infimum of the set of Grothendieck bounds; that set is nonempty precisely by Grothendieck's inequality, which is itself a milestone, and it is bounded below, so the infimum is not a junk value.

A Krivine scheme is a structure carrying two measurable $\pm1$-valued functions on Fin k → ℝ, each odd almost everywhere. Almost-everywhere oddness is forced: no $\pm1$-valued function satisfies $f(-0)=-f(0)$ at the origin, so a pointwise requirement would make the structure empty and every statement about schemes vacuous. With the null-set relaxation the half-space partition is a scheme in every dimension $k\ge1$, and the definition file constructs it, pinning down non-vacuity; dimension $k=0$ admits no scheme. The correlation function is the explicit double Gaussian integral against the correlated-pair density, scaled by $\pi/2$, and the coefficients $b_1,b_3$ are read off as $H'(0)$ and $H'''(0)/6$ — where $H$ fails to be three times differentiable at $0$ these are the ambient junk value $0$, which a solver should keep in mind when reading the coefficient milestones.

No trivializing reading is available for the goal: it pins $K_G$ between two explicit numerical constants, so it can be satisfied neither vacuously nor by a degenerate convention. Solvers should be aware that the source paper states its two theorems in abridged form and refers to its companion paper for the full proofs, and that the further bounds reported there — the stronger lower rungs $27\pi/49$ and $51\pi/92$, and the upper values $1.781801841033$ and $1.7813319810625639$ — are explicitly described as system-tested but not author-verified; they are deliberately outside this mission's milestone list.

Selected references

• A. Grothendieck, Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79.
• J.-L. Krivine, Sur la constante de Grothendieck, C. R. Acad. Sci. Paris (1977).
• M. Braverman, K. Makarychev, Y. Makarychev, A. Naor, The Grothendieck constant is strictly smaller than Krivine's bound, FOCS 2011, 453–462. https://doi.org/10.1109/FOCS.2011.77
• A. Naor, O. Regev, Krivine schemes are optimal, Proc. Amer. Math. Soc. 142 (2014), 4315–4320. https://doi.org/10.1090/S0002-9939-2014-12145-3
• N. Alon, A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), 787–803. https://doi.org/10.1137/S0097539704441629
• A. Li, R. Saha, A. Xue, S. Chaudhuri, A. Klivans, P. K. Kothari, R. Meka, Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human–AI Mathematical Collaboration, arXiv:2608.11195v3, 2026. https://arxiv.org/abs/2608.11195
• R. Saha, A. Li, A. Xue, S. Chaudhuri, A. Klivans, P. K. Kothari, R. Meka, New upper and lower bounds for the Grothendieck constant, 2026 (companion paper containing the full proofs).