Operations Research

Motivation

In stochastic linear optimization under bandit feedback a learner repeatedly chooses a point $x_t$ from a compact decision set $D\subset\mathbb R^n$ and observes only the random cost $\ell_t$ of that point, whose mean is $\mu\cdot x_t$ for an unknown vector $\mu$. The problem models online routing, ad placement and other sequential decisions with linearly structured costs. The quality of a learner is measured by its regret against the best fixed decision.

For the $K$-armed bandit the achievable regret for a fixed instance is logarithmic in the horizon $T$ (Lai and Robbins 1985; Auer, Cesa-Bianchi and Fischer 2002). Dani, Hayes and Kakade (COLT 2008) showed that for linear costs the picture depends on the geometry of $D$. Their Theorem 1 gives polylogarithmic regret when the decision set has a positive gap between the best and second-best extreme point (a polytope, for instance), and their Theorem 2 gives $O^*(n\sqrt T)$ regret for every decision set. Their Theorem 3 shows that the second rate cannot be improved in general: on a decision set with zero gap, every algorithm pays $\Omega(\sqrt T)$ in expectation.

Timeline:

• 2002: Auer, Using confidence bounds for exploitation–exploration trade-offs (JMLR 3), introduces confidence-bound algorithms for linear bandits on finite decision sets.
• 2008: Dani, Hayes and Kakade prove the $O^*(n\sqrt T)$ upper bound for ConfidenceBall₂ and the $\Omega(\sqrt T)$ lower bound on a product of circles, the subject of this mission. A hypercube lower bound for the adversarial setting appears in their NIPS 2007 paper.
• 2010: Rusmevichientong and Tsitsiklis, Linearly parameterized bandits (Math. OR 35), give $\Omega(n\sqrt T)$ lower bounds on the unit sphere.
• 2020: Lattimore and Szepesvári, Bandit Algorithms, Theorems 24.1 and 24.2, give minimax lower bounds on the hypercube and the unit ball with Gaussian noise.

Setting

The decision set is the unit circle $D_2=S^1=\{x\in\mathbb R^2: x_1^2+x_2^2=1\}$. An unknown mean vector $\mu\in\mathbb R^2$ is drawn once, uniformly from the circle $D_2/2$ of radius $1/2$; concretely $\mu=\mu(\theta)=\tfrac12(\cos\theta,\sin\theta)$ with $\theta$ uniform on $[0,2\pi)$.

On each round $t=1,\dots,T$ the algorithm plays $x_t\in D_2$ and observes a cost $\ell_t\in\{-1,+1\}$ with $\Pr(\ell_t=+1)=(1+\mu\cdot x_t)/2$, so that $\mathbb E[\ell_t]=\mu\cdot x_t$. Given the decision, the cost is independent of the past.

An algorithm may be randomised. It draws a seed $s$ once from a probability measure $\rho$ on a measurable space $S$, and chooses $x_t$ as a function of $s$ and the costs $\ell_1,\dots,\ell_{t-1}$ observed so far, measurably in $s$.

The regret over $T$ rounds is

$$R=\sum_{t=1}^T(\mu\cdot x_t-\mu\cdot x^*),\qquad \mu\cdot x^*=\min_{x\in D_2}\mu\cdot x,$$

so each round costs $r_t=\mu\cdot x_t+\tfrac12\ge0$ when $\|\mu\|=1/2$. The expected regret $\mathbb E R=\mathbb E_\mu\,\mathbb E(R\mid\mu)$ averages over the seed, the prior and the costs.

In the Lean development these objects are unitCircle, meanVec, optCost, RandomizedPolicy and expectedRegret in the namespace StochLinOpt.LowerBound.

Formalization targets

Goal: Theorem 3 for $n=2$

There is a universal constant $c>0$ such that for every randomised algorithm and every $T\ge1$,

$$\mathbb E R\ \ge\ c\sqrt T.$$

The constant is left existential, which is the form that survives any later improvement of the constant; it is chosen before the algorithm and before $T$.

Milestones

1. Section 6.1, Eq. (3). For $\|\mu_1\|=\|\mu_2\|=1/2$, $x\in S^1$, a posterior probability $p\in[0,1]$ of $\mu=\mu_1$ and a cost $\ell\in\{\pm1\}$, the Bayes-updated bias $b_{t+1}$ satisfies $|b_{t+1}-b_t|\le|(\mu_1-\mu_2)\cdot x|$, where $b_t=2p-1$.
2. Lemma 15. With $\varepsilon=\|\mu_1-\mu_2\|>0$ and the same data,

$$\mathbb E_\mu(r_t\mid\mathcal H_t)\ge\frac1{16}\Big(\varepsilon^2+\frac{|b_{t+1}-b_t|^2}{\varepsilon^2}\Big)\mathbf 1\{|b_t|\le1/2\}.$$

3. Theorem 4 (Freedman). For a martingale difference sequence $X_1,\dots,X_T$ bounded above by $b$, with conditional variance sum $V$, and all $a,v>0$,

$$\Pr\Big(\sum_i X_i\ge a,\ V\le v\Big)\le\exp\Big(\frac{-a^2}{2v+2ab/3}\Big).$$

Significance

The lower bound shows that the $\sqrt T$ dependence of the problem-independent upper bound (Theorem 2 of the same paper) is necessary. It also shows that the gap-dependent polylogarithmic rate of Theorem 1 cannot extend to decision sets without a gap, such as the sphere. Together with the upper bound it characterises the minimax regret of stochastic linear bandits in $T$ up to logarithmic factors, and in the paper's general-$n$ form it also underlies the claim that the price of bandit information is $\Theta^*(\sqrt n)$.

The result is proved in the paper for $n=2$ and has not been machine-checked. The mission produces a checked Bayesian lower bound over all randomised algorithms, with an explicit probability model for the protocol. Two related platform results are different theorems: BanditAlgorithm.linear_bandit_unit_ball_minimax_lower_bound (Lattimore–Szepesvári Theorem 24.2: unit ball, Gaussian noise, a worst-case $\mu$) and BanditAlgorithm.linear_bandit_hypercube_minimax_lower_bound (Theorem 24.1: hypercube). The $\{-1,+1\}$ costs, the circle and the uniform prior used here are not covered by either.

Difficulty

The obvious attempt is a two-point change-of-measure argument with a fixed pair of means at distance $\varepsilon$. It fails as stated because the decision set has no gap: an algorithm that plays close to the optimum of both candidates learns slowly but also pays little. The per-round trade-off between regret and information (Lemma 15) is exact only while the posterior is undecided, $|b_t|\le1/2$. Turning it into a bound on the whole horizon requires controlling how long the posterior stays undecided, which is a statement about a martingale whose step sizes are chosen by the algorithm; a concentration bound that ignores the accumulated conditional variance (Azuma–Hoeffding with worst-case steps) is too weak for this. The averaging step from a two-point prior to the uniform prior on the circle is also part of the formal work.

Formalization scope

Vectors are Fin 2 → ℝ with the dot product ⬝ᵥ; Euclidean norms are written through dot products, never with Lean's sup norm. Rounds are 0-indexed internally: the Lean index $t$ is the paper's round $t+1$. The expected regret is the exact finite expectation

$$\mathbb E R=\int_S\frac1{2\pi}\int_0^{2\pi}\sum_{\ell\in\{\pm1\}^T}\prod_{t=1}^T\frac{1+\ell_t\,\mu(\theta)\cdot x_t}{2}\;R\;d\theta\,d\rho(s),$$

so no infinite product of measures is needed. A randomised algorithm is a seeded policy, which covers every randomised algorithm. The optimal cost is the infimum of $\mu\cdot x$ over the compact circle and is attained. Every junk value in the model (a non-integrable integrand) could only make the lower bound harder to prove, never easier.

A statement over deterministic algorithms only, over a worst-case $\mu$ instead of the uniform prior, or with the constant allowed to depend on the algorithm or on $T$ would be a weaker theorem. The goal quantifies $\exists c>0$ before the algorithm and $T$, and fixes the prior.

Corrections relative to the printed paper:

• General $n$ is not stated. Theorem 3 as printed claims $\mathbb E R\ge\frac1{10}n\sqrt T$ for every even $n$. It is false for $n>10$: on $D_n$ with $\mu\in D_n/n$ each round has regret at most $1$, so at $T=1$ the claim would need $\mathbb E R\ge n/10>1$. The general case rests on Lemma 16, which has no proof. The goal is the $n=2$ case, which Section 6.1 proves.
• The constant. For $n=2$ the paper prints $\frac15\sqrt T$; its proof gives $c=\frac1{16}\min(\frac12-\frac1e,\frac1{64})=\frac1{1024}$. The proof's Freedman step prints $2\exp(-\frac{1/4}{1/8+\varepsilon/3})\le 2/e^2$; with $v=1/32$ the denominator is $1/16+\varepsilon/3$, and the bound $2/e^2$ then needs $\varepsilon=T^{-1/4}\le3/16$. Small $T$ is covered by the first round, whose expected regret is $1/2$. The goal leaves $c$ existential.
• Theorem 4. The printed variance sum runs to $n$; it runs to $T$. The conditioning is on a general filtration, and square-integrability of the steps is assumed so that the conditional variance is defined.
• Lemma 15. Its right side depends on the round-$t$ cost $\ell_t$, which is not part of $\mathcal H_t$; the Lean statement holds for either value of $\ell_t$.

Welcome contributions: a Lean proof of Freedman's inequality (reusable across the bandit and concentration missions on the platform); the averaging argument from two-point priors to the uniform prior; and the stopped-martingale bookkeeping for the bias sequence.

Selected references

• Varsha Dani, Thomas P. Hayes, Sham M. Kakade, Stochastic Linear Optimization under Bandit Feedback, Proceedings of the 21st Annual Conference on Learning Theory (COLT), 2008.
• David A. Freedman, On tail probabilities for martingales, The Annals of Probability 3(1):100–118, 1975. https://doi.org/10.1214/aop/1176996452
• Colin McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998. https://doi.org/10.1007/978-3-662-12788-9_6
• Peter Auer, Using confidence bounds for exploitation–exploration trade-offs, JMLR 3:397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• Paat Rusmevichientong, John N. Tsitsiklis, Linearly parameterized bandits, Mathematics of Operations Research 35(2):395–411, 2010. https://doi.org/10.1287/moor.1100.0446
• Tor Lattimore, Csaba Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 24. https://doi.org/10.1017/9781108571401

Motivation

Many combinatorial optimization problems are linear programs over a polytope whose vertices are the zero–one incidence vectors of the feasible objects: matchings, stable sets, spanning trees. The edges of such a polytope (pairs of vertices joined by a one-dimensional face) govern the behaviour of the simplex method and of local-search procedures, which move from vertex to vertex along edges: a pivot of the simplex method on a nondegenerate basis replaces a vertex by one of its neighbours.

In December 1971 M. L. Balinski asked when two matchings $M_1, M_2$ of a graph are neighbours on the matching polyhedron determined by Edmonds (Edmonds 1965). V. Chvátal answered a more general question in §6 of On certain polytopes associated with graphs (Chvátal 1975): he characterized the neighbours on the stable set polytope of an arbitrary graph. Since matchings of $G$ are the stable sets of the line graph $L(G)$, Balinski's question is the special case of line graphs (Corollary 6.3 of the paper).

Setting

Let $G=(V,E)$ be a finite undirected loopless graph. A stable set is a set of vertices no two of which are adjacent. $S(G)$ denotes the set of all zero–one vectors $x=(x_u : u\in V)$ such that $\{u : x_u=1\}$ is stable, and the stable set polytope is

$$P(G)=\operatorname{conv} S(G)\subseteq \mathbb R^V .$$

For $y\in S(G)$ the corresponding stable set is $Y=\{u : y_u=1\}$.

For an integer-valued vector $c=(c_u : u\in V)$ write $cx=\sum_{u\in V}c_ux_u$. Two vectors $y, z$ are neighbours in $P(G)$ if there is an integer-valued $c$ such that $y$ and $z$ are the only two vectors which maximize $cx$ over $S(G)$; in particular $y\neq z$. This is the definition the paper states at the start of the proof of Theorem 6.2.

A bicoloration of a graph $T$ is a partition $V=B\cup R$, $B\cap R=\emptyset$, such that every edge joins $B$ to $R$. Every tree has one.

In the Lean development these objects are stableVectors G ($S(G)$), stablePolytope G ($P(G)$), onesSet y ($Y$), AreNeighbors G y z and IsBicoloration T B R, all in the namespace ChvatalPolytopes.Neighbors.

Formalization targets

Goal: Theorem 6.2 (p. 149)

For $y,z\in S(G)$ with corresponding stable sets $Y,Z$,

$$y \text{ and } z \text{ are neighbours in } P(G) \iff \text{the subgraph } H \text{ of } G \text{ induced by } (Y-Z)\cup(Z-Y) \text{ is connected.}$$

Milestone: Lemma 6.1 (p. 149)

For a tree $T=(V,E)$ with a bicoloration $V=B\cup R$ there are nonnegative integers $c_u$ ($u\in V$) and $m$ with

$$\sum_{u\in V}c_ux_u\le m\quad\text{for all } x\in S(T),$$

with equality exactly when $x$ is the incidence vector of $B$ or of $R$.

Milestone: the certificate of the "if" part (p. 149, proof of Theorem 6.2, (i))

If $H$ is connected with spanning tree $T$, and $c_u$ ($u\in (Y-Z)\cup(Z-Y)$), $m$ are as in Lemma 6.1 for $T$, extend $c$ by $c_u=1$ on $Y\cap Z$ and $c_u=-1$ outside $Y\cup Z$. Then

$$\sum_{u\in V}c_ux_u\le m+|Y\cap Z|\quad\text{for all } x\in S(G),$$

with equality if and only if $x=y$ or $x=z$.

Significance

Theorem 6.2 describes the 1-skeleton of the stable set polytope of every graph by a condition that can be checked in linear time, although optimizing over $P(G)$ is NP-hard in general and no complete linear description of $P(G)$ is known for general graphs. Through line graphs it gives the adjacency criterion for the matching polytope (two matchings are neighbours if and only if their symmetric difference is a single path or cycle), which settled Balinski's question. Characterizations of this type underlie the analysis of simplex-type and pivoting algorithms on combinatorial polytopes and the study of their diameters.

The result has been proved since 1975. The mission asks for a machine-checked proof of the theorem as stated in the paper; no formal proof of Theorem 6.2 or of the matching-polytope corollary is known to exist on Prove2Me or in Mathlib. The two milestones isolate the constructive half (Lemma 6.1 and the weighting built from it), which is reusable for any statement that needs an explicit objective singling out two stable sets.

Difficulty

The "only if" direction and the equality analysis are elementary; the substance lies in the "if" direction. An objective that makes both $y$ and $z$ optimal is easy to write down, for example $c=y+z$; the difficulty is to make them the only optimal vectors. Any stable set that agrees with $Y$ on some connected pieces of $H$ and with $Z$ on others ties with $y$ and $z$ under naive weightings, so the weights on $(Y-Z)\cup(Z-Y)$ must be chosen so that every mixed choice loses strictly. The integrality requirement on $c$ and the need to control all of $S(G)$, not only the stable sets contained in $Y\cup Z$, rule out a direct perturbation argument.

Formalization scope

• Graphs. $V$ is a finite type with decidable equality and $G$ is a SimpleGraph V; loops and multiple edges are excluded, as in the paper.
• $S(G)$ and $P(G)$. $S(G)$ is the set of incidence vectors in V → ℝ of stable finsets; $P(G)$ is convexHull ℝ (S G).
• Neighbours. Defined exactly as on p. 149: $y\ne z$ and, for some $c : V\to\mathbb Z$, the set of maximizers of $cx$ over $S(G)$ equals $\{y,z\}$. The face-lattice notion of an edge of $P(G)$ is not used; its equivalence with this definition is not part of the paper.
• Induced subgraph and connectedness. $H$ is G.induce of the set $(Y\setminus Z)\cup(Z\setminus Y)$, and "connected" is Mathlib's SimpleGraph.Connected, which requires at least one vertex. For $y=z$ both sides of the goal are therefore false.
• Trees. SimpleGraph.IsTree, which includes connectedness; a spanning tree of $H$ is a graph $T$ on the vertex set of $H$ with $T\le H$ and T.IsTree. In Lemma 6.1 the integers $c_u$ and $m$ are natural numbers.

A trivializing formalization — defining neighbours through the symmetric-difference condition or through Lemma 6.1's certificate, or omitting $y\neq z$ from the definition — is excluded: neighbours are defined only through unique maximizers of integer objectives over $S(G)$.

A complete development needs only finite graphs, induced subgraphs, spanning trees of connected graphs (available in Mathlib) and finite sums. Contributions welcome beyond the milestones: the equivalence of this notion of neighbours with the one-dimensional faces of $P(G)$, and Corollary 6.3 for the matching polytope via line graphs.

Selected references

• V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory, Series B 18 (1975), 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
• M. W. Padberg, On the facial structure of set packing polyhedra, Mathematical Programming 5 (1973), 199–215. https://doi.org/10.1007/BF01580121

Motivation

The stability number $\alpha(G)$ of a graph, the largest number of pairwise non-adjacent vertices, is the optimum of an integer program over the stable set polytope $P(G)$. Linear programming duality turns any explicit linear description of $P(G)$ into a certificate of optimality for $\alpha(G)$, which is why the question "which inequalities are needed to describe $P(G)$?" has been central to polyhedral combinatorics since Edmonds' description of the matching polytope (Edmonds 1965). Chvátal's 1975 paper (doi:10.1016/0095-8956(75)90041-6) initiated the systematic study of $P(G)$ for arbitrary graphs: which graph operations preserve a known description, and which inequalities are facets, i.e. indispensable in every description.

Section 4 of the paper treats one such operation, gluing two graphs along a complete subgraph, and one family of facets, the "rank" inequality $\sum_u x_u\le\alpha(G)$ for graphs whose critical edges connect all vertices. Combining the two yields a purely graph-theoretic fact about $\alpha$-critical graphs (graphs in which deleting any edge increases the stability number): no complete subgraph separates such a graph. The fact is due to Berge (Graphes et hypergraphes, 1970, Ch. 13, §3, Corollary 2); Chvátal's derivation obtains it from polyhedral arguments. $\alpha$-critical graphs were studied by Erdős and Gallai, Hajnal, Andrásfai and Lovász, and their structure is closely tied to the facets of $P(G)$.

Setting

Graphs are finite, undirected and loopless: $G=(V,E)$. A stable set is a set of pairwise non-adjacent vertices; $\alpha(G)$ is the largest size of a stable set. The incidence vector of $s\subseteq V$ is $\chi^s\in\mathbb R^V$ with $\chi^s_u=1$ for $u\in s$ and $0$ otherwise. $S(G)$ is the set of incidence vectors of stable sets and

$$P(G)=\operatorname{conv}S(G)\subseteq\mathbb R^V .$$

A finite system $\sum_{u\in V}a_{iu}x_u\le b_i$ $(i\in J)$ is a defining linear system of $P$ if its solution set is exactly $P$. An inequality $\sum_u a_ux_u\le b$ is a facet of $P$ if every defining linear system of $P$ contains, for some $t>0$, the inequality $\sum_u ta_ux_u\le tb$.

An edge $e$ of $G$ is critical if $\alpha(G-e)=\alpha(G)+1$; $E^*$ denotes the set of critical edges, $G^*=(V,E^*)$, and $G$ is $\alpha$-critical if every edge is critical. For graphs $G_1=(V_1,E_1)$, $G_2=(V_2,E_2)$ put $G_1\cap G_2=(V_1\cap V_2,E_1\cap E_2)$ and $G_1\cup G_2=(V_1\cup V_2,E_1\cup E_2)$. A vertex set $K$ is a cutset of $G$ if two vertices outside $K$ are joined by no path of $G-K$, the subgraph induced on $V\setminus K$.

In Lean, all objects live in the namespace ChvatalPolytopes.Separation: stablePolytope G, IsFacet P a b, IsCriticalEdge, criticalGraph G (for $G^*$), IsAlphaCritical G and IsCutset G K.

Formalization targets

Goal: Corollary 4.3 (p. 144)

For a finite connected $\alpha$-critical graph $G$ and any $K\subseteq V$ inducing a complete subgraph,

$$K \text{ is not a cutset of } G .$$

The goal is pure graph theory; its proof in the paper consists of the two polyhedral theorems below.

Milestones

1. Proposition 2.1 (pp. 139–140). For a finite nonempty set $S$ of solutions of $-x_u\le0$ $(u\in V)$, $\sum_u a_{iu}x_u\le b_i$ $(i\in J)$: the solution set equals $\operatorname{conv}S$ if and only if for every $c\in\mathbb Z^V$

$$\max\{cx:x\in S\}=\min\Big\{\sum_i\lambda_ib_i:\lambda\ge0,\ \sum_i\lambda_ia_{iu}\ge c_u\ (u\in V)\Big\}.$$

2. Theorem 4.1 (p. 141). If $G_1\cap G_2$ is complete, the union of defining linear systems of $P(G_1)$ and $P(G_2)$ (each containing its nonnegativity rows) is a defining linear system of $P(G_1\cup G_2)$.
3. Theorem 4.2 (p. 143). If $G^*$ is connected, then

$$\sum_{u\in V}x_u\le\alpha(G)$$

is a facet of $P(G)$.

Significance

Theorem 4.1 says that clique-sums are harmless for linear descriptions of $P(G)$: a description of a graph glued along a clique is the union of descriptions of the pieces. It underlies the later decomposition theory of stable set polytopes (clique cutsets appear throughout the study of perfect and $t$-perfect graphs). Theorem 4.2 supplies a large class of facets with a combinatorial certificate, and was the starting point of the study of rank facets. Corollary 4.3 illustrates how polyhedral statements yield structural graph theory: the facet in Theorem 4.2 cannot coexist with a clique cutset.

All three results are proved in the paper, and Berge's corollary was known before it. None of them has, to the knowledge of this mission, a machine-checked proof; Mathlib has stable sets (IsIndepSet, indepNum), cliques and convex hulls, but no stable set polytope, no notion of facet via defining systems, and no $\alpha$-critical graphs. The mission produces these definitions and the formal proofs of Proposition 2.1, Theorems 4.1, 4.2 and Corollary 4.3.

Difficulty

Proposition 2.1 requires LP duality in the form "min = max with both optima attained" together with a separation argument that reduces arbitrary objectives to integral ones; the "if" direction fails without the nonnegativity rows, so the statement is sensitive to the exact form of the system. In Theorem 4.1 the inclusion $P(G_1\cup G_2)\subseteq$ (solutions of the union) is routine; the difficulty is the converse: a point whose restrictions lie in $P(G_1)$ and in $P(G_2)$ is a convex combination of stable sets on each side, and the two combinations have to be matched on the clique $V_1\cap V_2$ to produce stable sets of $G_1\cup G_2$. Theorem 4.2 concerns every defining linear system, so it cannot be proved by exhibiting one description; the natural route via "affinely independent tight points" is a different definition of facet and needs full-dimensionality of $P(G)$ to be equivalent. Finally, the goal requires translating a cutset into a decomposition $G=G_1\cup G_2$ with complete intersection, and then showing that a union of two systems on smaller vertex sets cannot contain a positive multiple of $\sum_{u\in V}x_u\le\alpha(G)$.

Formalization scope

• Graphs are SimpleGraph V on a Fintype V with DecidableEq V. $S(G)$ is a set of functions V → ℝ (incidence vectors of stable finsets), and $P(G)$ is convexHull ℝ (stableVectors G).
• Linear systems are indexed by finite types with real coefficients. "Defining linear system" is equality of the solution set with the polytope. IsFacet quantifies over all finite index types J : Type and all real systems whose solution set equals the polytope; it is the paper's definition, not the affinely-independent-points characterization.
• Proposition 2.1: "min = max" means an attained minimum equal to the maximum; the hypothesis $S\neq\emptyset$ is added (the paper's $\max$ over $S$ needs it), and the nonnegativity rows are kept.
• Theorem 4.1: the glued graph $G$ lives on a type $V$ with finsets $V_1\cup V_2=V$; $G_1,G_2$ are the induced subgraphs on $V_1,V_2$; "$G_1\cap G_2$ complete" is encoded as "$V_1\cap V_2$ is a clique of $G$ and no edge joins $V_1-V_2$ to $V_2-V_1$", which is equivalent to the paper's hypotheses. The rows of each system are evaluated on the restriction of $x$.
• Theorem 4.2: "$G^*$ connected" is Mathlib's Connected, which requires $V\neq\emptyset$ — for $V=\emptyset$ the statement would be false. $\alpha(G)$ is indepNum, cast to $\mathbb R$.
• Corollary 4.3: "complete subgraph" is any clique set G.IsClique K, not only maximal cliques (the paper reserves "clique" for maximal complete subgraphs, but the corollary speaks of complete subgraphs), including $K=\emptyset$. "Cutset" means two vertices outside $K$ joined by no path of $G-K$. The formalization "$G-K$ is not connected" is ruled out: under Mathlib's convention it would make $K=V$ a cutset and the statement false for $K_1$ and $K_2$.
• Reusable infrastructure: the stable set polytope, facets via defining systems, Proposition 2.1 (shared with the other missions of this series), critical edges and $\alpha$-critical graphs. Contributions of intermediate lemmas (LP duality in the attained form, full-dimensionality of $P(G)$, the cutset–decomposition equivalence) are welcome.

Selected references

• V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• C. Berge, Graphes et hypergraphes, Dunod, Paris, 1970 (English translation: Graphs and Hypergraphs, North-Holland, 1973), Chapter 13, §3.
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
• M. W. Padberg, On the facial structure of set packing polyhedra, Math. Programming 5 (1973) 199–215. https://doi.org/10.1007/BF01580121
• L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4

Motivation

Many combinatorial optimization problems ask for the best subset of a finite set subject to combinatorial side conditions. The polyhedral method replaces the finite family of feasible subsets by the convex hull of their incidence vectors and asks for an explicit system of linear inequalities describing that convex hull; once such a system is known, linear programming duality gives min–max theorems and certificates of optimality. The maximum weight stable set problem is the central test case: it is NP-hard in general, so no tractable complete description of its polytope is expected for all graphs, and the question becomes for which graphs a simple description suffices.

V. Chvátal's 1975 paper On certain polytopes associated with graphs answers this question for the two simplest families of valid inequalities, and its Section 3 connects the answer to Berge's perfect graphs. The result is a standard entry point to polyhedral combinatorics and is one of the ingredients behind the later polynomial-time algorithms for stable sets in perfect graphs by Grötschel, Lovász and Schrijver.

Timeline. Berge (1961) introduced perfect graphs and conjectured that a graph is perfect if and only if its complement is. Lovász (Normal hypergraphs and the perfect graph conjecture, Discrete Math. 1972; A characterization of perfect graphs, J. Combin. Theory Ser. B 1972) proved this, together with the characterization of perfection by $\alpha(G_A)\,\omega(G_A)\ge|A|$ and the invariance of perfection under vertex duplication. Fulkerson's theory of antiblocking polyhedra (1971–72) gave a polyhedral route to the same equivalence. Chvátal (received 1972, published 1975) gave the self-contained polyhedral statement formalized here, with a proof based on Lovász's two theorems.

Setting

A graph $G=(V,E)$ is finite, undirected and loopless. A stable set is a set of vertices no two of which are adjacent. A clique is a maximal complete subgraph, and $C(G)$ is the set of vertex sets $W\subseteq V$ of the cliques of $G$.

$S(G)\subseteq\mathbb R^V$ is the set of zero–one vectors $x=(x_u:u\in V)$ such that $\{u:x_u=1\}$ is stable, and the stable set polytope is $P(G)=\operatorname{conv}S(G)$. A finite system of linear inequalities is a defining linear system of $P(G)$ if its solution set is exactly $P(G)$. For $c\in\mathbb R^V$ write $cx=\sum_{u\in V}c_ux_u$.

$G$ is perfect (the paper's $\alpha$-perfect) if for every zero–one vector $c$,

$$\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\ \lambda_W\in\{0,1\},\ \sum_{W\in C(G),\,u\in W}\lambda_W\ge c_u\ (u\in V)\Big\}.$$

For $A\subseteq V$, $G_A$ is the induced subgraph, $\alpha(G_A)$ its stability number and $\omega(G_A)$ its clique number. To duplicate a vertex $u$ is to add a new vertex $u'$ adjacent to all neighbours of $u$ but not to $u$.

In the Lean development these are stableVectors G, stablePolytope G, maximalCliques G, IsPerfect G and duplicate G u in the namespace ChvatalPolytopes.Perfect.

Formalization targets

Goal: Theorem 3.1 (p. 140)

For every graph $G$, the system

$$-x_u\le0\quad(u\in V),\qquad\sum_{u\in W}x_u\le1\quad(W\in C(G))$$

is a defining linear system of $P(G)$ if and only if $G$ is perfect. Both directions are required.

Milestones

1. Proposition 2.1 (pp. 139–140). For a finite nonempty set $S$ of solutions of $-x_u\le0$, $\sum_u a_{iu}x_u\le b_i$ $(i\in J)$, the solution set equals $\operatorname{conv}S$ if and only if for every $c\in\mathbb Z^V$

$$\max\{cx:x\in S\}=\min\Big\{\sum_i\lambda_ib_i:\lambda\ge0,\ \sum_i\lambda_ia_{iu}\ge c_u\ (u\in V)\Big\}.$$

2. Lovász's first theorem (§3, p. 140). Every nonperfect $G$ has $A\subseteq V$ with $\alpha(G_A)\,\omega(G_A)<|A|$.
3. Lovász's second theorem (§3, p. 140). Duplicating a vertex of a perfect graph gives a perfect graph.
4. Condition (iii) (p. 141). $G$ is perfect if and only if for every $c\in\mathbb Z^V$

$$\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\lambda_W\ge0,\ \sum_{W\ni u}\lambda_W\ge c_u\ (u\in V)\Big\}.$$

Significance

The result. The nonnegativity and clique inequalities are valid for $P(G)$ for every graph. Theorem 3.1 says they are complete exactly for perfect graphs, so on perfect graphs the maximum weight stable set problem is a linear program over an explicitly described polytope, and weighted min–max theorems (stable sets versus clique covers) follow from LP duality. Combined with the perfect graph theorem, it gives a polyhedral characterization of perfect graphs, and it is the model for later results that identify graph classes by the facets of their stable set polytopes (odd-cycle inequalities, $t$-perfection, Section 7 of the same paper).

Formalizing it. The result is classical and proved. No machine-checked version of it is known, and Mathlib has neither perfect graphs nor stable set polytopes. The mission produces a formal statement of the polyhedral characterization with the paper's own notion of perfection, a formal version of the convex-hull/LP min–max principle (Proposition 2.1), which is reusable for any 0–1 polytope, and formal statements of the two theorems of Lovász that the proof relies on.

Difficulty

Proposition 2.1 reduces Theorem 3.1 to the equivalence of perfection with a fractional min–max for all integer weights. The obvious approach to that equivalence fails in both directions. From perfection one only gets the min–max for zero–one weights and zero–one multipliers; general integer weights do not reduce to zero–one weights by linearity, because the minimum over clique covers is not additive in $c$. Conversely, a fractional clique cover of value $\alpha$ does not directly produce an integral one. The paper crosses this gap with two theorems of Lovász: a numerical certificate of nonperfection, and the invariance of perfection under vertex duplication. Both are substantial graph-theoretic results in their own right, and neither follows from the definitions by routine manipulation.

Proposition 2.1 itself needs separation of a point from a polytope by an integral objective and LP strong duality with the nonnegativity rows handled separately.

Formalization scope

Vertices form a finite type V with decidable equality; a graph is a SimpleGraph V. $S(G)$ is a set of functions V → ℝ, and $P(G)$ is Mathlib's convexHull ℝ of it. $C(G)$ is the finset of finsets that are maximal among cliques (Maximal), as on the page; with $V=\emptyset$ the only maximal clique is $\emptyset$. "Defining linear system" is an equality of sets. Every "max = min" is written out in full: there is a value $m$ that is the maximum over $S$ (attained and an upper bound), some feasible multiplier vector attains $m$, and every feasible multiplier vector has objective at least $m$. Clique multipliers are functions Finset V → ℝ read only on $C(G)$.

Explicit conventions and added hypotheses:

• In Proposition 2.1 the index set $J$ is a finite type, coefficients are real, the nonnegativity rows are kept as a separate conjunct $x\ge0$, and $S$ is assumed nonempty (the paper's $\max$ over $S$ needs it).
• $\alpha$ and $\omega$ are Mathlib's indepNum and cliqueNum (natural numbers) of G.induce A.
• The duplicated graph lives on Option V, with none the new vertex.

Perfection is the paper's zero–one min–max, not "the clique system defines $P(G)$" (which would make the goal a tautology) and not Berge's $\chi(G_A)=\omega(G_A)$ (a different definition, equivalent only through the perfect graph theorem). $P(G)$ is the convex hull of $S(G)$, never the solution set of an inequality system.

Needed infrastructure, all reusable: integral separation from a rational polytope and LP strong duality in the form $\max\{cx:Ax\le b,x\ge0\}=\min\{\lambda b:\lambda A\ge c,\lambda\ge0\}$; basic facts about stable sets and maximal cliques of induced subgraphs and of duplicated graphs; invariance of IsPerfect under graph isomorphism and under taking induced subgraphs. Proofs of the Lovász milestones, which have independent value for a Mathlib theory of perfect graphs, are welcome.

Selected references

• V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4
• L. Lovász, A characterization of perfect graphs, J. Combin. Theory Ser. B 13 (1972) 95–98. https://doi.org/10.1016/0095-8956(72)90045-7
• D. R. Fulkerson, Anti-blocking polyhedra, J. Combin. Theory Ser. B 12 (1972) 50–71. https://doi.org/10.1016/0095-8956(72)90032-9
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

Motivation

A system that processes a stream of tasks can often be configured in several ways, and the configuration affects both the cost of the current task and the cost of switching before the next one: paging schemes, replicated files, server placements. When the future is unknown, the natural worst-case yardstick is competitive analysis, introduced by Sleator and Tarjan for list update and paging (Sleator–Tarjan 1985): an on-line strategy is compared with the optimal strategy that knows the whole input in advance.

Borodin, Linial and Saks (J. ACM 1992; conference version STOC 1987) proposed metrical task systems as a single model containing all such problems, and determined the exact deterministic competitive ratio of every such system. Their theorem is the starting point of the on-line-algorithms literature on metrical task systems, the $k$-server problem (Manasse–McGeoch–Sleator 1990) and their randomized variants.

Timeline. 1985: Sleator and Tarjan introduce competitive analysis for paging and list update. 1987: Borodin, Linial and Saks prove $w(S,d)=2n-1$ for every $n$-state metrical task system (journal version 1992). 1990: Manasse, McGeoch and Sleator extend the task-system model to restricted task sets and pose the $k$-server conjecture. The randomized ratio of the uniform task system, bounded in the same paper between $H(n)$ and $2H(n)$, is the subject of the companion mission.

Setting

A task system $(S,d)$ has a finite set $S$ of $n$ states and a transition-cost matrix $d$ with $d(i,i)=0$, $d(i,j)>0$ for $i\neq j$, and the triangle inequality $d(i,j)+d(j,k)\ge d(i,k)$. It is metrical if also $d(i,j)=d(j,i)$.

A task $T$ is a vector of nonnegative processing costs $T(s)$, $s\in S$. Given a task sequence $\mathbf T=T^1\cdots T^m$ and an initial state $s_0$, a schedule is a map $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$; task $T^i$ is processed in state $\sigma(i)$, and the cost is

$$c(\mathbf T;\sigma)=\sum_{i=1}^m d(\sigma(i-1),\sigma(i))+\sum_{i=1}^m T^i(\sigma(i)).$$

The off-line optimum $c_0(\mathbf T)$ is the minimum over all schedules. An on-line algorithm $A$ chooses $\sigma(i)$ knowing only $s_0$ and $T^1,\dots,T^i$; its cost is $c_A(\mathbf T)$. For $w>0$, $A$ is $w$-competitive if there is a constant $K_w$ with $c_A(\mathbf T)\le w\,c_0(\mathbf T)+K_w$ for every finite task sequence. The competitive ratio of $A$ is $w(A)=\inf\{w: A\text{ is }w\text{-competitive}\}$, and the competitive ratio of the task system is $w(S,d)=\inf_A w(A)$.

For the upper bound the paper also uses continuous-time schedules, in which task $T^i$ occupies the interval $[i,i+1)$ and the scheduler may change state at any real time, paying $\int_i^{i+1}T^i(\sigma(t))\,dt$ for processing. For a general (possibly asymmetric) matrix $d$, the cycle offset ratio $\psi(d)$ is the maximum over closed walks $s_0,\dots,s_k=s_0$ of $\sum_i d(s_{i-1},s_i)\big/\sum_i d(s_i,s_{i-1})$; it equals $1$ when $d$ is symmetric.

Formalization targets

Goal: Theorem 1.1

For every metrical task system $(S,d)$ with $n$ states,

$$w(S,d)=2n-1 .$$

The value depends on $n$ only, not on the distances.

Milestones

• Lemma 2.1. If $c_0(T^1\cdots T^m)\to\infty$ along an infinite task sequence $\mathbf T$, then $w(A)\ge w_{\mathbf T}(A)=\limsup_m c_A/c_0$.
• Theorem 2.2. Against the cruel taskmaster $M(\varepsilon)$, which charges $\varepsilon$ in the state the algorithm currently occupies,

$$w_{\mathbf T(\varepsilon)}(A)\ge\frac{2n-1}{1+\varepsilon/\min_{i\neq j}d(i,j)} .$$

• Lemma 3.1. Every on-line continuous-time algorithm is matched, on every task sequence, by an on-line discrete-time algorithm.
• Lemmas 6.3, 6.4, 6.2. Properties of the functions $f_k$ that drive the algorithm $A^*_d$: $f_k(s)-f_k(s')\le d(s',s)$; the identity $2\sum_{s\ne s_k}f_k(s)+f_k(s_k)=C_{k-1}+\sum_{i\le k}d(s_i,s_{i-1})$; and $f_k\le h_k$, the off-line cost at the $k$-th transition time.
• Theorem 6.1 (= Theorem 1.2). For every task system, symmetric or not, $A^*_d$ has competitive ratio at most $(2n-1)\psi(d)$.

Significance

The theorem settles the deterministic competitive ratio of the whole class of metrical task systems: the lower bound says that no deterministic on-line strategy can beat $2n-1$ on any metric, and the upper bound supplies one algorithm that achieves it on every metric. For asymmetric costs the same algorithm gives $(2n-1)\psi(d)$. The $2n-1$ lower bound is also the benchmark against which restricted models, such as paging and the $k$-server problem, measure their improvements, and the randomized question it leaves open drove much of the later work on metrical task systems.

The result was proved in 1987 and is standard; to the best of our knowledge no machine-checked proof exists. A formal development would provide a reusable model of deterministic on-line algorithms and competitiveness (on-line maps from task prefixes, additive competitiveness, infima over algorithms), an adversary construction by mutual recursion with an arbitrary algorithm, and an exact treatment of continuous-time schedules with piecewise-constant task costs. These pieces are reusable for other competitive-analysis results.

Difficulty

The lower bound is not a single bad input: the adversary is built from the algorithm it plays against, so the hard task sequence exists only as a recursion interleaved with the algorithm's choices, and the bound must hold for every deterministic on-line map, including ones that behave erratically. Obtaining the exact constant $2n-1$, rather than some $\Omega(n)$ bound, requires a sharp estimate of the off-line cost of that sequence.

The upper bound needs an algorithm defined in continuous time, whose transition times are determined by accumulated processing costs; the budgets can be zero, so transitions can be instantaneous, and a formal cost must remain well defined before one knows that only finitely many transitions occur. Relating the off-line cost function at those times to the recursively defined $f_k$ (Lemma 6.2) requires reasoning about all continuous-time off-line schedules. Finally, the goal combines both directions through infima over all on-line algorithms, and the discretization of Lemma 3.1 must be composed with the continuous-time algorithm.

Formalization scope

States form a finite type S (Fintype, DecidableEq, Nonempty); the goal is stated for all $n\ge1$, where $n=1$ gives $w(S,d)=1$. Task costs are finite nonnegative reals; the paper also allows $+\infty$ entries, which are excluded (this affects neither bound). A task sequence is T : Fin m → S → ℝ, with T i the paper's $T^{i+1}$, and a schedule is σ : Fin (m+1) → S. An on-line algorithm is a map sending $(s_0,[T^1,\dots,T^i])$ to $\sigma(i)$, so on-line behaviour is built into the type. Competitiveness is written additively, $c_A\le w\,c_0+K$, with $K$ independent of the task sequence and of $s_0$.

The competitive ratio competitiveRatio d is the real infimum of the set of all $w$ for which some on-line algorithm is $w$-competitive. It is not defined as an infimum of per-algorithm real infima: a non-competitive algorithm has $W_A=\emptyset$, whose real infimum is $0$, and that would drag $w(S,d)$ to $0$ for every system. Since the goal's value $2n-1$ is at least $1$ while the empty set's real infimum is $0$, the goal cannot hold vacuously.

Continuous-time algorithms are given as lists of $(\text{state},\text{length})$ pieces per unit interval; processing integrals are exact finite sums. The algorithm $A^*_d$ minimizes over states different from the current one, as its proof requires (the printed rule ranges over all states, and would stall); ties are left arbitrary. Its budgets may be $0$, its entry times are Option ℝ, and its cost is a sum in $[0,\infty]$, so that Theorem 6.1 itself asserts that only finitely many transitions occur. The ratio $\psi(d)$ excludes closed walks that never move, and Theorems 2.2 and 6.1 require $n\ge2$, where $\min_{i\ne j}d(i,j)$ and $\psi(d)$ are defined. Lemma 3.1 is stated comparing $A$ with $A'$ (the printed statement says "as well as $A$").

A complete development needs: the discrete model and off-line optimum (finite minimum over schedules), limsup arguments in EReal, continuous-time schedules with piecewise-constant costs, and the recursion defining $A^*_d$. Proofs of any milestone, including the purely combinatorial Lemmas 6.3 and 6.4, are welcome, as is a formal composition of Lemma 3.1 with Theorem 6.1.

Selected references

• A. Borodin, N. Linial, M. E. Saks, An optimal on-line algorithm for metrical task system, Journal of the ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Communications of the ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, Journal of Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W