Theoretical Computer Science

Motivation

A multicommodity flow problem asks to route several commodities simultaneously through a capacitated network, each from its own source to its own sink. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest routable flow equals the capacity of the smallest separating cut. For many commodities the natural analogue fails: the max-flow can be strictly smaller than the min-cut, already for four commodities (Okamura and Seymour, 1981). Leighton and Rao asked how large the gap can be, and showed that for uniform demands it is at most logarithmic in the number of nodes. The result turned the min-cut, an NP-hard quantity, into something approximable by a linear program, and became the basis of the first polylogarithmic approximation algorithms for sparsest cut, balanced cut, minimum feedback arc set, crossing number and VLSI layout (Leighton–Rao, J. ACM 1999).

Timeline:

• 1956–1963. Ford and Fulkerson prove max-flow = min-cut for one commodity; Hu (1963) proves equality for two commodities.
• 1981–1990. Okamura and Seymour give a 4-commodity example with max-flow 3/4 and min-cut 1. Schrijver (1990), combining Lomonosov and Papernov, characterizes demand graphs for which equality always holds. Shahrokhi and Matula (1990) prove equality for uniform demands under a condition on the dual.
• 1988. Leighton and Rao (FOCS 1988) prove the $\Theta(\log n)$ gap for uniform demands; the journal version (1999) is the source of this mission.
• 1995. Linial, London and Rabinovich, and independently Aumann and Rabani, extend the bound to arbitrary demands with $O(\log k)$ for $k$ commodities, via metric embeddings (Combinatorica 1995).

Setting

A network is a finite set $V$ of $n$ nodes with a capacity $C(u,v)=C(v,u)\ge0$ for every pair; the pair is an edge when $C(u,v)>0$. For $U\subseteq V$ with complement $\bar U$, the cut capacity $C(U,\bar U)$ is the total capacity of the edges joining $U$ to $\bar U$. As in the paper, the network is assumed connected: $C(U,\bar U)>0$ for every nonempty proper $U$.

In the uniform multicommodity flow problem (UMFP) every unordered pair of nodes is a commodity with demand one. A routing of value $\lambda$ sends $\lambda$ units between every pair simultaneously, so that the total flow of all commodities over each edge, in both directions together, is at most its capacity. The max-flow $f$ is the largest such $\lambda$ (the concurrent max-flow).

The min-cut (sparsest cut) of the UMFP is

$$\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|},$$

the minimum over cuts of the cut capacity divided by the demand separated by the cut. The quantity $C(U,\bar U)/(|U||\bar U|)$ is the ratio cost of the cut.

The milestones use the dual objects. A distance function $d$ assigns a nonnegative length to each edge; $d(u,v)$ is then the shortest-path distance, $d(T,u)=\min_{t\in T}d(t,u)$, and the total weight is $W=\sum_{e}C(e)d(e)$. The distance constraint (5) is $\sum_{\{u,v\}}d(u,v)\ge1$, summed over unordered pairs. A set of nodes has radius at most $\Delta$ if some centre reaches all its nodes by walks inside the set of length at most $\Delta$. Throughout, $\log n=\log_2 n$.

Formalization targets

Goal: Theorem 2 (p. 795)

$$\Omega\!\left(\frac{\mathcal S}{\log n}\right)\le f\le\mathcal S$$

for every uniform multicommodity flow problem: there is one absolute constant $c>0$ such that $c\,\mathcal S/\log n\le f\le\mathcal S$ for every connected network with $n\ge2$ nodes. The goal fixes no constant, so it is the form any improved argument would still prove.

Milestones, in the order the argument uses them

1. Weak duality (§1.2, pp. 789–790): every concurrent flow of value $\lambda$ satisfies $\lambda\,|U||\bar U|\le C(U,\bar U)$ for every cut.
2. LP duality (§2.2, p. 796): every distance function satisfying (5) has $W\ge f$, and some such function has $W=f$.
3. Lemma 3 (p. 797): for every $\Delta>0$, $V$ splits into components of radius at most $\Delta$ with at most $4W\log n/\Delta$ capacity between components.
4. Corollary 4 (pp. 798–799): either a set of at least $2n/3$ nodes has radius at most $1/(2n^2)$, or some cut has ratio cost at most $36W\log n$.
5. Lemma 5 (p. 799): if $|T|\ge 2n/3$ and $\sum_{u\notin T}d(T,u)\ge 1/(2n)$, some cut has ratio cost at most $6W$.
6. Lemma 6 (p. 800): a distance function satisfying (5) yields a cut of ratio cost at most $36W\log n$.

Companion

$\mathcal S\le 36\,f\log n$ and $f\le\mathcal S$: Theorem 2 with the constant its proof produces.

Significance

The theorem says that the LP relaxation of uniform sparsest cut has integrality gap $O(\log n)$, and the expander example of §2.1 (Theorem 1) shows this is tight. Combined with the cut-finding argument, it gives an $O(\log n)$-approximation for sparsest cut and, through the paper's Section 3, approximation algorithms for balanced separators, minimum cut linear arrangement, crossing number, VLSI layout area, feedback arc set and the emulation of networks. Region-growing decompositions of the kind in Lemma 3 reappear in low-diameter decompositions, multicut (Garg–Vazirani–Yannakakis), and metric embedding.

The result is proved; no machine-checked proof of it is known. A formalization would provide: concurrent multicommodity flow and its LP dual on finite graphs, the uniform sparsest cut, a verified region-growing decomposition, and the max-flow min-cut gap theorem itself. The LP-duality milestone, which the paper cites rather than proves, is a reusable piece of flow theory in its own right.

Difficulty

The upper bound $f\le\mathcal S$ is a counting argument. The lower bound is the content. The natural idea, rounding an optimal dual distance function by a threshold and cutting the long edges, does not work: the paper notes (p. 797) that no thresholding rule is known that always yields a good cut, because edges with large distance need not form a sparse cut. Any argument must convert the fractional dual into a single cut while losing only a $\log n$ factor against the total weight $W$, which requires a global property of the distance function rather than the lengths of individual edges. The LP-duality step needs a correct dual for the concurrent flow problem with shortest-path distances, which Mathlib does not provide off the shelf.

Formalization scope

• Nodes and capacities. V is a Fintype with decidable equality; capacities are a symmetric nonnegative real function vanishing on the diagonal, and the graph is the simple graph of pairs with positive capacity. Goal-level statements assume 2 ≤ Fintype.card V and connectivity in the form $C(U,\bar U)>0$ for every nonempty proper $U$ (the paper's standing assumption, p. 789).
• Demands and flows. Each unordered pair is encoded as two ordered commodities with demand $\tfrac12$ (the paper's footnote 2). Flows are arc flows with conservation per commodity, and both directions of an edge share its capacity. The max-flow is the real supremum of feasible values; with $n\ge2$ that set is nonempty and bounded.
• Cuts. The min-cut ranges over nonempty proper subsets only. Including $U=\emptyset$ or $U=V$ would give $0/0$, which Lean evaluates to $0$ and which would make the goal trivially true; this formalization excludes it.
• Distances. $d(u,v)$ is an infimum over walks in the graph, meaningful under connectivity; the radius of a component is measured by walks inside it.
• Constants. The goal keeps the page's $\Omega$ with a single universal constant chosen before the network. The milestones carry the constants computed in the paper's proofs ($36$ in Corollary 4 and Lemma 6, $6$ in Lemma 5), and each statement says so.
• Algorithms. "We can find" is formalized as existence. Running times and the remark that the proofs yield polynomial-time algorithms (p. 801) are out of scope.

Contributions welcome: proofs of any milestone; a general LP-duality theorem for concurrent multicommodity flow, reusable for the product and directed variants; and a general region-growing lemma.

Selected references

• T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
• F. Shahrokhi and D. W. Matula, The maximum concurrent flow problem, J. ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620
• H. Okamura and P. D. Seymour, Multicommodity flows in planar graphs, J. Combin. Theory Ser. B 31:75–81, 1981. https://doi.org/10.1016/S0095-8956(81)80012-3
• N. Linial, E. London and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
• V. Chvátal, Linear Programming, W. H. Freeman, 1983.

Motivation

Many dense combinatorial optimization problems (Max-Cut, graph bisection, quadratic assignment on dense instances) have objective functions that are sums of matrix entries over rectangles $S\times T$. If a matrix can be replaced by a simple surrogate that agrees with it on every rectangle up to a small error, such problems can be solved approximately on the surrogate. Frieze and Kannan's paper Quick approximation to matrices and applications (Combinatorica 19 (1999) 175–220) supplies this surrogate: a sum of a bounded number of cut matrices. Their decomposition is a "weak" form of Szemerédi's regularity lemma whose number of pieces grows only like $1/\varepsilon^2$, against a tower-type bound for Szemerédi's lemma. It underlies constant-time sampling algorithms for dense instances, the theory of graph limits (the cut distance of Lovász and Szegedy), and the cut-norm approximation algorithm of Alon and Naor.

Timeline:

• 1978: Szemerédi's regularity lemma, with a number of parts of tower type in $1/\varepsilon$.
• 1996: Frieze and Kannan announce the weak regularity lemma (FOCS 1996).
• 1999: the journal paper proves the matrix version, its algorithmic forms, and applications to Max-Cut, Max-SNP problems and pseudo-regular partitions.
• 2004–2006: Alon and Naor approximate the cut norm via Grothendieck's inequality; Lovász and Szegedy build graph limits on the cut distance.

Setting

Let $R$ and $C$ be finite sets, $|R|=m$, $|C|=n$, and let $A$ be a real $R\times C$ matrix. For $S\subseteq R$, $T\subseteq C$ write

$$A(S,T)=\sum_{(i,j)\in S\times T}A(i,j).$$

The Frobenius norm is $\|A\|_F=\big(\sum_{i,j}A(i,j)^2\big)^{1/2}$, and the cut norm is $\|A\|_C=\max_{S\subseteq R,\,T\subseteq C}|A(S,T)|$.

For $S\subseteq R$, $T\subseteq C$ and $d\in\mathbb R$, the cut matrix $\mathrm{CUT}(S,T,d)$ has entry $d$ on $S\times T$ and $0$ elsewhere; it has rank at most one. A cut decomposition of width $s$ writes

$$A=D^{(1)}+\dots+D^{(s)}+W,\qquad D^{(t)}=\mathrm{CUT}(R_t,C_t,d_t),$$

with error matrix $W$. In the Lean development these are blockSum, frobNorm, cutNorm, cutMatrix and cutSum in the namespace FriezeKannan.CutDecomp.

Formalization targets

Goal: Theorem 7 (p. 188)

For every real $R\times C$ matrix $A$ and every $\varepsilon>0$ there are $s\le1/\varepsilon^2$ cut matrices $D^{(t)}=\mathrm{CUT}(R_t,C_t,d_t)$ such that $W^{(s)}=A-(D^{(1)}+\dots+D^{(s)})$ satisfies

$$|W^{(s)}(S,T)|\le\varepsilon\sqrt{|S|\,|T|}\;\|A\|_F\qquad\forall S\subseteq R,\ T\subseteq C. \tag{17}$$

Milestones (the steps of the proof, p. 188)

1. With $d=W(S,T)/(|S||T|)$ for nonempty $S,T$:

$$\|W-\mathrm{CUT}(S,T,d)\|_F^2-\|W\|_F^2=-|S|\,|T|\,d^2=-\frac{W(S,T)^2}{|S|\,|T|}.$$

2. If $|W(S,T)|>\varepsilon\sqrt{|S||T|}\,\|A\|_F$, this drop is at most $-\varepsilon^2\|A\|_F^2$.
3. If $\|W^{(t)}\|_F^2\le(1-\varepsilon^2t)\|A\|_F^2$, then either $W^{(t)}$ satisfies (17), or one more cut matrix gives $\|W^{(t+1)}\|_F^2\le(1-\varepsilon^2(t+1))\|A\|_F^2$.

Companion statements

• The Remark after Theorem 7 (the case $m=1$): a real $n$-vector $a$ is a weighted sum of at most $\varepsilon^{-2}$ 0-1 vectors plus an error $w$ with $|w(S)|\le\varepsilon\sqrt n\,|a|$ for all $S$.
• Inequality (1), p. 178: $\|M\|_C\le\sup_{x\ne0}\|Mx\|_1/\|x\|_\infty\le4\|M\|_C$.
• §2.3, p. 179: the symmetrised error $\bar W=(W+W^T)/2$ satisfies $\|\bar W\|_C\le\|W\|_C$.

Significance

Theorem 7 says that the width needed to approximate a matrix on all rectangles, with error measured against $\sqrt{|S||T|}\|A\|_F$, depends on $\varepsilon$ only, not on $m$ or $n$. Since $|S||T|\le mn$, it gives a cut decomposition with $\|W\|_C\le\varepsilon\sqrt{mn}\|A\|_F$, the error of the paper's algorithmic Theorem 2. It is the existence statement behind the paper's constant-time approximation schemes for dense Max-Cut and Max-SNP problems and behind its pseudo-regular partitions of graphs (§5.1), and it is the matrix form of the weak regularity lemma used throughout the theory of dense graph limits.

The result is proved in the paper, by an elementary argument. Its formalization adds a machine-checked weak regularity lemma for real matrices with explicit constants, stated in a form (finite index types, block sums, cut matrices) that downstream developments in graph limits, property testing and approximation algorithms can import. To the best of the curators' knowledge it has no machine-checked proof; Mathlib contains Szemerédi's regularity lemma for graphs but not this matrix decomposition or the cut norm of matrices.

Difficulty

The obvious decomposition, one cut matrix per nonzero entry, achieves $W=0$ but has width $mn$; the content is that width $1/\varepsilon^2$ suffices uniformly in the dimensions. Bounding the error on a single rectangle is easy; bounding it on all $2^{m+n}$ rectangles at once, with an error that scales as $\sqrt{|S||T|}$ rather than as $\sqrt{mn}$, is the point. The bound is also against the Frobenius norm of the original matrix $A$, not of the current error, so the argument must track a single global quantity across all steps. In Lean, the main friction is bookkeeping: real casts of cardinalities inside square roots, the division by $|S||T|$, and the identification of the squared Frobenius norm with a double sum.

Formalization scope

• Index sets are arbitrary finite types R, C with decidable equality; subsets are Finsets, and $|S|$ is the cardinality cast to $\mathbb R$. Empty $R$ or $C$ is allowed.
• $\|A\|_F$ is the real square root of the sum of squares (frobNorm); Mathlib's scoped matrix norms are not used. The cut norm is a genuine maximum over the finite nonempty set of pairs of subsets.
• A family of $s$ cut matrices is three functions on Fin s; $s=0$ is allowed (for $\varepsilon\ge1$ or $A=0$ no cut matrix is needed). No nonemptiness, disjointness or sign condition is imposed on $R_t$, $C_t$, $d_t$.
• Added hypotheses, each disclosed in the statement's Formalization Note: $\varepsilon>0$ (the paper's implicit range of the error parameter; $\varepsilon<1$ is not assumed); nonempty $S,T$ in milestone 1 (they make $d$ well defined); the strict inequality $>$ in milestone 2 (the negation of (17); the page prints $\ge$); a nonempty column set for inequality (1) (the supremum over $\mathbb R^n\setminus\{0\}$ needs $n\ge1$). Inequality (1) is stated without division, as the existence of a nonzero $x$ with $\|M\|_C\|x\|_\infty\le\|Mx\|_1$ together with $\|Mx\|_1\le4\|M\|_C\|x\|_\infty$ for all $x$.
• The width bound $s\le1/\varepsilon^2$ is the theorem; without it the statement is trivial (one cut matrix per entry gives $W=0$). A formalization that drops it, bounds the error by $\|W\|_F$ instead of $\|A\|_F$, or uses $\sqrt{mn}$ in place of $\sqrt{|S||T|}$ proves a different theorem.
• Reusable infrastructure: the identity $\|M\|_F^2=\sum_{i,j}M(i,j)^2$, block sums of cut matrices and their sums, and the cut norm with its basic properties (transpose invariance, comparison with the $\infty\to1$ norm). Contributions of these as standalone lemmas, and of the milestones in the listed order, are welcome.

Selected references

• A. Frieze and R. Kannan, Quick approximation to matrices and applications, Combinatorica 19(2) (1999) 175–220. https://doi.org/10.1007/s004930050052
• A. Frieze and R. Kannan, The regularity lemma and approximation schemes for dense problems, Proc. 37th FOCS (1996) 12–20. https://doi.org/10.1109/SFCS.1996.548459
• E. Szemerédi, Regular partitions of graphs, Problèmes combinatoires et théorie des graphes, Colloq. Internat. CNRS 260 (1978) 399–401.
• N. Alon and A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35(4) (2006) 787–803. https://doi.org/10.1137/S0097539704441629
• L. Lovász and B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96(6) (2006) 933–957. https://doi.org/10.1016/j.jctb.2006.05.002

Pricing with unit-demand consumers

A seller with $n$ distinct items faces $m$ consumers, each of whom wants at most one item. Choosing item prices to maximise revenue in this setting is the unit-demand envy-free pricing problem, introduced by Rusmevichientong and studied in algorithmic game theory and revenue management since the mid-2000s. Optimal prices are hard to compute in general, so the guarantees of simple pricing rules matter. The simplest such rule is uniform pricing: put one price $q$ on every item and choose $q$ to maximise revenue.

Aggarwal, Feder, Motwani and Zhu (ICALP 2004) and Guruswami, Hartline, Karlin, Kempe, Kenyon and McSherry (SODA 2005) analysed uniform pricing; in the min-buying model it recovers a $1/(1+\ln m)$ fraction of the optimum, a bound Berbeglia and Joret attribute to Aggarwal et al. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) observed that the min-buying problem is a special case of assortment optimisation under a regular discrete choice model, and that uniform pricing then coincides with the revenue-ordered assortments heuristic. Their general guarantee for that heuristic yields a second bound for uniform pricing, in terms of the spread of the valuations rather than the number of consumers. This mission formalizes that bound (Corollary 4.7) together with the reduction it rests on (Theorem 4.6).

Setting

Unit-demand min-pricing ($\mathrm{UDP}_{\min}$). There are items $[n]$ and consumers $[m]$, $m\ge 1$. Consumer $i$ is interested in a set $B_i\subseteq[n]$ and has a valuation $v_i>0$. Given a price assignment $p:[n]\to\mathbb R_{>0}$, consumer $i$ buys a cheapest item of $B_i$ if its price is at most $v_i$, and nothing otherwise. The seller's revenue is

$$\mathrm{rev}_{\mathrm{UDP}}(p)=\sum_{i:\ B_i\ne\emptyset,\ \min_{x\in B_i}p(x)\le v_i}\ \min_{x\in B_i}p(x),$$

the optimum is $\mathrm{OPT}_{\mathrm{UDP}}=\sup_{p>0}\mathrm{rev}_{\mathrm{UDP}}(p)$, and uniform pricing earns $\mathrm{UP}=\sup_{q>0}\mathrm{rev}_{\mathrm{UDP}}(q,\dots,q)$. Write $v_{\max}=v_m$ and $v_{\min}=v_1$ for the extreme valuations.

Regular choice models. A finite product set $\mathcal C$ carries choice probabilities $\mathcal P(x,S)$ for $x\in\mathcal C$, $S\subseteq\mathcal C$, with no-purchase probability $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular if (i) all probabilities are nonnegative, (ii) $\mathcal P(x,S)=0$ for $x\notin S$, (iii) $\sum_{x\in S}\mathcal P(x,S)\le1$, and (iv) $\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$. With revenues $r:\mathcal C\to\mathbb R_{>0}$, an assortment earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)r(x)$ and $\mathrm{OPT}=\max_S\mathrm{rev}(S)$. If $r_1<\dots<r_k$ are the distinct revenues and $S_i=\{x: r(x)\ge r_i\}$, revenue-ordered assortments earn $\mathrm{RO}=\max_i\mathrm{rev}(S_i)$.

The reduction. From a $\mathrm{UDP}_{\min}$ instance the paper builds $\mathcal C=[n]\times\{v_1,\dots,v_m\}$, $r((x,v))=m\,v$, and $\mathcal P=\frac1m\sum_i\mathcal P_i$, where $\mathcal P_i$ spreads probability one over the set $Q_i(S)$ of pairs $(x,v)\in S$ with $x\in B_i$, $v\le v_i$ and $v$ minimal among the pairs of $S$ whose item lies in $B_i$.

Formalization targets

Goal: Corollary 4.7

$$\mathrm{OPT}_{\mathrm{UDP}}\ \le\ \Big(1+\ln\frac{v_{\max}}{v_{\min}}\Big)\cdot\mathrm{UP}.$$

The bound is the paper's "approximates the optimum revenue to within a factor of $1/(1+\ln\rho)$, $\rho:=v_m/v_1$", stated in product form.

Milestones

1. Lemma 4.5. Some optimal price assignment takes only valuations as prices; in particular $\mathrm{OPT}_{\mathrm{UDP}}$ is attained.
2. Regularity of the reduction's choice model (proof of Theorem 4.6, pp. 17–18).
3. Assortments to prices: $\mathrm{rev}(S)=\mathrm{rev}_{\mathrm{UDP}}(p_S)$ with $p_S(x)=\min\{v:(x,v)\in S\}$ (p. 19).
4. Prices to assortments: for valuation-valued $p$, $\mathrm{rev}(S_p)=\mathrm{rev}_{\mathrm{UDP}}(p)$ with $S_p=\{(x,v): v\ge p(x)\}$ (p. 19).
5. Theorem 4.6 for the explicit instance: regularity, positive revenues, equal optima, and the two-way correspondence between threshold sets and uniform valuation prices.
6. Theorem 3.2 for an arbitrary regular model:

$$\mathrm{OPT}\le\Big(\sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\Big)\mathrm{RO},\qquad \sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\le 1+\ln\frac{r_k}{r_1},\qquad r_0:=0.$$

Significance

The corollary gives a uniform-pricing guarantee that is independent of the number of consumers and items: when valuations lie within a factor $\rho$ of each other, a single price recovers a $1/(1+\ln\rho)$ fraction of the optimum, which improves on $1/(1+\ln m)$ whenever $\rho<m$. More broadly, Theorem 4.6 places $\mathrm{UDP}_{\min}$ inside the class of regular choice models, so every guarantee proved for revenue-ordered assortments under regularity transfers to uniform pricing.

All results here are proved in the paper. Nothing in this mission is formalized elsewhere as far as a search of the platform shows: there is no regular choice model, no $\mathrm{UDP}_{\min}$ problem and no revenue-ordered guarantee on Prove2Me. The mission produces the reduction as reusable infrastructure, a machine-checked version of the paper's Lemma 4.5 (whose appendix proof is an informal repair argument), and the first formal guarantee for uniform pricing.

Difficulty

The reduction is where the work sits. Regularity hinges on the no-purchase case of axiom (iv): enlarging an assortment can only make $Q_i$ nonempty, never empty, and this must be checked for the specific sets $Q_i(S)$ whose definition depends on the whole of $S$. The revenue identities require tracking the minimum over $B_i$ of a price function obtained from an assortment, including items absent from $S$, which receive the paper's "$+\infty$" price. Lemma 4.5 is needed to make the optimum of the uncountable pricing problem coincide with that of a finite assortment problem, and the statement is about a supremum over a continuum of price vectors whose attainment is not obvious. Theorem 3.2 has to relate the optimum to threshold sets of an arbitrary regular model, where products may share revenues and the optimal assortment need not be a threshold set.

The naive route of comparing uniform pricing to the optimum directly, consumer by consumer, does not give a bound in terms of $v_m/v_1$; the reduction to a regular model is what supplies it.

Formalization scope

• Items and consumers are finite types X and M, with Nonempty M ($m\ge1$). Valuations satisfy $v_i>0$ as a field of the instance; the paper says "non-negative", but its reduction ($r=m\,v>0$) and its ratio $v_m/v_1$ need positivity.
• A consumer with $B_i=\emptyset$ pays $0$. Ties among cheapest items do not affect payments, so payments are defined directly.
• $\mathrm{OPT}_{\mathrm{UDP}}$ and $\mathrm{UP}$ are real suprema over positive price assignments and positive uniform prices; both index sets are nonempty and the revenues are bounded by $\sum_i v_i$. Uniform pricing ranges over all $q>0$, not only valuations.
• The no-purchase option is not a product: it is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$, and regularity includes axiom (iv) for it. OPT is a maximum over all Finset C; RO is a maximum over the $k$ threshold sets only. Distinct revenues are sorted 0-based (Fin k), with $r_0=0$ handled as a separate case.
• The paper's $+\infty$ price for $p_S$ is the real $1+\sum_i v_i$, which exceeds every valuation, as its Remark on p. 18 allows. The valuation set collapses equal valuations.
• Approximation factors are in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$; $\ln$ is Real.log applied to ratios $\ge1$.
• Trivializing readings are excluded: Theorem 4.6 is stated for the explicit instance of its proof, not as the bare existence of a regular instance with the same optimum (a single product of revenue $\mathrm{OPT}_{\mathrm{UDP}}$ would satisfy that); $\mathrm{OPT}_{\mathrm{UDP}}$ ranges over all positive price assignments, not uniform ones; valuations are positive, so no logarithm takes a junk value.
• Theorem 3.2 is restated here for this mission's copy of the regular model; it is also the goal of mission I of this series. Reusable pieces: the regular choice model and revenue-ordered value, and the $\mathrm{UDP}_{\min}$ model. Contributions of any milestone, and alternative proofs of Lemma 4.5, are welcome.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82 (2020). https://arxiv.org/abs/1606.01371
• G. Aggarwal, T. Feder, R. Motwani and A. Zhu, Algorithms for multi-product pricing, ICALP 2004. https://doi.org/10.1007/978-3-540-27836-8_8
• V. Guruswami, J. D. Hartline, A. R. Karlin, D. Kempe, C. Kenyon and F. McSherry, On profit-maximizing envy-free pricing, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070598
• P. Rusmevichientong, B. Van Roy and P. W. Glynn, A nonparametric approach to multiproduct pricing, Operations Research 54(1), 2006. https://doi.org/10.1287/opre.1050.0236
• A. Aouad, V. Farias, R. Levi and D. Segev, The approximability of assortment optimization under ranking preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1754

Motivation

Prediction with expert advice asks a master algorithm to combine the binary predictions of a pool of $n$ prediction algorithms, trial after trial, so that it makes few more mistakes than the best member of the pool, without any probabilistic assumption on the data. Littlestone and Warmuth's Weighted Majority Algorithm WM (Littlestone and Warmuth 1994) keeps a weight per member, predicts with the weighted vote, and multiplies the weights of the wrong members by a factor $\beta<1$ after each of its own mistakes. Its mistake bound is of order $\log n + m$, where $m$ is the number of mistakes of the best member on the whole sequence.

That bound compares the master with a single fixed member. In many applications the member that predicts well changes over time: one algorithm is accurate for a while, then a second one, then a third. Against a shifting target of this kind, WM can do badly, because the weight of a member that was wrong for a long time has become so small that it takes many mistakes to recover it. Section 3 of the paper introduces the variant WML, which never decreases a weight that is already small relative to the total, and proves that it pays only a logarithmic cost per change of target. This was the first result of what is now called tracking the best expert; it was later refined by Herbster and Warmuth's Fixed-Share algorithm (Herbster and Warmuth 1998).

Timeline. 1989: a conference version of the paper appears at FOCS. 1994: the journal version, the source of this mission, gives Lemma 3.1 and Theorem 3.1 in their present form. 1998: Herbster and Warmuth's Tracking the Best Expert generalizes the shifting bound to other loss functions.

Setting

A run takes place over $T$ trials $t = 0, \dots, T-1$. In trial $t$ each member $i \in \{1,\dots,n\}$ of the pool predicts $x_i^{(t)} \in \{0,1\}$, the master predicts $\lambda^{(t)} \in \{0,1\}$, and the label $\rho^{(t)} \in \{0,1\}$ is revealed. The predictions of the pool and the labels are arbitrary.

The master keeps weights $w_i^{(t)} > 0$, the weights at the beginning of trial $t$. Let $W^{(t)} = \sum_j w_j^{(t)}$ be the total weight and $q_b^{(t)}$ the total weight of the members predicting $b$. WML has parameters $0 < \beta < 1$ and $0 \le \gamma < \tfrac12$:

1. it predicts $0$ if $q_0^{(t)} > q_1^{(t)}$, $1$ if $q_1^{(t)} > q_0^{(t)}$, and either value on a tie;
2. if $\lambda^{(t)} \ne \rho^{(t)}$, each member $i$ with $x_i^{(t)} \ne \rho^{(t)}$ and $w_i^{(t)} > \frac{\gamma}{n} W^{(t)}$ has its weight multiplied by $\beta$; all other weights stay;
3. if $\lambda^{(t)} = \rho^{(t)}$, no weight changes.

With $\gamma = 0$ this is WM. Write $m$ for the number of mistakes of the master and

$$u = \frac{1+\beta}{2} + (1-\beta)\gamma ,$$

which lies in $[\tfrac12, 1)$ for the stated parameter ranges.

Formalization targets

Goal: Theorem 3.1 (p. 224)

Split the sequence into consecutive segments $\mathcal S_1, \dots, \mathcal S_k$, with $l_i$ trials in $\mathcal S_i$, and let $m_i$ be the smallest number of mistakes any single pool member makes on $\mathcal S_i$. If $\gamma > 0$ and every initial weight is at least $\beta\gamma/n$ times the total initial weight, then

$$m \le \sum_{i=1}^{k} \min\left( l_i,\ \frac{\log\big(n/(\beta\gamma)\big) + m_i \log(1/\beta)}{\log(1/u)} \right).$$

The partition is arbitrary and unknown to the algorithm; the bound holds for all partitions simultaneously.

Milestone: Lemma 3.1 (pp. 223–224)

The single-segment case, $k = 1$, together with the statement that the weight floor survives the run: if every initial weight is at least $\beta\gamma/n$ times the total, then

$$m \le \frac{\log\big(n/(\beta\gamma)\big) + m_0 \log(1/\beta)}{\log(1/u)},$$

and every final weight is at least $\beta\gamma/n$ times the total final weight.

Milestone: the contraction step (p. 224, proof of Lemma 3.1)

On every mistake trial, $W^{(t+1)} \le u\, W^{(t)}$.

Significance

The result. Theorem 3.1 shows that an online algorithm with no knowledge of when or how often the best predictor changes can compete with the best sequence of predictors, at a price of $O(\log(n/(\beta\gamma)))$ mistakes per segment. The $\min$ with $l_i$ says that a segment never costs more than its length. The bound is the template for later tracking and adaptive-regret results in online learning and for algorithms whose weights are kept bounded away from zero.

Formalizing it. The result is proved in the paper; no machine-checked proof of a shifting-target bound exists on Prove2Me or, to our knowledge, in Mathlib. This mission produces a formal model of WML in which ties are arbitrary (a run is a relation, so the bounds cover every tie-breaking rule), the per-mistake contraction, the single-sequence bound with its preserved invariant, and the segment bound. The model of trials, majority votes and mistake counts is reusable for the other algorithms of the paper.

Difficulty

The standard argument for WM compares the decrease of the total weight with the final weight of the best member. For a shifting target this fails twice. First, the best member of a later segment may have been wrong during all earlier segments; under WM its weight has shrunk by $\beta$ per mistake, and the master has to make many mistakes before that member regains influence. Second, the floor that prevents this also prevents some wrong members from being penalized, so the total weight shrinks by less on each mistake than under WM. The statement has to control both effects at once, and the per-segment accounting has to restart from whatever weights the previous segments left behind. A natural first idea, applying the single-sequence bound to each part of an arbitrary (interleaved) partition, does not work: for interleaved subsequences the inequality is false, and the theorem is about consecutive segments.

Formalization scope

The pool is Fin n with $n > 0$; trials are Fin T; binary values are Bool; weights are real, w : ℕ → Fin n → ℝ, with w t the weights at the beginning of trial $t$, w 0 the initial and w T the final weights. A run is the relation IsWMLRun β γ x ρ w lam; it fixes positive initial weights, the majority rule with arbitrary ties, and the update, whose threshold is strict and uses the total weight at the beginning of the trial. Logarithms are natural logarithms; the base cancels in every ratio. The minimum over the pool is an infimum in ℕ over Fin n. Segments are given by monotone boundaries b : Fin (k+1) → ℕ with b 0 = 0 and b (Fin.last k) = T; empty segments are allowed and contribute $0$.

The paper allows $\gamma = 0$ for the algorithm, but then the bounds read $\log(n/0) = +\infty$. In Lean, n / 0 = 0, so the bounds assume $\gamma > 0$; the contraction milestone holds for $0 \le \gamma < \tfrac12$ and is stated so. The hypothesis $\gamma < \tfrac12$ is kept as stated in the paper, not replaced by $u < 1$. A trivializing formalization, such as fixing the tie-breaking rule, dropping the strict weight test, letting the floor hypothesis be unsatisfiable, or allowing interleaved subsequences (which makes the goal false), is ruled out: a run exists for every input from every positive initial weights, and equal initial weights satisfy the floor.

Contributions welcome: proofs of the three statements, and lemmas on restricting a WML run to a block of trials, which the goal needs and which apply to any segment-wise analysis.

Selected references

• N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
• N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Proc. 30th IEEE FOCS, 256–261, 1989. https://doi.org/10.1109/SFCS.1989.63487
• M. Herbster, M. K. Warmuth, Tracking the Best Expert, Machine Learning 32, 151–178, 1998. https://doi.org/10.1023/A:1007424614876

Motivation

Online bipartite matching asks an algorithm to assign arriving requests to resources it cannot reassign later. In display advertising, the requests are page views (impressions) and the resources are advertisers who have bought a fixed number of impressions in advance; each impression must be served immediately or lost. In the adversarial model, Karp, Vazirani and Vazirani (STOC 1990) showed that the RANKING algorithm achieves a $1 - 1/e$ fraction of the optimum in expectation, and that no online algorithm does better. Advertising systems, however, have historical traffic data, which motivates the i.i.d. model: the impression types are drawn independently from a distribution that is known in advance.

Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) were the first to beat $1 - 1/e$ in this model, with an algorithm that achieves $\approx 0.67$ with high probability. Their Section 3 asks the complementary question: how close to $1$ can any online algorithm get when the distribution is known? Their Theorem 3 answers that the expected approximation factor of every online algorithm is bounded strictly away from $1$, already on a graph with six vertices. Later work in the same model (Manshadi, Oveis Gharan and Saberi, SODA 2011, arXiv:1007.1673) sharpened both the algorithmic and the hardness side.

Setting

An instance consists of a bipartite graph $G = (A, I, E)$ between a finite set $A$ of advertisers and a finite set $I$ of impression types, a distribution $D$ on $I$, and a number $n$ of arrivals. In this mission $D$ is the uniform distribution on $I$. Online, $n$ impressions arrive one at a time; their types $\omega(0), \dots, \omega(n-1)$ are independent draws from $D$. When impression $t$ arrives, the algorithm must immediately either assign it to an advertiser $a$ with $(a, \omega(t)) \in E$ that has not yet been used, or leave it unassigned. Each advertiser can be used at most once, and decisions are final.

A deterministic online algorithm decides what to do with arrival $t$ from the types $\omega(0), \dots, \omega(t)$ seen so far; it knows $G$, $D$ and $n$, but not the future. A randomized online algorithm is a probability distribution over deterministic ones. $\mathrm{ALG}(\omega)$ is the number of impressions the algorithm assigns on the arrival sequence $\omega$. $\mathrm{OPT}(\omega)$ is the size of a maximum matching of the realization graph, which has one node per arrival $t$, joined to every advertiser adjacent to $\omega(t)$: the most impressions that could have been assigned with hindsight. The expected approximation factor of an algorithm is

$$\mathbb E\!\left[\frac{\mathrm{ALG}(\omega)}{\mathrm{OPT}(\omega)}\right],$$

the expectation taken over the algorithm's randomness and the arrivals.

The 6-cycle instance has $A = \{a, b, c\}$, $I = \{x, y, z\}$ and $E = \{(x,a),(y,a),(y,b),(z,b),(z,c),(x,c)\}$, with the uniform distribution and $n = 3$. The family $\Gamma_k$ consists of $k$ disjoint copies of the 6-cycle, with the uniform distribution on its $3k$ impression types and $n = 3k$ arrivals.

Formalization targets

Goal: Theorem 3

On the 6-cycle, every randomized online algorithm satisfies

$$\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le \frac{26}{27},$$

and there are a constant $c < 1$ and a threshold $K_0$ such that for every $k \ge K_0$ and every randomized online algorithm on $\Gamma_k$,

$$\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le c .$$

The second part is the paper's "there exists a family of instances with $n \to \infty$ for which no algorithm can achieve an expected approximation of $1 - o(1)$", stated on the paper's own family. It leaves $c$ unspecified: Appendix B estimates $c \approx 0.9898$ through approximate counts, and a sharper constant would not invalidate the goal.

Milestones

1. The $(x, y, y)$ scenario (§3, p. 4). For every deterministic online algorithm on the 6-cycle and every type $u$ of the first arrival there is a type $v$ with $\mathrm{ALG}(u, v, v) \le 2$ and $\mathrm{OPT}(u, v, v) = 3$.
2. Theorem 3, first sentence (p. 4). The bound $26/27$ on the 6-cycle, for every randomized online algorithm.

Significance

Theorem 3 sets the ceiling against which algorithms in the i.i.d. model are measured. It rules out an online algorithm with expected factor arbitrarily close to $1$, even though the distribution is known and the instance is tiny, so a constant-factor gap between online and offline matching is intrinsic to the model and not an artefact of adversarial arrivals. The paper's positive results ($1 - 1/e$ for the Suggested Matching algorithm, $\approx 0.67$ for Two Suggested Matchings) sit between $1 - 1/e$ and this ceiling.

The single-instance bound has a short counting proof. The family statement is argued in the paper only in outline: Appendix B approximates the fractions of copies receiving $1$, $2$, $3$ or more impressions, assumes the most favourable outcome on each, and reports the resulting ratio as approximately $0.9898$. A machine-checked proof of the family statement would turn that sketch into a theorem with an explicit constant. To our knowledge neither part has been formalized before.

Difficulty

The single-cycle bound reduces to a finite check, but the paper's "without loss of generality (from the symmetry of the 6-cycle)" hides the cases the algorithm can choose: assigning the first impression to either neighbour, or not assigning it at all. Each case needs its own bad continuation. The passage from deterministic to randomized algorithms is an averaging step.

The family bound is harder. On $\Gamma_k$ the algorithm sees all arrivals in all copies and may coordinate its decisions across copies, so the per-copy loss of the single cycle does not transfer by independence. Moreover the target is the expectation of a ratio, $\mathbb E[\mathrm{ALG}/\mathrm{OPT}]$, not a ratio of expectations: a bound on the expected loss must be combined with concentration of the number of copies that receive exactly three impressions, and with a lower bound on $\mathrm{OPT}$ that holds with high probability. The approximations "$\simeq 3/e^3$, $9/(2e^3)$, $27/(6e^3)$" of Appendix B have unquantified errors and cannot be used as they stand.

Formalization scope

The model is formalized for general finite $A$ and $I$ with uniform arrivals. Arrival sequences are functions Fin n → I. A deterministic online algorithm is a function that receives the time $t$, the prefix of the first $t$ types (Fin t → I) and the current type, and returns an advertiser or none; it cannot read later arrivals. A proposal of a non-adjacent or already used advertiser leaves the impression unassigned, so the encoding covers all online algorithms, including ones that skip an impression while a neighbour is free. A randomized online algorithm is a probability distribution (PMF) on the finite type of deterministic algorithms; by Kuhn's theorem this is equivalent to fresh random choices at each step. $\mathrm{OPT}$ is the maximum size of an injective, edge-respecting partial assignment of arrivals to advertisers. The expected approximation factor is a finite average over all $|I|^n$ arrival sequences, weighted by the algorithm distribution.

The explicit instantiations of the paper's asymptotic wording are as follows:

• "no algorithm can achieve an expected approximation of $1 - o(1)$" becomes $\exists\, c < 1,\ \exists K_0,\ \forall k \ge K_0,\ \forall P:\ \mathbb E[\mathrm{ALG}/\mathrm{OPT}] \le c$ on $\Gamma_k$, with $n = 3k$ tied to $k$, and with $c$ and $K_0$ chosen before $k$ and before the algorithm.
• The paper's constant $0.9898$ is not part of the statement.

Lean's division sets $x/0 = 0$. A formalization of the form "there is an instance on which every algorithm has expected factor at most $26/27$" would be satisfied trivially by a graph without edges, where $\mathrm{OPT} = 0$; the statements here are on the paper's explicit instances, where every impression type has an adjacent advertiser and $\mathrm{OPT} \ge 1$ on every arrival sequence.

A complete development needs finite case analysis on runs of online algorithms, averaging over mixed strategies, and, for the family, concentration inequalities for occupancy counts (Azuma or McDiarmid, both available on the platform) together with bounds on maximum matchings of disjoint unions. The online-algorithm model and the averaging lemmas are reusable for other lower bounds in the i.i.d. model. Proofs of either milestone, and independent proofs of the family statement with any explicit $c < 1$, are welcome.

Selected references

• J. Feldman, A. Mehta, V. Mirrokni, S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, FOCS 2009; arXiv:0905.4100v1. https://arxiv.org/abs/0905.4100
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
• V. H. Manshadi, S. Oveis Gharan, A. Saberi, Online Stochastic Matching: Online Actions Based on Offline Statistics, SODA 2011; arXiv:1007.1673. https://arxiv.org/abs/1007.1673

Motivation

Single-machine scheduling with precedence constraints asks for an order in which one machine processes jobs while respecting prescribed comparisons between them. For the objective of minimizing total weighted completion time, the structure of the precedence order can influence the quality of approximation algorithms. Ambühl, Mastrolilli, Mutsanas, and Svensson connect one such approach to coloring a graph built from the order's incomparable pairs. A bounded number of colors would make a certain class of coloring-based guarantees uniform over the class of precedence orders. Their Theorem 4.3 shows that canonical interval orders have no such uniform bound for this particular graph. Ambühl et al., §4.2, p. 658

An interval order is a partial order whose elements can be represented by closed real intervals, with one element strictly before another when the first interval ends before the second begins. Interval orders are a familiar restriction of general precedence systems. The paper distinguishes them from semiorders, represented by intervals of equal length, for which it reports a three-element realizer bound and a corresponding scheduling guarantee. The chromatic obstruction here explains why that particular bounded-color route cannot be extended uniformly from semiorders to all interval orders. It does not assert that every scheduling approach to interval orders fails. Ambühl et al., §§3–4.2, pp. 656–658

Setting

For an integer $n\ge2$, let $[n]$ be a linearly ordered set with $n$ points. The canonical interval order $I_n$ has one element for every pair of distinct points $a<b$ in $[n]$, viewed as the closed interval $[a,b]$. For two such intervals, write $S\le_{I_n}T$ when $S=T$ or the right endpoint of $S$ is strictly less than the left endpoint of $T$. Thus intervals that touch at an endpoint remain incomparable. The formalization represents each interval by its two-element endpoint set, and its order relation is equivalent to this endpoint rule. Ambühl et al., §4.2, p. 658

For any partial order $P$ on a ground set $N$, an ordered incomparable pair is $(x,y)$ with neither $x\le_P y$ nor $y\le_P x$. Both $(x,y)$ and $(y,x)$ are vertices when $x$ and $y$ are incomparable. A linear extension of $P$ is a linear order on the same elements that contains all comparisons of $P$. It reverses $(x,y)$ if it places $y$ before $x$. The graph $G_P$ has the ordered incomparable pairs as vertices. Two distinct vertices form an edge when no linear extension reverses both, while each singleton can be reversed by some linear extension. This singleton condition is the minimality clause in the paper's definition through its hypergraph of incomparable pairs. Ambühl et al., §2.1, p. 655, §3, p. 656

A proper $k$-coloring assigns one of $k$ colors to every vertex of $G_P$ so that endpoints of an edge have different colors. The graph's chromatic number $\chi(G_P)$ is the least positive number of colors that works, when the graph is nonempty. The mission uses the equivalent predicate that no proper map into a fixed $k$-element color set exists once $n$ is large enough. This also gives a clear interpretation at $k=0$.

Formalization targets

The goal is Theorem 4.3: for each fixed integer $k$, all sufficiently large canonical interval orders have incomparable-pairs graphs with chromatic number greater than $k$. With $k\ge0$, the Lean target is

$$\forall k\in\mathbb N,\ \exists n_0\ge2,\ \forall n\ge n_0,\quad G_{I_n}\text{ is not $k$-colorable}.$$

The paper states $k$ as an integer. Its negative cases are immediate from nonnegativity of chromatic numbers; the target states the substantive range. The threshold $n_0$ may depend on $k$, while $I_n$ and $G_{I_n}$ are constructed from $n$ rather than supplied as arbitrary objects. Ambühl et al., Theorem 4.3, p. 658

Two assertions from the theorem's proof serve as milestones. First, $\chi(G_{I_n})$ is nondecreasing as $n$ increases. Second, for four endpoints $i<j<\ell<m$, the vertices $(\{i,j\},\{j,\ell\})$ and $(\{j,\ell\},\{\ell,m\})$ are adjacent in $G_{I_n}$. They are recorded with their wording and provenance from §4.2. A separately published theorem on hypergraph Ramsey numbers is included as a reference because the source uses that theorem in its large-$n$ argument. Ambühl et al., proof of Theorem 4.3, p. 658

Significance

The result provides a precise structural limitation: across the canonical interval orders, the chromatic numbers of $G_{I_n}$ cannot be bounded by one constant. The graph $G_P$ is a specific graph of ordered incomparable pairs, distinct from other graphs that can be associated with a scheduling instance. Thus the conclusion addresses the bounded-color approach attached to this graph, without asserting an algorithmic impossibility for interval-order scheduling. The paper contrasts this limitation with the bounded-realizer situation for semiorders. Ambühl et al., §§3–4.2, pp. 656–658

The theorem is proved in the 2011 paper. The remaining work in this mission is a machine-checked development of its definition layer, its two stated supporting assertions, and the unbounded-color conclusion. The partial-order property of $I_n$ is already proved in the definition file; the three theorem statements are open proof targets in the proposal. A completed formalization would also give reusable components for finite interval orders, ordered incomparable pairs, and coloring arguments in dimension theory.

Difficulty

A pair of intervals overlapping or touching is easy to recognize as incomparable, but graph adjacency has a stronger meaning: it quantifies over every linear extension of the entire partial order. A local test based only on the four displayed intervals would silently change the graph. Likewise, the fact that two vertices have different endpoint descriptions does not by itself make them adjacent. The formal argument must connect the canonical interval representation to the global extension-based edge condition, then show that a bounded coloring cannot persist as the endpoint set grows. Ambühl et al., proof of Theorem 4.3, p. 658

Formalization scope

The endpoint set is Fin n, hence indexed $0,\ldots,n-1$ rather than the paper's $1,\ldots,n$; the shift preserves order. Elements of $I_n$ are exactly two-element subsets of this set. The order relation includes equality and strict separation of endpoint sets and is proved to be a partial order. The graph is defined for an arbitrary binary relation so it can be reused, but every target here applies it to the concrete partial order $I_n$. Vertices are ordered incomparable pairs, and adjacency retains both singleton reversibility and failure of simultaneous reversibility. Defining adjacency directly from the desired four-point pattern would trivialize the target and is excluded.

Colorable n k means existence of a proper function from all vertices of $G_{I_n}$ to Fin k. For an empty graph, zero-colorability is allowed by this representation. The theorem therefore includes a threshold $n_0\ge2$ and quantifies over every $n\ge n_0$; the assertion itself forces the threshold past any empty-graph exceptions. The formal target uses natural $k$; the paper's negative integer values need no separate theorem. No asymptotic notation or unspecified constants occur. The source's Ramsey number $R(3:4,\ldots,4)$ is not hard-coded into the goal, because the source asserts existence of a suitable threshold, not that the least threshold equals that value.

The printed adjacency justification names an alternating-cycle pair set different from the two adjacent vertices in the preceding sentence. The milestone formalizes the adjacency assertion itself and records the printed explanation verbatim for review; it does not turn the mismatched pair set into a hypothesis. The mission needs finite order embeddings, linear extensions, graph colorings, and a finite Ramsey theorem. The existing published Ramsey theorem is referenced as a reusable result. No scheduling approximation algorithm, polynomial-time statement, or numerical scheduling guarantee is formalized in this mission.

Selected references

• Christoph Ambühl, Monaldo Mastrolilli, Nikolaos Mutsanas, and Ola Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4), 653–669, 2011. DOI: 10.1287/moor.1110.0512

Motivation

Single-machine scheduling with precedence constraints, written $1|\mathrm{prec}|\sum w_jC_j$ in the notation of Graham et al., asks for an order of $n$ weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph built from the precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain $(2-2/f)$-approximations for orders of fractional dimension at most $f$. This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.

Setting

An instance $S$ consists of a finite set $N$ of jobs, a partial order $P$ on $N$ (reflexive, antisymmetric, transitive; $(i,j)\in P$ with $i\ne j$ means job $i$ finishes before job $j$ starts), processing times $p_j\ge 0$ and weights $w_j\ge 0$.

Two jobs $x,y$ are incomparable, $x\parallel y$, when neither $(x,y)$ nor $(y,x)$ lies in $P$. The set $\operatorname{inc}(P)$ of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of $P$ is a linear order $L\supseteq P$ on $N$; it reverses $(x,y)\in\operatorname{inc}(P)$ when $y<x$ in $L$. A nonempty multiset $L_1,\dots,L_t$ of linear extensions is a $k:t$-realizer if every incomparable pair is reversed by at least $k$ of them. The fractional dimension $\operatorname{fdim}(P)$ is the least ratio $t/k$ over all $k:t$-realizers.

The vertex cover graph $G^S_P$ has the incomparable pairs as nodes; nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell),(k,j)\in P$ (symmetrically closed). Node $(i,j)$ has weight $w_{(i,j)}=p_iw_j$, and $w(C)=\sum_{u\in C}w_u$. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$. The LP relaxation [CS-LP] asks for $x\in[0,1]^{\operatorname{inc}(P)}$ with $x_u+x_v\ge1$ on every edge, minimizing $\sum_u w_ux_u$. For a solution $x$ write $V_a=\{u: x_u=a\}$, and for a linear extension $L$ let $I_{1/2}(L)$ be the pairs of $V_{1/2}$ reversed in $L$.

The graph of incomparable pairs $G_P$ (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.

Formalization targets

Goal: Theorem 5.1 (p. 658)

For an instance $S$, a $k:t$-realizer $L_1,\dots,L_t$ of $P$, and a half-integral optimal solution $x$ of [CS-LP], put $C_i=V_1\cup\bigl(V_{1/2}\setminus I_{1/2}(L_i)\bigr)$. Then every $C_i$ is a vertex cover of $G^S_P$, and

$$\frac1t\sum_{i=1}^t w(C_i)\;\le\;\Bigl(2-\frac{2}{t/k}\Bigr)\mathrm{OPT}.$$

Milestones

• Proposition 3.2 (p. 657): $G^S_P=G_P$.
• Footnote 4 (p. 659): the pairs reversed by a linear extension are independent in $G^S_P$.
• Eq. (4): $\frac1t|\{i: L_i\text{ reverses }u\}|\ge k/t$ for every incomparable pair $u$.
• Eq. (5): $\frac1t\sum_i w(I_{1/2}(L_i))\ge \frac kt\,w(V_{1/2})$.
• Hochbaum's observation (§5, p. 659): for half-integral feasible $x$, $V_1\cup C$ covers $G^S_P$ whenever $C$ covers $G^S_P[V_{1/2}]$.
• Eqs. (6)–(8): $\frac1t\sum_iw(C_i)\le w(V_1)+(1-\frac kt)w(V_{1/2})\le 2(1-\frac kt)(w(V_1)+\frac12w(V_{1/2}))\le(2-\frac2{t/k})\mathrm{OPT}$ when $P$ is not a linear order.

Significance

The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an $\alpha$-approximate vertex cover of $G^S_P$ into an $\alpha$-approximate schedule, Theorem 5.1 gives a $(2-2/f)$-approximation for $1|\mathrm{prec}|\sum w_jC_j$ whenever the precedence order has an efficiently samplable realizer with $t/k\le f$. The paper applies it to interval orders ($3/2$), convex bipartite orders and semiorders ($4/3$), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, $k$-fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.

Difficulty

Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion $G_P\subseteq G^S_P$ in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of $P$ by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality $t\ge 2k$ used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of $(x,y)$ and $(y,x)$.

Formalization scope

• Jobs form a finite type N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.
• $\operatorname{inc}(P)$ is the subtype IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a $k:t$-realizer is a family Fin t → LinearExtension P with $t>0$. Reversal of $(x,y)$ means $y<x$ in $L$ throughout; the page's "$y>x$" in Eq. (4) and "$\mathrm{Prob}[j>i]$" in Eq. (5) are the same family of inequalities because $\operatorname{inc}(P)$ is symmetric.
• $G^S_P$ is the symmetric closure of the printed three-case rule on distinct nodes. $G_P$ is defined through linear extensions and hyperedge minimality, never through the three-case rule, so Proposition 3.2 is a genuine statement and not a definitional equality.
• [CS-LP] drops the constant term $\sum_jp_jw_j+\sum_{(i,j)\in P}p_iw_j$ of [CS-IP], which does not affect optimality. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$, taken over a finite nonempty family.
• Not formalized: "efficiently samplable", "polynomial time" and "randomized algorithm". The expectation over a uniformly sampled $L_i$ is stated as the average $\frac1t\sum_{i=1}^t$, which is equivalent to it and stronger than the existence of one good index. The existence of a half-integral optimal [CS-LP] solution (Nemhauser–Trotter, cited) is a hypothesis on $x$. The conversion of a vertex cover into a schedule (Theorem 2.1, cited) is not formalized; the goal is stated for vertex covers of $G^S_P$.
• Constants: $2-2/(t/k)$ in real arithmetic; it equals $2-2k/t$, and equals $2$ when $k=0$.
• The paper assumes $\operatorname{fdim}(P)\ge2$, i.e. $P$ is not a linear order. Eqs. (6)–(8) carry that hypothesis as the paper does; the goal omits it because for a linear order both sides are $0$.
• Conclusion (a), that each $C_i$ is a vertex cover, is part of the goal and is not assumed.

Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the approximability of single-machine scheduling with precedence constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4), 2009 (reference [2] of the paper).
• J. R. Correa, A. S. Schulz, Single-machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992 (reference [7]).
• S. Felsner, W. T. Trotter, Dimension, graph and hypergraph coloring, Order 17(2):167–177, 2000 (reference [13]).
• D. S. Hochbaum, Efficient bounds for the stable set, vertex cover and set packing problems, Discrete Appl. Math. 6(3):243–254, 1983 (reference [20]).
• G. L. Nemhauser, L. E. Trotter, Vertex packings: structural properties and algorithms, Math. Programming 8(1):232–248, 1975 (reference [29]).