Combinatorics

Motivation

A set function $f : 2^{\mathcal N} \to \mathbb R$ on a finite ground set $\mathcal N$ is submodular if it has diminishing returns, equivalently if $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ for all $A, B \subseteq \mathcal N$. Cut functions of graphs and hypergraphs, coverage functions, entropy, and many facility-location and welfare objectives are submodular. Unconstrained Submodular Maximization (USM) asks, given a nonnegative submodular $f$ through a value oracle, for a set $S \subseteq \mathcal N$ of maximum value. It contains Max-Cut, Max-DiCut and Max Facility Location as special cases, and it is a subroutine in algorithms for constrained submodular maximization.

Timeline:

• Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) gave a uniformly random set achieving $1/4$ of the optimum, a deterministic local search achieving $1/3 - \varepsilon/n$, a randomized local search achieving $2/5$, and proved that no algorithm making polynomially many value queries achieves $1/2 + \varepsilon$.
• Oveis Gharan and Vondrák (SODA 2011) improved the ratio to about $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) to about $0.42$.
• Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015) gave the double greedy algorithms: a deterministic linear-time $1/3$-approximation (this mission) and a randomized linear-time $1/2$-approximation, matching the query lower bound.

Setting

Let $\mathcal N$ be a finite ground set and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ a nonnegative submodular function. Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$, and let $OPT$ denote a set attaining it.

Algorithm 1 (DeterministicUSM) fixes an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and maintains two solutions, starting from $X_0 = \emptyset$ and $Y_0 = \mathcal N$. In iteration $i = 1, \dots, n$ it computes

$$a_i = f(X_{i-1} \cup \{u_i\}) - f(X_{i-1}), \qquad b_i = f(Y_{i-1} \setminus \{u_i\}) - f(Y_{i-1}).$$

If $a_i \ge b_i$ it sets $X_i = X_{i-1} \cup \{u_i\}$, $Y_i = Y_{i-1}$; otherwise $X_i = X_{i-1}$, $Y_i = Y_{i-1} \setminus \{u_i\}$. A tie adds $u_i$. After $n$ iterations $X_n = Y_n$, which is the output.

The analysis uses the hybrid sets $OPT_i = (OPT \cup X_i) \cap Y_i$, which agree with $X_i$ and $Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on $u_{i+1}, \dots, u_n$. In Lean, the run is state f l i, the state $(X_i, Y_i)$ after the first $i$ entries of the order l, and $OPT_i$ is optI O (state f l i).

Formalization targets

Goal: Theorem I.1

For every nonnegative submodular $f$ and every order of $\mathcal N$,

$$X_n = Y_n \qquad\text{and}\qquad f(OPT) \le 3\, f(X_n).$$

Milestones

1. Lemma II.1. For every $1 \le i \le n$, $a_i + b_i \ge 0$.
2. The hybrid sequence. $OPT_i$ agrees with $X_i, Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on the rest; $OPT_0 = OPT$ and $OPT_n = X_n = Y_n$.
3. Lemma II.2. For every $1 \le i \le n$,

$$f(OPT_{i-1}) - f(OPT_i) \le [f(X_i) - f(X_{i-1})] + [f(Y_i) - f(Y_{i-1})].$$

4. The telescoped display. $f(OPT_0) - f(OPT_n) \le [f(X_n) - f(X_0)] + [f(Y_n) - f(Y_0)] \le f(X_n) + f(Y_n)$.
5. Theorem II.3 (tightness). For every $\varepsilon > 0$ there is a nonnegative submodular $f$ with $f(OPT) > 0$ and an order on which $f(X_n) \le (1/3 + \varepsilon)\, f(OPT)$.

Significance

The result. Algorithm 1 is the deterministic member of the double greedy family. It makes one pass over the ground set with four value queries per element, and it guarantees $1/3$ of the optimum for every order, without the polynomial-but-large running time and the $\varepsilon/n$ loss of local search. Its analysis, which charges the decrease of $f(OPT_i)$ to the increases of $f(X_i)$ and $f(Y_i)$, is the template the paper then refines into the randomized $1/2$-approximation (Theorem I.2) and its continuous counterpart on the multilinear extension. Theorem II.3 shows that $1/3$ is the exact ratio of this algorithm, so the improvement to $1/2$ requires randomization (or a different deterministic rule) rather than a sharper analysis.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal statement of the algorithm as printed, a checked proof of its guarantee for every order, and a checked tight instance. The definitions of the run and of $OPT_i$ are the same objects the randomized and fractional analyses reason about, so a complete development here is the first step toward the paper's main theorem.

Difficulty

The individual inequalities are short; the difficulty lies in the bookkeeping. Each step needs the invariants $X_{i-1} \subseteq Y_{i-1}$ and $u_i \in Y_{i-1} \setminus X_{i-1}$, which follow from the order being an enumeration (no repetitions, every element present), and the identification of $OPT_i$ from $OPT_{i-1}$ in each branch of the algorithm. Summing Lemma II.2 needs a telescoping over the run defined as a fold. The naive idea of comparing $f(X_n)$ with $f(OPT)$ directly, without the hybrid sets, gives no bound: the greedy choices are made against $X$ and $Y$, not against $OPT$. For Theorem II.3 the difficulty is producing an explicit instance, checking that it is submodular and nonnegative, and tracing the run, including the ties, which the algorithm resolves by adding.

Formalization scope

• The ground set is a finite type X with decidable equality; subsets are Finset X; $f$ is real valued, Finset X → ℝ, and nonnegativity is the hypothesis ∀ S, 0 ≤ f S where the page uses it (the goal, the telescoped display and the tight example). Lemma II.1, Lemma II.2 and the hybrid-sequence milestone do not assume it.
• Submodularity is the lattice form $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ of the paper's footnote 1, through the published definition NonmonotoneSubmod.Shared.Submodular. The paper's main-text sentence ("for every $A \subseteq B \subseteq \mathcal N$ and $u \in \mathcal N$") would force monotonicity when $u \in B \setminus A$ and is read as the footnote. $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT f, the maximum of $f$ over all subsets.
• The order $u_1, \dots, u_n$ is a list l with l.Nodup and ∀ x, x ∈ l; $u_i$ is l[i - 1]. Every statement quantifies over all such lists. No nonemptiness of $\mathcal N$ is assumed: for an empty ground set the goal reads $f(\emptyset) \le 3 f(\emptyset)$.
• The tie rule is line 5's $a_i \ge b_i$: ties add $u_i$.
• Where a milestone mentions an optimal solution, it takes a set O with ∀ S, f S ≤ f O.
• The goal is stated multiplied out, $f(OPT) \le 3 f(X_n)$, because $f(OPT)$ may be $0$.
• Trivializing formalizations ruled out. The paper's Theorem I.1 reads "there exists a deterministic linear time $(1/3)$-approximation algorithm"; without the running time that existential is satisfied by exhaustive search, so the goal is the guarantee of the printed Algorithm 1 for every order. Running time is not formalized: the algorithm evaluates $f$ on four sets per element, $n$ elements in all. Theorem II.3 requires $f(OPT) > 0$, without which $f \equiv 0$ would satisfy it.
• Needed infrastructure: elementary lemmas on List.foldl over List.take, on membership in the states of the run, and on telescoping sums over $1 \le i \le n$. A reusable lemma "the run keeps $X_i \subseteq Y_i$ and decides exactly $u_1, \dots, u_i$" would serve all three missions of this paper. Contributions of proofs of any milestone, of the goal from the milestones, and of the tight instance (e.g. the paper's five-vertex directed cut function) are welcome.

Selected references

• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205)
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011. https://doi.org/10.1137/090779346
• S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
• M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011. https://doi.org/10.1007/978-3-642-22006-7_29

Motivation

In make-to-order production, chemical process industries and other manufacturing settings modelled as projects, activities do not only occupy machines for a while: they also consume intermediate products at their start and deposit products into storage facilities at their completion. Storage is bounded above by a tank or warehouse capacity and below by a safety stock. Resources of this kind are called cumulative resources (or inventory resources, reservoirs in the constraint-programming literature). They were introduced into resource-constrained project scheduling by Neumann and Schwindt (2002), and Chapter 2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), develops their theory in §2.12.

A scheduler handling cumulative resources needs a finite combinatorial description of which schedules respect the inventory bounds at every instant, because the time axis is continuous and cannot be checked point by point in a search procedure. Theorem 2.12.4 of the book gives such a description, and it is the basis of the branch-and-bound procedure of Neumann and Schwindt for the problem $PSc|temp|C_{\max}$.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$ with $n\ge 1$, where $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i\ge 0$, with $p_0=p_{n+1}=0$ and $p_i>0$ for the real activities.

For each cumulative resource $k$ in a set $\mathcal R^\gamma$, every activity $i$ has an integer demand $r_{ik}$. If $r_{ik}<0$, activity $i$ withdraws $-r_{ik}$ units of $k$ at its start; if $r_{ik}>0$, it deposits $r_{ik}$ units at its completion; $r_{ik}=0$ means $k$ is not used. The demand $r_{0k}$ of the project beginning is the initial stock. Write $V_k^-=\{i\mid r_{ik}<0\}$ and $V_k^+=\{i\mid r_{ik}>0\}$. Each resource has a safety stock $\underline R_k\in\mathbb Z$ and a storage capacity $\overline R_k\in\mathbb Z$.

A schedule is a vector $S=(S_i)_{i\in V}$ of real start times with $S_0=0$ and $S_i\ge 0$. The active set and the inventory of $k$ at time $t\ge 0$ are

$$\mathcal A_k(S,t)=\{i\in V_k^-\mid S_i\le t\}\cup\{i\in V_k^+\mid S_i+p_i\le t\},\qquad r_k(S,t)=\sum_{i\in\mathcal A_k(S,t)} r_{ik}.$$

The schedule is inventory-feasible if $\underline R_k\le r_k(S,t)\le\overline R_k$ for all $k$ and all $t\ge 0$.

Two standing assumptions of the section are used throughout: (2.12.1) $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$, so the final inventory is admissible; and Remark 2.12.2, $\underline R_k\le 0\le\overline R_k$.

A nonempty $F\subseteq V$ is a $k$-surplus set if $\sum_{i\in F}r_{ik}>\overline R_k$, and a $k$-shortage set if $\sum_{i\in F}r_{ik}<\underline R_k$. A $k$-surplus set $F$ is minimal if no $k$-surplus set arises from $F$ by removing a nonempty set of replenishing activities, and none arises by adding a nonempty set of depleting activities. Minimal $k$-shortage sets are defined with the roles of replenishing and depleting activities exchanged. $\mathcal F_k^+$ and $\mathcal F_k^-$ denote the minimal $k$-surplus and $k$-shortage sets.

Formalization targets

Goal: Theorem 2.12.4

A schedule $S$ is inventory-feasible if and only if

$$\forall k,\ \forall F\in\mathcal F_k^+\ \exists j\in F,\ i\notin F:\ r_{jk}>0,\ r_{ik}<0,\ S_j+p_j\ge S_i,$$ $$\forall k,\ \forall F\in\mathcal F_k^-\ \exists j\in F,\ i\notin F:\ r_{jk}<0,\ r_{ik}>0,\ S_j\ge S_i+p_i.$$

Milestones

1. The invariance claim after Remark 2.12.2 (p. 131): adding the same integer $a_k$ to $r_{0k}$, $\underline R_k$ and $\overline R_k$ does not change the set of inventory-feasible schedules.
2. Lemma 2.12.3 (a): for every $k$-surplus set $F$ there is a minimal $k$-surplus set $F'$ with $\emptyset\ne F'\cap V_k^+\subseteq F\cap V_k^+$ and $F'\cap V_k^-\supseteq F\cap V_k^-$.
3. Lemma 2.12.3 (b): the shortage counterpart.
4. Theorem 2.12.4 (a) on its own: the upper constraints $r_k(S,t)\le\overline R_k$ hold for all $t\ge 0$ iff condition (a) holds.
5. Theorem 2.12.4 (b) on its own: the lower constraints hold for all $t\ge 0$ iff condition (b) holds.

Significance

The theorem turns a constraint over a continuum of time points into finitely many disjunctions, each a choice among precedence relations. An inventory excess caused by a minimal surplus set is removed by a start-to-completion relation $S_j+p_j\ge S_i$ (a replenishment is postponed until after a withdrawal starts, equivalently a maximum time lag), and a shortage by a completion-to-start relation $S_j\ge S_i+p_i$. Consequences stated in the book: the feasible region of $PSc|temp|C_{\max}$ is a finite union of polyhedra; branching on these relations, organized as pairs of strict orders and reflexive relations, is a complete search scheme; and minimal delaying alternatives for surplus and shortage sets can be enumerated. Because every problem with renewable resources can be rewritten as one with cumulative resources (p. 130), the book also concludes that this union of polyhedra is in general disconnected.

The result is proved in the book (and in Neumann and Schwindt, 2002). To our knowledge it has no machine-checked proof. This mission produces a Lean formalization of the model, of the one-sided minimality notion, and of the two-sided characterization with its supporting lemma.

Difficulty

The combinatorial core is simple to state but easy to state wrongly. The natural first idea, to use inclusion-minimal surplus sets as for renewable resources, gives a different family $\mathcal F_k^+$ and a false theorem: the book's minimality allows removing only replenishing activities and adding only depleting ones. The existence lemma needs Remark 2.12.2 to keep at least one replenishing activity in the minimal set, and the sufficiency direction needs (2.12.1) to guarantee a depleting activity outside the minimal set. Both membership conditions of the active set are closed at $t$, so activities that deplete or replenish exactly at the critical instant must be counted on the correct side; a half-open reading changes which schedules are feasible. The initial stock $r_{0k}$ is handled by the same active-set rule as any other demand, which matters for the invariance claim.

Formalization scope

• Activities are Fin (n + 2), activity $n+1$ is Fin.last (n + 1); resources are an arbitrary type K. Demands, safety stocks and capacities are integers (ℤ); start times are reals (ℝ); durations are natural numbers cast to ℝ.
• The inventory constraints are required for every $t\ge 0$. The book prints (2.12.2) for $0\le t\le\bar d$, but its proof of Theorem 2.12.4 works with an arbitrary $t\ge 0$ (the necessity half uses the last completion time of a replenishing activity, which need not be at most $\bar d$). The two readings coincide for schedules with $S_{n+1}\le\bar d$ whose activities all finish by $S_{n+1}$.
• A schedule satisfies $S_0=0$ and $S_i\ge 0$ and is not required to be time-feasible; time lags play no role in this section's results and are not part of the model.
• (2.12.1) and Remark 2.12.2 are explicit hypotheses (TotalDemandWithinBounds, BoundsStraddleZero) wherever the book's proofs use them. Surplus and shortage sets are nonempty by definition, and minimality uses proper inclusions.
• A formalization in which $\mathcal F_k^+$ is empty or trivial (for instance, minimality with non-strict inclusions, which no set satisfies) makes condition (a) vacuous; the definitions here follow p. 131 exactly, and a concrete instance with a nonempty $\mathcal F_k^+$ has been checked locally.

Reusable parts: the cumulative-resource model and inventory profile, which later missions on continuous cumulative resources (§2.12.2) or on the NP-completeness of $PSc|temp|C_{\max}$ (Theorem 2.12.1) can build on. Contributions welcome: proofs of the lemmas, of either half of the theorem, and finite-sum lemmas about Finset.filter that the proofs need.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §2.12.1, pp. 128–135. https://doi.org/10.1007/978-3-540-24800-2
• K. Neumann, C. Schwindt, Project scheduling with inventory constraints, Mathematical Methods of Operations Research 56 (2003) 513–533 (cited in the book as 2002). https://doi.org/10.1007/s001860200251

Motivation

Resource-constrained project scheduling asks for start times of the activities of a project so that prescribed time lags between activities are respected and, at every moment, the activities in progress do not require more of any renewable resource (staff, machines, reactors) than is available. When the time lags include maximum time lags (deadlines relative to other activities), even finding a feasible schedule is NP-hard, and the feasible region is in general neither convex nor connected. Branch-and-bound methods for this problem (the problem $PS|temp|C_{\max}$ in the notation of Neumann, Schwindt & Zimmermann) do not search over schedules directly. They search over strict orders of the activities, that is, over sets of precedence constraints "$j$ starts after $i$ has finished".

This mission formalizes the theory behind that search, as developed by Bartusch, Möhring & Radermacher (1988) and presented in §2.3 of Neumann, Schwindt & Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). Its goal, Theorem 2.3.10, says when a strict order resolves every resource conflict.

Setting

A project has activities $V = \{0, 1, \dots, n+1\}$, where $0$ and $n+1$ are fictitious activities marking the project's start and completion and $1, \dots, n$ are the real activities ($n \ge 1$). Activity $i$ has duration $p_i \in \mathbb Z_{\ge 0}$, with $p_0 = p_{n+1} = 0$ and $p_i > 0$ for real activities. Time lags are encoded in the project network $N$: an arc $\langle i, j\rangle \in E$ with integer weight $\delta_{ij}$ imposes $S_j - S_i \ge \delta_{ij}$. The book's standing assumptions give, for every node $i$, a path from $0$ to $i$ of nonnegative length and a path from $i$ to $n+1$ of length at least $p_i$.

A schedule is a vector $S \in \mathbb R^{n+2}$ with $S_0 = 0$ and $S_i \ge 0$. It is time-feasible if $S_j - S_i \ge \delta_{ij}$ for all arcs. The set of time-feasible schedules is $\mathcal S_T$.

Each renewable resource $k \in \mathcal R$ has a capacity $R_k$, and activity $i$ uses $r_{ik} \le R_k$ units of it while in progress, with $r_{0k} = r_{n+1,k} = 0$. The active set at time $t$ is $\mathcal A(S,t) = \{ i \mid S_i \le t < S_i + p_i\}$, and $S$ is resource-feasible if $\sum_{i \in \mathcal A(S,t)} r_{ik} \le R_k$ for all $k$ and all $t \ge 0$. The feasible region $\mathcal S$ consists of the schedules that are both time-feasible and resource-feasible.

A strict order $O \subseteq V \times V$ is an asymmetric, transitive relation. Its order polyhedron is

$$\mathcal S_T(O) = \{ S \in \mathcal S_T \mid S_j \ge S_i + p_i \ \text{for all } (i,j) \in O\}.$$

$O$ is time-feasible if $\mathcal S_T(O) \ne \emptyset$, and feasible if moreover $\mathcal S_T(O) \subseteq \mathcal S$. The order network $N(O)$ adds to $N$, for each $(i,j) \in O$, an arc $\langle i,j\rangle$ of weight $p_i$, or raises the weight of an existing arc to $\max(\delta_{ij}, p_i)$. A schedule $S$ induces the strict order $O(S) = \{(i,j) \mid i \ne j,\ S_j \ge S_i + p_i\}$.

A set $F \subseteq V$ is forbidden if $\sum_{i \in F} r_{ik} > R_k$ for some resource $k$. It is a minimal forbidden set if no proper subset of it is forbidden. $\mathcal F$ denotes the set of minimal forbidden sets.

Formalization targets

Goal: Theorem 2.3.10 (Bartusch et al. 1988)

For every time-feasible strict order $O$,

$$O \text{ feasible} \iff \forall F \in \mathcal F\ \exists\, i, j \in F:\ N(O) \text{ has a path from } i \text{ to } j \text{ of length} \ge p_i .$$

Milestones

1. Proposition 2.3.3. A strict order $O$ is time-feasible if and only if $N(O)$ has no cycle of positive length.
2. Bartusch et al.'s criterion (quoted in the proof of Theorem 2.3.10). A schedule $S$ is resource-feasible if and only if every $F \in \mathcal F$ contains distinct $i, j$ with $S_j \ge S_i + p_i$.
3. Proposition 2.3.6. For time-feasible $S$, the strict order $O(S)$ is feasible if and only if $S \in \mathcal S$.
4. Theorem 2.3.7. $\mathcal S = \bigcup_{O \in \mathcal O} \mathcal S_T(O)$, where $\mathcal O$ is the finite set of inclusion-minimal feasible strict orders.
5. Remark 2.3.11. A time-feasible schedule partitions $F$ if and only if every $\mathcal A(S,t) \cap F$, $t \ge 0$, is feasible. A time-feasible order is feasible if and only if it breaks up all (equivalently, all minimal) forbidden sets. A time-feasible schedule is feasible if and only if it partitions all forbidden sets.

Significance

Theorem 2.3.10 turns the feasibility of a strict order, which is a statement about infinitely many schedules and all times $t$, into a finite check: one longest-path computation in $N(O)$ for each minimal forbidden set. Together with Proposition 2.3.3 and the structural Theorem 2.3.7, it shows that $\mathcal S$ is a finite union of polyhedra indexed by feasible strict orders. This justifies the enumeration schemes of Chapter 2 of the book (branching on the pairs that break up a minimal forbidden set) and the notions of active and stable schedules developed in later sections.

All results in this mission are proved in the literature. For the resource-feasibility criterion, the book cites Bartusch et al. (1988) instead of proving it. To our knowledge, none of these results has been machine-checked. A formal development would give a verified foundation for the order-based description of the feasible region, on which later missions of this series (active schedules, delaying modes, stable schedules) build.

Difficulty

The sufficiency half of the goal is short once the criterion is available: a path of length $\ge p_i$ in $N(O)$ forces $S_j \ge S_i + p_i$ on the whole order polyhedron. The necessity half carries the content. If for some minimal forbidden set $F$ no path in $N(O)$ between elements of $F$ reaches the required length, one must construct a schedule in $\mathcal S_T(O)$ in which all activities of $F$ are simultaneously in progress. This means adding the reverse constraints $S_j - S_i < p_i$ for all $i, j \in F$ to the temporal system without creating a cycle of positive length, while keeping $S_0 = 0$ and $S \ge 0$. The obvious reading "no single arc gives a precedence, so they can overlap" fails because maximum time lags combine into long paths through activities outside $F$. The standing assumption that every node is reachable from $0$ by a path of nonnegative length is needed here: without it the equivalence is false.

Formalization scope

• The activity set is Fin (n + 2): 0 is the project start and Fin.last (n + 1) the project completion. Durations and resource data are natural numbers, arc weights are integers, and start times are real numbers.
• Strict orders are finite sets of pairs, Finset (Fin (n+2) × Fin (n+2)), required to be asymmetric and transitive.
• Resource constraints hold for every $t \ge 0$. The book's (2.1.4) writes $0 \le t \le \bar d$. In Chapter 2 schedules are not bounded by $\bar d$, and the book's proofs and Remark 2.3.11 use all $t \ge 0$. This is a convention of the whole series, not a strengthening.
• A path is a walk (nodes may repeat) and its length is the sum of its arc weights. A cycle of positive length is a closed walk with at least one arc and positive length. For a time-feasible order, $N(O)$ has no cycle of positive length. In that case "some path of length $\ge p_i$" coincides with the book's "longest path length $\ge p_i$", so no supremum over paths appears.
• The standing assumptions of the book form a single predicate Project.StandingAssumptions, which is a hypothesis of every theorem: $n \ge 1$; $p_0 = p_{n+1} = 0$ and $p_i > 0$ otherwise; no loops; $r_{0k} = r_{n+1,k} = 0$ and $r_{ik} \le R_k$; and the two path conditions of p. 8.
• Minimal forbidden sets and inclusion-minimal feasible orders use Mathlib's Minimal, taken among forbidden sets and among feasible strict orders respectively.
• The goal is an equivalence, and both directions are required. Weakening it to sufficiency, or dropping the time-feasibility of $O$ or the minimality of $F$, would change the theorem. Keeping the book's cut-off $t \le \bar d$ would also change it, because a schedule could then have an unresolved conflict after $\bar d$ and still be called feasible.
• Theorem 1.3.3 of Chapter 1 (a time-feasible schedule exists if and only if the network has no cycle of positive length) is needed for Proposition 2.3.3 and is restated here for $N(O)$. Chapter 1's mission is drafted separately.
• Useful infrastructure beyond this mission: longest-path potentials on integer-weighted digraphs without positive cycles (feasibility of difference constraints), and the walk and cycle API on Network. Contributions of this general lemma layer are welcome.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. https://doi.org/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), 201–240. https://doi.org/10.1007/BF02283745

Motivation

A basic question of combinatorial geometry asks when a family of sets can be pierced (or stabbed) by few points. For intervals on the real line the answer is classical: if every two of finitely many closed intervals intersect, one point meets all of them, namely the rightmost left endpoint. This is the one-dimensional case of Helly's theorem. The situation changes as soon as the sets are allowed to have holes. Unions of two intervals can intersect pairwise without any point being common to three of them, so no single point suffices, and it is not obvious that any bound depending only on the number of holes exists.

This mission formalizes the answer given in Section 8.6 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer, 2007): pairwise intersecting unions of $d$ intervals can always be pierced by $2d^2$ points. The section uses the result to illustrate a general method of combinatorics, in which a linear programming relaxation of a covering problem is bounded through LP duality and then rounded. The same scheme, a bound on the fractional transversal number followed by a rounding step, appears across discrete geometry and combinatorial optimization.

Timeline.

• 1970: Gyárfás and Lehel prove that a bound depending only on $d$ exists; their bound is exponential in $d$ (A Helly-type problem in trees, in Combinatorial Theory and its Applications, North-Holland).
• 1992: Alon and Kleitman solve the Hadwiger–Debrunner $(p,q)$-problem with a method combining fractional transversals and LP duality (Adv. Math. 96).
• 1997: Kaiser proves the bound $d^2$ using algebraic topology (Discrete Comput. Geom. 18).
• 1998: Alon gives the short LP-duality proof of the bound $2d^2$ formalized here (Discrete Comput. Geom. 19).
• 2001: Matoušek shows that the transversal number cannot in general be below a constant multiple of $d^2/\log d$ (Discrete Comput. Geom. 26).

Setting

Fix an integer $d \ge 1$. A $d$-interval is a union of $d$ closed intervals on the real line,

$$J = [a_1,b_1] \cup \dots \cup [a_d,b_d], \qquad a_k \le b_k .$$

The numbers $a_k$ and $b_k$ are the endpoints of $J$. A finite family $\mathcal J$ of $d$-intervals is pairwise intersecting if $J_1 \cap J_2 \ne \emptyset$ for all $J_1, J_2 \in \mathcal J$. A set $X$ of real numbers is a transversal of $\mathcal J$ if every $J \in \mathcal J$ contains a point of $X$.

More generally, for a finite set $V$ and a system $\mathcal F$ of subsets of $V$: a transversal is a set $X \subseteq V$ meeting every member; the transversal number $\tau(\mathcal F)$ is the smallest size of a transversal; a matching is a subsystem of pairwise disjoint members, and the matching number $\nu(\mathcal F)$ is the largest size of a matching. The fractional transversal number $\tau^*(\mathcal F)$ is the optimal value of the linear program

$$\min \sum_{v\in V} x_v \quad \text{s.t.} \quad \sum_{v \in F} x_v \ge 1 \ (F \in \mathcal F),\ x \ge 0,$$

and the fractional matching number $\nu^*(\mathcal F)$ is the optimal value of

$$\max \sum_{F\in\mathcal F} y_F \quad \text{s.t.} \quad \sum_{F :\, v \in F} y_F \le 1 \ (v \in V),\ y \ge 0 .$$

Formalization targets

Goal: Theorem 8.6.1

$$\mathcal J \text{ finite, pairwise intersecting family of } d\text{-intervals} \;\Longrightarrow\; \exists X \subset \mathbb R,\ |X| \le 2d^2,\ X \cap J \ne \emptyset \ \ \forall J \in \mathcal J .$$

This is the book's theorem with its constant $2d^2$.

Milestones

1. Lemma 8.6.2. If $J_1,\dots,J_n$ ($n \ge 1$, repetitions allowed) are $d$-intervals with $J_i \cap J_j \ne \emptyset$ for all $i,j$, then some endpoint of some $J_i$ lies in at least $n/2d$ of the $J_j$.
2. §8.6, p. 182. For every finite set system with nonempty members,

$$\nu(\mathcal F) \le \nu^*(\mathcal F) = \tau^*(\mathcal F) \le \tau(\mathcal F).$$

3. Lemma 8.6.3. If $\mathcal J$ is a finite pairwise intersecting family of $d$-intervals and $P$ its set of endpoints, there are weights $x_p \ge 0$, $p \in P$, with $\sum_{p \in J \cap P} x_p \ge 1$ for every $J \in \mathcal J$ and $\sum_{p\in P} x_p \le 2d$.

Significance

The result. Theorem 8.6.1 shows that the piercing number of pairwise intersecting $d$-intervals is bounded by a function of $d$ alone, and that this function is polynomial. The section also states, without proof, the extension $\tau(\mathcal J) \le 2d^2\,\nu(\mathcal J)$ for arbitrary finite families of $d$-intervals. Upper bounds of this kind feed into piercing and hitting-set questions for families with bounded "complexity", and the chain $\nu \le \nu^* = \tau^* \le \tau$ is the standard frame in which such bounds are proved.

Formalizing it. The theorem, both lemmas and the duality chain are proved in the literature and in the book. None of them is on the platform. The work consists of formalizing the book's proof: a double-counting argument, LP duality for the pair of fractional programs together with the rationality of an optimal basic solution, and a rounding step. The general-set-system milestone is reusable for any transversal problem, independent of $d$-intervals.

Difficulty

The obvious generalization of the one-dimensional argument fails: for $d \ge 2$ no point need be common to all members, so there is no single extremal endpoint to choose, and a greedy piercing procedure has no control over how many points it uses. The difficulty is to obtain a bound that does not depend on the size of the family. In the book's route the counting statement of Lemma 8.6.2 holds only for equal weights, while the fractional programs produce arbitrary real weights, and the passage between the two, as well as the passage from a fractional transversal of small total weight to an actual finite set of points, are the steps that need care.

Formalization scope

A $d$-interval is stored as data: two functions left, right : Fin d → ℝ with left k ≤ right k, together with the set toSet $= \bigcup_k [a_k,b_k]$. Components are indexed $0,\dots,d-1$. Endpoints are those of the given components, so they depend on the representation, as in the book's proofs. Families are Finsets of such data; Lemma 8.6.2 uses a Fin n-indexed sequence, since the proof of Lemma 8.6.3 applies it to a sequence with repetitions. The hypotheses $d \ge 1$ (the book's definition) and, in Lemma 8.6.2, $n \ge 1$ are explicit. The quantity $n/2d$ is real division. Transversal sizes are cardinalities of a Finset ℝ bounded by $2d^2$.

For set systems, $V$ is a finite type and $\mathcal F$ a Finset (Finset V) with nonempty members; without this assumption no transversal exists and both fractional programs degenerate. The numbers $\tau^*$ and $\nu^*$ are expressed through optimal feasible solutions, not as infima or suprema, so no junk value of an empty or unbounded set is involved. $\tau$ is an sInf over $\mathbb N$ that is attained under the nonemptiness assumption, and $\nu$ is a maximum over the finite family of matchings.

A trivializing formalization is ruled out: the pairwise-intersection hypothesis is satisfiable by nonempty families, the transversal is required to meet the actual sets $J$, not a representation artifact, and the bound $2d^2$ and $2d$ are the book's constants, not weakened ones.

Needed infrastructure: finite sums over Finset ℝ, LP duality for a finite primal–dual pair in inequality form (or a direct proof of the chain), rationality of an optimal vertex, and a left-to-right sweep over a sorted finite set of reals. Contributions of a general LP duality statement for set-system relaxations are welcome and reusable.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.6. https://doi.org/10.1007/978-3-540-30717-4
• N. Alon, Piercing d-intervals, Discrete Comput. Geom. 19 (1998) 333–334.
• N. Alon, D. Kleitman, Piercing convex sets and the Hadwiger–Debrunner (p, q)-problem, Adv. Math. 96 (1992) 103–112.
• T. Kaiser, Transversals of d-intervals, Discrete Comput. Geom. 18 (1997) 195–203.
• J. Matoušek, Lower bounds on the transversal numbers of d-intervals, Discrete Comput. Geom. 26 (2001) 283–287.
• A. Gyárfás, J. Lehel, A Helly-type problem in trees, in Combinatorial Theory and its Applications (P. Erdős, A. Rényi, V. T. Sós, eds.), North-Holland, 1970, 571–584.

Motivation

A binary error-correcting code is a set of $n$-bit words chosen so that the words stay distinguishable after a few bits have been corrupted in transmission. A code can correct any $r$ errors exactly when every two of its words differ in at least $2r+1$ positions. The more words the code has, the more information each transmitted block carries. So the central quantitative question of coding theory is how large a code of given length and minimum distance can be. Codes are used in every technology that transmits or stores data, from disks and phones to deep-space probes.

In 1973 Philippe Delsarte showed that an upper bound on this maximum size is the optimum value of an explicit linear program (Delsarte, An algebraic approach to the association schemes of coding theory, Philips Res. Repts. Suppl. 10, 1973). The bound was far stronger than the classical volume argument and remains a standard tool. This mission formalizes the self-contained proof of the bound in §8.4 of Matoušek and Gärtner's textbook (Springer 2007). That proof follows Best, Brouwer, MacWilliams, Odlyzko and Sloane (IEEE Trans. Inform. Theory 24, 1978). The mission also covers the step of Delsarte's original argument that the book isolates as a lemma.

Timeline.

• 1950: Hamming introduces single-error-correcting codes and the sphere-packing bound.
• 1973: Delsarte proves the linear programming bound using association schemes.
• 1978: Best et al. give the elementary parity proof and small improvements, among them $A(17,3) \le 6552$.
• 2005: Schrijver replaces the linear program by a semidefinite program and improves many entries of the code tables (IEEE Trans. Inform. Theory 51).

Setting

A word is $\mathbf w = (w_1,\dots,w_n) \in \{0,1\}^n$, and a code is any set $C \subseteq \{0,1\}^n$. The Hamming distance $d_H(\mathbf w,\mathbf w')$ is the number of positions $j$ with $w_j \ne w'_j$. The weight $|\mathbf w|$ is the number of ones in $\mathbf w$. The word $\mathbf w \oplus \mathbf w'$ is the entrywise sum modulo 2. For $I \subseteq \{1,\dots,n\}$, the restricted distance $d^I_H(\mathbf w,\mathbf w')$ counts only the differing positions that lie in $I$.

A code has distance $d$ if $d_H(\mathbf w,\mathbf w') \ge d$ for all distinct $\mathbf w,\mathbf w' \in C$ (Definition 8.4.1). The quantity $A(n,d)$ is the maximum of $|C|$ over all codes $C \subseteq \{0,1\}^n$ with distance $d$.

For $0 \le i,t \le n$ the Krawtchouk numbers are

$$K_t(n,i) = \sum_{j=0}^{\min(i,t)} (-1)^j \binom ij \binom{n-i}{t-j}.$$

The distance distribution of a code $C$ is

$$\tilde x_i(C) = \frac{1}{|C|}\,\bigl|\{(\mathbf w,\mathbf w')\in C^2 : d_H(\mathbf w,\mathbf w') = i\}\bigr|, \qquad i=0,\dots,n.$$

The Delsarte linear program has variables $x_0,\dots,x_n$. It maximizes $x_0+\dots+x_n$ subject to:

• $x_0 = 1$;
• $x_i = 0$ for $1 \le i \le d-1$;
• $\sum_{i=0}^n K_t(n,i)\,x_i \ge 0$ for $1 \le t \le n$;
• $x \ge 0$.

For Delsarte's original argument, $M_i$ is the $2^n\times 2^n$ matrix whose $(\mathbf v,\mathbf w)$ entry is $1$ when $d_H(\mathbf v,\mathbf w) = i$ and $0$ otherwise. The weights are $\tilde y_i = |\{(\mathbf w,\mathbf w')\in C^2 : d_H = i\}| / (2^n\binom ni)$.

Formalization targets

Goal: Theorem 8.4.3 (the Delsarte bound)

$$A(n,d) \;\le\; \max\Bigl\{\textstyle\sum_{i=0}^n x_i \;:\; x \text{ feasible for the Delsarte program}\Bigr\}\quad\text{for all } n, d.$$

The goal is stated against every upper bound $v$ of the objective on the feasible set. No particular optimum value is fixed, so the statement covers every $n$ and $d$ at once.

Milestones, in attack order

1. Lemma 8.4.5. For every $I$ and $C$, the pairs in $C^2$ with even $d^I_H$ are at least as many as the pairs with odd $d^I_H$.
2. Corollary 8.4.6. $\sum_{(\mathbf w,\mathbf w')\in C^2}(-1)^{(\mathbf w\oplus\mathbf w')^T\mathbf v}\ge 0$ for every $\mathbf v$.
3. Proposition 8.4.4. $\sum_{i=0}^n K_t(n,i)\,\tilde x_i(C) \ge 0$ for every $C$ and every $t = 1,\dots,n$.
4. §8.4, p. 160. The values $\tilde x_i(C)$ sum to $|C|$. For a nonempty code with distance $d$, the vector $\tilde x(C)$ is feasible for the program.
5. Lemma 8.4.2 (sphere-packing bound). $A(n,2r+1) \le \lfloor 2^n / \sum_{i=0}^r\binom ni\rfloor$.
6. Lemma 8.4.7. $\tilde M = \sum_{i=0}^n \tilde y_i M_i$ is positive semidefinite.

Significance

The Delsarte bound turns an extremal problem over the $2^{2^n}$ subsets of the cube into a linear program with $n+1$ variables. For $A(17,3)$ it gives $6553$, while the sphere-packing bound gives $7281$. Many entries of the standard code tables rest on this bound or its refinements. The positive semidefiniteness in Lemma 8.4.7 is the starting point of the semidefinite programming bounds of Schrijver and of later work. The same framework also underlies the linear programming bounds for spherical codes and sphere packings.

The theorem is classical and fully proved in the literature. Neither Mathlib nor this platform has a formal statement or proof of it. Mathlib has Hamming distance and binomial coefficients, but it has no $A(n,d)$, no Krawtchouk numbers and no LP bound for codes. This mission would produce the first formal statement and proof. It would also produce reusable identities on Krawtchouk sums and character sums over $\{0,1\}^n$.

Difficulty

Two of the program's constraints are immediate once $\tilde x_i$ is defined: $\tilde x_0 = 1$, and $\tilde x_i = 0$ for $i < d$. The difficulty lies in the Krawtchouk constraints. They do not follow from counting pairs at a single distance. They require a sign-weighted count over all words of weight $t$, and the sum must then be regrouped by the distance of each pair. That regrouping identifies a count of words, split by how many ones they share with a fixed word, with the Krawtchouk number. Formally this is an exchange of finite sums together with a binomial counting identity, and the index bookkeeping, including the range $j \le \min(i,t)$, has to be exact.

The obvious attempt proves the inequality one distance class at a time. It fails because the individual terms $K_t(n,i)\,\tilde x_i$ have no sign. Only the whole sum is nonnegative.

Formalization scope

• Words and codes. Words are Fin n → Bool, with bit $1$ as true. The book's positions $1,\dots,n$ become 0, …, n-1. Codes are Finsets of words, and $d_H$ is Mathlib's hammingDist.
• The maximum $A(n,d)$. $A(n,d)$ is a Finset.sup over the finite family of codes with distance $d$. This family contains the empty code, so the maximum is attained.
• Krawtchouk numbers. $K_t(n,i)$ is an integer, and its natural-number subtractions are honest for $i \le n$ and $j \le t$.
• LP variables and the $x_i = 0$ constraints. The LP variables are indexed by Fin (n+1) with no index shift. The constraints $x_i = 0$ are imposed for $1 \le i < d$, so they are vacuous for $d \le 1$.
• The empty code. Lean's convention $1/0 = 0$ gives $\tilde x(\emptyset) = 0$. Proposition 8.4.4 then holds trivially, and the feasibility milestone carries the hypothesis $C \ne \emptyset$ that the book's division presupposes.
• The sphere-packing floor. The floor in the sphere-packing bound is natural-number division by a denominator that is at least $1$.
• Positive semidefiniteness. This is Mathlib's Matrix.PosSemidef over $\mathbb R$.

No trivialization. The goal is not stated as "$A(n,d) \le \sup$" with a real supremum, which Lean would evaluate to $0$ on an empty or unbounded set. Its hypothesis ranges over upper bounds of a feasible program: $(1,0,\dots,0)$ is always feasible, so the hypothesis is never vacuous.

Contributions welcome. Useful lemmas include:

• Krawtchouk identities, for example $\sum_{t}K_t(n,i) = 2^n[i=0]$ and $K_i(n,t)\binom ni = K_t(n,i)\binom nt$;
• counting words of weight $t$ that meet a fixed support in exactly $j$ positions;
• general facts on character sums $\sum_{\mathbf w\in C}(-1)^{\mathbf w^T\mathbf v}$.

These are reusable for other LP and SDP bounds in coding theory.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.4. https://doi.org/10.1007/978-3-540-30717-4
• P. Delsarte, An algebraic approach to the association schemes of coding theory, Philips Research Reports Supplements 10, 1973.
• M. R. Best, A. E. Brouwer, F. J. MacWilliams, A. M. Odlyzko, N. J. A. Sloane, Bounds for binary codes of length less than 25, IEEE Trans. Inform. Theory 24 (1978), 81–93. https://doi.org/10.1109/TIT.1978.1055827
• A. Schrijver, New code upper bounds from the Terwilliger algebra and semidefinite programming, IEEE Trans. Inform. Theory 51 (2005), 2859–2866. https://doi.org/10.1109/TIT.2005.851748

Motivation

Scheduling indivisible jobs on parallel machines to finish all of them as early as possible is a basic problem in operations research and in the theory of algorithms. In the unrelated machines model each job may take a different time on each machine, with no relation between the rows of the time table, as when machines of different types (black-and-white, duplex, colour copiers in the book's example) handle jobs of different kinds. Minimizing the makespan in this model is NP-hard, so the question is how close to the optimum a polynomial-time algorithm can get.

• 1990. Lenstra, Shmoys and Tardos (Math. Programming 46, 259–271) give a polynomial-time algorithm that rounds a basic optimal solution of a linear programming relaxation and returns a schedule of makespan at most $2\,t_{\mathrm{opt}}$. The same paper shows that approximating the optimum makespan within a factor less than $3/2$ is NP-hard.
• 2007. Matoušek and Gärtner present the algorithm in §8.3 of Understanding and Using Linear Programming in a simplified, somewhat less efficient form: minimize $t^*(T) + T$ over the thresholds $T$ rather than binary-searching for the smallest $T$ with $t^*(T) \le T$. This mission follows the book's presentation.

The gap between $3/2$ and $2$ for the general unrelated-machines problem has remained open since 1990; it is the standard example of LP rounding driven by the sparsity of basic solutions.

Setting

There are $m$ machines $M$ and $n$ jobs $J$; $d_{ij} > 0$ is the running time of job $j$ on machine $i$. A schedule is a map $\sigma : J \to M$ assigning each job to one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i} d_{ij}$, the makespan of $\sigma$ is the largest load, and $t_{\mathrm{opt}}$ is the makespan of an optimal schedule, one whose makespan is at most that of every schedule.

For a real threshold $T$, the linear program $\mathrm{LPR}(T)$ in the variables $t$ and $x_{ij}$ is

$$\begin{aligned} \text{minimize } \ & t \\ \text{subject to } \ & \textstyle\sum_{i \in M} x_{ij} = 1 \ \ (j \in J), \qquad \textstyle\sum_{j \in J} d_{ij} x_{ij} \le t \ \ (i \in M),\\ & x_{ij} \ge 0, \qquad x_{ij} = 0 \ \text{ whenever } d_{ij} > T . \end{aligned}$$

Its optimal value is $t^*(T)$, with $t^*(T) = \infty$ when $\mathrm{LPR}(T)$ is infeasible. The constraint matrix $A$ has one row per machine, one per job and one per pair with $d_{ij} > T$; the column of $x_{ij}$ carries $d_{ij}$ in the row of machine $i$, $1$ in the row of job $j$, and $1$ in the row of the constraint $x_{ij} = 0$ if present. Assumption 8.3.1 on a solution $x^*$ is that the columns of $A$ belonging to its nonzero variables are linearly independent; basic feasible solutions satisfy it. The support graph of $x^*$ is the bipartite graph $G = (M \cup J, E)$ with $E = \{\{i,j\} : x^*_{ij} > 0\}$.

Formalization targets

Goal: Theorem 8.3.4

Let $T^*$ minimize $t^*(T) + T$ over all real $T$ and let $(t^*, x^*)$ be an optimal solution of $\mathrm{LPR}(T^*)$ satisfying Assumption 8.3.1. Then there is a schedule $\sigma$ with $x^*_{\sigma(j) j} > 0$ for every job $j$ and

$$\max_{i \in M} \sum_{j : \sigma(j) = i} d_{ij} \;\le\; 2\, t_{\mathrm{opt}} .$$

Milestones

1. Lemma 8.3.2. Every subgraph of the support graph $G$ has at most as many edges as vertices: $|E'| \le |M'| + |J'|$.
2. Lemma 8.3.3. For $T \ge 0$ and an optimal solution $(t^*, x^*)$ of $\mathrm{LPR}(T)$ satisfying Assumption 8.3.1, some schedule along the edges of $G$ has makespan at most $t^* + T$.
3. Proof of Theorem 8.3.4, first step. $\mathrm{LPR}(t_{\mathrm{opt}})$ is feasible and $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$.
4. Proof of Theorem 8.3.4, second step. $t^*(T^*) + T^* \le 2\,t_{\mathrm{opt}}$.

Significance

The theorem gives a polynomial-time 2-approximation for an NP-hard problem, and its proof isolates a reusable principle: a basic solution of an assignment-type LP has a support graph in which every subgraph has at most as many edges as vertices (a pseudoforest), so all but a matching's worth of the fractional assignment is already integral. The same sparsity argument underlies rounding results for the generalized assignment problem and for many later scheduling and allocation relaxations.

The result has been proved since 1990 and is textbook material. It is not formalized on Prove2Me or, to the maintainers' knowledge, in Mathlib. This mission produces a machine-checked version of the rounding theorem together with the counting lemma on basic solutions, the relaxation inequality $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$, and the bound on the chosen threshold, each stated on shared definitions of the scheduling LP.

Difficulty

The obvious approach, rounding every job to the machine carrying the largest fraction of it, can overload a machine by many jobs at once and gives no constant factor. The bound $t^* + T$ needs two facts that are not visible from the LP value alone: that the support of a basic solution is sparse in the precise sense of Lemma 8.3.2, which has to be read off the linear independence of columns of the constraint matrix after deleting rows; and that the jobs left fractional can be matched injectively to machines, which requires a Hall-type condition derived from that sparsity. Relating linear independence of real column vectors to an edge count in a bipartite graph, and then producing a matching, is where the formal work lies.

A second subtlety is the threshold $T$: the bound $t^* + T \le 2 t_{\mathrm{opt}}$ holds only because $T^*$ is chosen by minimizing over thresholds, and the relaxation at $T = t_{\mathrm{opt}}$ must be compared with the one at $T^*$ through optimal solutions of different linear programs.

Formalization scope

Machines are Fin m, jobs are Fin n (0-based; the book's machines $1,\dots,m$ and jobs $m+1,\dots,m+n$ are disjoint index sets), running times form d : Matrix (Fin m) (Fin n) ℝ, and the standing hypothesis $d_{ij} > 0$ of §8.3 appears in every theorem. A schedule is a function Fin n → Fin m; the makespan is the supremum of the loads over the finite type Fin m, which is the maximum for $m \ge 1$. The optimum $t_{\mathrm{opt}}$ is the makespan of a schedule assumed optimal, never an infimum.

Optimal values of $\mathrm{LPR}(T)$ are never written as sInf: statements quantify over optimal solutions, i.e. feasible $(t, x)$ with $t \le t'$ for every feasible $(t', x')$. The book's convention $t^*(T) = \infty$ for infeasible $\mathrm{LPR}(T)$ is encoded by letting thresholds without an optimal solution impose no condition in the minimality hypothesis on $T^*$, which reads $t^* + T^* \le t + T$ for every real $T$ and every optimal solution $(t, x)$ of $\mathrm{LPR}(T)$. The constraint matrix used in Assumption 8.3.1 has rows indexed by Fin m ⊕ Fin n ⊕ {(i, j) // T < d i j} and excludes the column of $t$, as on p. 151.

"Efficiently construct" in Lemma 8.3.3 and "computes" in Theorem 8.3.4 are formalized by the property of the constructed schedule, not by its running time: every job goes to a machine $i$ with $x^*_{ij} > 0$. This constraint is what rules out the trivializing formalization — "some schedule has makespan at most $2 t_{\mathrm{opt}}$" is true of the optimal schedule itself and says nothing about the rounding.

A complete development needs: finite linear algebra (a linearly independent family of vectors supported on $k$ coordinates has at most $k$ members), Hall's marriage theorem (available in Mathlib as Finset.all_card_le_biUnion_card_iff_exists_injective), and the existence of an optimal solution of a feasible, bounded linear program (used to apply the minimality of $T^*$ at $T = t_{\mathrm{opt}}$). The counting lemma for basic solutions and the definitions of $\mathrm{LPR}(T)$ are reusable for other assignment relaxations. Proofs of any milestone, and alternative proofs of Lemma 8.3.3 by the direct pseudoforest argument of p. 153–154, are welcome.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.3, pp. 148–156. https://doi.org/10.1007/978-3-540-30717-4
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990), 259–271. https://doi.org/10.1007/BF01585745

Motivation

Voting rules, committee procedures and any other method that turns individual rankings into one collective choice face the same question: can the rule be designed so that no participant ever gains by misreporting their ranking? The Gibbard–Satterthwaite theorem (Gibbard, 1973; Satterthwaite, 1975) answers no. When at least three alternatives can be chosen and all strict rankings are admissible, the only rules immune to manipulation are dictatorships. The result is the starting point of mechanism design without money. It explains why the positive results of the transferable-utility chapters of the book (Groves, VCG, posted prices) depend on quasi-linear preferences, and why research on voting turned to restricted preference domains and weaker solution concepts.

This mission formalizes Chapter 8 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), §§8.2–8.3. The book's route to the theorem follows Reny (2001). Strategy-proofness implies Maskin monotonicity, and every monotone rule with full range over at least three alternatives is dictatorial. The second step is the Muller–Satterthwaite theorem (Muller and Satterthwaite, 1977), which is stronger than Gibbard–Satterthwaite because monotonicity is weaker than strategy-proofness. The chapter closes with the classical escape route: on single-peaked preferences (Moulin, 1980) the median voting rule is strategy-proof and not dictatorial.

Timeline. Arrow (1951/1963) proved the impossibility of non-dictatorial preference aggregation under independence of irrelevant alternatives. Gibbard (1973) and Satterthwaite (1975) proved the manipulation version independently, and Satterthwaite showed the two theorems are equivalent. Muller and Satterthwaite (1977) showed that on the full domain strategy-proofness is equivalent to a monotonicity condition (strong positive association). Moulin (1980) characterized strategy-proof rules on single-peaked domains that depend only on reported peaks. Reny (2001) gave the short common proof of Arrow's and the Muller–Satterthwaite theorems that the book follows.

Setting

There is a finite set $I=\{1,\dots,N\}$ of agents and a finite set $A$ of alternatives. Each agent $i$ has a preference relation $R_i$ over $A$; $a\,R_i\,b$ reads "$a$ is weakly preferred to $b$". Every $R_i$ is a linear order: complete, transitive, and the only indifference is among identical alternatives. Its strict part is $P_i$. The set of all linear orders over $A$ is $\mathcal R$, and a profile is $R=(R_1,\dots,R_N)\in\mathcal R^N$. $(R_i',R_{-i})$ is the profile obtained from $R$ by replacing agent $i$'s preference with $R_i'$.

A direct mechanism is a function $f:\mathcal R^N\to A$ (Definition 8.1). It is

• dominant strategy incentive-compatible (DSIC) if $f(R_i,R_{-i})\,R_i\,f(R_i',R_{-i})$ for all $i$, $R$, $R_i'$ (Definition 8.2);
• dictatorial if some agent $i$ satisfies $f(R)\,R_i\,a$ for all profiles $R$ and all $a\in A$ (Definition 8.3);
• monotone if $f(R)=a$ and, for every $i$, $a\,R_i\,b\Rightarrow a\,R_i'\,b$ for all $b$, together imply $f(R')=a$ (Definition 8.4);
• set-monotone if $f(R)\in B$ and, for every $i$, $R_i'$ differs from $R_i$ only in the ranking of elements of $B$, together imply $f(R')\in B$ (Definition 8.5);
• unanimity-respecting if $f(R)=a$ whenever every agent ranks $a$ at the top (Definition 8.6).

"The range of $f$ is $A$" means that every alternative is chosen at some profile.

For §8.3 the alternatives are labelled $1,\dots,K$. A preference is single-peaked if it has a top alternative $k(i)$ and declines monotonically to the right and to the left of it. $\hat{\mathcal R}$ is the set of single-peaked preferences, and on the restricted domain $\hat{\mathcal R}^N$ DSIC and dictatorship are read with all profiles and deviations taken from $\hat{\mathcal R}$.

Formalization targets

Goal: Proposition 8.5 (Muller–Satterthwaite)

$$|A|\ge 3,\quad f(\mathcal R^N)=A,\quad f\ \text{monotone}\ \Longrightarrow\ \exists\, i\in I\ \ \forall R\in\mathcal R^N\ \forall a\in A:\ f(R)\,R_i\,a.$$

This is the book's own capstone ("the core of the proof", p.144). No constant needs to be fixed, and the statement is strictly stronger than the necessity half of Gibbard–Satterthwaite.

Milestones

• Proposition 8.2: DSIC $\Rightarrow$ monotone.
• Proposition 8.3: monotone $\Rightarrow$ set-monotone.
• Proposition 8.4: monotone and full range $\Rightarrow$ respects unanimity.
• Proposition 8.1 (Gibbard–Satterthwaite): for $|A|\ge3$ and full range, $f$ is DSIC $\iff$ $f$ is dictatorial.
• Proposition 8.6: for $|A|\ge3$ and at least two agents, there is a mechanism on $\hat{\mathcal R}^N$ with range $A$ that is DSIC on $\hat{\mathcal R}^N$ and not dictatorial on $\hat{\mathcal R}^N$.

Significance

The result itself. Proposition 8.5 turns an incentive question into a purely ordinal one: any full-range rule that is Maskin monotone is a dictatorship once three alternatives are available. With Proposition 8.2 it gives Gibbard–Satterthwaite. Proposition 8.6 marks the boundary of the impossibility: with a one-dimensional ordering of alternatives and single-peaked preferences, the median voter rule escapes it.

Formalizing it. All results are classical and proved. The platform already has a proved Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite, Algorithmic Game Theory III), derived from Arrow's theorem in the alternative Mathlib environment c5ea0035…. It uses strict-order profiles and a one-agent-deviation monotonicity. This mission adds Maskin monotonicity, the Muller–Satterthwaite theorem, Reny's direct proof route, and the single-peaked possibility result, none of which is on the platform, all in the default environment.

Difficulty

Propositions 8.2–8.4 are short. The difficulty is in Proposition 8.5. Its proof moves one alternative up or down agents' rankings one agent at a time, and it has to keep the chosen alternative pinned at every step using only monotonicity, set-monotonicity and unanimity. It needs a pivotal agent, whose identity depends on the pair of alternatives, and then an argument that the pivots for different alternatives coincide. The argument uses a third alternative $c$ in an essential way. With two alternatives the conclusion is false (majority rule), so any argument that never uses $|A|\ge3$ cannot succeed. Formally, each "move $b$ just below $a$ in agent $j$'s ranking" is an explicit construction of a new linear order, together with a check that the monotonicity hypothesis applies. The figures on pp.146–149 describe these orders only partially ("the other alternatives in arbitrary order"). For Proposition 8.6, the obstacle is that DSIC must be checked against every single-peaked misreport, not only misreports of the peak.

Formalization scope

• A linear order is the structure LinPref A (relation rel, completeness, transitivity, antisymmetry). A profile is ι → LinPref A for a finite agent type ι, and a direct mechanism is (ι → LinPref A) → A. $A$ is a Fintype. "The range of $f$ is $A$" is Function.Surjective f, and $|A|\ge3$ is 3 ≤ Fintype.card A.
• Monotonicity is the book's Definition 8.4 for arbitrary pairs of profiles, with the lower-contour condition required for each agent separately. Dictatorship is ∃ i, ∀ R a, f R ≥_{R_i} a, with the agent chosen before the profile. A weaker monotonicity (one-agent deviations only) or a weaker dictatorship ("some agent's top is chosen at some profile") would trivialize the goal and is ruled out.
• §8.3: the labelling is lab : A ≃ Fin K (labels $0,\dots,K-1$). The restricted domain is a predicate on LinPref A, and DSIC, dictatorship and full range are relativized to profiles in the domain (IsDSICOn, IsDictatorialOn, HasFullRangeOn). Values of the mechanism off the domain are never consulted.
• Two corrections of the page. The left-hand clause of single-peakedness is printed as $(\ell-1)\,R_i\,\ell$ and is used as $\ell\,R_i\,(\ell-1)$ (the book's words "decline monotonically to the left"). Proposition 8.6 carries the added hypothesis $N\ge2$, since with one agent every onto strategy-proof rule is dictatorial.
• Proposition 8.6 is an existence statement. The median voting mechanism is the book's witness, but the statement does not fix it.
• Reusable beyond this mission: the linear-order profile model, Maskin monotonicity and the restricted-domain notions, which apply to Arrow-type results, implementation theory and Moulin's characterization. Proofs of any milestone, or an independent formal proof of Proposition 8.5, are welcome.

Selected references

• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Ch. 8. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• A. Gibbard, "Manipulation of voting schemes: a general result", Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
• M. A. Satterthwaite, "Strategy-proofness and Arrow's conditions", Journal of Economic Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• E. Muller and M. A. Satterthwaite, "The equivalence of strong positive association and strategy-proofness", Journal of Economic Theory 14 (1977) 412–418. https://doi.org/10.1016/0022-0531(77)90140-5
• P. J. Reny, "Arrow's theorem and the Gibbard–Satterthwaite theorem: a unified approach", Economics Letters 70 (2001) 99–105. https://doi.org/10.1016/S0165-1765(00)00332-3
• H. Moulin, "On strategy-proofness and single peakedness", Public Choice 35 (1980) 437–455. https://doi.org/10.1007/BF00128122
• S. Barberà, "An introduction to strategy-proof social choice functions", Social Choice and Welfare 18 (2001) 619–653. https://doi.org/10.1007/s003550100151