Combinatorics

Motivation

Set cover asks for the fewest sets from a family $\mathcal S$ of $m$ subsets of a ground set $X$ of $n$ elements whose union contains $X$. It is NP-hard, and the best ratio achievable in polynomial time is $\Theta(\log n)$ (Feige 1998, doi:10.1145/285055.285059).

Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; preliminary version STOC 2003) introduced an online version. The instance $(X,\mathcal S)$ is known in advance, but an adversary reveals elements one at a time, and each revealed element must be covered at once, by sets that can never be removed later. The set $X'\subseteq X$ of elements that will actually be revealed is unknown. The paper's motivating example is a network of servers: the potential clients and the servers that can serve each client are known, but which clients will request service is not, and every activated server costs money.

The question is how much an algorithm loses against an offline adversary who knows $X'$ and covers it with a family $\mathcal C_{OPT}$. This mission formalizes the paper's answer for unit costs (Section 2): a deterministic algorithm whose cover is within a factor $O(\log m\log n)$ of $|\mathcal C_{OPT}|$. Section 3 of the paper extends the algorithm to weighted sets and Section 4 proves a nearly matching lower bound; those are separate missions of this series.

Setting

An instance consists of a finite ground set $X$ with $n=|X|$ elements and a finite family $\mathcal S$ of $m=|\mathcal S|$ sets. For an element $j$, $\mathcal S_j$ is the collection of sets containing $j$. Every set has cost $1$, so the cost of a family is its number of members.

The adversary gives a sequence $\sigma$ of elements (the given elements form $X'$). A family $\mathcal C_{OPT}\subseteq\mathcal S$ covers $\sigma$ if each element of $\sigma$ lies in some member of it.

The algorithm keeps a weight $w_S>0$ for every set, initially $w_S=1/(2m)$, and a cover $\mathcal C$, initially empty. The weight of an element is $w_j=\sum_{S\in\mathcal S_j}w_S$, and $C$ is the set of elements covered by members of $\mathcal C$. The potential is

$$\Phi=\sum_{j\notin C}n^{2w_j}.$$

When the adversary gives an element $j$:

1. if $w_j\ge1$, nothing changes;
2. otherwise a weight augmentation is performed: (a) $k$ is the minimal integer with $2^k w_j>1$; (b) every $S\in\mathcal S_j$ gets the weight $2^k w_S$; (c) at most $4\log n$ sets from $\mathcal S_j$ are added to $\mathcal C$, so that $\Phi$ does not exceed its value before the augmentation.

Step (c) prescribes a property of the chosen sets, not the sets themselves. A run on $\sigma$ is any sequence of iterations, one per arrival, in which every iteration makes an admissible choice.

Formalization targets

Goal: Theorem 2.3

For $n\ge2$, every arrival sequence $\sigma$, and every family $\mathcal C_{OPT}$ covering $\sigma$: a run of the algorithm on $\sigma$ exists, and every run ends with a cover $\mathcal C$ that covers every element of $\sigma$ and satisfies

$$|\mathcal C|\;\le\;\lceil 4\ln n\rceil\cdot|\mathcal C_{OPT}|\cdot(\log_2 m+2).$$

The paper states $|\mathcal C|=O(|\mathcal C_{OPT}|\log m\log n)$; the displayed bound is the constant its proof produces. Because the bound holds for every covering family, it holds in particular for an optimal one.

Milestones

Lemma 2.1. In every run, the number of iterations with a weight augmentation is at most

$$|\mathcal C_{OPT}|\cdot(\log_2 m+2).$$

Lemma 2.2. In an iteration with a weight augmentation, from a state with positive weights, there is a family $F\subseteq\mathcal S_j$ with $|F|\le\lceil4\ln n\rceil$ such that

$$\Phi_e\le\Phi_s,$$

where $\Phi_s$ is the potential before the iteration and $\Phi_e$ the potential after it, computed with the augmented weights and the cover $\mathcal C\cup F$.

Significance

The theorem shows that online set cover over a known instance admits a deterministic $O(\log m\log n)$-competitive algorithm. Section 4 of the paper shows this is nearly optimal: no deterministic algorithm achieves $o\!\left(\frac{\log m\log n}{\log\log m+\log\log n}\right)$ over a wide range of parameters. Its multiplicative weight updates were developed further into the online primal–dual framework for covering problems of Buchbinder and Naor (FnT TCS 3(2–3), 2009), whose Section 5.1 restates this algorithm.

The result is proved in the paper; it is not machine-checked. The Prove2Me platform has the weighted version's final counting step from the Buchbinder–Naor monograph, but no statement of Section 2. A complete development here gives a checked proof of the unweighted competitive ratio with an explicit constant, together with a reusable formal model of an online algorithm with a nondeterministic step, whose correctness includes the existence of an admissible choice at every step.

Difficulty

The central step is Lemma 2.2: a family of at most $\lceil4\ln n\rceil$ sets that keeps the potential from increasing must exist at every augmentation. The obvious rules fail. Adding every set of $\mathcal S_j$ can exceed the cardinality bound, since $\mathcal S_j$ may contain up to $m$ sets. Adding nothing, or a single set, can increase $\Phi$: every uncovered element sharing a set with $j$ has its weight raised, and its term $n^{2w}$ grows by a factor up to $n^{2\delta}$. The paper's argument is non-constructive, and a formal proof must establish existence for a finite averaging statement over real powers of $n$.

The second difficulty is that the algorithm is nondeterministic. A statement "every run has property P" is empty if no run exists, and the existence of a run is exactly Lemma 2.2 applied at every step under the invariants that weights stay positive and that each arriving element lies in some set. Feasibility (that every given element ends up covered) is not part of the algorithm's rule; it follows from the potential never increasing, which needs $n\ge2$ and a careful treatment of the initial potential, which is at most $n^2$ and equals $n^2$ when every element lies in every set.

Formalization scope

The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (finite types E of elements and T of set indices, incidence elemSets), with the published elementWeight ($w_j$) and coveredBy ($j\in C$). Its positive cost field is not used: all sets have unit cost and the cover is measured by its cardinality. $n=|E|$ and $m=|T|$. Weights are real numbers; $n^{2w_j}$ is the real power.

The algorithm is the definition OnlineSetCover.Unweighted.Algorithm: a relation Step for one iteration (recording whether a weight augmentation occurred) and Run for a sequence of iterations from the initial state, counting augmentations. Arrival sequences are lists and may repeat elements.

Explicit forms of the paper's asymptotic and unspecified quantities:

• the paper's "$4\log n$" sets per augmentation is $\lceil 4\ln n\rceil$ (natural logarithm, rounded up: the proof repeats a random choice that many times and needs $(1-\delta/2)^{4\log n}\le n^{-2\delta}$);
• Lemma 2.1's $\log m+2$ is $\log_2 m+2=\log_2(4m)$ (weights grow from $1/(2m)$ to at most $2$ by factors at least $2$);
• Theorem 2.3's $O(|\mathcal C_{OPT}|\log m\log n)$ is $\lceil4\ln n\rceil\cdot|\mathcal C_{OPT}|\cdot(\log_2 m+2)$;
• $k$ ranges over natural numbers; for $w_j<1$ the minimal integer with $2^kw_j>1$ is one;
• the paper's remark "(Clearly, $2^k\cdot w_j<2$.)" is not encoded; the correct bound is $\le2$ ($w_j=1/2$ gives $k=2$) and is not a hypothesis anywhere.

The goal adds the hypothesis $n\ge2$, which the paper's $\log n$ assumes tacitly: for $n=1$ no set may be added and the element is never covered.

Replacing the algorithm by the set of states whose potential is at most the initial one, or dropping the existence of a run from the goal, gives a weaker theorem; part (a) of the goal rules this out.

A complete development needs elementary real analysis (Real.rpow, Real.log, $1-x\le e^{-x}$), a finite probabilistic or averaging argument for Lemma 2.2, and induction over runs. Contributions are welcome on any milestone; a derandomized averaging lemma for Lemma 2.2 would be reusable in the weighted mission of this series.

Selected references

• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM J. Comput. 39(2):361–370, 2009. https://doi.org/10.1137/060661946
• 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
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3):93–263, 2009. https://doi.org/10.1561/0400000024

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

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

Chapter IX of von Neumann and Morgenstern's Theory of Games and Economic Behavior asks when a game played by many participants is really several separate games played side by side. The authors' motivation (41.1) is methodological: the general theory of the $n$-person game becomes unmanageable as $n$ grows, and one way to gain insight into large games is to isolate classes of games that can be analysed exactly. The first such class consists of games whose players fall into groups that have no dealings with each other — the book's example is the internal economies of two countries whose connections are disregarded (41.2.4). Such a game is the composition of its constituents, and the question of the chapter is how to recognise a composite game from its characteristic function alone and how far a given game can be decomposed.

The answer (§43) is a structure theorem. The groups of players that can be split off form a Boolean algebra of sets; its atoms, the minimal splitting sets, form a partition of the set of players, the decomposition partition $\Pi_\Gamma$; and every splitting set is a union of blocks of $\Pi_\Gamma$. The book remarks (41.3.3) that the splitting condition (41:7) is exactly Carathéodory's criterion of measurability, transported from measures to characteristic functions. The mission formalizes §43, together with the criterion (42:G) of §42 on which it rests.

Setting

Let $I$ be a finite set of players. A characteristic function is a real number $v(S)$ for every subset $S \subseteq I$ (every coalition, including the empty set $\ominus$ and $I$). Write $-S = I - S$. From 42.4.1 on the book works in the domain of constant-sum games, whose characteristic functions are, by (42:D), exactly the functions satisfying

$$\text{(42:6:a)}\ v(\ominus) = 0,\qquad \text{(42:6:b)}\ v(S) + v(-S) = v(I),\qquad \text{(42:6:c)}\ v(S) + v(T) \leqq v(S \cup T)\ \text{ if } S \cap T = \ominus .$$

For $J \subseteq I$ with complement $K = I - J$, the game is decomposable with respect to $J$ and $K$ if there are constant-sum games $\Delta$ on the players $J$ and $\mathrm H$ on the players $K$ with $v(R) = v_\Delta(R \cap J) + v_{\mathrm H}(R \cap K)$ for all $R \subseteq I$ — formula (41:3). The $J$-constituent $\Delta$ is the game on $J$ with $v_\Delta(S) = v(S)$ for $S \subseteq J$ (41:4).

A splitting set (43.1) is a $J \subseteq I$ satisfying (41:6),

$$v(S \cup T) = v(S) + v(T) \quad \text{for } S \subseteq J,\ T \subseteq I - J .$$

The game is indecomposable if $\ominus$ and $I$ are its only splitting sets (43.3.1). A minimal splitting set is a splitting set $J \neq \ominus$ none of whose proper subsets $J' \neq \ominus$ is splitting (43.3.2), and $\Pi_\Gamma$ is the system of all minimal splitting sets. The game is inessential (42:F) if it is strategically equivalent to the zero game, i.e. $v(S) + \sum_{k \in S} \alpha^0_k = 0$ for all $S$, for some reals $\alpha^0_k$ (the transformation (42:5)).

Formalization targets

Goal: (43:F), (43:G), (43:H)

For every $v$ satisfying (42:6:a)–(42:6:c):

$$J_1 \neq J_2 \in \Pi_\Gamma \Rightarrow J_1 \cap J_2 = \ominus, \qquad \bigcup_{J \in \Pi_\Gamma} J = I, \qquad K \text{ splitting} \iff K = J_1 \cup \dots \cup J_p,\ J_i \in \Pi_\Gamma .$$

The goal combines the partition property and the characterization of all splitting sets; it is the book's own summary of §43.3 and does not presuppose that $\Pi_\Gamma$ is a partition.

Milestones

In attack order: the criterion (42:G) (decomposability $\iff$ (41:6) $\iff$ (41:7)); the closure properties (43:A) (complements), (43:B) ($\ominus$, $I$), (43:C) (intersections and unions); (43:D) (splitting sets of a constituent) and (43:E) (a constituent is indecomposable iff its set is minimal); (43:F), (43:G) separately; (43:I) (a minimal splitting set is disjoint from, or inside, any splitting set); the restatement (43:H*) ($K$ splits iff every block of $\Pi_\Gamma$ lies inside or outside $K$); and the two extreme cases (43:J) ($\Pi_\Gamma$ = all singletons iff the game is inessential) and (43:K) ($\Pi_\Gamma = \{I\}$ iff the game is indecomposable).

Significance

The decomposition partition is canonical: every constant-sum game splits uniquely into indecomposable constituents, and (43:E) identifies them as the constituents on the blocks of $\Pi_\Gamma$. The two extreme cases (43:J), (43:K) show that inessentiality and indecomposability are opposite ends of one scale. Chapter IX uses this structure in §§44–47, where solutions of decomposable games are related to solutions of their constituents ((46:A)–(46:I)); a formal decomposition partition is the prerequisite for that later work, and a candidate follow-up mission.

The results are classical and proved in the book. The mission's contribution is a machine-checked version: a formal definition layer for splitting sets of a set function on a finite set, the Boolean-algebra closure, and the atomic decomposition. The combinatorial core — that the sets satisfying a Carathéodory-type additivity condition form a Boolean algebra of a finite set, whose atoms partition it — is reusable outside game theory (for instance for finitely additive decompositions of set functions). No machine-checked version of these results is known to exist; they are formalized here for the first time as far as a search of the platform shows.

Difficulty

The individual steps are elementary, but the obvious argument for the key closure property (43:C) fails: to show that $J' \cup J''$ is splitting one cannot simply add the identities (41:6) for $J'$ and for $J''$, since a pair $S \subseteq J' \cup J''$, $T \subseteq I - (J' \cup J'')$ is not of the form those identities control, and $J' \cap J''$ may be nonempty — the book's footnote on p. 354 singles out overlapping splitting sets as the case its proof is really about. Likewise (43:D) is not a tautology: that a set self-contained within a self-contained set is self-contained in the whole game has to be proved (footnote 1, p. 355). Formally, the main work is bookkeeping of set identities and the passage between subsets of $J$ (players of the constituent) and subsets of $I$.

Formalization scope

• Players. The set of players $I$ is an arbitrary finite type ι with decidable equality (the book's $I = (1, \dots, n)$; in Chapter IX players are also named $1', \dots, k', 1'', \dots, l''$). Coalitions are Finset ι, $-S$ and $I - J$ are the complement Sᶜ in $I$, and $v$ is a function Finset ι → ℝ.
• Standing hypotheses. Every theorem assumes (42:6:a)–(42:6:c) (the structure IsConstantSum), the chapter's domain from 42.5.3 on ("in the remainder of this chapter we will continue to consider constant-sum games", p. 353). $v(I)$ is arbitrary: the statements are not restricted to zero-sum games, which would be a weaker special case. (43:K) additionally assumes $I$ nonempty ([Nonempty ι], the book's $n \geqq 1$); every other statement holds without it. (43:E) assumes $J \neq \ominus$, since the book's constituent is a game and has at least one player.
• Characteristic functions only. Games are represented by their characteristic functions, as the book does throughout §§42–43 by (42:D). Decomposability quantifies over constant-sum characteristic functions $v_\Delta$, $v_{\mathrm H}$ on the subtypes ↥J, ↥Jᶜ; the $J$-constituent is $v$ restricted to subsets of ↥J. Sums of sets are unions; "disjunct" is Disjoint.
• Π_Γ. decompositionPartition v is the set of minimal splitting sets; that it is a partition is proved, not assumed. An aggregate of minimal splitting sets is a finite family A, its sum A.sup id; the empty aggregate gives $\ominus$.
• No trivialization. A definition of splitting sets that quantified over $T \subseteq I$ instead of $T \subseteq I - J$, or complements taken in an ambient type larger than $I$, would change the theorems; here the complement is in the finite type of players itself. With $I$ empty all statements except (43:K) hold trivially, and (43:K) carries the nonemptiness hypothesis.
• Contributions welcome. Proofs of the milestones in the listed order; general Mathlib-style lemmas on Boolean subalgebras of Finset ι and their atoms, which would shorten (43:F)–(43:H).

Selected references

• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (page-for-page reprint of the 3rd edition, 1953), Chapter IX, §§41–43, pp. 339–357. https://doi.org/10.1515/9781400829460
• C. Carathéodory, Vorlesungen über reelle Funktionen, Teubner, Leipzig–Berlin, 1918, Chapter V (the measurability criterion to which (41:7) corresponds, cited by the book on p. 343).

Motivation

Johnson's 1954 paper in Naval Research Logistics Quarterly is the starting point of machine scheduling theory. Its first section solves the two-machine flow shop: $n$ items must pass through machine 1 and then machine 2, and an explicit ordering rule minimizes the total elapsed time. Its second section treats three machines. There the problem "loses some of the nice structure of the two-stage case" (p. 65), and the general three-machine problem was later shown to be strongly NP-hard (Garey, Johnson and Sethi, 1976). Johnson nevertheless identifies a restricted case, in which the middle machine is dominated by the first (or the last), where the two-machine rule still gives an optimal schedule. That case, and the structural facts behind it, are the content of this mission.

The three-machine results are still the reference point for polynomially solvable flow shops and for lower bounds in branch-and-bound methods for the general problem.

Timeline.

• 1954: Johnson proves the two-machine rule (Theorem 1) and, for three machines, the reduction to a common ordering (Lemma 3), a closed form for the elapsed time, and optimality of the rule on $A_i + B_i$, $B_i + C_i$ when $\min A_i \ge \max B_j$ (Theorem 2), with the mirror case $\min C_i \ge \max B_j$ asserted.
• 1976: Garey, Johnson and Sethi show that minimizing makespan in a three-machine flow shop is strongly NP-hard in general, so some restriction of Theorem 2's kind is unavoidable for an exact ordering rule.

Setting

There are $n$ items and three machines. Item $i$ needs processing time $A_i > 0$ on machine 1, $B_i > 0$ on machine 2 and $C_i > 0$ on machine 3, in that order. Each machine handles at most one item at a time, and processing is not interrupted.

A schedule assigns each item start times $s^1_i, s^2_i, s^3_i$. It is feasible when all start times are at least $0$ on machine 1, the processing intervals of distinct items on the same machine do not overlap, and $s^1_i + A_i \le s^2_i$, $s^2_i + B_i \le s^3_i$. The three machines may process the items in different orders. The total elapsed time (makespan) is $\max_i (s^3_i + C_i)$.

An ordering $\sigma$ lists the items, $\sigma(k)$ being the item in position $k$. Its as-soon-as-possible schedule processes the items in the order $\sigma$ on every machine and starts each item on each machine as early as the rules allow. For an ordering, with positions $1, \dots, n$, Johnson defines

$$K_u = \sum_{i=1}^{u} A_i - \sum_{i=1}^{u-1} B_i, \qquad H_v = \sum_{i=1}^{v} B_i - \sum_{i=1}^{v-1} C_i,$$

the sums running over the items in the first $u$ (resp. $v$) positions.

Johnson's three-stage rule says that item $i$ definitely precedes item $j$ when

$$\min(A_i + B_i,\ C_j + B_j) < \min(A_j + B_j,\ C_i + B_i) \tag{IV}$$

and calls them indifferent under equality. An ordering is consistent with (IV) when no item placed later is definitely preferred to an item placed earlier.

Formalization targets

Goal: Theorem 2 (p. 67)

If every $A_i$ is at least every $B_j$, then an ordering consistent with (IV) exists, and for every such ordering $\sigma$ the as-soon-as-possible schedule of $\sigma$ is feasible and satisfies

$$\operatorname{makespan}(\text{as-soon-as-possible schedule of } \sigma) \le \operatorname{makespan}(s) \quad \text{for every feasible schedule } s .$$

Milestones

1. Lemma 3 (p. 65). Every feasible schedule is matched or beaten by the as-soon-as-possible schedule of some single ordering.
2. Closed form (p. 66). For every ordering, the total idle time of machine 3 is $\sum_i Y_i = \max_{1 \le u \le v \le n}(H_v + K_u)$, so that

$$\operatorname{makespan} = \sum_{i=1}^{n} C_i + \max_{1 \le u \le v \le n} (K_u + H_v),$$

the "maximum walk" of p. 68. 3. Special case (p. 67). If $\min A_i \ge \max B_j$ then $\max_{u \le v} K_u = K_v$, so the makespan is $\sum_i C_i + \max_v (H_v + K_v)$. 4. (III) $\Leftrightarrow$ (IV) (p. 67). Interchanging the items in positions $j, j+1$ changes $H$ and $K$ only at $j, j+1$, and the interchange is strictly worse for the diagonal terms exactly when (IV) holds. 5. Lemma 4 (p. 67). Relation (IV) is transitive, except when the middle item is indifferent to both others. 6. Mirror case (p. 68). The conclusion of Theorem 2 also holds when every $C_i$ is at least every $B_j$.

Significance

The result. Theorem 2 gives an $O(n \log n)$ exact method for a class of three-machine flow shops, in a problem that is strongly NP-hard in general. Lemma 3 says that, for three machines, permutation schedules are dominant; Johnson's example on p. 65 shows this fails for four machines. The closed form of milestone 2 expresses the makespan of any ordering as a longest path in a grid, the device behind most later flow-shop lower bounds.

Formalizing it. All results are proved on paper, some tersely: Lemma 3's proof is two lines and cites the wrong lemma, Lemma 4 is proved by reference to Lemma 2, and the mirror case is asserted without proof. A search of Mathlib and of the platform catalog found no machine-checked proof of any of them. The mission produces a checked account of the three-machine flow shop, including the comparison against all feasible schedules rather than only permutation schedules, and pins down the exact form of the hypotheses (see below).

Difficulty

The interchange argument of the two-machine case does not transfer directly. For a general ordering the makespan involves $\max_{u \le v}(H_v + K_u)$, and interchanging adjacent items changes terms that depend on everything placed earlier; the page notes that "the decision is not independent of what precedes the interchanged elements". The hypothesis $\min A \ge \max B$ is what makes $K$ nondecreasing along the ordering, collapsing the double maximum to the diagonal. A second obstacle is that (IV) is not a total preorder: ties break transitivity, so passing from "no adjacent pair can be improved" to "optimal" needs the all-pairs consistency and the tie exception of Lemma 4. Finally, Lemma 3 is a statement about arbitrary start-time schedules, so the reduction to orderings must handle machines whose orders differ.

Formalization scope

Items are Fin n; processing times are real-valued functions A B C : Fin n → ℝ, assumed positive in each theorem that is about schedules (the paper's standing assumption, p. 61). A schedule is three start-time functions; feasibility is spelled out as above with non-overlap written as a disjunction of inequalities. The makespan is the maximum of the machine-3 completion times together with $0$, so the empty instance has makespan $0$. An ordering is an Equiv.Perm (Fin n) with σ k the item in position k; positions are 0-based, so the Lean K u, H v are the paper's $K_{u+1}$, $H_{v+1}$. Statements with maxima over positions assume $n \ge 1$.

Hypotheses made explicit or corrected:

• $\min A_i \ge \max B_i$ is read globally, $B_j \le A_i$ for all $i, j$, as in the section heading. The pointwise reading $B_i \le A_i$ makes Theorem 2 false (an instance with five items is recorded in the Formalization Note of the goal).
• Consistency with (IV) is required for all pairs of positions, not only adjacent ones.
• Lemma 4 carries Lemma 2's exception for an item indifferent to both others; without it the statement is false.
• Lemma 3's proof cites "Lemma 2" where Lemma 1 is meant.
• The interchange equivalence (milestone 4) is stated for arbitrary reals, which is stronger than the page needs.

Optimality in the goal is against every feasible schedule. A formalization that compares only orderings with each other, or that defines the objective as the closed form $\sum C + \max(K_u + H_v)$, would drop Lemma 3's content and is ruled out: the makespan is the latest completion time of a start-time schedule. The existence clause keeps the optimality clause from being vacuous.

A complete development needs finite sums over initial segments of Fin n, Finset.sup', and permutation manipulations (adjacent transpositions, bubble-sort arguments). The feasibility model and the closed form are reusable for other flow-shop results; contributions of general lemmas on adjacent interchanges of permutations are welcome.

Selected references

• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117

Motivation

A b-matching with upper bounds in a graph $G=(V,E)$ assigns a nonnegative integer $x_e\le d_e$ to every edge so that the edges at each node $i$ carry at most $b_i$ in total. Maximizing a linear objective over such assignments is an integer program that contains ordinary matching ($b\equiv 1$, $d\equiv 1$) and appears in assignment, transportation and scheduling models with capacities on both nodes and arcs. Edmonds and Johnson showed that the integer hull of this system is described by adding the blossom (matching) inequalities to the linear relaxation (Edmonds–Johnson 1970; cited in the paper as [8], [13]). There are exponentially many blossom inequalities, so a cutting-plane method needs a separation procedure: given a fractional point $\bar x$, find a violated blossom inequality or certify that none exists.

M. W. Padberg and M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7 (1982), gave this procedure. Section 1 of the paper computes a minimum-capacity cut with an odd number of odd-labelled nodes in polynomial time; Sections 2 and 3 reduce blossom separation to that computation. This mission formalizes Section 3, the case with upper bounds $d$. The companion mission Odd Minimum Cut-Sets and b-Matchings 1 formalizes Section 1.

Timeline: Edmonds (1965) describes the perfect matching polytope; Edmonds and Johnson (1970) extend the description to capacitated $b$-matching; Gomory and Hu (1961) give the cut-tree that Section 1 of Padberg–Rao relies on; Padberg and Rao (1982) reduce separation to odd minimum cuts. Later work (Letchford, Reinelt and Theis, 2008) shortened the resulting algorithms; the reduction itself is the one stated here.

Setting

Let $G=(V,E)$ be a finite simple undirected graph, $b\in\mathbb Z_{>0}^V$ and $d\in\mathbb Z_{>0}^E$. The system is

$$Ax\le b,\qquad x\le d,\qquad x\ge 0, \tag{3.1}$$

with $A$ the node–edge incidence matrix. For $W\subseteq V$ write $E(W)$ for the edges with both ends in $W$ and $(W:V-W)$ for the cut-set of $W$, the edges with exactly one end in $W$. For $T\subseteq (W:V-W)$ with $b(W)+d(T)=\sum_{i\in W}b_i+\sum_{e\in T}d_e$ odd, the blossom inequality is

$$x(W)+x(T)=\sum_{e\in E(W)}x_e+\sum_{e\in T}x_e\le \tfrac12\bigl(b(W)+d(T)-1\bigr). \tag{3.3}$$

Let $\bar x$ be a real point feasible for (3.1) and $\bar s=b-A\bar x$ its node slacks. Let $E(\bar x)$ be the edges with $\bar x_e>0$. The labelled weighted graph $G(\bar x,d)$ has nodes $V$, a special node $S$, and one new node $i_e$ for each $e\in E(\bar x)$. For each such edge $e=[i,j]$, where $i$ is the end the construction scans first, it has an edge $[i,i_e]$ of weight $d_e-\bar x_e$ and an edge $[i_e,j]$ of weight $\bar x_e$. Each $i\in V$ is joined to $S$ with weight $\bar s_i$. There are no other edges. A node $i_e$ is odd iff $d_e$ is odd; $S$ is odd iff $b(V)$ is odd; a node $i\in V$ is odd iff $b_i$ plus the $d_e$ of the subdivided edges scanned from $i$ is odd. A node set $U$ is odd when it contains an odd number of odd nodes, and $\bar y(U:\tilde V-U)$ denotes the total weight of the edges leaving $U$ (its cut capacity).

Formalization targets

Goal: Theorem 3.1

For every feasible $\bar x$ and every scan order,

$$\exists\,W\subseteq V,\ T\subseteq (W:V-W):\ b(W)+d(T)\text{ odd},\ \bar x(W)+\bar x(T)>\tfrac12\bigl(b(W)+d(T)-1\bigr)$$ $$\Longleftrightarrow\quad \exists\,U\subseteq \tilde V \text{ odd}:\ \bar y(U:\tilde V-U)<1 .$$

The paper's closing sentence, that $W$ and $T$ can be obtained constructively from the proof of Lemma 3.2, describes the proof and is not part of the formal statement.

Milestones

1. Eq. (3.6): $2x(W)+x(W:V-W)+x(T)+s(W)+t(T)=b(W)+d(T)$ for $T\subseteq(W:V-W)$, with $t=d-x$.
2. Eq. (3.7): $\bar x$ violates (3.3) for $(W,T)$ iff $\bar x(W:V-W)+d(T)-2\bar x(T)+\bar s(W)<1$.
3. Lemma 3.1: if $T\subseteq (W:V-W)\cap E(\bar x)$ and $b(W)+d(T)$ is odd, some odd $U$ with $S\notin U$ has $\bar y(U:\tilde V-U)$ equal to the left side of (3.7) (Eq. (3.8)).
4. Lemma 3.2: every odd $U$ with $S\notin U$ and capacity $<1$ arises this way from some $(W,T)$ with $b(W)+d(T)$ odd.

Significance

Theorem 3.1 is what makes the blossom inequalities of capacitated $b$-matching usable in a linear-programming based cutting-plane method: combined with the odd minimum cut algorithm of Section 1, it separates them in polynomial time. By the equivalence of separation and optimization, it also yields a polynomial-time algorithm for capacitated $b$-matching through the ellipsoid method. The paper notes the further consequence that every odd cut-set of capacity less than one, not only a minimum one, gives a violated inequality.

The results are proved in the 1982 paper; none of them has a machine-checked proof that this mission is aware of. What the mission adds is a formal statement of the graph $G(\bar x,d)$ and of the reduction, and a checked proof of it. The definitions of the capacitated $b$-matching system, its blossom inequalities and the subdivided graph are reusable for later work on matching polytopes and on the uncapacitated case of Section 2.

Difficulty

The identities (3.6) and (3.7) are bookkeeping over incidences. The substance is the correspondence between node sets $W$ with complemented edge sets $T$ and odd node sets $U$ of $G(\bar x,d)$. In one direction the right $U$ must pick, for every cut edge, the side of $i_e$ that makes the edge contribute $\bar x_e$ or $d_e-\bar x_e$ as (3.7) requires, and its parity must be computed through the orientation-dependent labels. In the other direction an arbitrary odd cut of capacity below one must be shown to have this shape; this uses $d_e\ge 1$ to exclude every other position of a new node $i_e$, and it uses the evenness of the total label to pass from an odd set containing $S$ to its complement. A point $\bar x$ whose blossom violation uses an edge $e\in T$ with $\bar x_e=0$ has no new node for $e$. Such a $T$ has to be ruled out, and the argument uses the capacity bound. It is not an assumption of the theorem.

Formalization scope

The graph is a Mathlib SimpleGraph V on a finite type with decidable adjacency; edges are elements of G.edgeFinset : Finset (Sym2 V). The data are b : V → ℕ and d : Sym2 V → ℕ, positive on nodes and on edges, and a real point x : Sym2 V → ℝ. Feasibility means the linear relaxation of (3.1); integrality of $\bar x$ is not assumed. All halves and differences are computed in ℝ. When $W=V$ the cut-set is empty, so the paper's convention "$T$ is empty" holds automatically.

$G(\bar x,d)$ is fixed by definitions from $(G,b,d,\bar x)$ and an orientation tail choosing the end of each edge scanned first; every theorem quantifies over the orientation. The node type is Option V ⊕ {e // e ∈ E(x̄)}, with none the special node $S$. Weights are a symmetric function on nodes with $0$ meaning "no edge". The labels are given in closed form. The paper assigns them by a sequential scan that flips the parity of the scanned end by $d_e$, and addition mod 2 does not depend on the order of the scan. "The cut capacity of an odd minimum cut-set is less than one" is stated as "some odd cut has capacity less than one"; the two agree, and the formulation avoids a minimum over a possibly empty family.

Two trivializing formalizations are ruled out: $G(\bar x,d)$ is constructed, not an arbitrary labelled graph assumed to satisfy (3.8); and no infimum over odd cuts is taken, since a real sInf of an empty family is $0$ and would make the right side true when no odd cut exists.

Contributions welcome: proofs of the milestones, lemmas on cut capacities of symmetric weight functions on finite types, and parity bookkeeping for labelled node sets.

Selected references

• M. W. Padberg, M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7(1), 67–80, 1982. https://doi.org/10.1287/moor.7.1.67
• J. Edmonds, E. L. Johnson, Matching: a well-solved class of integer linear programs, in Combinatorial Structures and Their Applications, Gordon and Breach, 89–92, 1970; reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, 27–30, 2003. https://doi.org/10.1007/3-540-36478-1_3
• R. E. Gomory, T. C. Hu, Multi-terminal network flows, Journal of the SIAM 9(4), 551–570, 1961. https://doi.org/10.1137/0109047
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
• A. N. Letchford, G. Reinelt, D. O. Theis, Odd minimum cut sets and b-matchings revisited, SIAM Journal on Discrete Mathematics 22(4), 1480–1487, 2008. https://doi.org/10.1137/060664793