Theoretical Computer Science

Motivation

In the single-machine scheduling problem $1|\mathrm{prec}|\sum w_jC_j$, a set $N$ of $n$ jobs, each with a processing time $p_j\ge 0$ and a weight $w_j\ge 0$, is processed on one machine without interruption, subject to precedence constraints given by a partial order $P$ on $N$. The aim is to minimize the weighted sum of completion times $\sum_j w_jC_j$. The problem is strongly NP-hard for general precedence constraints (Lawler 1978; Lenstra and Rinnooy Kan 1978), and its approximability was a recurring open question in scheduling theory (Schuurman and Woeginger 1999).

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 $G^S_P$ built from the instance. Many problems on partial orders become polynomial when the order is an interval order, so it is natural to ask whether this one does too. Section 7 of Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 2011) answers no: the problem stays NP-hard on interval orders. The proof is a reduction from vertex cover in connected graphs of maximum degree 3. This mission formalizes the correctness of that reduction.

Setting

A poset $P=(N,P)$ is read as a reflexive relation: $(x,y)\in P$ means $x\le y$. Jobs $x,y$ are incomparable if neither $(x,y)$ nor $(y,x)$ is in $P$, and $\operatorname{inc}(P)$ is the set of ordered incomparable pairs. The vertex cover graph $G^S_P$ has one node $(i,j)$ for each incomparable pair, weighted $p_iw_j$. Two 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)\in P$ and $(k,j)\in P$. Write $w(C_I)$ for the minimum weight of a vertex cover of $G^S_I$.

A poset is an interval order if each element $x$ can be assigned a closed real interval $[a_x,b_x]$ such that $x<y$ if and only if $b_x<a_y$.

The reduction starts from a graph $G=(V,E)$ with vertices $v_1,\dots,v_N$ and a spanning tree $T=(V,E_T)$ rooted at $v_1$, numbered so that each parent comes before its children. The paper uses a breadth-first search tree.

• Stage 1. The graph $G'$ is built from $T$. Each $v_i$ gets a pendant path $v_i - u^i_1 - u^i_2$. Each non-tree edge $\{v_i,v_j\}\in E\setminus E_T$ with $i<j$ gets the path $v_i - e^{ij}_1 - e^{ij}_2 - u^j_2$. The non-tree edges themselves are not edges of $G'$.
• Stage 2. The scheduling instance $S$ has jobs $s_0$, $s_1,\dots,s_N$, $m_1,\dots,m_N$, $e_1,\dots,e_N$, and $b_{ij}$ for each non-tree edge. Their intervals, processing times and weights are given in a table on p. 662. For example, $s_j$ has interval $[i,j]$, processing time $1/k^j$ and weight $k^i$, where $v_i$ is the parent of $v_j$. The precedence constraints $I$ are the interval order of these intervals. With $n$ the number of jobs, the parameter is $k=n^2+1$.
• The set $D$. It is $\{(s_0,s_1)\}\cup\{(s_i,s_j): v_i \text{ parent of } v_j\}\cup\{(s_i,m_i),(m_i,e_i)\}\cup\{(s_i,b_{ij}),(b_{ij},m_j)\}$. The graph $G'_I$ is the subgraph of $G^S_I$ induced by $D$.

Formalization targets

Goal: Theorem 7.1 (p. 661)

For every connected graph $G$ of maximum degree at most $3$, every parent-first spanning tree $T$ and every $m\in\mathbb N$, the precedence constraints $I$ of $S$ form an interval order, and

$$G \text{ has a vertex cover of size} \le m \iff \lfloor w(C_I)\rfloor \le m + |V| + |E\setminus E_T|.$$

Milestones, in the order the proof uses them

• Claim 1 (p. 662): $\tau(G') = \tau(G)+|V|+|E\setminus E_T|$, where $\tau$ is the vertex cover number.
• Remark 7.1 (p. 662): for jobs with intervals $[a,b]$ and $[c,d]$ and $a\le d$, $p_i\le 1/k^{\lceil b\rceil}$ and $w_j\le k^{\lceil c\rceil}$. On incomparable pairs $p_iw_j\in\{1\}\cup[0,1/k]$. Moreover, $p_iw_j\ge k$ forces $b<c$, and $p_iw_j=1$ forces $\lceil b\rceil=\lceil c\rceil$.
• Claim 2 (p. 663): an incomparable pair $(i,j)$ has $p_iw_j=1$ if it is in $D$, and $p_iw_j\le 1/k$ otherwise.
• Claim 3 (p. 663): $G'_I\cong G'$.
• §7, p. 664: with $k=n^2+1$, $\sum_{(i,j)\in\operatorname{inc}(I)\setminus D}p_iw_j<1$, and hence $w(C'_I)=\lfloor w(C_I)\rfloor$.

Significance

The result. Interval orders are a standard tractable class: several scheduling and order-theoretic problems that are hard in general become polynomial on them (Papadimitriou and Yannakakis 1979). Theorem 7.1 puts $1|\mathrm{prec}|\sum w_jC_j$ outside this pattern. Section 6 of the same paper shows that the problem nonetheless has a $3/2$-approximation on interval orders, so hardness and approximability are separated on this class. The paper also remarks that the proof makes weighted vertex cover NP-hard to approximate within some factor $r>1$ on the graphs $G^S_I$ arising from interval orders.

Formalizing it. The theorem is proved in the paper. Nothing in this mission is open, and none of it has been machine-checked before. The work splits into the following parts:

• a gadget argument on unweighted vertex covers (Claim 1, after Alimonti and Kann);
• an exact case analysis of incomparable pairs in a concrete interval order (Remark 7.1, Claim 2);
• a graph isomorphism (Claim 3);
• a rounding argument that links weighted and unweighted optima.

The definitions of $G^S_P$ and of minimum-weight vertex covers are shared with the other missions of this series.

Difficulty

The construction is explicit, and each step is elementary. The work is in the bookkeeping. Claim 2 requires classifying every incomparable pair of jobs, including pairs of different kinds such as $(b_{ij}, s_\ell)$, by comparing ceilings of interval endpoints. Half-integer endpoints ($m_i$, $b_{ij}$) are exactly what separates weight-one pairs from comparable ones. Claim 3 requires checking adjacency in $G^S_I$ for all pairs of nodes of $D$ in both directions. The paper writes out two cases in each direction and calls the rest similar.

Claim 1 has a direction that is not simply local. A vertex cover of $G'$ that misses both endpoints of a non-tree edge has to be repaired by swapping gadget vertices, and the repair must be repeated without increasing the size.

A natural first idea is to treat the light nodes (weight at most $1/k$) as negligible one at a time. This does not suffice: the argument needs their total weight to stay below $1$, which is what forces $k$ to grow with $n^2$.

Formalization scope

• Graph and tree. $G$ is a SimpleGraph (Fin N); vertex $v_{i+1}$ is i, and the root is index 0. The tree is a TreeLayout: a parent function returning none exactly at the root, with each parent of smaller index and adjacent in $G$. The statements hold for every such layout. This is stronger than the paper's breadth-first tree, and the proof uses only "parent before child".
• Hypotheses of the goal. Connectivity and the degree bound ((G.neighborSet v).ncard ≤ 3) are kept as in the paper. They matter only for the NP-completeness of the source problem.
• Jobs. The jobs form an inductive type with one constructor per row of the table. Their order is a PartialOrder instance: $x\le y$ iff $x=y$ or $b_x<a_y$. Processing times and weights are real numbers. Section 1 of the paper asks for nonnegative integers, but the instance uses $1/k^j$ and the formalization follows the instance as printed.
• Constants. The constants are explicit: $k=n^2+1$ with $n$ the cardinality of the job type, and $c=|V|+|E\setminus E_T|$. Remark 7.1 and Claim 2 are stated for every real $k>1$.
• Optimum values. $w(C_I)$ is a minimum over the finite family of vertex covers. Unweighted cover numbers are Mathlib's SimpleGraph.vertexCoverNum. The floor is Nat.floor, which agrees with the integer floor because $w(C_I)\ge 0$.
• Not formalized. The goal's wording ("NP-hard") is not formalized. Neither are the NP-completeness of degree-3 vertex cover (Garey, Johnson and Stockmeyer), the polynomial size of the construction, or Theorem 2.1 (cited), which turns a vertex cover of $G^S_I$ into a schedule. What is stated is the correctness of the reduction: the instance has interval-order constraints, and its optimum decides the vertex cover question.
• No trivialization. The instance $S$ is built from $G$ and $T$ exactly as in the table. The goal quantifies over all graphs and layouts, never over an instance $S$ assumed to have the properties.
• Contributions. Contributions are welcome on any milestone. Claims 1 and 3 are independent of the weights, and Claim 2 is independent of the graph theory.

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):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-1
• 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
• P. Alimonti, V. Kann, Some APX-completeness results for cubic graphs, Theoret. Comput. Sci. 237(1–2):123–134, 2000. https://doi.org/10.1016/S0304-3975(98)00158-3
• M. R. Garey, D. S. Johnson, L. Stockmeyer, Some simplified NP-complete graph problems, Theoret. Comput. Sci. 1(3):237–267, 1976. https://doi.org/10.1016/0304-3975(76)90059-1
• C. H. Papadimitriou, M. Yannakakis, Scheduling interval-ordered tasks, SIAM J. Comput. 8(3):405–409, 1979. https://doi.org/10.1137/0208031

Why the variable cost matters

The problem $1|\mathrm{prec}|\sum w_jC_j$ asks for an order in which to process jobs on one machine, respecting precedence constraints, so as to minimize the weighted sum of completion times. It is strongly NP-hard, and for decades the best approximation ratio known has been $2$, achieved by several unrelated algorithms (LP relaxations, Sidney decompositions, primal–dual methods).

Correa and Schulz (2005) and Ambühl and Mastrolilli (2009) showed that the problem is a special case of weighted vertex cover: its objective splits into a fixed cost, the same for every feasible solution, and a variable cost, which equals the weight of a vertex cover in an auxiliary graph $G^S_{\mathbf P}$. Approximating vertex cover in $G^S_{\mathbf P}$ within a factor $\alpha$ therefore approximates the scheduling problem within $\alpha$. Uhan observed that the classical 2-approximations owe their guarantee to the fixed cost and can be arbitrarily bad on the variable cost alone.

Section 8 of Ambühl, Mastrolilli, Mutsanas and Svensson, Math. Oper. Res. 36(4) (2011) (DOI), proves the converse: approximating the variable cost is as hard as approximating vertex cover itself. A better-than-2 algorithm for $1|\mathrm{prec}|\sum w_jC_j$ must therefore either exploit the fixed cost or improve on the best known approximation for vertex cover, a long-standing open question.

Setting

Scheduling instance. A finite set $N$ of jobs, a partial order $\mathbf P = (N,P)$ (reflexive; $(i,j) \in P$, $i \ne j$, means $i$ precedes $j$), processing times $p_j \ge 0$ and weights $w_j \ge 0$.

Incomparable pairs. Jobs $x,y$ are incomparable, $x \parallel y$, if neither $(x,y)$ nor $(y,x)$ lies in $P$. The set $\operatorname{inc}(\mathbf P)$ consists of the ordered pairs $(x,y)$ with $x \parallel y$.

The vertex cover graph $G^S_{\mathbf P}$. One node per incomparable pair $(i,j)$, of weight $w_{(i,j)} = p_i w_j$. Distinct nodes $(i,j)$ and $(k,\ell)$ are adjacent when, in one of the two orders, $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell),(k,j) \in P$. For a set $C$ of nodes, $w(C) = \sum_{u\in C} w_u$; for a vertex cover $C$ this is the variable cost, and $\tau_w(G^S_{\mathbf P})$ is its minimum over all vertex covers.

The instance $S(G,k)$. Given a graph $G=(V,E)$ with $V = \{v_1,\dots,v_n\}$ and $k > 0$, the instance has jobs $v'_i$ (processing time $k^{-i}$, weight $0$) and $v''_i$ (processing time $0$, weight $k^{i}$), and precedence constraints $v'_i < v''_j$ and $v'_j < v''_i$ for each edge $\{v_i,v_j\} \in E$, plus $v'_i < v''_j$ for all $i<j$. The nodes $(v'_i, v''_i)$ of $G^S_{\mathbf P}$ have weight $1$ and are called heavy; all others are light. For a set $C$ of nodes, $C_G = \{v_i : (v'_i,v''_i)\in C\}$. The vertex cover number of $G$ is $\tau(G)$.

Formalization targets

Goal: Theorem 8.1

For every graph $G$ on $n$ vertices, every $r \ge 1$, $\varepsilon>0$ and every $k \ge 1$ with $k > n^2r/\varepsilon$: if $C$ is a vertex cover of $G^S_{\mathbf P}$ for $S = S(G,k)$ with $w(C) \le r\,\tau_w(G^S_{\mathbf P})$, then $C_G$ is a vertex cover of $G$,

$$|C_G| \le r\Bigl(\tau(G) + \frac{n^2}{k}\Bigr),$$

and, when $E \ne \emptyset$,

$$|C_G| \le r\Bigl(1+\frac{n^2}{k}\Bigr)\tau(G) < (r+\varepsilon)\,\tau(G).$$

The paper words the theorem as "approximating the variable cost of $1|\mathrm{prec}|\sum w_jC_j$ is as hard as approximating vertex cover"; the statement above is the mathematical content its proof establishes.

Milestones (§8, p. 664)

1. In $G^S_{\mathbf P}$, every heavy node has weight $1$, every light node has weight at most $1/k$, and the light nodes have total weight at most $n^2/k$ (for $k \ge 1$).
2. Heavy nodes $(v'_i,v''_i)$ and $(v'_j,v''_j)$ are adjacent if and only if $\{v_i,v_j\}\in E$; for $k>1$ the subgraph induced by the weight-1 nodes is isomorphic to $G$ via $(v'_i,v''_i) \mapsto v_i$.

Significance

The result. Theorem 8.1 is one half of an equivalence: by Theorem 2.1 (Correa–Schulz, Ambühl–Mastrolilli), minimizing the variable cost is a special case of weighted vertex cover; by Theorem 8.1, it is also as hard to approximate. Any hardness of approximation for vertex cover (NP-hardness of factor $1.36$ by Dinur and Safra; factor $2-\delta$ under the unique games conjecture by Khot and Regev) transfers to the variable cost. It also explains why the known 2-approximations must rely on the fixed cost, and it frames the later result of Bansal and Khot that the full objective is hard to approximate within $2-\delta$ under a variant of the unique games conjecture.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The mission produces a checked account of the reduction: the vertex cover graph of an arbitrary precedence-constrained instance, the adjacency-poset instance built from a graph, and the quantitative transfer of approximation ratios. The definition of $G^S_{\mathbf P}$ is shared with the other missions of this series.

Difficulty

The construction is short; the care is in the bookkeeping. One must check that the precedence relation is a partial order, determine exactly which ordered pairs are incomparable, verify that two heavy nodes are adjacent only through the third clause of the adjacency rule and only when the corresponding vertices are adjacent in $G$, and bound the weights of all remaining nodes, including the many nodes of weight $0$. The transfer then compares an approximate cover of $G^S_{\mathbf P}$ with an optimal one whose heavy part comes from an optimal cover of $G$; the additive error $n^2/k$ must be converted into a multiplicative one, which requires $\tau(G)\ge 1$.

A first reading of the page suggests that $G^S_{\mathbf P}$ has at most $n^2$ nodes; it does not. The pairs $(v'_i,v'_j)$ and $(v''_i,v''_j)$ with $i\ne j$ are incomparable nodes of weight $0$, so there can be up to $4n^2-2n$ nodes. Only nodes of positive weight are few.

Formalization scope

• Model. Jobs form a finite type; precedence constraints are an explicit reflexive partial-order relation P : N → N → Prop. Processing times and weights are nonnegative reals. The vertex cover graph is a SimpleGraph on the subtype of incomparable ordered pairs, using the symmetric closure of the printed adjacency rule without loops. Vertex covers are Mathlib's SimpleGraph.IsVertexCover; $\tau(G)$ is Mathlib's vertexCoverNum, finite for a finite graph and converted with toNat; $\tau_w(G^S_{\mathbf P})$ is a minimum over finite vertex covers.
• The instance. The graph is a SimpleGraph (Fin n); i : Fin n stands for $v_{i+1}$, so exponents are $i+1$ and the order $i<j$ is that of Fin n. Jobs are Fin n ⊕ Fin n ($v'$ left, $v''$ right). The parameter $k$ is in $\mathbb R_{\ge 0}$.
• Added hypotheses. $k \ge 1$, implicit in the page ("$k > n^2r/\varepsilon$" does not imply it when $\varepsilon$ is large, and for $k<1$ the light nodes outweigh the heavy ones). The isomorphism with $G$ is stated for $k > 1$, since at $k=1$ some light nodes also have weight $1$. The multiplicative bound requires $E \ne \emptyset$; the additive bound holds for every graph.
• Not formalized. The phrases "approximation algorithm", "polynomial time" and "as hard as"; the passage from vertex covers of $G^S_{\mathbf P}$ to schedules (Theorem 2.1, cited from Correa–Schulz and Ambühl–Mastrolilli); the fixed cost. What is stated instead is the explicit map $C \mapsto C_G$ and the ratio it achieves, $r(1+n^2/k) < r+\varepsilon$. The false count "at most $n^2$ vertices" is not stated.
• Ruled out. The goal is not a statement about an arbitrary graph or an assumed cover of $G$: it concerns the specific instance $S(G,k)$ and every $C$ that is an $r$-approximate vertex cover of its graph, and the fact that $C_G$ covers $G$ is a conclusion, not a hypothesis.
• Welcome contributions. Proofs of the two milestones and of the goal; general lemmas on $G^S_{\mathbf P}$ (weights of vertex covers, behaviour under induced subgraphs) are reusable across the series.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• J. R. Correa, A. S. Schulz, Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• C. Ambühl, M. Mastrolilli, Single Machine Precedence Constrained Scheduling Is a Vertex Cover Problem, Algorithmica 53(4):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-6
• I. Dinur, S. Safra, On the Hardness of Approximating Minimum Vertex Cover, Annals of Mathematics 162(1):439–485, 2005. https://doi.org/10.4007/annals.2005.162.439
• S. Khot, O. Regev, Vertex Cover Might Be Hard to Approximate to within 2 − ε, Journal of Computer and System Sciences 74(3):335–349, 2008. https://doi.org/10.1016/j.jcss.2007.06.019
• N. Bansal, S. Khot, Optimal Long Code Test with One Free Bit, FOCS 2009, 453–462. https://doi.org/10.1109/FOCS.2009.23

Motivation

A retailer, an airline or an online platform decides which products to show a customer. Showing more is not always better: a customer who would have bought an expensive product may switch to a cheap one once it is offered. The assortment problem asks for the set of products that maximises expected revenue, given a model of how customers choose. It is a central problem of revenue management (Talluri and van Ryzin, 2004), and it is NP-hard even for mixtures of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, 2014).

The standard heuristic in practice is revenue-ordered assortments: sort the products by price and only consider the sets consisting of the most expensive products down to some threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin, 2004), but not in general. Berbeglia and Joret (arXiv:1606.01371) ask how much revenue the heuristic can lose under every reasonable choice model, and answer with guarantees that depend only on the prices.

Timeline:

• 2004: Talluri and van Ryzin prove revenue-ordered assortments optimal under the multinomial logit model.
• 2014: Rusmevichientong et al. show NP-hardness of the assortment problem for mixtures of logits, and prove that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit models.
• 2016–2019: Berbeglia and Joret prove the guarantees $1/k$ and $1/(1+\ln(r_k/r_1))$ under any regular choice model and show them tight (arXiv v1 2016, v3 2019; Algorithmica 2020). Aouad, Farias, Levi and Segev (2018) show that under random utility models no efficient algorithm does essentially better than these ratios.

Setting

There is a finite nonempty set $\mathcal C$ of products. For a choice set $S\subseteq\mathcal C$, $\mathcal P(x,S)$ is the probability that a customer offered $S$ buys product $x$, and $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ is the probability that the customer buys nothing. The system $\mathcal P$ is a regular discrete choice model if

1. $\mathcal P(x,S)\ge0$ for every $x\in\mathcal C\cup\{0\}$;
2. $\mathcal P(x,S)=0$ whenever $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ and $x\in S\cup\{0\}$.

Axiom 4, regularity, says that adding products never makes a given product, or leaving without buying, more likely. Every random utility model is regular.

Each product has a positive price $r(x)>0$. The revenue of $S$ is $\operatorname{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\operatorname{rev}(S)$. Let $0<r_1<\cdots<r_k$ be the distinct prices, so $k$ counts price levels and not products, and set $r_0=0$. The revenue-ordered assortments are $S_i=\{x\in\mathcal C : r(x)\ge r_i\}$, $i=1,\dots,k$, and the heuristic earns

$$\mathrm{RO}=\max_{1\le i\le k}\operatorname{rev}(S_i).$$

Formalization targets

Goal: Theorem 3.2

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

The goal fixes no constant beyond the paper's own quantities. Both parts are required: the sum form is the sharper bound, and the paper shows it is attained (Theorem 3.4, a later mission of this series).

Milestones

• Lemma 2.1: $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$.
• Inequality (5): $\operatorname{rev}(S_i)\ge r_i\sum_{x\in S^*\cap S_i}\mathcal P(x,S^*)$ for every $S^*$ and $i\in[k]$.
• Theorem 3.1: $\mathrm{OPT}\le k\cdot\mathrm{RO}$.
• Rearrangement (proof of Theorem 3.2): $\operatorname{rev}(S^*)=\sum_{\ell}(r_\ell-r_{\ell-1})\sum_{x\in S^*\cap S_\ell}\mathcal P(x,S^*)$, and $\operatorname{rev}(S^*)\le\sum_\ell\frac{r_\ell-r_{\ell-1}}{r_\ell}\operatorname{rev}(S_\ell)$.
• Logarithmic bound: $\sum_{\ell=1}^k\frac{a_\ell-a_{\ell-1}}{a_\ell}\le1+\ln(a_k/a_1)$ for $0=a_0<a_1<\cdots<a_k$.

Significance

The theorem shows that a pricing-only quantity controls the loss of the most common heuristic in revenue management, uniformly over all regular choice models, including every random utility model, mixtures of logits and Markov chain models. Combined with the hardness result of Aouad et al., it shows that revenue-ordered assortments achieve essentially the best ratio, as a function of $k$ or of $r_k/r_1$, that an efficient algorithm can achieve. The same analysis transfers to the envy-free pricing and Stackelberg problems studied in the later sections of the paper.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a Lean formalization of regular choice models, the revenue-ordered heuristic and its two guarantees, on which the paper's tightness examples, the purchase-probability bound (Theorem 3.3) and the applications to pricing can build.

Difficulty

The argument is short, but two points are easy to get wrong. First, revenues of $S_i$ and of an optimal $S^*$ involve choice probabilities evaluated at different sets, so the comparison must pass through $S^*\cap S_i$, using regularity once for products and once for the no-purchase option. A model that only assumes regularity for products does not satisfy the theorem. Second, the bound runs over distinct price levels, not products, and the first summand uses the convention $r_0=0$; indexing by products or dropping $r_0$ gives a different quantity. The comparison of the sum with $\ln(r_k/r_1)$ is a Riemann-sum estimate for $\int dt/t$ and needs a real-analysis lemma not phrased this way in Mathlib.

Formalization scope

• Products are a finite nonempty type C with decidable equality; choice sets are Finset C. The choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S = 1 - ∑ x ∈ S, P x S.
• IsRegular P carries axioms (i)–(iv), with (i) and (iv) each split into a product case and a no-purchase case. The no-purchase case of (i) is redundant with (iii) and is kept to match the page.
• r : C → ℝ with the hypothesis ∀ x, 0 < r x. revenue P r S is $\operatorname{rev}(S)$ and opt P r is the maximum over all Finset C (Finset.sup'), including the empty set.
• Price levels are 1-based: level r i is $r_i$ for $1\le i\le k$ and level r 0 = 0; numVals r is $k$, the number of distinct values. roSet r i is $S_i$; roValue P r is the maximum over $i\in\{1,\dots,k\}$ only.
• Approximation guarantees are stated in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$, never as a ratio. $\ln$ is Real.log, applied to $r_k/r_1\ge1$.
• Ruled out: a maximum over all subsets in place of $\mathrm{RO}$ (which makes the bound trivial), a regularity axiom without its no-purchase case, the logarithmic form alone in place of the sum form, and any specific choice model (logit, Markov chain, random utility) in place of an arbitrary regular $\mathcal P$.

Needed infrastructure: finite sums over price levels and summation by parts, the comparison of $(b-a)/b$ with $\ln(b/a)$, and the sorted enumeration of a finite set of reals (Finset.orderEmbOfFin). The regular model and the revenue-ordered sets are shared with the other missions of this series. Contributions of any milestone, alternative proofs of the logarithmic bound, and proofs that specific choice models are regular 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
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• 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.1724
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191

Motivation

Sparse graphs with small nontrivial eigenvalues, expanders, are basic objects in combinatorics and theoretical computer science. They are used in error-correcting codes, derandomization, sorting networks, and the analysis of random walks. The Alon–Boppana bound says that a $d$-regular graph on $n$ vertices has a nontrivial eigenvalue of absolute value at least $2\sqrt{d-1}-o(1)$ (Alon 1986; Nilli 1991). Graphs that reach $2\sqrt{d-1}$ are Ramanujan graphs.

The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (1988) and Margulis exist only for degrees $d = p+1$ with $p$ prime, and only for very sparse sequences of vertex counts. Constructions with $\lambda\le 2\sqrt{d-1}+\varepsilon$ for every degree came from Mohanty, O'Donnell and Paredes (STOC 2020, arXiv:1909.06988), but their graphs also do not have every number of vertices. Alon (arXiv:2003.11673, Combinatorica 41, 2021) asked for near-Ramanujan graphs of every degree and every large size. Theorem 1.3 of that paper answers this up to $\varepsilon$: for every $d$, every $\varepsilon>0$ and every large $n$ with $nd$ even there is an explicit $(n,d,\lambda)$-graph with $\lambda\le 2\sqrt{d-1}+\varepsilon$.

Setting

A $(n,d,\lambda)$-graph is a $d$-regular simple graph on $n$ vertices in which every nontrivial eigenvalue of the adjacency matrix $A$ has absolute value at most $\lambda$. The trivial eigenvalue is $d$, with the constant eigenvector $\mathbf 1$. Equivalently, every eigenvalue $\mu$ of $A$ with an eigenvector $f\ne0$, $\sum_v f(v)=0$, satisfies $|\mu|\le\lambda$.

Distances $\operatorname{dist}(v,w)$ are graph distances, and they are $\infty$ between components. The $k$-neighbourhood of a vertex $v$ is $B(v,k)=\{w:\operatorname{dist}(v,w)\le k\}$. The $k$-neighbourhood of an edge $uv$ is $B(u,k)\cup B(v,k)$, and $N_i$ is the set of vertices at distance exactly $i$ from $\{u,v\}$. A set contains no cycle if the subgraph induced on it is a forest. A ball contains at most one cycle if its induced subgraph has at most as many edges as vertices.

The construction starts from a $d$-regular graph $H$ on a vertex set $V$ and a set $U\subseteq V$. Write $N(U)$ for the set of neighbours of $U$, and let $m$ be a perfect matching on $N(U)$. Then $H'$ is the subgraph induced on $V\setminus U$, $M$ is the graph of matching edges $\{x,m(x)\}$, and $G=H'\cup M$.

Formalization targets

Goal: Theorem 1.3, relative to the input graph

Let $d\ge3$, $\varepsilon>0$, $r=\lceil 2/\varepsilon\rceil$. Suppose $H$ is an $(N,d,2\sqrt{d-1}+\varepsilon/2)$-graph in which the $(2r+4)$-neighbourhood of every vertex contains at most one cycle, and $r\le\log_{d-1}N$. Then for every $u$ with $ud$ even and $u\le N/(2d^{2r+3})$,

$$\exists\, G \text{ on } N-u \text{ vertices}:\quad G \text{ is an } \bigl(N-u,\ d,\ 2\sqrt{d-1}+\varepsilon\bigr)\text{-graph}.$$

The hypotheses on $H$ are what Theorem 3.3 (Mohanty–O'Donnell–Paredes) supplies, and that theorem is not formalized.

Milestones

• Lemma 3.1 (p. 10). A $d$-regular graph whose $(2r+4)$-balls contain at most one cycle has a set $U$ with $|U|\ge n/(2d^{2r+3})$, cycle-free $(r+1)$-balls, and pairwise distances $\ge 2r+3$.
• Lemma 3.2 (p. 11). If the $r$-neighbourhood of an edge $uv$ contains no cycle and $A f=\mu f$ with $\mu\ge2\sqrt{d-1}$, then

$$\sum_{w\in N_i}f^2(w)\ \ge\ \sum_{w\in N_{i-1}}f^2(w),\qquad 1\le i\le r .$$

• The variational characterization of nontrivial eigenvalues (§2.4, p. 8).
• In $G=H'\cup M$: $G$ is $d$-regular on $|V|-|U|$ vertices and $A_G=A_{H'}+A_M$. Matching edges have cycle-free $(r-1)$-neighbourhoods and pairwise disjoint $r$-neighbourhoods.
• Inequalities (9), (10), (11) (p. 13), and the spectral step: for every admissible $U$ and $m$, $G$ is an $(N-|U|,d,2\sqrt{d-1}+\varepsilon)$-graph.

Significance

Theorem 1.3 shows that the size restrictions of algebraic Ramanujan constructions cost nothing spectrally: up to an arbitrarily small $\varepsilon$, the Alon–Boppana bound is attained by explicit graphs on every admissible vertex count. The deletion method is local. It turns any near-Ramanujan graph whose short cycles are sparse into graphs of all nearby sizes, so it applies to future constructions as well. Lemma 3.2 is a self-contained delocalization statement in the tradition of Kahale 1995: eigenvectors of eigenvalues at least $2\sqrt{d-1}$ in absolute value cannot concentrate near tree-like edges.

The result is proved on paper. To our knowledge none of it is formalized; Mathlib has adjacency matrices, extended graph distance and acyclicity, but no theory of expanders. A complete development would give machine-checked versions of a delocalization lemma, of the greedy selection of far-apart vertices away from short cycles, and of the variational eigenvalue bound for induced subgraphs. It would also check two points the paper passes over. The proof of Theorem 1.3 treats only positive eigenvalues $\lambda\ge2\sqrt{d-1}$. And its claim that the $r$-neighbourhood of a matching edge is cycle-free fails when two deleted vertices are at distance exactly $2r+3$. This mission states the corrected forms (see Formalization scope).

Difficulty

The spectral bound for $G$ does not follow from interlacing alone. Deleting vertices is harmless, since by (9) the quadratic form of $H'$ is controlled by $H$. But the added matching contributes up to $\sum_{x\in N(U)}f(x)^2$ to $f^tA_Gf$, which can be as large as $\|f\|^2$ for an eigenvector concentrated on $N(U)$. The obvious estimate therefore gives only $\lambda\le 2\sqrt{d-1}+1+\varepsilon/2$. Closing the gap requires showing that an eigenvector of a large eigenvalue spreads its mass over the $r$ layers around each matching edge (Lemma 3.2). That in turn needs those neighbourhoods to be trees in $G$ and pairwise disjoint, which is where Lemma 3.1's choice of $U$ is used. The combinatorial part, tracking distances and cycles in $G$ when $G$ mixes edges of $H$ with matching edges, is the main formalization burden.

Formalization scope

• Representation. Vertex sets are finite types. Graphs are Mathlib SimpleGraphs with real adjacency matrices adjMatrix ℝ. The (n, d, λ) predicate requires IsRegularOfDegree d, symmetry, row sums $d$, and $|\mu|\le\lambda$ for every eigenpair $(\mu,f)$ with $f\ne0$, $\sum f=0$. Distances use the extended SimpleGraph.edist, never dist (which is $0$ across components). Cycle conditions are on induced subgraphs, and "at most one cycle" on a ball is $|E|\le|V|$. Deleted vertices are a Finset U; the new graph lives on the subtype {v // v ∉ U}. The matching is a fixed-point-free involution of $N(U)$.
• Explicit quantities replacing the paper's asymptotics. The paper writes "sufficiently large $n$" and $u=o(n)$. The goal instead takes any $u\le N/(2d^{2r+3})$ (the size Lemma 3.1 guarantees) with $ud$ even, plus Lemma 3.1's side condition $r\le\log_{d-1}N$. The equality $r=\lceil2/\varepsilon\rceil$ is used as $\lceil2/\varepsilon\rceil_+\in\mathbb N$. The paper's "every degree $d$" becomes $d\ge3$, the range of its proof.
• Corrections. (11) and Lemma 3.2's companion are stated for $|\mu|\ge2\sqrt{d-1}$, both signs. The matching-edge note is stated for the $(r-1)$-neighbourhood, which still yields the factor $1/r$ in (11). Lemma 3.2 itself is stated as printed.
• Out of scope. Theorem 3.3 ([18]) is a cited input: its graph is the hypothesis $H$. All claims of explicitness and polynomial running time are out of scope, as is §4's remark on applying the method to LPS graphs directly.
• No trivialization. The input hypotheses are exactly Theorem 3.3's conclusions plus Lemma 3.1's side condition, and they are met by high-girth Ramanujan graphs. No hypothesis mentions the spectrum or Rayleigh quotients of the constructed graph, and the goal's graph must be $d$-regular on exactly $N-u$ vertices.
• Reusable infrastructure. Welcome contributions include the variational characterization for symmetric matrices with constant row sums, a forest edge-count lemma for balls, BFS-layer structure of cycle-free balls in regular graphs, and the edge-disjoint decomposition $A_{G}=A_{H'}+A_M$. Each is useful beyond this mission.

Selected references

• N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673
• S. Mohanty, R. O'Donnell, P. Paredes, Explicit near-Ramanujan graphs of every degree, STOC 2020. https://arxiv.org/abs/1909.06988
• A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988). https://doi.org/10.1007/BF02126799
• N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986). https://doi.org/10.1007/BF02579166
• A. Nilli, On the second eigenvalue of a graph, Discrete Mathematics 91 (1991). https://doi.org/10.1016/0012-365X(91)90112-F
• N. Kahale, Eigenvalues and expansion of regular graphs, J. ACM 42 (1995). https://doi.org/10.1145/210118.210136

Motivation

Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a $d$-regular graph is governed by the Alon–Boppana bound $2\sqrt{d-1}$, and graphs attaining it, Ramanujan graphs, were constructed explicitly by Lubotzky, Phillips and Sarnak (LPS 1988) and by Margulis. These constructions exist only for special degrees ($d = p+1$ with $p$ prime) and special numbers of vertices (orders of $PSL(2,\mathbb F_q)$ or $SL(2,\mathbb F_q)$). Applications often need a graph of a prescribed size $n$.

N. Alon's paper Explicit expanders of every degree and size (arXiv:2003.11673v1; Combinatorica 41, 2021) shows how to obtain explicit near-Ramanujan graphs on exactly $n$ vertices. This mission formalizes the spectral core of its Theorem 1.2: a Ramanujan graph on $m$ vertices can be enlarged to $n = m + r$ vertices, with degree raised by one, while the nontrivial eigenvalues stay within a constant factor of optimal.

Setting

Let $V$ be a finite set of $m \ge 1$ vertices. A $(n,d,\lambda)$-graph is a $d$-regular graph on $n$ vertices whose adjacency matrix $A$ satisfies $|\mu| \le \lambda$ for every nontrivial eigenvalue $\mu$, that is, every eigenvalue other than the top eigenvalue $d$ of the constant vector $\mathbf 1$. For a symmetric $A$ with $A\mathbf 1 = d\,\mathbf 1$, the nontrivial eigenvalues are those with an eigenvector $f \ne 0$ satisfying $\sum_v f(v) = 0$. Graphs may carry loops, at most one per vertex, and a loop adds one to the degree: it is a diagonal entry $1$ of $A$.

Fix an integer $p \ge 0$ and let $H$ be an $(m, p+1, 2\sqrt p)$-graph on $V$, a $(p+1)$-regular Ramanujan graph. Let $R = \{u_1, \dots, u_r\}$ be $r$ new vertices and let $W_1, \dots, W_r \subseteq V$ be pairwise disjoint sets of $p+2$ vertices each. Put $W = \bigcup_i W_i$ and $L = V \setminus W$. The graph $G$ on $U = V \cup R$ is obtained from $H$ by joining each $u_i$ to every vertex of $W_i$ and adding one loop at each vertex of $L$. Its adjacency matrix is

$$A_G = A_H + A_R + A_L,$$

where $A_H$ is the adjacency matrix of $H$ (zero on $R$), $A_R$ that of the stars joining $u_i$ to $W_i$, and $A_L$ the diagonal matrix of the loops. Every vertex of $G$ has degree $p+2$.

Formalization targets

Goal: Theorem 1.2, spectral core

$$A_G \text{ is an } \Big(m+r,\; p+2,\; \sqrt{2(p+1)} + \sqrt p + \frac{(p+1)\,r}{m}\Big)\text{ matrix.}$$

The paper states $\lambda \le \sqrt{2(d-1)} + \sqrt{d-1} + o(1)$ for $d = p+2$; its proof gives $\sqrt{2(p+1)} + \sqrt p + o(1)$, which is stronger, and the error term it produces is $(p+1)r/m$. The goal is parametrised by $H$, $r$ and the sets $W_i$, so it does not depend on how $m$ and $r$ are chosen.

Milestones

1. The variational characterization of the nontrivial eigenvalues: for a symmetric matrix with constant row sums and $\lambda \ge 0$, $|\mu| \le \lambda$ for every nontrivial eigenvalue if and only if $|f^tAf| \le \lambda\|f\|^2$ whenever $\sum f = 0$.
2. The Cauchy–Schwarz display: $\sum_U f = 0$ implies $|\sum_V f|^2 = |\sum_R f|^2 \le |R| \sum_R f^2$.
3. Inequality (3): $|f^tA_Hf| \le b^2(p+1) + c^2\, 2\sqrt p$ with $b^2 = (\sum_V f)^2/m$ and $c^2 = \sum_V f^2 - b^2$.
4. Display (4): $f^tA_Lf = \sum_{v\in L} f^2(v)$.
5. Inequality (5): $|f^tA_Rf| \le \frac{p+2}{x}\sum_R f^2 + x\sum_W f^2$ for every $x > 0$.
6. Inequality (6): for $\sum_U f = 0$ and $x > 0$,

$$|f^tA_Gf| \le (2\sqrt p+1)\sum_L f^2 + (2\sqrt p+x)\sum_W f^2 + \frac{p+2}{x}\sum_R f^2 + (p+1)\frac rm \sum_R f^2.$$

Significance

With $H$ the Lubotzky–Phillips–Sarnak graph on $m = |SL(2,\mathbb F_q)|$ vertices for the largest suitable prime $q$ with $m \le n$, and $r = n - m$, the distribution of primes in arithmetic progressions gives $r = o(m)$, and the goal yields an explicit $(n, p+2, \lambda)$-graph with $\lambda \le (1+\sqrt2)\sqrt{d-1} + o(1)$ for every sufficiently large $n$. This is within a factor of about $1.21$ of the Ramanujan bound $2\sqrt{d-1}$, for every number of vertices, by an elementary modification of an existing graph. The statement is useful independently of LPS: any Ramanujan graph, or any graph with a bound on its nontrivial eigenvalues, can be padded to a nearby size in the same way.

The result is proved in the paper. No formalization of it, of the $(n,d,\lambda)$ notion, or of the variational characterization of nontrivial eigenvalues for regular graphs exists on the platform. The mission produces a checked version of the spectral argument, and the variational characterization (milestone 1) is a general fact about symmetric matrices with constant row sums that applies to any spectral expander argument.

Difficulty

The vertices of $W$ and $L$ lie in the old graph $H$, whose spectrum is controlled, but the new vertices of $R$ are not; and a vector orthogonal to $\mathbf 1$ on $U$ need not be orthogonal to the constant vector on $V$. Bounding $f^tA_Gf$ by applying the Ramanujan bound for $H$ to $f$ restricted to $V$ therefore fails: the restriction has a component along the trivial eigenvector of $H$, whose eigenvalue $p+1$ is large. The argument must show that this component is small, of order $r/m$, and must balance the star edges between $R$ and $W$ against the loops on $L$ so that every vertex class gets the same coefficient. The naive bound $|f^tA_Rf| \le \|A_R\|\,\|f\|^2 = \sqrt{p+2}\,\|f\|^2$ added to $2\sqrt p$ for $H$ and $1$ for $L$ gives a constant larger than $\sqrt{2(p+1)}+\sqrt p$; the stated constant needs the weighted estimate.

On the Lean side, milestone 1 concerns the spectrum of a symmetric matrix on the invariant subspace $\mathbf 1^\perp$, while Mathlib states the spectral theorem for the whole space.

Formalization scope

• Vertices of $G$ are the disjoint union $V \oplus \mathrm{Fin}\, r$. $G$ is represented by its real adjacency matrix, since it has loops; $H$ is a Mathlib SimpleGraph with adjMatrix.
• The $(n,d,\lambda)$ predicate is stated for matrices: $|V| = n$, symmetry, $A\mathbf 1 = d\,\mathbf 1$, and $|\mu| \le \lambda$ for every eigenpair $(\mu, f)$ with $f \ne 0$ and $\sum f = 0$. For simple graphs, $d$-regularity is added.
• The paper's $o(1)$ terms are replaced by the explicit quantities its proof produces: $(p+1)r/m$ in the goal, and $(p+1)\frac rm\sum_R f^2$ in (6). Inequality (3) is stated with the corrected relation $b^2 + c^2 = \sum_V f^2$; the paper's "$b^2 + c^2 = 1$" holds only for unit restrictions.
• The bound uses $\sqrt p = \sqrt{d-2}$, as in the proof and the abstract, which implies the printed $\sqrt{d-1}$.
• $p$ is any natural number. The hypothesis "$p$ prime, $p \equiv 1 \pmod 4$" serves only to obtain $H$ from LPS, and $H$ is a hypothesis here. The sets $W_i$ are arbitrary pairwise disjoint sets of size $p+2$, not the paper's consecutive blocks of a numbering of $SL(2,\mathbb F_q)$.
• Out of scope: the existence of the prime $q$ and the estimate $n - m = o(m)$; the numbering of $SL(2,\mathbb F_q)$; the "strongly explicit" and polynomial-time claims; the LPS construction (Theorem 2.1, cited); the variant that replaces loops by a matching for even $n$.
• The goal cannot be satisfied trivially: dropping the condition $\sum f = 0$ makes it false, since $p+2$ is always an eigenvalue, and for $p \ge 2$ and small $r/m$ the bound is below $p + 2$ (for $p = 5$ it is about $5.70 + 6r/m$). At $p = 1$ the bound $3 + 2r/m$ is at least the degree $3$, so that case holds trivially; it is the paper's statement there as well.
• Contributions welcome: proofs of each milestone, especially the variational characterization, which is reusable for mission 3 of this series and for any regular-graph spectral argument.

Selected references

• N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673
• A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988) 261–277. https://doi.org/10.1007/BF02126799
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8

Motivation

Linear programming, $\min\{c^\top x : Ax=b,\ x\ge0\}$ with $A\in\mathbb R^{d\times n}$, is the basic model of operations research, and the complexity of solving it is a central question of algorithm theory. Interior-point methods follow the central path: primal–dual pairs $(x,s)$ with $x,s>0$ and $x_is_i=t$ for every $i$, as the path parameter $t$ decreases to $0$. A classical short-step method needs $O(\sqrt n\log(n/\delta))$ iterations, each solving a linear system with the matrix $A\frac XSA^\top$, for a total of roughly $n^{2.5}$ operations or more.

Cohen, Lee and Song (J. ACM 68(1), 2021; arXiv:1810.07896) showed that linear programs can be solved in time $n^{\omega+o(1)}\log(n/\delta)$ (for the current values of the matrix multiplication exponent $\omega$ and its dual $\alpha$), matching the cost of multiplying two $n\times n$ matrices. The analysis has two halves: a data structure that maintains the projection matrix lazily, and the stochastic central path method, which replaces each Newton step by a sparse random step and proves that the iterates still stay close to the central path. This mission formalizes the second half.

Timeline: Karmarkar's projective method (1984) gave the first polynomial interior-point method; Renegar (1988) gave the $O(\sqrt n\log(1/\delta))$ path-following bound; Vaidya (1989) reduced the per-iteration cost with low-rank updates; Lee and Sidford (2014–2015) reduced the iteration count to $\widetilde O(\sqrt d)$; Cohen, Lee and Song (STOC 2019, J. ACM 2021) reached $n^\omega$; van den Brand (2020) derandomized the result.

Setting

Vectors are in $\mathbb R^n$ and products, quotients and roots of vectors are coordinatewise. For $\epsilon$ and vectors $a,b$, $a\approx_\epsilon b$ means $(1-\epsilon)b_i\le a_i\le(1+\epsilon)b_i$ for all $i$; $a\approx_\epsilon t$ for a scalar $t$ is defined likewise. The number of variables is $n\ge10$ and $A$ has full row rank $d\le n$.

The potential is $\Phi_\lambda(r)=\sum_{i=1}^n\cosh(\lambda r_i)$, evaluated at $r=\mu/t-1$ with $\mu=xs$; it is small exactly when every $x_is_i$ is close to $t$.

StochasticStep (Algorithm 1) takes positive $x,s$, a direction $\delta_\mu$, a sampling parameter $k$ and the output $\widetilde v$ of a data structure with $x/s\approx_{\epsilon_{\mathrm{mp}}}\widetilde v$. It rescales to $\overline x=x\sqrt{\widetilde v/w}$, $\overline s=s\sqrt{w/\widetilde v}$ ($w=x/s$), draws a sparse vector $\widetilde\delta_\mu$ with independent coordinates, $\widetilde\delta_{\mu,i}=\delta_{\mu,i}/p_i$ with probability $p_i=\min(1,k(\delta_{\mu,i}^2/\|\delta_\mu\|_2^2+1/n))$ and $0$ otherwise, and computes the step $(\widetilde\delta_x,\widetilde\delta_s)$ through the projection $\overline P=\sqrt{\overline X/\overline S}A^\top(A\frac{\overline X}{\overline S}A^\top)^{-1}A\sqrt{\overline X/\overline S}$. The draw is repeated until $\|\overline s^{-1}\widetilde\delta_s\|_\infty$ and $\|\overline x^{-1}\widetilde\delta_x\|_\infty$ are at most $1/(100\log n)$; the output is $(x+\widetilde\delta_x,s+\widetilde\delta_s)$.

Main (Algorithm 2) sets $\epsilon=\frac1{40000\log n}$, $\epsilon_{\mathrm{mp}}=\frac1{40000}$, $k=1000\epsilon\sqrt n\log^2n/\epsilon_{\mathrm{mp}}$, $\lambda=40\log n$, starts at $t=1$, and in each iteration sets $t^{\mathrm{new}}=(1-\frac{\epsilon}{3\sqrt n})t$, takes the direction

$$\delta_\mu=\Big(\frac{t^{\mathrm{new}}}{t}-1\Big)xs-\frac\epsilon2t^{\mathrm{new}}\frac{\nabla\Phi_\lambda(\mu/t-1)}{\|\nabla\Phi_\lambda(\mu/t-1)\|_2},$$

runs StochasticStep, and falls back to a deterministic ClassicalStep whenever $\Phi_\lambda(\mu^{\mathrm{new}}/t^{\mathrm{new}}-1)>n^3$.

Formalization targets

Goal: Lemma 4.14

For every iteration $j$, almost surely Assumption 4.1 holds for the input of iteration $j$ (in particular $x^js^j\approx_{0.1}t_j$ and $\|\delta_\mu\|_2\le\epsilon t_j$), almost surely the resampling loop of iteration $j$ succeeds with positive probability, and

$$\mathbb P(\text{ClassicalStep is used in iteration }j)\le\frac{10}{n^2}.$$

The paper writes $O(1/n^2)$; its proof gives the constant $10$.

Milestones

Lemma A.1 (variance of a product), Lemma 4.12 (properties of $\Phi_\lambda$), Lemma 4.2 (explicit step), Lemma 4.3 and Claim 4.7 (moments and success probability of the sampled step), Lemma 4.8 (moments of $\mu^{\mathrm{new}}$), and Lemma 4.13:

$$\mathbf E\Big[\Phi_\lambda\Big(\frac{\mu^{\mathrm{new}}}{t^{\mathrm{new}}}-1\Big)\Big]\le\Phi_\lambda\Big(\frac\mu t-1\Big)-\frac{\lambda\epsilon}{15\sqrt n}\Big(\Phi_\lambda\Big(\frac\mu t-1\Big)-10n\Big).$$

Significance

Lemma 4.14 is what makes the randomized method usable: the iterates stay in the $0.1$-neighbourhood of the central path along the whole run, and the expensive fallback is rare enough that its expected cost, $\widetilde O(n^{2.5})\cdot 10/n^2$, is negligible. The paper's cost bound (Lemma 4.16) and its main theorem rest on it. The same potential-based "stochastic central path" analysis was reused in later solvers, for instance for empirical risk minimization (Lee, Song and Zhang, COLT 2019).

The result is proved in the paper; no machine-checked version exists. A formalization pins down the probabilistic model that the paper leaves implicit (independence of the sampled coordinates, the law of the resampling loop, a data structure and fallback that see only the past) and checks the constants, several of which are tight against printed slack (Remark 4.4).

The running-time claims of the paper (Theorem 2.1's expected time $n^{\omega+o(1)}$, Lemma 4.16, Section 5) are not part of this mission: they live in an arithmetic cost model that Lean does not have. The accuracy guarantee of Theorem 2.1 (Lemma A.6, ClassicalStep from [57]) is also outside the mission.

Difficulty

The obvious argument would bound each quantity under the product law of the sparse direction. But StochasticStep resamples, so the step actually taken is distributed according to that law conditioned on a success event, and expectations and variances shift. A second difficulty is that $\Phi_\lambda$ is controlled only in expectation, while Assumption 4.1 must hold surely at every iteration; this is reconciled by the deterministic ClassicalStep fallback, which caps $\Phi_\lambda$ at $n^3$, and by an induction over iterations of $\mathbf E[\Phi]\le10n$ under the trajectory law. Claim 4.7 needs a Bernstein inequality, which Mathlib does not yet provide.

Formalization scope

Coordinates are Fin n, vectors Fin n → ℝ, $A$ a Matrix (Fin d) (Fin n) ℝ with A.rank = d, and $\log$ the natural logarithm. $\|\cdot\|_2$ is written out as $\sqrt{\sum_iv_i^2}$; $\|\cdot\|_\infty\le c$ is stated coordinatewise. The sampled direction has law Measure.pi of two-point laws; the step taken by StochasticStep has that law conditioned (ProbabilityTheory.cond) on the success event, and every $\mathbf E$, $\mathbf{Var}$ of Lemmas 4.3, 4.8 and 4.13 is under this conditioned law. mp.Query is replaced by its value $\overline P(\overline X\overline S)^{-1/2}\widetilde\delta_\mu$; the data structure and ClassicalStep are arbitrary measurable functions $U_j$, $C_j$ of the history with the only properties the paper uses. The trajectory is Mathlib's Ionescu-Tulcea measure, with kernels equal to the step law of Main. $n$ is the number of variables of the program the loop runs on.

Deviations from the page, all recorded in the items: Assumption 4.1 is used with $\epsilon\le1/(40000\log n)$ instead of the printed $<$, because Main sets $\epsilon$ to exactly that value; $O(1/n^2)$ is instantiated as $10/n^2$, the constant of the paper's proof; the conclusions of Lemma 4.14 are stated for every iteration index rather than while $t>\delta^2/(32n^3)$; at $\nabla\Phi_\lambda=0$ the second term of $\delta_\mu$ is $0$. No hypothesis $k\le n$ is imposed.

A trivializing formalization is ruled out: every statement that integrates against the conditioned law also concludes that this law is a probability measure (so it cannot be the zero measure), the goal concludes that each resampling loop succeeds with positive probability, the oracles $U_j$, $C_j$ cannot see the coins of the current iteration, and the goal is about the whole iterated process from the initial point, not one step from an arbitrary law.

Contributions welcome: a Bernstein inequality for bounded independent sums, conditional-law lemmas for cond of Measure.pi, and Markov-kernel measurability for the step law; these are reusable beyond this mission.

Selected references

• M. B. Cohen, Y. T. Lee, Z. Song, Solving Linear Programs in the Current Matrix Multiplication Time, J. ACM 68(1), Article 3, 2021. https://doi.org/10.1145/3424305 (arXiv:1810.07896, https://arxiv.org/abs/1810.07896)
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984. https://doi.org/10.1007/BF02579150
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40, 1988. https://doi.org/10.1007/BF01580724
• P. M. Vaidya, Speeding-up linear programming using fast matrix multiplication, Proc. 30th FOCS, 1989.
• Y. T. Lee, A. Sidford, Path finding methods for linear programming, FOCS 2014. https://doi.org/10.1109/FOCS.2014.52
• Y. T. Lee, Z. Song, Q. Zhang, Solving Empirical Risk Minimization in the Current Matrix Multiplication Time, COLT 2019. https://arxiv.org/abs/1905.04447
• J. van den Brand, A deterministic linear program solver in current matrix multiplication time, SODA 2020. https://doi.org/10.1137/1.9781611975994.16