Operations Research

Motivation

Integer programming asks whether a system of linear inequalities $Ax\le b$ has a solution $x\in\mathbb Z^n$. In fixed dimension $n$ it is solvable in polynomial time: Lenstra (1983) proved this by showing that a convex body without integer points is "flat" in some integral direction, so that the search splits into few lower-dimensional subproblems. Kannan's 1987 paper in Mathematics of Operations Research sharpened this approach. It computes a Korkine–Zolotarev ("reduced") basis of a lattice, solves the shortest and closest vector problems exactly in $n^{O(n)}$ operations, and runs integer programming in $O(n^{9n/2}s)$ arithmetic operations. Underneath the algorithm sits a purely geometric statement, Theorem (5.5): a lattice-free convex body meets only boundedly many integer translates of some integral subspace.

Timeline.

• Korkine and Zolotareff (1873): the reduced bases used here.
• Minkowski (1896): a symmetric convex body of volume greater than $2^n$ contains a nonzero integer point.
• Khinchine (1948): lattice-free convex bodies have lattice width bounded by a function of $n$ alone (the flatness theorem).
• Lenstra (1983): integer programming in fixed dimension is polynomial, via a flat direction.
• Kannan (1987, this paper): Theorem (5.5), with subspaces $V$ of any dimension between $1$ and $n-1$ and an explicit bound $n^{2(n-\dim V)}$.
• Kannan and Lovász (1988), Banaszczyk et al. (1999), and later work: polynomial bounds on the flatness constant.

Setting

$\mathcal R^n$ is Euclidean space with dot product $(a,b)$ and length $|a|$, and $\mathbb Z^n$ is the set of integer vectors. For linearly independent $b_1,\dots,b_m\in\mathcal R^k$, the lattice $L(b_1,\dots,b_m)$ is the set of integer combinations $\sum_j\lambda_jb_j$, $\lambda_j\in\mathbb Z$, and $b_1,\dots,b_m$ is a basis. Gram–Schmidt orthogonalisation gives $b_1^*,\dots,b_m^*$ and unit vectors $u_j=b_j^*/|b_j^*|$, and $b_i(j)=(b_i,u_j)$, so $b_i=\sum_jb_i(j)u_j$ and $b_j(j)=|b_j^*|$. The determinant is $d(L)=\prod_j|b_j^*|$. $\Lambda_1(L)$ is the length of a shortest nonzero vector of $L$. The projected lattice $L_j(b_1,\dots,b_m)$ is the image of $L$ under orthogonal projection onto the complement of $\operatorname{span}(b_1,\dots,b_{j-1})$. A basis is reduced (Definition 2.6) if $b_j(j)=\Lambda_1(L_j)$ for every $j$ and $|b_i(j)|\le b_j(j)/2$ for $i>j$.

A convex body is a convex set of positive volume, which for a convex set means nonempty interior. A subspace $V$ has a basis of integer vectors if it is the real span of integer vectors. Its integer translates are the sets $z+V$ with $z\in\mathbb Z^n$.

In Lean, $\mathcal R^k$ is EuclideanSpace ℝ (Fin k), a basis is b : Fin m → EuclideanSpace ℝ (Fin k), the lattice is lattice b = Submodule.span ℤ (Set.range b), $|b_j^*|$ is gsLen b j, $b_i(j)$ is gsCoeff b i j, $d(L)$ is latticeDet b, $\Lambda_1$ is lambdaOne, $L_{j+1}$ is projLattice b j, and a reduced basis is IsReduced b.

Formalization targets

Goal: Theorem (5.5), corrected reading

For $n\ge2$ and every bounded convex set $K\subseteq\mathcal R^n$ with nonempty interior and $K\cap\mathbb Z^n=\emptyset$ there is a subspace $V$ spanned by integer vectors with $1\le\dim V\le n-1$ and

$$\#\{\,z+V : z\in\mathbb Z^n,\ (z+V)\cap K\ne\emptyset\,\}\ \le\ n^{2(n-\dim V)}.$$

The printed theorem allows "an $i$ dimensional space $V$" with $1\le i\le n$ and bound $n^{2(n-i+1)}$. Taken literally that is trivial ($V=\mathcal R^n$, one translate). The proof on the same page takes $V=\operatorname{span}(b_1,\dots,b_{i-1})$, of dimension $i-1$, and remarks that this "ensures that the subspace $V$ is always of dimension at least 1". The goal states that reading.

Milestones

1. Theorem (1.11), Minkowski's convex body theorem (referenced from the platform, in Mathlib's general form).
2. Theorem (1.12): every $m$-dimensional lattice has a nonzero vector with $|v|\le\sqrt m\,d(L)^{1/m}$.
3. Proposition 1.9: a primitive lattice vector belongs to some basis.
4. Proposition 2.16, existence form: every lattice has a reduced basis.
5. Proposition 4.2: for any $b_0$ with projection $\bar b_0$ onto the span, some $b\in L$ has $|b-\bar b_0|\le\frac12(\sum_jb_j(j)^2)^{1/2}\le\frac{\sqrt m}2\max_jb_j(j)$.
6. Proposition 4.3: for a reduced basis and $i$ maximising $b_i(i)$, the tail $(\lambda_i,\dots,\lambda_m)$ of every closest lattice point to $b_0$ lies in an explicit set of at most $m^{m-i+1}$ integer vectors.

Significance

Theorem (5.5) is a structural form of the flatness theorem. For $\dim V=n-1$ it says that a lattice-free convex body meets fewer than $n^2$ consecutive integer hyperplanes of some integral direction. For smaller $\dim V$ it gives a finer decomposition of $\mathbb Z^n$ into translates, each a lower-dimensional integer program. This is the recursion behind fixed-dimension integer programming, and statements of this form are used in lattice-point enumeration, in the geometry of numbers (covering minima), and in cutting-plane theory (lattice-free bodies define split and intersection cuts). Propositions 4.2 and 4.3 are the correctness core of exact closest-vector enumeration.

The results are proved in the literature, though Theorem (5.5) is proved "albeit sketchily" in the paper itself. As far as is known, none of them is formalized: Mathlib has Minkowski's convex body theorem and the ZLattice API, but not Gram–Schmidt lattice invariants, Korkine–Zolotarev bases, Hermite-type bounds, nearest-plane rounding, or any flatness theorem. This mission produces the first machine-checked versions. It also corrects three statements that are wrong as printed (below), so the formal statements are the ones that can be relied on.

Difficulty

The naive route to (5.5) is to take a flat direction directly: bound the lattice width of $K$ and count hyperplanes. That needs a flatness theorem with an explicit bound below $n^2$, which is itself the hard part. The paper's argument instead needs John's theorem (every convex body lies between an ellipsoid and its $n$-fold dilation), a reduced basis of the transformed lattice, and a counting argument across projected lattices that combines Minkowski's bound on each $L_i$ with the covering estimate of Proposition 4.2. None of John's theorem, reduced bases or the projected-lattice counting is in Mathlib.

Proposition 4.3 is also delicate as printed: the per-coordinate count on p. 24 undercounts the integers in a closed interval, so the printed arithmetic cannot be transcribed as it stands. Proposition 2.16 in the paper is the correctness of the algorithm SHORTEST. Here only the existence of a reduced basis is needed, which requires attainment of $\Lambda_1$ on every projected lattice and a lifting argument (Proposition 1.9).

Formalization scope

Conventions: indices are 0-based (Fin m), so the paper's $L_j$ is projLattice b (j-1) and its bound $n^{n-i+1}$ is m ^ (m - i). Gram–Schmidt is Mathlib's unnormalised gramSchmidt. Lattices are Submodule ℤs of a real Euclidean space generated by a linearly independent family, and $m\le k$ is allowed, because (1.12) and 4.2 are applied to projected lattices. The goal counts translates as sets with Set.encard, so the bound includes finiteness. $K$ is assumed convex, bounded and with nonempty interior, but not closed.

Three printed statements are corrected, and the corrections are recorded in each item's Formalization Note.

• (1.12)'s constant $\frac12\sqrt n$ is false for $n\le7$ (for example $L=\mathbb Z$, or the hexagonal lattice) and is replaced by $\sqrt n$, the constant the paper's own later proofs use.
• Proposition 4.2's second sentence is stated for $\bar b_0$ instead of $b_0$.
• Proposition 4.3 fails at $n=1$ and is stated for $m\ge2$ with the proof's explicit candidate set $T$, since an existential $T$ is satisfied by the set of tails of closest points and says nothing.

Trivializing formalizations are ruled out: the goal forbids $\dim V=n$, which gives one translate, and $\dim V=0$, where no translate meets $K$. It requires nonempty interior (the empty set would satisfy everything) and counts with encard (an infinite count cannot become $0$).

Out of scope: the paper's algorithms (SHORTEST, SELECT-BASIS, ENUMERATE, CLP, CLP′, ILP) and their operation and bit counts (Theorems 2.17, 3.9, 4.5, 5.4), because Mathlib has no cost model. Also out of scope is §6 (NP-completeness of the $L_2$ closest vector problem and Cook reductions), because Mathlib has no complexity classes. The definitions of this mission (lattice, gsLen, gsCoeff, latticeDet, lambdaOne, projLattice, IsReduced) are reusable for any later work on lattice reduction. Contributions are welcome at every level: John's theorem, Hermite-type bounds, Korkine–Zolotarev existence, and the counting lemmas.

Selected references

• R. Kannan, Minkowski's Convex Body Theorem and Integer Programming, Mathematics of Operations Research 12(3):415–440, 1987. https://doi.org/10.1287/moor.12.3.415
• H. W. Lenstra Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4):538–548, 1983. https://doi.org/10.1287/moor.8.4.538
• R. Kannan, L. Lovász, Covering minima and lattice-point-free convex bodies, Annals of Mathematics 128(3):577–602, 1988. https://doi.org/10.2307/1971436
• A. K. Lenstra, H. W. Lenstra Jr., L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen 261:515–534, 1982. https://doi.org/10.1007/BF01457454
• F. John, Extremum problems with inequalities as subsidiary conditions, Studies and Essays presented to R. Courant, 1948, 187–204.

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

Variational inequalities and complementarity problems are the standard formulation of equilibrium in operations research and mathematical economics: traffic equilibria, spatial price equilibria, Nash equilibria of convex games, and the optimality conditions of constrained optimization all take this form. Many applications have two features that the classical theory does not cover. The feasible set of a player or a flow can depend on the current state (a quasi-variational inequality, as in generalized Nash games with shared constraints), and the response map can be set-valued (a subdifferential, or a best-response correspondence). D. Chan and J. S. Pang (Math. Oper. Res. 7 (1982) 211–222) introduced the generalized quasi-variational inequality covering both, proved existence theorems for it, and derived existence for a new generalized implicit complementarity problem.

Timeline of the results this mission builds on:

• 1966: Hartman and Stampacchia prove existence for the variational inequality on a compact convex set.
• 1973: Bensoussan, Goursat and Lions introduce quasi-variational inequalities for impulse control.
• 1976: Saigal extends the complementarity problem to set-valued maps.
• 1974: Moré gives coercivity conditions for nonlinear complementarity problems; a special version of the lemma of §3 appears there.
• 1979: Fang and Peterson prove a general existence theorem for generalized variational inequalities (report, University of Maryland Baltimore County); the lemma of §3 and the constant-$K$ case of Theorem 3.2 are taken from there.
• 1982: Chan and Pang prove existence for the generalized quasi-variational inequality using the Eilenberg–Montgomery fixed point theorem, and derive existence for the generalized implicit complementarity problem under strong copositivity (Theorem 4.2), the goal of this mission.

Setting

Throughout, $\mathbb R^n$ carries the Euclidean inner product $x^T y$ and norm $\|x\|$. A point-to-set mapping $K$ assigns to each $x\in\mathbb R^n$ a set $K(x)\subseteq\mathbb R^n$. Given point-to-set mappings $K$ and $f$, the problem $\mathrm{GQVI}(K,f)$ asks for vectors $x,y$ with

$$x\in K(x),\qquad y\in f(x),\qquad (x'-x)^T y\ge 0\ \text{ for all } x'\in K(x).$$

A cone is a convex set containing $0$ and closed under nonnegative scaling. The dual cone of a set $S$ is $S^*=\{y : y^T x\ge 0 \text{ for all } x\in S\}$. For a point-to-point map $m$, a cone-valued map $L$ and a point-to-set map $f$, the problem $\mathrm{GICP}(L,m,f)$ asks for $x,y$ with

$$x\in m(x)+L(x),\qquad y\in f(x)\cap L(x)^*,\qquad y^T\big(x-m(x)\big)=0 .$$

A mapping $f$ is upper semicontinuous on a set $C$ at $x\in C$ if for each open $G\supseteq f(x)$ there is a neighbourhood $N$ of $x$ with $f(y)\subseteq G$ for $y\in N\cap C$; lower semicontinuous if for each open $G$ meeting $f(x)$, $f(y)$ meets $G$ for all $y$ near $x$ in $C$; continuous if both. A set $S$ is contractible if some point $x\in S$ and a continuous $g:S\times[0,1]\to S$ satisfy $g(x',0)=x'$, $g(x',1)=x$. $B_r$ is the closed ball of radius $r$ about the origin, $C_r$ its boundary sphere. For point-to-set maps $\mu$ and $K$, the coercivity function is

$$C_{\mu,K}(r,x^0)=\inf_{x\in K(x)\cap C_r}\Big[\inf_{y\in\mu(x)}(x-x^0)^T y\Big]\Big/(r+\|x^0\|),$$

with $\inf\emptyset=+\infty$. The map $\mu$ is strongly copositive with respect to $K$ at $x^0$ if $x^0\in K(x^0)$ and for some $\alpha>0$ and $y^0\in\mu(x^0)$, $(y-y^0)^T(x-x^0)\ge\alpha\|x-x^0\|^2$ for all $x\in K(x)$ and $y\in\mu(x)$. For $\mu$ and $q\in\mathbb R^n$, $(\mu+q)(x)=\{y+q : y\in\mu(x)\}$.

Formalization targets

Goal: Theorem 4.2 (p. 218)

Let $\tilde L$ be a closed cone with nonempty interior, $m$ continuous, $K(x)=m(x)+\tilde L$, and $\mu$ a mapping with nonempty contractible compact values, upper semicontinuous on $\mathbb R^n$. If some $\tilde u$ satisfies $\tilde u-m(x)\in\tilde L$ for all $x$, and $\mu$ is strongly copositive with respect to $K$ at $\tilde u$, then for every $q$

$$\exists\, x,y:\quad x-m(x)\in\tilde L,\quad y\in\mu(x)+q,\quad y\in\tilde L^*,\quad y^T(x-m(x))=0 .$$

Milestones, in the order the proof uses them

• Theorem 3.1 (p. 214): for continuous $\varphi$ quasi-concave in its first argument on a nonempty compact convex $C$, some $u^*\in V(u^*)=K(u^*)\cap C$ and $w^*\in f(u^*)$ satisfy $\varphi(v,u^*,w^*)\le\varphi(u^*,u^*,w^*)$ for all $v\in V(u^*)$.
• Lemma of §3 (p. 215): a variational inequality on $W\cap E$ at a point of $W\cap E^0$ extends to $W$.
• Theorem 3.2 (p. 215): existence for $\mathrm{GQVI}(K,f)$ from a compact truncation $C=U\cap E$ and a boundary condition on $\partial E$.
• Theorem 4.1 (p. 217): if $C_{\mu,K}(r,x^0)\ge 0$, then $\mathrm{GQVI}(K,\mu+q)$ has a solution in $B_r$ whenever $\|q\|\le C_{\mu,K}(r,x^0)$.
• Corollary 4.1 (pp. 217–218): under the coercivity condition (4), $\mathrm{GQVI}(K,\mu+q)$ is solvable for every $q$, with bounded solution set.
• Lemma 4.1 (p. 218): strong copositivity at $x^0$ implies coercivity (4) at $x^0$.
• Proposition 2.1 (p. 213): $\mathrm{GICP}(L,m,f)$ and $\mathrm{GQVI}(m+L,f)$ have the same solutions.

Significance

Theorem 4.2 gives existence for complementarity problems whose cone is translated by a state-dependent map $m$ and whose response map is set-valued. It contains existence for the implicit complementarity problem of Capuzzo-Dolcetta, Mosco and Pang ($\tilde L=\mathbb R^n_+$) with strongly monotone data (Corollary 4.2 of the paper), and Saigal's generalized complementarity problem ($m\equiv0$). Theorems 3.2 and 4.1 are general-purpose existence tools for quasi-variational inequalities with set-valued maps; Theorem 3.2 reduces to the Fang–Peterson theorem when $K$ is constant, and Corollary 3.1 to the Hartman–Stampacchia theorem when in addition $f$ is single-valued.

All results of the paper are proved; none is open. To our knowledge none of them has been formalized: no proof assistant library contains quasi-variational inequalities with set-valued maps, and Mathlib has neither Kakutani's nor the Eilenberg–Montgomery fixed point theorem (nor Brouwer's). A formal proof of the goal therefore also produces a reusable library of set-valued existence theory.

Difficulty

The whole chain rests on Theorem 3.1, whose proof applies the Eilenberg–Montgomery fixed point theorem for upper semicontinuous maps with acyclic (here contractible) compact values; this in turn needs either singular homology or an approximation argument, neither of which is available in Mathlib. Replacing "contractible" by "convex" to use Kakutani's theorem would prove a strictly weaker theorem: the paper states contractible values deliberately. The second difficulty is that the fixed point only solves the problem on the truncation $V(x)=K(x)\cap C$; turning it into a solution over all of $K(x)$ needs the boundary argument of Theorem 3.2, and for Theorem 4.2 the continuity of $x\mapsto (m(x)+\tilde L)\cap B_\rho$, which is where the solidity of $\tilde L$ is used. The obvious approach of applying Theorem 3.2 directly with $C=\mathbb R^n$ fails because $C$ must be compact.

Formalization scope

The space is EuclideanSpace ℝ (Fin n), so all norms and balls are Euclidean (not the sup norm of Fin n → ℝ). Point-to-set mappings are functions into Set; semicontinuity "on $C$" is Mathlib's UpperHemicontinuousOn/LowerHemicontinuousOn with neighbourhoods relative to $C$, and "on $\mathbb R^n$" is UpperHemicontinuous. Cones are PointedCone ℝ _ (convex, containing $0$, as footnote 1 of the paper says). Balls are centred at the origin.

Conventions that the Lean statements make explicit:

• The paper takes its semicontinuity from Berge, whose upper semicontinuous maps have compact values. Theorems 3.1, 3.2, 4.1 and Corollary 4.1 are false without this ($K(x)\equiv(0,1)$, $C=[0,1]$, $f\equiv\{1\}$), so each one carries an explicit closedness hypothesis on $K(x)\cap C$ or $K(x)\cap B_\rho$. Theorem 4.2 needs none, since $m(x)+\tilde L$ is closed.
• Every infimum uses $\inf\emptyset=+\infty$. Bounds of the form $C_{\mu,K}(r,x^0)\ge c$, condition (v) of Theorem 3.2, and the limit (4) are stated in universally quantified form. A real-valued $C_{\mu,K}$ would be wrong: it returns $0$ on an empty set.
• Lemma 4.1 is stated at the same point $x^0$, which is what its proof gives. In Corollary 4.1 the bound $r$ on the solutions is chosen after $q$.
• Three glyphs are illegible in the scan and are read from the proofs: $\le$ in Theorem 3.1, $\ge 0$ in Theorem 3.2(v), and $\ge$ in the Lemma of §3.

A trivializing formalization is ruled out: the GQVI solution tests over all of $K(x)$, not over $V(x)=K(x)\cap C$, and the GICP solution keeps both the dual-cone condition and the complementarity equation. Dropping any of these would turn the goal into a restatement of Theorem 3.1.

A complete development needs: an Eilenberg–Montgomery (or at least Kakutani plus an acyclicity argument) fixed point theorem for set-valued maps, Berge's maximum theorem, and basic facts on hemicontinuity of intersections and translates of set-valued maps. The fixed point theorems, the maximum theorem and the hemicontinuity lemmas are reusable far beyond this mission. Contributions of any of these as separate theorems are welcome.

Selected references

• D. Chan, J. S. Pang, The generalized quasi-variational inequality problem, Mathematics of Operations Research 7(2) (1982) 211–222. https://doi.org/10.1287/moor.7.2.211
• S. Eilenberg, D. Montgomery, Fixed point theorems for multi-valued transformations, American Journal of Mathematics 68 (1946) 214–222. https://doi.org/10.2307/2371832
• C. Berge, Topological Spaces, Macmillan, New York, 1963.
• S. C. Fang, E. L. Peterson, Generalized variational inequalities, Mathematics Research Report 79-10, Department of Mathematics, University of Maryland Baltimore County, 1979 (no public link).
• J. J. Moré, Coercivity conditions in nonlinear complementarity problems, SIAM Review 16(1) (1974) 1–16. https://doi.org/10.1137/1016001
• P. Hartman, G. Stampacchia, On some non-linear elliptic differential-functional equations, Acta Mathematica 115 (1966) 271–310. https://doi.org/10.1007/BF02392210
• R. Saigal, Extension of the generalized complementarity problem, Mathematics of Operations Research 1(3) (1976) 260–266. https://doi.org/10.1287/moor.1.3.260

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

Battery-powered and energy-harvesting wireless devices cannot treat transmission power as free: a control algorithm that maximizes throughput without regard to energy will drain a device long before the network's other resources are exhausted. Chapter 6 of Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) extends the drift-plus-penalty framework of Chapter 5 to problems with an explicit average-resource-budget constraint, and works out the Energy Constrained Control Algorithm (ECCA) of Neely [116] as its flagship example: a joint flow-control and power-allocation policy that keeps every data queue and a virtual "excess energy" queue bounded by an explicit, finite constant on every single time slot — not merely in expectation or in the long run.

Setting

A multi-user wireless downlink serves $L$ users over $L$ channels with a time-varying collective topology state $S(t)$ and link rate function $C_i(P,S(t))$ under power allocation $P=(P_1,\dots,P_L)$, subject to a per-slot power budget $\sum_i P_i(t)\le P_{max}$ and a target average power constraint $P_{av}<P_{max}$. Exogenous arrivals $A_i(t)\le\hat R$ are entirely admitted or entirely dropped each slot (no transport-layer storage). The ECCA algorithm runs, every slot: flow control — admit $A_i(t)$ into queue $i$ if $U_i(t)\le V$ (a fixed parameter), otherwise drop it entirely; power allocation — choose $P(t)$ to maximize $\sum_i[U_i(t)C_i(P,S(t))-D(t)P_i(t)]$ subject to the power budget, where $D(t)$ is a virtual power queue tracking accumulated excess energy expenditure, updated by $D(t{+}1)=\max[D(t)-P_{av},0]+\sum_i P_i(t)$.

Formalization targets

Goal — Theorem 6.3 (ECCA Performance)

$$U_i(t)\le U_{max}:=V+\hat R\ \ \forall i,t,\qquad D(t)\le D_{max}:=\beta V+\beta\hat R+P_{max}\ \ \forall t,$$

$\text{and consequently, for every $T$-slot interval, } \sum_{\tau} \textstyle\sum_i P_i(\tau) \le P_{av}\cdot T+D_{max},$ where $\beta>0$ is the constant in the rate function's marginal-benefit inequality $C_i(P,S)\le C_i(P^{[i]},S)+\beta P_i$ ($P^{[i]}$ being $P$ with its $i$-th entry zeroed). These bounds hold for every topology state process $S(t)$ and every admissible arrival process $A(t)$, on every sample path — the weakest, most general level, with no distributional assumption whatsoever on either process.

Significance

Theorem 6.3 gives a hard, deterministic worst-case guarantee — every queue in the system, actual or virtual, is bounded by an explicit closed-form constant on every single slot, not merely on average or asymptotically — which is exactly the kind of guarantee a resource-constrained embedded or battery-powered device needs: a device can be provisioned with buffer and battery-reserve capacity of the theorem's own $U_{max}$, $D_{max}$ and know, with certainty rather than in expectation, that it will never overflow. The corollary that no $T$-slot interval spends more than $P_{av}\cdot T+D_{max}$ in energy translates directly into a battery-lifetime guarantee. This is also, methodologically, the one point in the whole book's drift-plus-penalty method where an elementary induction — not a probabilistic Lyapunov drift argument — suffices, because ECCA's flow control rule directly caps $U_i(t)$ regardless of what the channel or arrivals do.

Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for virtual queue, energy-constrained control, power allocation — no faithful hits; one unrelated coincidental keyword match in a neural-coding combinatorics item was checked and is not relevant). This mission is the first formalization of the ECCA performance guarantee.

Difficulty

The obvious first idea is to bound $U_i(t)$ and $D(t)$ by unrolling their recursions and applying a probabilistic drift argument, as in every other capstone in this series. This is unnecessary and would in fact obscure the actual mechanism: $U_i(t)\le U_{max}$ follows from a two-case induction that needs no probability at all — if $U_i(t)\le V$, the flow control rule admits at most $\hat R$ more, giving $U_i(t{+}1)\le V+\hat R$; if $U_i(t)>V$, flow control drops everything, so $U_i(t{+}1)\le U_i(t)\le U_{max}$ by the induction hypothesis. The harder part is $D(t)\le D_{max}$: it requires connecting the virtual queue's own accumulation to the fact that the power-allocation optimization (6.14) will stop spending power on link $i$ once $D(t)$ grows past $U_i(t)\cdot\beta$ — a consequence of $P(t)$'s optimality for (6.14) together with the $\beta$-inequality on $C_i$, not a property one can read off the $D$-recursion alone.

Formalization scope

The power-allocation rule is stated as an explicit optimality hypothesis (hPopt): for every competing power vector $P'$ respecting the budget, the objective (6.14) at the chosen $P(t)$ is at least as large — the faithful rendering of "$P(t)$ is chosen to maximize (6.14)" without needing Lean's argmax/IsMaxOn machinery. The rate function's $\beta$-inequality is stated exactly as the book gives it, using Function.update P i 0 for $P^{[i]}$. Out of scope for this mission: the throughput conclusion under i.i.d. $A(t), S(t)$ (an expectation/liminf statement, unlike the rest of this theorem, needing the same conditional-expectation machinery as the other chapters' capstones) and Theorem 6.2 (the general GCLC framework this specializes, which needs Assumptions 1-4's four simultaneous existential clauses over an "S-only" policy) — both left for a future mission. A trivializing formalization to rule out: weakening the two sample-path conclusions to a limsup/expectation-style bound (the convention used elsewhere in this series) would misstate this theorem, whose entire distinguishing content is that the bounds hold for every time slot and every sample path, not merely in the long run.

Selected references

• Georgiadis, Neely & Tassiulas, Resource Allocation and Cross-Layer Control in Wireless Networks, Foundations and Trends in Networking, Vol. 1, No. 1 (2006), pp. 1-144. https://doi.org/10.1561/1300000001
• Neely, "Energy optimal control for time-varying wireless networks", IEEE Transactions on Information Theory, 52(7), 2006. https://doi.org/10.1109/TIT.2006.876219

Motivation

Chapters 3-4 of Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) answer "can the network stay stable?" — the backpressure algorithm's throughput optimality (Theorem 4.5) says yes, for any arrival rate inside the capacity region. But networks are usually operated with plenty of unused capacity precisely so that they can also serve a second goal: maximizing some concave utility (throughput, fairness, revenue) of the rates actually delivered. Answering "how close to utility-optimal can a stable policy get, and at what congestion cost?" needs a single theorem that treats stability and utility optimization in one drift analysis. Theorem 5.4, adapted from Neely, Modiano & Li [108], Georgiadis, Neely & Tassiulas [115] and Neely [116], is that theorem, and it is the technique — "Lyapunov optimization" or "drift-plus-penalty" — behind a large fraction of the cross-layer control literature that followed this book.

Setting

A network of $N$ queues has backlog vector $U(t)=(U_1(t),\dots,U_N(t))$, and a $K$-dimensional control process $R(t)=(R_1(t),\dots,R_K(t))$ influencing the system's dynamics (e.g. admitted data rates). For any nonnegative function $L$ of the backlog vector, the one-step Lyapunov drift is $\Delta(U(t)):=\mathbb E\{L(U(t{+}1))-L(U(t))\mid U(t)\}$, the expected one-slot change in $L$ conditioned on the current backlog. Given any scalar-valued concave utility function $g$ of a $K$-dimensional rate vector and an arbitrary target value $g^*$, the goal is to stabilize $U(t)$ while making the time-average utility of $R(t)$ close to $g^*$. The time-average rate vector is $r(t):=\frac1t\sum_{\tau=0}^{t-1}\mathbb E\{R(\tau)\}$ (5.18), and the achieved long-run utility is $\bar g:=\limsup_{t\to\infty}\frac1t\sum_{\tau=0}^{t-1}\mathbb E\{g(R(\tau))\}$.

Formalization targets

Milestone — Lemma 5.3 (Lyapunov Drift)

$$\Delta(U(t))\le\mathbb E\{y(t)\mid U(t)\}-\mathbb E\{x(t)\mid U(t)\}\ \forall t \ \Longrightarrow\ \limsup(\text{avg }x)\le\limsup(\text{avg }y),\ \liminf(\text{avg }x) \le\liminf(\text{avg }y).$$

The most abstract drift lemma in the whole book: $x(t),y(t)$ are arbitrary scalar processes, not necessarily linear or even a function of $U(t)$.

Goal — Theorem 5.4 (Lyapunov Optimization)

$$\Delta(U(t))-V\,\mathbb E\{g(R(t))\mid U(t)\}\le B-\varepsilon\sum_{i=1}^N U_i(t)-Vg^*\ \forall t$$ $$\Longrightarrow\quad \limsup_{t\to\infty}\tfrac1t\sum_\tau\sum_i\mathbb E\{U_i(\tau)\}\le\frac{B+V(\bar g-g^*)}\varepsilon, \qquad \liminf_{t\to\infty}g(r(t))\ge g^*-\frac BV.$$

This is the weakest, most general level — a drift-minus-utility condition, checked against an arbitrary target $g^*$, with no reference to any specific control policy.

Significance

Theorem 5.4 is the abstract engine that every concrete utility-maximizing algorithm in the rest of the chapter (the CLC1 joint flow-control/routing/scheduling algorithm of Theorem 5.1, and its robustness variant under approximate scheduling, Corollary 5.2) instantiates by exhibiting a control rule whose per-slot decision satisfies (5.19) for some $V,\varepsilon,B$ — the drift condition does the work of turning a per-slot optimization rule into a global performance guarantee. Its $[O(1/V),O(V)]$ tradeoff (utility gap shrinks like $1/V$, congestion grows like $V$) is the quantitative signature of every "Lyapunov optimization"/"drift-plus-penalty" algorithm in the cross-layer control literature that followed this book, making Theorem 5.4 the single result a reader needs to understand that entire family of algorithms at once, independent of which specific control problem it is applied to.

Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for Lyapunov optimization, drift-plus-penalty, utility fairness, concave utility — no hits at all, not even an adjacent object). This mission is the first formalization of the book's utility-optimization engine.

Difficulty

The central subtlety, flagged explicitly by the book's own notation, is that (5.20) and (5.21) compare two different kinds of quantity that are easy to conflate: $\bar g$ is a limsup of an expectation of utility, $\mathbb E\{g(R(\tau))\}$, while $g(r(t))$ in (5.21) is the utility evaluated at the time-averaged expected rate. Jensen's inequality (using $g$'s concavity) is exactly what would relate $g(\mathbb E\{R(t)\})$ to $\mathbb E\{g(R(t))\}$ — and it is not proved or needed by this theorem's own statement, only by later results that connect the two more tightly. A formalization that silently merges these into one "utility" quantity would be proving something the book does not claim. The second trap is the target $g^*$: it is a free parameter of the hypothesis, not the true optimal utility — the theorem's strength is exactly that it says nothing special about how $g^*$ was chosen, so a formalization must not add a hidden side condition forcing $g^*$ to equal a genuine optimum.

Formalization scope

∆(U(t)) is restated locally in this chunk's own sub-namespace (drafts cannot import chunk 04-backpressure's copy), via Mathlib's condExp on the σ-algebra generated by the current backlog vector, exactly as in Chapter 4. Explicit Measurable/Integrable guards on U, R, g∘R and every drift term prevent condExp/∫ from silently defaulting to 0 (a trivializing formalization this mission rules out: without these guards, a non-integrable process would satisfy the hypotheses vacuously and "prove" a stability/utility conclusion for a process that is not actually controlled). r(t) and \bar g are written inline as their defining Cesàro averages rather than as separate named definitions, since each is used exactly once. Out of scope for this mission: Theorem 5.1 (the CLC1 algorithm's concrete instantiation), Corollary 5.2 (the robustness-to-suboptimal-scheduling variant), and Lemma 5.5 (continuity of near-optimal solutions, which needs the capacity region Λ as a hypothesis object). All three need substantially more setup (a named algorithm, or the capacity-region machinery of Chapter 3) than this session's time budget allowed without approximating either — left for a future mission rather than approximated.

Selected references

• Georgiadis, Neely & Tassiulas, Resource Allocation and Cross-Layer Control in Wireless Networks, Foundations and Trends in Networking, Vol. 1, No. 1 (2006), pp. 1-144. https://doi.org/10.1561/1300000001
• Neely, Modiano & Li, "Fairness and optimal stochastic control for heterogeneous networks", IEEE/ACM Transactions on Networking, 16(2), 2008. https://doi.org/10.1109/TNET.2007.900405
• Neely, "Energy optimal control for time-varying wireless networks", IEEE Transactions on Information Theory, 52(7), 2006. https://doi.org/10.1109/TIT.2006.876219