Linear Optimization

Pooling inventory among independent retailers

Retailers that sell the same product can raise their joint profit by pooling: stock left over at one location is shipped to meet unmet demand at another, and stock can be held in shared warehouses until demand is known (Eppen 1979; Eppen and Schrage 1981). When the retailers are independent firms, pooling creates two questions at once. After demand is realized, the extra profit from shipping must be split in a way no group of retailers would reject. Before demand is realized, each retailer chooses its own stock, and that choice depends on how the split will be made. A split that is fair ex post may lead to stocking decisions that are poor for the system as a whole.

Anupindi, Bassok and Zemel (MSOM 2001) model the ex-post split as a cooperative game, the ex-ante stocking as a non-cooperative game, and ask whether a single allocation rule can serve both. Their framework is a standard reference for "coopetition" models in supply chains, where firms compete on stocking decisions and cooperate on redistribution.

Setting

There are retailers $\mathcal N=\{1,\dots,N\}$ and warehouses $\mathcal W=\{1,\dots,W\}$. Retailer $n$ has unit cost $c_n$, revenue $r_n$ and salvage value $v_n$; warehouse $w$ has purchasing cost $c_w$ and salvage value $v_w$. Shipping from location $i$ to retailer $n$ costs $t_{i,n}$ per unit, and a fraction $\beta_{i,n}\in[0,1]$ of the customers at $n$ accept service from $i$.

Before demand, retailer $n$ chooses a position $\vec Z_n=(X_n,Y_{1,n},\dots,Y_{W,n})$: local stock $X_n$ and claims $Y_{w,n}$ on warehouse stock, so warehouse $w$ holds $Y_w=\sum_nY_{w,n}$. A profile is $[Z]=(\vec Z_1,\dots,\vec Z_N)$. Demand $\vec D$ is random with law $\mu$. After demand, retailer $n$ has local sales $S_n=\min\{X_n,D_n\}$, residual inventory $H_n=\max\{X_n-D_n,0\}$ and residual demand $E_n=\max\{D_n-X_n,0\}$.

The snapshot allocation game SAG$([Z],\vec D)$ gives each coalition $\mathcal S\subseteq\mathcal N$ the value $W^*_{\mathcal S}([Z],\vec D)$: the optimal value of the linear program (6), which ships $q_{i,n}$ units from $i\in\mathcal S\cup\mathcal W$ to $n\in\mathcal S$ at profit $r_n-v_i-t_{i,n}$ per unit, subject to $\sum_nq_{i,n}\le H_i$, $\sum_nq_{w,n}\le\sum_{n\in\mathcal S}Y_{w,n}$ and $\sum_iq_{i,n}/\beta_{i,n}\le E_n$. Its core is the set of allocations $\alpha$ with $\sum_{j\in\mathcal S}\alpha_j\ge W^*_{\mathcal S}$ for every $\mathcal S$ and $\sum_{j\in\mathcal N}\alpha_j=W^*_{\mathcal N}$ (7).

An allocation rule AR-$m$ assigns surplus $\alpha^m_n([Z],\vec D)$; retailer $n$ earns

$$P^m_n([Z],\vec D)=r_nS_n+v_nH_n-c_nX_n-\sum_w(c_w-v_w)Y_{w,n}+\alpha^m_n([Z],\vec D)\qquad(9)$$

and expects $J^m_n([Z])=E_{\vec D}P^m_n$. A Nash equilibrium (10) is a profile at which no retailer gains by changing its own position. The first-best profile $[Z]^{c*}$ maximizes the expected centralized profit $J^c_{\mathcal N}([Z])=E_{\vec D}P^c_{\mathcal N}([Z],\vec D)$, where $P^c_{\mathcal N}=\sum_n[r_nS_n+v_nH_n-c_nX_n]-\sum_w(c_w-v_w)Y_w+W^*_{\mathcal N}$.

The fractional rule AR-f (11) pays $\alpha^f_n=\theta_nP^c_{\mathcal N}-[\,r_nS_n+v_nH_n-c_nX_n-\sum_w(c_w-v_w)Y_{w,n}]$ with fixed shares $\theta_n\in(0,1)$, $\sum_n\theta_n=1$. The dual allocation (8) is $\alpha^d_n=\nu_nH_n+\sum_w\gamma_wY_{w,n}+\delta_nE_n$ for optimal dual prices $(\nu,\gamma,\delta)$ of (6) for $\mathcal N$. The modified rule AR-c is $\alpha^c_n([Z],\vec D)=\alpha^f_n([Z],\vec D)+w_n([Z]^{c*},\vec D)$ with $w_n=\alpha^d_n([Z]^{c*},\cdot)-\alpha^f_n([Z]^{c*},\cdot)$.

Formalization targets

Goal: Corollary 5.1 (p. 361)

For a first-best profile $[Z]^{c*}$ and a measurable choice of dual prices at $[Z]^{c*}$,

$$[Z]^{c*}\ \text{is a pure Nash equilibrium under AR-c, and}\ \ \alpha^c([Z]^{c*},\vec D)\in\operatorname{Core}\big(\mathrm{SAG}([Z]^{c*},\vec D)\big)\ \ \forall\vec D,$$

with integrable side payments.

Milestones

• Examples 1 and 2 (pp. 358–359): a transfer-price allocation outside the core; the dual allocation $(8,8,8,0)$ and the non-dual core allocation $(0,0,0,24)$.
• Theorem 4.1 (p. 358): if all inventory is claimed, the core of SAG$([Z],\vec D)$ is nonempty and contains the dual allocation (8) for every optimal dual.
• Theorem 5.2 (p. 361): under AR-f every first-best profile is a Nash equilibrium.
• Theorem 5.1 (p. 361): for any rule and any of its equilibria $[Z]^{m*}$ there are integrable demand-dependent side payments that leave the set of equilibria unchanged and put the allocations at $[Z]^{m*}$ in the core for every $\vec D$.

Significance

The goal answers the paper's central question positively: there is an allocation mechanism under which the centrally optimal stock levels are an equilibrium of the decentralized stocking game, while every ex-post split of the pooling surplus is stable against all coalitions. Theorem 4.1 is the ex-post half: shadow prices of the shipping LP give a stable split for every realization, independently of who owns which units. The paper also shows (Proposition 5.1, not included here) that the dual allocation alone does not induce first-best stocking, which is why the side payments of Theorem 5.1 are needed.

The results are proved in the paper; Theorem 4.1 is proved there only by reference to the LP-game literature (Owen 1975; Samet and Zemel 1984). None of them has a machine-checked proof. The mission would produce the first formal treatment on Prove2Me of a linear-production (LP) game and its core, and of a model combining a cooperative second stage with a non-cooperative first stage.

Difficulty

Theorem 4.1 is an instance of Owen's theorem on LP games, but the instance is not a standard linear production game: coalition LPs have variables only on arcs inside the coalition, warehouse capacity is limited to the coalition's own claims, and the acceptance constraint divides by $\beta_{i,n}$, which may be zero, so the general theorem cannot be quoted as it stands. The paper leaves the dual of (6) unwritten, and Mathlib has no ready-made LP duality in this form.

The stochastic layer is the other obstacle. Expected payoffs are integrals, and the side payment is built from a choice of dual prices for each demand realization. Its integrability requires measurability of that choice and of the LP value as a function of demand; neither is given by the paper, which treats the side payments as "constants".

Formalization scope

Retailers are Fin N, warehouses Fin W, locations Fin N ⊕ Fin W; quantities, prices and demands are real numbers; demand is a probability measure on Fin N → ℝ; expectations are Bochner integrals. $W^*_{\mathcal S}$ is the real supremum of (6a) over the feasible set, and profiles are required to be nonnegative, which makes the feasible set nonempty and bounded. Arcs with $\beta_{i,n}=0$ carry no shipment. The core is the platform definition Supermodularity.Cooperative.Core. The dual of (6) is written out explicitly (the paper does not state it). The paper's continuous-CDF assumption is not used and is dropped.

Pinned readings:

1. "Dual prices" means any optimal solution of the dual of (6) for $\mathcal N$; Theorem 4.1 is stated for every such solution.
2. "Induces the same equilibrium inventory levels as the first-best" (Theorem 5.2) and "the NE using $\alpha^c$ is first-best" (Corollary 5.1) are stated as "every first-best profile is a Nash equilibrium", the direction the proofs give.
3. "$[Z]^{\tilde m*}=[Z]^{m*}$" (Theorem 5.1) is stated as equality of the two sets of equilibria; the continuity and unimodality assumptions, which only guarantee existence of an equilibrium, are dropped because the equilibrium is a hypothesis.
4. "An appropriate way of breaking ties" is a measurable choice of optimal dual prices; demand is almost surely nonnegative; the rule's payoffs in Theorem 5.1 are integrable.
5. The shares $\gamma_n$ of Theorem 5.2 are written $\theta_n$, and Eq. (11) is used with $+v_nH_n$ in the bracket (printed $-v_nH_n$), as the proof on p. 367 requires.

Not acceptable: a core without the efficiency equation (7b); a feasible set that lets $q_{i,n}/0=0$ sell to customers who balk; an arbitrary side payment instead of the constructed one; or a Nash equilibrium evaluated through non-integrable payoffs, whose Bochner integral is $0$ and makes every profile an equilibrium.

Useful infrastructure: finite-dimensional LP duality in inequality form, measurable selection of LP optimal solutions, and continuity of LP values in the right-hand side. All of it can be reused in other LP-game and two-stage stochastic programming missions.

Selected references

• R. Anupindi, Y. Bassok, E. Zemel, A General Framework for the Study of Decentralized Distribution Systems, Manufacturing & Service Operations Management 3(4):349–368, 2001. https://doi.org/10.1287/msom.3.4.349.9973
• G. Owen, On the core of linear production games, Mathematical Programming 9:358–370, 1975. https://doi.org/10.1007/BF01681356
• D. Samet, E. Zemel, On the core and dual set of linear programming games, Mathematics of Operations Research 9(2):309–316, 1984. https://doi.org/10.1287/moor.9.2.309
• G. D. Eppen, Effects of centralization on expected costs in a multi-location newsboy problem, Management Science 25(5):498–501, 1979. https://doi.org/10.1287/mnsc.25.5.498

Motivation

A Fisher market is the simplest model of a market in which prices are set by supply and demand: buyers bring money, sellers bring goods, and a price vector is an equilibrium when every buyer, spending her money optimally at those prices, leaves every good exactly sold out. Computing equilibria is one of the central questions of algorithmic game theory, because a polynomial-time algorithm is what would make the equilibrium concept usable as a prediction or as a pricing mechanism.

For linear utilities an equilibrium always exists, is rational, and can be computed in polynomial time (Eisenberg and Gale 1959; Devanur, Papadimitriou, Saberi and Vazirani, J. ACM 2008, https://doi.org/10.1145/1411509.1411512). The next natural class, additively separable, piecewise-linear, concave utilities, captures diminishing marginal utility and is the class studied by Vazirani and Yannakakis (J. ACM 58(3), Article 10, 2011, https://doi.org/10.1145/1970392.1970394). Their paper shows that equilibria in this class are hard to compute (PPAD-complete) and that deciding whether one exists is NP-complete. Both results rest on a structural fact proved first: whenever such a market has an equilibrium at all, it has one whose prices are rational numbers of polynomial bit length. That fact is the subject of this mission.

Timeline:

• 1959, Eisenberg and Gale: a convex program whose optimal solutions are the equilibria of linear Fisher markets; equilibrium prices are rational.
• 2008, Devanur, Papadimitriou, Saberi and Vazirani: a combinatorial polynomial-time algorithm for linear Fisher markets, based on a max-flow test of candidate prices.
• 2009, Chen, Dai, Du and Teng, and Chen and Teng (FOCS 2009; ISAAC 2009): PPAD-hardness for additively separable piecewise-linear concave utilities in Arrow–Debreu and Fisher markets.
• 2011, Vazirani and Yannakakis: rationality of equilibria with polynomial bit size (Theorem 4.1 for Fisher markets, Theorem 5.1 for Arrow–Debreu markets), PPAD membership, and NP-completeness of existence.

Setting

There are $n$ buyers $B=\{1,\dots,n\}$ and $g$ divisible goods $G=\{1,\dots,g\}$, one unit of each good. Buyer $i$ has a rational budget $e(i)>0$. For each buyer $i$ and good $j$ a function $f^i_j:\mathbb R_+\to\mathbb R_+$ gives the utility that $i$ derives from an amount of good $j$. It is piecewise linear and concave: it is given by a finite list of bounded segments $(c_1,a_1),\dots,(c_m,a_m)$ with rational amounts $a_k>0$, followed by a last, unbounded segment, with rational slopes $c_1\ge c_2\ge\dots\ge c_m\ge c_\infty\ge 0$. The function has slope $c_k$ on $[a_1+\dots+a_{k-1},\,a_1+\dots+a_k]$ and slope $c_\infty$ afterwards. Buyer $i$'s utility for a bundle $x=(x_1,\dots,x_g)$ is additively separable:

$$u_i(x)=\sum_{j\in G}f^i_j(x_j).$$

Given prices $p\in\mathbb R^g_{\ge0}$, a bundle $x\ge0$ is optimal for buyer $i$ if $\sum_jp_jx_j\le e(i)$ and no bundle $y\ge0$ with $\sum_jp_jy_j\le e(i)$ has $u_i(y)>u_i(x)$. The prices $p$ are equilibrium prices if there is an allocation $(x_{ij})$ that gives each buyer an optimal bundle and sells every good exactly: $\sum_ix_{ij}=1$ for every $j$.

The bit size of a rational number $a/b$ in lowest terms is the binary length of $|a|$ plus that of $b$. The encoding size $\|M\|$ of a market $M$ is $n+g$ plus the bit sizes of all budgets, slopes and amounts, plus the number of bounded segments.

For the intermediate results, fix positive prices $p$. The bang per buck of a segment $s$ of good $j$ is $\mathrm{slope}(s)/p_j$ and its value is $\mathrm{amount}(s)\cdot p_j$ (infinite for an unbounded segment). Sorting buyer $i$'s segments by decreasing bang per buck into classes of equal bang per buck, the first class at which the cumulative value exceeds $e(i)$ is her flexible class. Segments of strictly larger bang per buck are forced, the others undesirable. From these the paper defines $\mathrm{spent}(i)$ (value of the forced segments), $\mathrm{unspent}(i)=e(i)-\mathrm{spent}(i)$, $\mathrm{unsold}(j)$ (the part of good $j$ not taken by forced segments), and a network $N(p)$ from a source through goods and buyers to a sink.

Formalization targets

Goal: Theorem 4.1 (p. 10:9)

There is a polynomial $P$ such that for every Fisher market $M$ as above,

$$M\text{ has equilibrium prices }p\in\mathbb R^g\ \Longrightarrow\ M\text{ has equilibrium prices }q\in\mathbb Q^g\text{ with }\sum_{j}\operatorname{bits}(q_j)\le P(\|M\|).$$

The polynomial is fixed before the market. Nothing beyond the existence of some real equilibrium is assumed.

Milestones

1. Lemma 3.1 (p. 10:8). For positive prices with $\sum_jp_j=\sum_ie(i)$, $\mathrm{unspent}\ge0$ and $\mathrm{unsold}\ge0$: $p$ are equilibrium prices iff the max-flow value of $N(p)$ is $\sum_i\mathrm{unspent}(i)$.
2. Proof of Theorem 4.1, first sentence (p. 10:9). From a positive equilibrium $p'$ with $\sum_jp'_j=\sum_ie(i)$, build the linear program of §4, whose variables are prices and flows and whose combinatorial data are fixed by $p'$. Then $p'$, with a suitable flow, is an optimal solution of value $\sum_ie(i)$.
3. §4, second paragraph (p. 10:8). Every optimal solution of that LP with positive prices gives equilibrium prices.

Significance

The result is what makes the existence problem for these markets a problem in NP: a rational equilibrium of polynomial size is a certificate that can be checked, with Lemma 3.1, by one max-flow computation. The same rationality statement underlies the paper's PPAD-membership proof and its NP-completeness result for existence. It also marks the boundary with markets whose equilibria can be irrational, as happens for some non-separable utilities. In that sense it shows that separable piecewise-linear concave utilities keep the "linear" character of the problem even though computing an equilibrium becomes hard.

All three statements are proved in the source, and none of them has a machine-checked proof on the platform or, as far as is known, anywhere else. The mission produces the first formal account of piecewise-linear Fisher markets: the model, the forced/flexible/undesirable classification of segments, the max-flow test for equilibrium, and the linear program of §4. It also forces precision where the paper is informal. The §4 bang-per-buck inequalities are printed with their directions reversed, and the claim about optimal LP solutions needs positive prices. The formal statements record each of these choices.

Difficulty

The obvious argument is: "equilibria are solutions of a linear system, so a rational one exists". It fails as stated, because the set of equilibrium prices is not a polyhedron. Which segments a buyer buys depends on the prices themselves, through the ordering of the ratios $\mathrm{slope}/p_j$, so the equilibrium conditions are a finite union of polyhedral pieces glued along the price-dependent ordering. The work is to freeze the combinatorial structure of one given equilibrium and to show that the resulting fixed linear program still certifies equilibrium at every one of its optimal points. That second step is what Lemma 3.1 is for. The polynomial bit bound then needs a quantitative bound on the vertices of a rational LP, uniform in the market's encoding.

Formalization scope

Buyers and goods are Fin n and Fin g. Budgets, slopes and amounts are rationals (ℚ). Prices and allocations are reals (ℝ), so that "admits rational prices" is a real conclusion: the goal returns q : Fin g → ℚ whose cast is an equilibrium. The committed conventions are:

• each good has unit supply;
• budgets are positive;
• each $f^i_j$ is a list of (slope, amount) pairs of bounded segments together with the slope of its last, unbounded segment ("the last (infinite) segment", §6), with nonnegative slopes, positive amounts and nonincreasing slopes, stored inside the market structure;
• the unbounded segment has infinite value and, when flexible, gives its network edge infinite capacity; this is encoded logically (no upper bound on that edge);
• equilibrium requires exact clearing of every good, which by the paper's footnote 3 gives the same equilibrium prices as leaving zero-price goods partly unsold;
• the classes $Q_l$ are represented by the bang per buck of the flexible class, not by an index;
• parallel network edges are merged;
• max-flow is the supremum of the values of feasible flows on the good–buyer edges.

Hypotheses added relative to the page, each disclosed in its statement:

• positivity of the LP solution's prices (milestone 3).

The §2 condition on p. 10:7 is a sufficient condition for existence and is deliberately not a hypothesis of the goal, which assumes only that an equilibrium exists. Complexity-class statements ("in NP", "PPAD-complete") are out of scope. What is formalized is the explicit polynomial bit bound, with a polynomial chosen before the market. A goal with the polynomial chosen after the market, an encoding size that ignores the bits of the data, or an equilibrium notion without utility-maximizing bundles would be trivially satisfiable. The statements rule all three out.

Beyond this mission, a complete development needs LP theory with rational data: existence of optimal basic solutions and determinant bounds on their bit size. Existing platform results that may serve as substrate include SmaleNinth.exists_square_subsystem and SmaleNinth.abs_det_le_factorial_mul_pow. Contributions welcome: proofs of the milestones, a reusable bit-size theory for rational LP vertices, and the Arrow–Debreu analogue (Theorem 5.1).

Selected references

• V. V. Vazirani and M. Yannakakis, Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities, J. ACM 58(3), Article 10, 2011. https://doi.org/10.1145/1970392.1970394
• N. R. Devanur, C. H. Papadimitriou, A. Saberi and V. V. Vazirani, Market Equilibrium via a Primal–Dual Algorithm for a Convex Program, J. ACM 55(5), 2008. https://doi.org/10.1145/1411509.1411512
• E. Eisenberg and D. Gale, Consensus of Subjective Probabilities: The Pari-Mutuel Method, Ann. Math. Statist. 30(1), 1959. https://doi.org/10.1214/aoms/1177706369
• X. Chen, D. Dai, Y. Du and S.-H. Teng, Settling the Complexity of Arrow–Debreu Equilibria in Markets with Additively Separable Utilities, FOCS 2009. https://doi.org/10.1109/FOCS.2009.29
• W. C. Brainard and H. E. Scarf, How to Compute Equilibrium Prices in 1891, Cowles Foundation Discussion Paper 1272, 2000. https://cowles.yale.edu/research/cfdp-1272

Motivation

Interior point methods for a linear program $\min\{c^\top x : Ax\ge b\}$ with $A\in\mathbb R^{m\times n}$ follow the central path of the logarithmic barrier $-\sum_i\log s_i$, where $s=Ax-b$ is the slack vector. Renegar's path-following analysis (1988) gives $O(\sqrt m\,L)$ iterations, and for decades this was the best bound for methods whose iterations cost a linear system solve. Vaidya's volumetric barrier $-\log\det(A^\top S^{-2}A)$ and the hybrid volumetric barriers of Vaidya and of Anstreicher (references [45] and [2] of the paper) reached $O((m\,\mathrm{rank}(A))^{1/4}L)$ iterations at the price of more expensive linear algebra. Nesterov and Nemirovski showed that a universal barrier gives $O(\sqrt n\,L)$ iterations, but that barrier cannot be evaluated efficiently.

Lee and Sidford (FOCS 2014; full version arXiv:1312.6677) obtained $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ iterations, each costing $\tilde O(1)$ linear system solves, by following a weighted central path whose weights are recomputed from the slacks. The weights come from a weight function $g$, defined as the minimizer of a regularized D-optimal-design problem. This mission is about that weight function and the theorem (Theorem 1 of the paper) certifying its properties. The companion mission, Path-Finding Methods for Linear Programming I, formalizes the path-following framework (Theorem 5 of §IV.C) that consumes these properties.

Setting

Fix $A\in\mathbb R^{m\times n}$ with full column rank, $\mathrm{rank}(A)=n$, and $1\le n<m$. For vectors $s,w\in\mathbb R^m_{>0}$ write $S=\mathrm{diag}(s)$, $W=\mathrm{diag}(w)$, $W^\alpha=\mathrm{diag}(w_i^\alpha)$, and $A_s=S^{-1}A$. For a matrix $M$ let $\|v\|_M=\sqrt{v^\top Mv}$.

Projection matrix and slack sensitivity (Definition 2, p. 428). The projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A\,(A^\top S^{-1}WS^{-1}A)^{-1}A^\top S^{-1}W^{1/2}$, and the slack sensitivity is

$$\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\mathbb 1_i\big\|_{P_{S^{-1}A}(w)} .$$

Weight function (Definition 4, p. 428). A map $g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ is a weight function with constants $c_1,c_\gamma,c_r$ if it is differentiable and, for every $s>0$, with $G(s)=\mathrm{diag}(g(s))$, $G'(s)$ the Jacobian of $g$ at $s$, and $\|y\|_{G(s)}=\sqrt{\sum_ig_i(s)y_i^2}$:

1. Size: $\|g(s)\|_1\le c_1$;
2. Slack sensitivity: $c_\gamma\ge1$ and $\gamma(s,g(s))\le c_\gamma$;
3. Step consistency: $c_r\ge1$ and for all $r\ge c_r$, $y\in\mathbb R^m$: $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ and $\|y+r^{-1}G^{-1}G'Sy\|_\infty\le\|y\|_\infty+c_r\|y\|_{G(s)}$;
4. Uniformity: $\|g(s)\|_\infty\le2$.

The regularized objective (6), p. 429. For $\alpha,\beta\in\mathbb R$,

$$\hat f(s,w)=\mathbb 1^\top w-\frac1\alpha\log\det\big(A_s^\top W^\alpha A_s\big)-\beta\sum_{i\in[m]}\log w_i ,\qquad g(s)=\arg\min_{w\in\mathbb R^m_{>0}}\hat f(s,w).$$

At $\alpha=1,\beta=0$ this is the D-optimal design problem, dual to computing the John ellipsoid of the polytope $\{y:|[A(y-x)]_i|\le s_i\}$ (§V.B).

Formalization targets

Goal: Theorem 1 (Properties of Weight Function), §V.A, p. 429

With

$$\alpha=1-\Big(\log_2\frac{2m}{\mathrm{rank}(A)}\Big)^{-1},\qquad \beta=\frac{\mathrm{rank}(A)}{2m},$$

the objective $\hat f(s,\cdot)$ has a unique minimizer over $\mathbb R^m_{>0}$ for every $s>0$, and the resulting $g$ is a weight function with

$$c_1(g)=2\,\mathrm{rank}(A),\qquad c_\gamma(g)=2,\qquad c_r(g)=2\log_2\frac{2m}{\mathrm{rank}(A)} .$$

Milestones: the three bullets of Theorem 1

• Size: every minimizer $w$ of $\hat f(s,\cdot)$ satisfies $\|w\|_1\le2\,\mathrm{rank}(A)$.
• Slack sensitivity: every minimizer $w$ satisfies $\gamma(s,w)\le2$.
• Step consistency: any map $g$ selecting a minimizer at every $s>0$ is differentiable on $\mathbb R^m_{>0}$ and satisfies the two step-consistency inequalities for every $r\ge2\log_2\frac{2m}{\mathrm{rank}(A)}$.

A supporting (non-milestone) item states the existence and uniqueness of the minimizer on its own.

Significance

The result. Theorem 1 is the input that turns the weighted path-following framework into an $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$-iteration method: the framework needs $O(c_\gamma^{-1}c_r^{-3}c_1^{-1/2})$-sized steps in $t$ (p. 428), and Theorem 1 makes that $\tilde\Omega(1/\sqrt{\mathrm{rank}(A)})$. The step consistency bound is what allows the weights to be recomputed after each Newton step without losing centrality. The same construction underlies later work on Lewis-weight barriers and on fast approximate John ellipsoids and maximum flow (§VIII of the paper).

Formalizing it. The theorem is proved in the full version of the paper (arXiv:1312.6677); the FOCS extended abstract contains no proofs. No part of it has a machine-checked proof. A complete formalization would give a verified account of leverage-score calculus (sums of leverage scores equal the rank; derivatives of projection matrices), of the convexity of $w\mapsto-\log\det(A^\top W^\alpha A)$ for $\alpha\in(0,1)$, and of differentiability of an argmin via the implicit function theorem, none of which is currently packaged in Mathlib in this form.

Difficulty

Size and slack sensitivity are statements about the minimizer, which is only characterized implicitly; they require precise matrix calculus for $\log\det(A_s^\top W^\alpha A_s)$ and a comparison between the matrices $A^\top WA$ (which defines $\gamma$) and $A^\top W^\alpha A$ (which defines $g$). The specific values of $\alpha$ and $\beta$ matter here: the unregularized choice $\alpha=1$, $\beta=0$ makes the problem degenerate (p. 429).

The hard part is step consistency. The Jacobian $G'$ of an argmin is available only implicitly, as the solution of a linear system obtained by differentiating the optimality condition. A bound on $\|G'\|$ that depends on $m$ is easy to get and useless: the theorem needs the operator norm of $I+r^{-1}G^{-1}G'S$ in the $G(s)$-norm to be at most $1$ as soon as $r$ exceeds $2\log_2(2m/\mathrm{rank}(A))$, and an $\ell_\infty$ bound with only an additive $c_r\|y\|_{G(s)}$ loss.

Existence and differentiability of the minimizer are conclusions, not hypotheses. The minimization is over an open orthant on which the objective is not obviously coercive or strictly convex for $\alpha<1$, and differentiability of $g$ requires the Hessian of $\hat f$ at the minimizer to be invertible.

Formalization scope

Vectors are Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; inverses are Matrix.inv, $\log\det$ is Real.log (Matrix.det …), $w_i^\alpha$ is Real.rpow, $\log_2$ is Real.logb 2, the Jacobian is fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm on Fin m → ℝ.

Conventions and pinned hypotheses:

• Full column rank A.rank = n is assumed in every theorem. The paper never states it, but without it $A_s^\top W^\alpha A_s$ is singular and every formula is undefined (in Lean, Matrix.inv and Real.log would return junk $0$).
• $1\le n<m$. $\beta=\mathrm{rank}(A)/(2m)$ and $\log_2(2m/\mathrm{rank}(A))$ need $\mathrm{rank}(A)\ge1$; at $m=\mathrm{rank}(A)$ the page's $\alpha$ is $0$ and $1/\alpha$ in (6) is undefined.
• Reading of $\alpha$: the exponent $-1$ is the reciprocal of $\log_2\frac{2m}{\mathrm{rank}(A)}$, giving $\alpha\in(0,1)$.
• Size is an upper bound $\|g(s)\|_1\le c_1$ (the paper's weight function has $\|g(s)\|_1=\tfrac32\mathrm{rank}(A)$, while Theorem 1 reports $c_1=2\,\mathrm{rank}(A)$).
• The first step-consistency bullet (an operator-norm bound) is stated for every vector $y$.
• $g$ is any map $\mathbb R^m\to\mathbb R^m$ whose value at each positive $s$ minimizes $\hat f(s,\cdot)$ over $\mathbb R^m_{>0}$. Only its values on the open orthant matter. The goal also asserts that such minimizers exist and are unique, so it is not vacuous.

Ruling out trivializations: the goal does not assume $g$ to be a weight function or to be differentiable, and it does not replace $g$ by an arbitrary weight function; differentiability is a conclusion (a predicate using fderiv without it would make step consistency hold vacuously wherever $g$ fails to be differentiable).

Useful infrastructure, reusable beyond this mission: leverage scores and their sum; derivatives of $w\mapsto\log\det(A^\top WA)$ and of projection matrices; convexity of $-\log\det(A^\top W^\alpha A)$ in $w$ (related to the published ConvexOptimization.log_det_concaveOn); differentiability of the argmin of a strictly convex smooth function. Contributions of these as separate theorems are welcome, as is a proof of any single bullet of Theorem 1.

Selected references

• Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
• Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv, 2013. https://arxiv.org/abs/1312.6677
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40 (1988). https://doi.org/10.1007/BF01580724

Motivation

The minimum-cost circulation problem is a central problem of network optimization: transportation, assignment, shortest-path and maximum-flow problems are all special cases, and it is one of the few classes of linear programs with fast combinatorial algorithms. The oldest algorithm for it, the cycle-canceling algorithm of Klein (1967), repeatedly finds a residual cycle of negative cost and pushes as much flow as possible around it. With an arbitrary choice of cycle it can take exponentially many iterations even on integer data, and it need not terminate at all when capacities are irrational.

Goldberg and Tarjan (J. ACM 36(4), 1989) showed that one simple selection rule repairs this: always cancel a residual cycle whose mean cost (cost divided by number of arcs) is as small as possible. The resulting algorithm is strongly polynomial: its number of iterations is bounded by a polynomial in the number of vertices and arcs alone, independent of the magnitudes of capacities and costs. This mission formalizes that bound.

Timeline:

• 1967, Klein: the cycle-canceling algorithm, without an iteration bound.
• 1972, Edmonds and Karp: the first polynomial algorithm for minimum-cost flow (capacity scaling), polynomial in the bit length of the capacities.
• 1985, Tardos: the first strongly polynomial algorithm, introducing the arc-fixing idea that Theorem 3.8 generalizes.
• 1987–1989, Goldberg and Tarjan: generalized cost scaling and ε-optimality; in this paper, minimum-mean cycle canceling terminates after O(nm² log n) iterations for real costs (Theorem 3.9) and O(nm log(nC)) for integer costs bounded by C (Theorem 3.7).

Setting

A circulation network is a finite directed graph $G=(V,E)$ with $n=|V|$ vertices and $m=|E|$ arcs, which is symmetric ($(v,w)\in E$ iff $(w,v)\in E$, so $m$ counts both directions), together with real capacities $u(v,w)$ and real costs $c(v,w)$, the cost being antisymmetric: $c(v,w)=-c(w,v)$.

A circulation is a real function $f$ on arcs satisfying $f(v,w)\le u(v,w)$, $f(v,w)=-f(w,v)$ on every arc, and conservation $\sum_{v:(w,v)\in E} f(v,w)=0$ at every vertex $w$. Its cost is $\operatorname{cost}(f)=\tfrac12\sum_{(v,w)\in E}c(v,w)f(v,w)$, and $f$ is minimum-cost (optimal) if no circulation has smaller cost.

The residual capacity of an arc is $u_f(v,w)=u(v,w)-f(v,w)$; arcs with $u_f>0$ are residual arcs. A residual cycle is a simple cycle of residual arcs; its capacity is the minimum residual capacity along it, its cost $c(\Gamma)$ is the sum of its arc costs, and its mean cost is $c(\Gamma)/|\Gamma|$. Canceling a residual cycle raises the flow on each of its arcs by its capacity (and lowers the flow on each reverse arc by the same amount).

The minimum-mean cycle-canceling algorithm starts from any circulation and, while some residual cycle has negative cost, cancels a residual cycle whose mean cost is minimum among all residual cycles. Ties are broken arbitrarily, so the algorithm is a nondeterministic process; a run of length $K$ is any sequence $f_0,\dots,f_K$ of circulations produced by $K$ such iterations.

The analysis uses a price function $p:V\to\mathbb R$, the reduced cost $c_p(v,w)=c(v,w)+p(v)-p(w)$, and ε-optimality: for $\varepsilon\ge0$, $f$ is ε-optimal if some $p$ gives $c_p(v,w)\ge-\varepsilon$ on every residual arc. The quantity $\varepsilon(f)$ is the least such $\varepsilon$, and an arc is ε-fixed if all ε-optimal circulations carry the same flow on it.

Formalization targets

Goal: Theorem 3.9, with the proof's constant

For every circulation network with $n\ge2$ vertices, $m$ arcs, arbitrary real capacities and arbitrary real antisymmetric costs, every run of the minimum-mean cycle-canceling algorithm has length

$$K\ \le\ n\,m^2\,\lceil \ln n+1\rceil .$$

The statement quantifies over all starting circulations, all tie-breaking choices and all real data; it is the paper's $O(nm^2\log n)$ with the constant its proof establishes.

Milestones

In the order the proof uses them: Theorem 2.1 (optimal iff no negative residual cycle), Theorem 3.1 (optimal iff some price function has $c_p\ge0$ on residual arcs), Theorem 3.3 ($\varepsilon(f)=-\mu(f)$ for nonoptimal $f$, where $\mu(f)$ is the minimum cycle mean of the residual graph), Lemma 3.5 (a minimum-mean cancellation does not increase $\varepsilon(f)$), Lemma 3.6 ($m$ cancellations shrink $\varepsilon(f)$ by a factor $1-1/n$), and Theorem 3.8 (an arc with $|c_p(v,w)|\ge2n\varepsilon$ is ε-fixed).

Significance

Theorem 3.9 shows that a classical, natural algorithm is strongly polynomial: its iteration count depends only on the combinatorial size of the network. Combined with Karp's $O(nm)$ minimum-mean cycle algorithm it yields an $O(n^2m^3\log n)$ strongly polynomial algorithm (Theorem 3.10), and its method, measuring progress by the minimum cycle mean and fixing arcs once $\varepsilon(f)$ is small, underlies the faster cancel-and-tighten algorithm of Section 4 and later strongly polynomial analyses of network-flow and related algorithms.

The theorem has been proved since 1989; this mission's contribution is a machine-checked proof. To the best of the platform's catalogue, no cycle-canceling bound, minimum cycle mean or ε-optimality statement has been formalized. The platform does hold the negative-cycle optimality criterion in a different model (LinearOptimization.network_no_negative_cycle_optimal, Bertsimas–Tsitsiklis Theorem 7.6, with nonnegative flows and supplies) and a flow decomposition theorem (LinearOptimization.network_flow_decomposition); both are related to milestones here but are stated for a different network model.

Difficulty

The obvious potential function, the cost of the circulation, decreases at every iteration but by amounts that depend on the data, so it yields no bound independent of the capacities and costs. The analysis instead has to track $\varepsilon(f)$, an infimum over price functions, and relate it to the minimum cycle mean of a residual graph that changes after each cancellation, including arcs that appear only because of earlier cancellations. The strongly polynomial part needs a second ingredient: showing that the flow on some arc never changes again, which requires comparing the current circulation with all other ε-optimal circulations of the network, not only those the algorithm visits.

Formalization scope

Vertices form a finite type V; the arc set is E : Finset (V × V); capacities, costs and flows are real functions V → V → ℝ read only on E. $n$ is Fintype.card V and $m$ is E.card, counting $(v,w)$ and $(w,v)$ separately, as in the paper. Cycles are nonempty duplicate-free vertex lists, whose arcs are the cyclically consecutive pairs; one- and two-vertex cycles are allowed and have cost $0$. Minimum mean is taken over all residual simple cycles of the current circulation. $\varepsilon(f)$ is an infimum (sInf) over a set that is nonempty and bounded below for every circulation; its attainment is to be proved, never assumed.

Explicit constants replacing the paper's $O(\cdot)$:

• Theorem 3.9: the paper prints $O(nm^2\log n)$; its proof uses groups of $k=m\,n\lceil\ln n+1\rceil$ iterations, at most $m$ of them, so the goal states $K\le n\,m^2\lceil\ln n+1\rceil$ with the natural logarithm.
• The standing assumption $n\ge2$ (p. 874) is kept on the goal; the standing assumption $m\ge n$ is not used by the proof and is omitted.

"Terminates after at most $B$ iterations" means that every run has length at most $B$. Asserting only that some run is short, or that the process eventually stops, does not formalize the theorem; nor does a step relation that drops negativity, simplicity of the cycle, minimality of the mean over all residual cycles, or the update by exactly the cycle's capacity.

A complete development needs cycle decomposition of the difference of two circulations, LP duality for circulations (Theorem 3.1), and bookkeeping for the residual graph under cancellation. These are reusable for any cycle-canceling or cost-scaling analysis, and contributions of that infrastructure as separate lemmas are welcome. Theorem 3.7 (the integer-cost bound) and Section 4 are outside this mission.

Selected references

• A. V. Goldberg, R. E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, J. ACM 36(4):873–886, 1989. https://doi.org/10.1145/76359.76368
• M. Klein, A primal method for minimal cost flows with applications to the assignment and transportation problems, Management Science 14(3):205–220, 1967. https://doi.org/10.1287/mnsc.14.3.205
• É. Tardos, A strongly polynomial minimum cost circulation algorithm, Combinatorica 5(3):247–255, 1985. https://doi.org/10.1007/BF02579369
• A. V. Goldberg, R. E. Tarjan, Finding minimum-cost circulations by successive approximation, Mathematics of Operations Research 15(3):430–466, 1990. https://doi.org/10.1287/moor.15.3.430
• R. M. Karp, A characterization of the minimum cycle mean in a digraph, Discrete Mathematics 23(3):309–311, 1978. https://doi.org/10.1016/0012-365X(78)90011-0
• J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, J. ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699

Motivation

A branching in a directed graph is a set of edges that contains no cycle (even ignoring directions) and in which no two edges point to the same node; a connected branching is an arborescence, a tree rooted at one node with all edges directed away from the root. The optimum branching problem asks, for real weights on the edges, for a branching of maximum total weight. It contains the minimum-cost spanning arborescence problem (the directed analogue of the minimum spanning tree), which appears in network design, in the analysis of broadcast and routing structures, in phylogenetics, and in dependency parsing in computational linguistics, where maximum spanning arborescences are the standard decoding step of graph-based parsers.

J. Edmonds solved the problem in Optimum branchings (J. Res. Nat. Bur. Standards 71B (1967) 233–240). The paper gives an algorithm (the shrinking algorithm usually attributed to Chu–Liu and Edmonds) and, proved together with it, a polyhedral theorem: the linear system that every branching obviously satisfies has no other vertices. This was one of the first integral polyhedron theorems beyond bipartite matching and network flows, and together with Edmonds' matching polytope (1965) it set the pattern of polyhedral combinatorics: describe the convex hull of the combinatorial objects by linear inequalities, and prove optimality by a linear programming dual.

Timeline:

• 1965: Y. J. Chu and T. H. Liu describe the shrinking algorithm for the maximum arborescence.
• 1965: Edmonds, Paths, trees, and flowers and Maximum matching and a polyhedron with 0,1-vertices: the matching polytope.
• 1967: Edmonds, Optimum branchings: the algorithm, Theorem 2 (vertices of the branching polyhedron), and the dual certificate built along the algorithm.
• 1970–1971: Edmonds' matroid intersection theorem, which contains the branching polyhedron theorem as the intersection of a graphic matroid and a partition matroid.
• 1977–1986: faster implementations (Tarjan; Gabow, Galil, Spencer and Tarjan).

Setting

A graph $G$ consists of a finite set $V$ of nodes and a finite set $E$ of edges. Each edge $e$ is directed toward a node $\mathrm{front}(e)$, its front end, and away from a different node $\mathrm{rear}(e)$, its rear end. Parallel edges are allowed; loops are not.

For $F\subseteq E$, a node $v$ meets $k$ edges of $F$ if $\#\{e\in F:\mathrm{front}(e)=v\}+\#\{e\in F:\mathrm{rear}(e)=v\}=k$. A set $B\subseteq E$ is a forest if it contains no polygon, i.e. no nonempty $F\subseteq B$ in which every node meets zero or two edges of $F$; it is a branching if in addition distinct edges of $B$ have distinct front ends. The incidence vector $x^B\in\mathbb R^E$ of $B$ has $x^B_e=1$ for $e\in B$ and $0$ otherwise.

The branching polyhedron $P_G\subseteq\mathbb R^E$ is the set of $x$ with

• $(L_1)$ $x_e\ge0$ for every edge $e$;
• $(L_2)$ $\sum_{e:\,\mathrm{front}(e)=v}x_e\le1$ for every node $v$;
• $(L_3)$ $\sum_{e:\,\mathrm{front}(e),\mathrm{rear}(e)\in S}x_e\le|S|-1$ for every set $S$ of two or more nodes.

A vertex of a set $P\subseteq\mathbb R^E$ is a point of $P$ that is the unique maximizer over $P$ of some linear function $x\mapsto\sum_e c_ex_e$.

For weights $c\in\mathbb R^E$, the dual variables are $y_h$ for each node $v_h$ and $y_S$ for each $S$ with $|S|\ge2$; write $w_e=\sum_{S\ni\mathrm{front}(e),\mathrm{rear}(e)}y_S$ and $(b,y)=\sum_hy_h+\sum_S(|S|-1)y_S$. Edmonds' conditions are (15) $y_h\ge0$, (16) $y_S\ge0$, (17) $y_{\mathrm{front}(e)}+w_e\ge c_e$ for every edge, and, for a branching $B$, (18) $y_h\ne0\Rightarrow$ some edge of $B$ enters $v_h$, (19) $y_S\ne0\Rightarrow$ exactly $|S|-1$ edges of $B$ lie inside $S$, (20) $y_{\mathrm{front}(e)}+w_e=c_e$ for $e\in B$.

Formalization targets

Goal: Theorem 2 (p. 235)

$$\{x:\ x\text{ is a vertex of }P_G\}\;=\;\{x^B:\ B\text{ is a branching of }G\}.$$

Both inclusions, for every finite loopless directed multigraph.

Milestones

1. §5, p. 236: for every branching $B$, $x^B\in P_G$.
2. §5, p. 236: for every branching $B$, $x^B$ is a vertex of $P_G$.
3. §6, (12)–(14): if $B$ is a branching and $y$ satisfies (15)–(20), then $(c,x^B)=(b,y)$, $x^B$ maximizes $(c,x)$ over $P_G$, and $y$ minimizes $(b,y)$ subject to (15)–(17).
4. §7, p. 237: for every $c\in\mathbb R^E$ there are a branching $B$ and a $y$ satisfying (15)–(20).
5. Lemma 1, p. 236: for every $c\in\mathbb R^E$ some branching vector lies in $P_G$ and maximizes $\sum_ec_ex_e$ over $P_G$.

Significance

Theorem 2 says that the linear program $\max\{(c,x):x\in P_G\}$ always has an optimal solution that is a branching, and that every vertex of $P_G$ is one. Consequently optimum branchings, and after the reductions of the paper's §2 optimum spanning and rooted arborescences, can be computed by linear programming, and their optimality is certified by a dual vector satisfying (15)–(20). The same statement underlies the separation-based treatment of arborescence constraints in integer programming formulations of network design and of the asymmetric travelling salesman problem. The integrality of the dual for integer weights (the paper's §8) yields min–max theorems of König type for branchings.

The result is proved and classical; no machine-checked proof of it in a proof assistant is known. The mission asks for the paper's own proof chain: branching vectors are points and vertices of $P_G$, linear programming optimality from complementary slackness, existence of a dual certificate for every weight vector, and the deduction of Theorem 2. Proofs through matroid intersection or total dual integrality would also establish the goal and are welcome as alternative routes.

Difficulty

The inclusion "branching vectors are vertices" and the certificate criterion are short. The substance is Milestone 4: for arbitrary real weights, a branching and a dual vector satisfying the complementary slackness conditions must exist simultaneously. Finiteness gives an optimum branching at once, but that says nothing about optimality over the fractional points of $P_G$; the difficulty is the dual. The natural attempt, taking $y_S=0$ for all sets and $y_h$ the largest positive weight entering $v_h$, violates (20) as soon as the greedy choice closes a circuit: the $(L_3)$ duals of nested node sets, arising from repeatedly shrinking circuits, are needed, and they must be kept nonnegative through weight changes of the form $c_3+c_0-c_4$ on edges entering a shrunk circuit.

Formalization scope

A graph is a structure Graph V E with front rear : E → V and a proof that front e ≠ rear e; V and E carry Fintype and DecidableEq. Edge sets are Finset E; vectors are E → ℝ; the linear function with weights c is ∑ e, c e * x e. A branching is defined combinatorially (no nonempty edge subset in which every node meets zero or two edges, and distinct front ends), never by counting edges inside node sets, and $P_G$ is the solution set of $(L_1)$–$(L_3)$, never a convex hull; either shortcut would make half of Theorem 2 true by definition. A vertex is a unique maximizer of a linear function, as on p. 236 (Mathlib's Set.exposedPoints has the same content); the set variables of the dual are a function Finset V → ℝ whose values on sets of fewer than two nodes are ignored. The right side of $(L_3)$ is the real number $|S|-1$.

Implicit conventions made explicit: the no-loop condition is part of the graph (with a loop $e$, the vector of $\{e\}$ is a vertex of $P_G$ but not a branching); parallel edges are allowed; weights have arbitrary sign and the empty branching is allowed. The mission does not model the algorithm of §4 or Theorem 1's notion of a "good" algorithm; Milestone 4 states only the existence of a certificate, which is what Lemma 1 uses.

Useful reusable infrastructure: finite directed multigraphs with an edge type, forests via polygons, and a finite LP duality lemma for $\max\{c^\top x: x\ge0,\ Ax\le b\}$; contributions of either are welcome.

Selected references

• J. Edmonds, Optimum branchings, J. Res. Nat. Bur. Standards Sect. B 71B (1967), 233–240. https://doi.org/10.6028/jres.071b.032
• Y. J. Chu and T. H. Liu, On the shortest arborescence of a directed graph, Scientia Sinica 14 (1965), 1396–1400.
• 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
• R. E. Tarjan, Finding optimum branchings, Networks 7 (1977), 25–35. https://doi.org/10.1002/net.3230070103
• H. N. Gabow, Z. Galil, T. Spencer and R. E. Tarjan, Efficient algorithms for finding minimum spanning trees in undirected and directed graphs, Combinatorica 6 (1986), 109–122. https://doi.org/10.1007/BF02579168
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer (2003), Chapter 52.

Motivation

The stable set problem asks for a largest set of pairwise non-adjacent vertices in a graph; its size is the stability number $\alpha(G)$. It is NP-hard in general, and a standard way to attack it in integer programming is to write down linear inequalities valid for all stable sets and solve the resulting linear program. The weakest such relaxation uses only the edge inequalities $x_v+x_w\le 1$; its optimum can be as large as $|V|/2$ on graphs with small $\alpha(G)$. Adding, for every odd circuit $C$, the inequality $\sum_{u\in C}x_u\le\frac12(|C|-1)$ gives the odd-cycle relaxation, the first strengthening that cuts off the fractional point $x\equiv\frac12$ on odd cycles.

Section 7 of V. Chvátal, On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154, doi:10.1016/0095-8956(75)90041-6) identifies a graph class on which this relaxation is exact for the all-ones objective, with an integral certificate on the dual side: the series-parallel networks. The paper conjectures (Conjecture 7.3) that for these graphs the odd-cycle inequalities describe the whole stable set polytope; graphs with that property were later called t-perfect.

Timeline:

• 1960: G. A. Dirac, in "In abstrakten Graphen vorhandene vollständige 4-Graphen und ihre Unterteilungen" (Math. Nachr. 22), proves that graphs containing no subdivided $K_4$ have at least two vertices of degree at most two.
• 1975: Chvátal introduces the system (7.1) and proves Theorem 7.1 (this mission): on series-parallel networks, $\max\sum_u x_u$ subject to (7.1) and its dual both have zero–one optima. He conjectures the full polyhedral statement.
• 1979: M. Boulala and J.-P. Uhry, "Polytope des indépendants d'un graphe série-parallèle" (Discrete Math. 27), prove the conjecture: (7.1) defines the stable set polytope of every series-parallel graph.
• 1986: A. M. H. Gerards and A. Schrijver, "Matrices with the Edmonds–Johnson property" (Combinatorica 6), extend this to graphs with no odd-$K_4$ subdivision.

Setting

All graphs $G=(V,E)$ are finite, undirected and loopless, with no parallel edges. A stable set is a set of vertices no two of which are adjacent. We write $d(u)$ for the degree of $u$.

A set $C\subseteq V$ induces an odd circuit if the induced subgraph $G[C]$ is a cycle of length $2k+1$ with $k\ge1$; triangles count, and such a cycle has no chords. $Z(G)$ is the set of all such $C$. The odd-cycle system of $G$ is

$$\begin{aligned} 0\le x_u&\le 1 && (u\in V),\\ x_v+x_w&\le 1 && (vw\in E),\\ \textstyle\sum_{u\in C}x_u&\le \tfrac12(|C|-1) && (C\in Z(G)). \end{aligned}\tag{7.1}$$

Its linear programming dual for the objective $\sum_u x_u$, with $x\ge0$ read as sign constraints, has variables $y_u\ge0$, $z_e\ge0$, $w_C\ge0$ and reads

$$\min\ \sum_{u}y_u+\sum_{e}z_e+\sum_{C\in Z(G)}\tfrac12(|C|-1)\,w_C\quad\text{s.t.}\quad y_u+\sum_{e\ni u}z_e+\sum_{C\ni u}w_C\ge 1\ \ (u\in V).$$

A homeomorph of $K_4$ is a graph obtained from $K_4$ by subdividing its edges into paths through new vertices of degree two. $G$ is a series-parallel network if no subgraph of $G$ is a homeomorph of $K_4$.

Formalization targets

Goal: Theorem 7.1

For every series-parallel network $G$,

$$\exists\,x\in\{0,1\}^V\ \text{feasible for (7.1)}:\ \ \sum_u x_u=\max\Big\{\sum_u x'_u : x'\in\mathbb R^V\text{ satisfies (7.1)}\Big\},$$

and there is a zero–one dual feasible $(y,z,w)$ whose dual objective equals the minimum over all real dual feasible points. Both optimality claims are against real points. Chvátal's statement has no constants to improve; the formal goal is his theorem as printed.

Milestones

1. Dirac's theorem (§7, p. 150): a series-parallel network with at least two vertices has two distinct vertices of degree at most two.
2. Case 4 closure (p. 151): if $d(u)=2$ and the neighbours $v,w$ of $u$ are non-adjacent, deleting $u$ and identifying $v$ with $w$ yields a series-parallel network.
3. The combinatorial core (p. 151, (i)–(ii)): there are a stable set $S$ and a spanning subgraph $F\le G$ whose components are isolated vertices, isolated edges and odd circuits, such that with $a$ isolated vertices, $b$ isolated edges and $c_k$ circuits of length $2k+1$,

$$a+b+\sum_k k\,c_k=|S|.$$

Significance

The result. Theorem 7.1 says that on series-parallel networks the odd-cycle relaxation computes $\alpha(G)$ exactly, and that the optimum is certified by a covering of the vertex set by single vertices, edges and chordless odd circuits whose total weight equals $|S|$. This is a min–max theorem of König type for a non-bipartite, non-perfect class: odd cycles of length at least five are series-parallel and not perfect, so the clique inequalities of the perfect-graph theory (mission I of this series) do not suffice here. The statement is the unweighted case of the later polyhedral results of Boulala–Uhry and Gerards–Schrijver, and the combinatorial core (milestone 3) is the basis of a polynomial algorithm for $\alpha(G)$ on this class, as the paper remarks.

Formalizing it. The theorem has been proved since 1975; neither Mathlib nor the Prove2Me library contains a formal proof of it. A formal proof needs a working notion of graph subdivision (topological minor), which Mathlib does not have, Dirac's degree theorem, the induction of the paper with its four cases, and the passage from the combinatorial core to a pair of LP optima through weak duality. Each of these is reusable: topological minors and the $K_4$-subdivision-free class appear throughout structural graph theory.

Difficulty

The combinatorial core is proved by induction on $|V|$ removing a vertex of degree at most two, and three of the four cases are routine. The obstacle is Case 4 ($d(u)=2$, neighbours non-adjacent): deleting $u$ alone loses the information needed to recover $S$ and $F$, so the proof identifies the two neighbours. That requires the class to be closed under this identification, a statement about subdivisions that is not a local edge count, and a lifting of $(S',F')$ from the reduced graph with a case split on the component of $F'$ containing the merged vertex. A second gap is between $F$ and the dual: an odd-circuit component of $F$ may have chords in $G$ and so need not lie in $Z(G)$, and the zero–one dual solution must be extracted from it. Finally, Dirac's theorem itself is the one place where the absence of $K_4$ subdivisions is used positively, and it is not a consequence of a degree-counting argument.

Formalization scope

Graphs are SimpleGraph V on a Fintype V with decidable equality and decidable adjacency. $Z(G)$ is a Finset (Finset V) whose members induce a subgraph isomorphic to Mathlib's cycleGraph (2k+1), $k\ge1$. The dual variables are indexed by V, by the edge set G.edgeSet, and by the subtype of $Z(G)$; $x\ge0$ is a sign constraint with no dual variable. "Contains a homeomorph of $K_4$" is encoded by four distinct branch vertices and six paths (Walk.IsPath) that avoid other branch vertices and meet only at common endpoints; it is not the $K_4$-minor notion and not the series–parallel composition notion, whose equivalence with it is not part of the paper.

Conventions and implicit hypotheses made explicit:

• Dirac's theorem is stated with $|V|\ge 2$; as printed it fails for graphs with fewer than two vertices.
• In Case 4 the identified graph has vertex set $V\setminus\{u,w\}$, with $v$ representing $v\equiv w$; parallel edges merge.
• Optimality in the goal is against every real feasible point of each program. A statement comparing the zero–one points only with other zero–one points would reduce the primal half to $\alpha(G)\le\alpha(G)$ and is ruled out.
• In milestone 3 the sum $a+b+\sum_k k c_k$ is written as a sum over the connected components of $F$ of $1$ (one or two vertices) or $(n-1)/2$ ($n\ge3$ vertices).

Corollary 7.2 (stated without proof) and Conjecture 7.3 are not part of this mission. Contributions welcome: a general topological-minor library, Dirac's theorem, and a proof of the combinatorial core.

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
• G. A. Dirac, In abstrakten Graphen vorhandene vollständige 4-Graphen und ihre Unterteilungen, Math. Nachr. 22 (1960) 61–85 (reference [6], Satz 5, of the paper).
• R. J. Duffin, Topology of series-parallel networks, J. Math. Anal. Appl. 10 (1965) 303–318 (reference [7] of the paper).
• M. Boulala, J.-P. Uhry, Polytope des indépendants d'un graphe série-parallèle, Discrete Math. 27 (1979) 225–243.
• A. M. H. Gerards, A. Schrijver, Matrices with the Edmonds–Johnson property, Combinatorica 6 (1986) 365–379.

Motivation

The combinatorial diameter of a polyhedron is the largest distance, in its vertex-edge graph, between two vertices. It is a lower bound on the number of pivots any edge-following method such as the simplex method needs in the worst case, which is why the polynomial Hirsch conjecture — the diameter of $P = \{x \in \mathbb{R}^n : Ax \le b\}$ is bounded by a polynomial in $m$ and $n$ — is a central open question of linear optimization and discrete geometry. The best general upper bound is quasi-polynomial, $m^{1+\log n}$ (Kalai–Kleitman 1992); the original Hirsch bound $m - n$ is false for polytopes (Santos 2012).

A different line of work bounds the diameter by the arithmetic of the constraint matrix instead of its size. For an integer matrix $A$ let $\Delta$ be the largest absolute value of a sub-determinant of $A$. Dyer and Frieze (1994) showed that for totally unimodular $A$ ($\Delta = 1$) the diameter is polynomial, $O(m^{16} n^3 (\log mn)^3)$. Bonifas, Di Summa, Eisenbrand, Hähnle and Niemeier (SoCG 2012; Discrete Comput Geom 52, 2014) improved and generalized this to $O(\Delta^2 n^4 \log n\Delta)$ for all polyhedra and $O(\Delta^2 n^{3.5} \log n\Delta)$ for polytopes, bounds that do not depend on the number $m$ of inequalities. This mission formalizes the polytope case.

Setting

Let $A \in \mathbb{Z}^{m\times n}$ with rows $a_1,\dots,a_m$, let $b \in \mathbb{R}^m$, and let $P = \{x \in \mathbb{R}^n : Ax \le b\}$. A vertex of $P$ is an extreme point; for a polyhedron this is a point of $P$ at which $n$ linearly independent inequalities are tight. Two vertices $u \ne v$ are adjacent if the segment $[u,v]$ is an edge (a one-dimensional face) of $P$. This gives the polyhedral graph $G_P = (V, E)$, and the diameter of $P$ is at most $B$ if every two vertices are joined by a walk of at most $B$ edges.

$A$ has sub-determinants bounded by $\Delta$ if every $k\times k$ submatrix, for every $k \ge 1$, has determinant in $[-\Delta, \Delta]$. In particular every entry is at most $\Delta$ in absolute value.

For a vertex $v$ the normal cone $C_v$ is the set of objectives $c$ for which $v$ maximizes $c^T x$ over $P$. With $B_n$ the closed unit ball, the volume of a set $U \subseteq V$ of vertices is

$$\mathrm{vol}(U) = \mathrm{vol}\Big(\bigcup_{v\in U} C_v \cap B_n\Big),$$

and the neighbourhood $\mathcal N(I)$ of $I \subseteq V$ is the set of vertices outside $I$ adjacent to a vertex of $I$. A spherical cone is $S = C \cap B_n$ with $C$ closed under non-negative scaling; its dockable surface $D(S)$ is the $(n-1)$-dimensional measure of the part of its boundary inside the open ball. A cone of revolution of angle $0<\theta\le\pi/2$ is $\{x \in B_n : v^T x \ge \cos\theta\,\|v\|\,\|x\|\}$. $P$ is non-degenerate if every vertex has exactly $n$ tight inequalities.

Formalization targets

Goal: Theorem 2 (p. 105)

If $A \in \mathbb{Z}^{m\times n}$ has all sub-determinants bounded by $\Delta$ and $P$ is bounded, then

$$\operatorname{diam}(P) \le 2\Big\lfloor \sqrt{2\pi}\,\Delta^2 n^{5/2}\ln\!\big(2^n\, n!\, n^{n/2}\,\Delta^n\big)\Big\rfloor + 2 \;=\; O(\Delta^2 n^{3.5}\log n\Delta).$$

No non-degeneracy, full-dimensionality or rank condition is assumed, and the bound is uniform in $m$ and $b$.

Milestones

1. Lemma 3 (p. 108): for a vertex $v$ of a non-degenerate polytope, $D(S_v) \le \Delta^2 n^3\,\mathrm{vol}(S_v)$, where $S_v = C_v \cap B_n$.
2. Lemma 4 (p. 109): among spherical cones of a given volume, a cone of revolution has minimum dockable surface.
3. Lemma 5 (p. 110): for a cone of revolution, $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$.
4. Lemma 6 (p. 111): for every measurable spherical cone with $\mathrm{vol}(S) \le \frac12 \mathrm{vol}(B_n)$, $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$.
5. Lemma 1 (p. 105): for a non-degenerate polytope and $I \subseteq V$ with $\mathrm{vol}(I) \le \frac12\mathrm{vol}(B_n)$,

$$\mathrm{vol}(\mathcal N(I)) \ge \sqrt{\tfrac{2}{\pi}}\,\frac{1}{\Delta^2 n^{2.5}}\,\mathrm{vol}(I).$$

6. Eq. (1) (p. 105): if $I_j$ is the set of vertices at graph distance at most $j$ from a vertex $v$ and $\mathrm{vol}(I_j) \le \frac12\mathrm{vol}(B_n)$, then $j \le \sqrt{2\pi}\,\Delta^2 n^{2.5}\ln(2^n/\mathrm{vol}(I_0))$.

Significance

The result. Theorem 2 bounds the diameter of every integral polytope by a polynomial in the dimension and the largest sub-determinant, independently of the number of facets. For totally unimodular matrices, which cover network-flow, bipartite matching and transportation polytopes, it gives $O(n^{3.5}\log n)$, improving the Dyer–Frieze bound by a large polynomial factor. It shows that the obstruction to a polynomial Hirsch bound, if any, must come from matrices with large sub-determinants. The volume-expansion method — measuring breadth-first search by the volume of the normal fan it has covered — was later refined, for instance in the shadow-vertex analysis of Dadush–Hähnle, which improves the dependence on $n$.

Formalizing it. The theorem is proved (2012/2014); no machine-checked proof is known. A formal development needs, on top of Mathlib, the normal fan of a polytope and its relation to the vertex-edge graph, a Hausdorff-measure calculus for cones (surface of a cone in terms of its base), Lévy's isoperimetric inequality on the sphere in a measure-theoretic form, and explicit Gamma-function estimates. Each of these is reusable well beyond this paper.

Difficulty

The combinatorial side is short; the geometry is not. Lemma 4 is the spherical isoperimetric inequality of Lévy, which Mathlib does not have in any form, and which the paper cites rather than proves; the relations between the volume of a spherical cone, the area of its base, its lateral surface and the length of the base's boundary (Eq. (3), "basic integration") are also absent. Lemma 3 depends on the structure of the normal cone of a vertex of a non-degenerate polytope (full-dimensional, simplicial, generated by rows of $A$), none of which is available for Mathlib's extreme points. Lemma 1 depends on the normal fan of a polytope: the normal cones have pairwise disjoint interiors, cover $\mathbb{R}^n$, and share a facet exactly when their vertices are adjacent. The step from non-degenerate to arbitrary polytopes perturbs $b$ and needs the diameter not to decrease, a statement about the vertex-edge graph under perturbation. A shortcut through a finite graph abstraction is not available: the constant depends on the geometry of the normal cones, not only on the graph.

Formalization scope

The polyhedron is Hirsch.Hpoly (rowVec A) b, with rowVec A i the $i$-th row of $A \in$ Matrix (Fin m) (Fin n) ℤ as a vector of EuclideanSpace ℝ (Fin n). Vertices are Set.extremePoints ℝ P, adjacency is Hirsch.Adj, "diameter at most $B$" is Hirsch.DiamLE P B, all from the published Hirsch_model. The normal cone is the published FirstOrderOpt.ConvexTheory.normalCone. Volumes are Lebesgue measure with values in $[0,\infty]$; the dockable surface uses μHE[n-1], the Hausdorff measure normalized to agree with Lebesgue measure on hyperplanes, applied to frontier S ∩ Metric.ball 0 1. $\Delta$ is a natural number and the sub-determinant bound ranges over all sizes $k \ge 1$.

Explicit constants. The paper writes $O(\Delta^2 n^{3.5}\log n\Delta)$ in Theorem 2; the proof on pp. 105–106 yields $2\lfloor K\rfloor + 2$ with $K = \sqrt{2\pi}\,\Delta^2 n^{5/2}\ln(2^n n!\, n^{n/2}\Delta^n)$, from Eq. (1), the bound $\mathrm{vol}(I_0) \ge 1/(n!\,n^{n/2}\Delta^n)$ and the fact that the diameter is at most twice the number of breadth-first-search iterations needed to cover more than half of $B_n$. This explicit bound is the goal. The ratios $D/\mathrm{vol}$ of Lemmas 3, 5, 6 are stated in multiplicative form.

Non-degeneracy is a hypothesis of Lemma 3, Lemma 1 and Eq. (1) only, as in the paper's §1.1, and never of Theorem 2. The neighbourhood $\mathcal N(I)$ excludes $I$; including it would make Lemma 1 trivial, since its constant is below $1$. Lemma 4 is stated against every competitor: for every measurable spherical cone $S$ and every cone of revolution $S^*$ of the same volume, $D(S^*) \le D(S)$; it does not assert existence of a cone of a prescribed volume. The goal is Theorem 2 about the polytope and its graph, not an abstract statement about set families with a volume-expansion property; integrality of $A$ and the bound on minors of every size are both essential (scaling a real matrix down makes $\Delta$ arbitrarily small), and the raw Hausdorff measure μH[n-1] would put Lemmas 3 and 6 on incompatible scales.

Contributions are welcome at every level: the normal fan and its adjacency structure, cone surface formulas, the Gamma estimate $\Gamma(x+\frac12)/\Gamma(x) \ge \sqrt{x-\frac14}$, and a formal Lévy inequality.

Selected references

• N. Bonifas, M. Di Summa, F. Eisenbrand, N. Hähnle, M. Niemeier, On Sub-determinants and the Diameter of Polyhedra, Discrete Comput Geom 52 (2014) 102–115. https://doi.org/10.1007/s00454-014-9601-x
• M. Dyer, A. Frieze, Random walks, totally unimodular matrices, and a randomised dual simplex algorithm, Math. Program. 64 (1994) 1–16. https://doi.org/10.1007/BF01582563
• G. Kalai, D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26 (1992) 315–316. https://doi.org/10.1090/S0273-0979-1992-00285-9
• F. Santos, A counterexample to the Hirsch conjecture, Annals of Math. 176 (2012) 383–412. https://doi.org/10.4007/annals.2012.176.1.7
• T. Figiel, J. Lindenstrauss, V. Milman, The dimension of almost spherical sections of convex bodies, Acta Math. 139 (1977) 53–94 (Lévy's isoperimetric inequality, Theorem 2.1). https://doi.org/10.1007/BF02392234
• D. Dadush, N. Hähnle, On the shadow simplex method for curved polyhedra, Discrete Comput Geom 56 (2016). https://arxiv.org/abs/1412.6705