Operations Research

Motivation

An algorithm for linear programming is strongly polynomial if the number of arithmetic operations it performs is bounded by a polynomial in the dimension of the problem alone (the number of variables and constraints), independently of the bit lengths of the numbers in the input. Many combinatorial optimization problems are linear programs over polyhedra of the form $P = \{x \in \mathbb{R}^n : Ax \le b\}$ whose constraint matrix $A$ has entries $0, +1, -1$, but whose objective vector $w$ is an arbitrary rational weight vector. Polynomial-time algorithms for such problems (for instance the ellipsoid-based algorithms of Grötschel, Lovász and Schrijver for maximum-weight cliques in perfect graphs, submodular flows, and matroid polyhedra) have running times that depend on the length of $w$.

Frank and Tardos (Combinatorica 1987) remove this dependence once and for all: they replace $w$ by an integral objective $\tilde w$ whose entries have $O(n^3)$ bits and which has exactly the same optimal solutions and the same optimal dual bases as $w$ over every such polyhedron. Any algorithm that is polynomial in $n$ and in the length of the objective then becomes strongly polynomial. The tool is simultaneous Diophantine approximation, used through the lattice-basis-reduction algorithm of Lenstra, Lenstra and Lovász (Math. Ann. 1982). The technique extends Tardos's strongly polynomial algorithm for linear programs with small constraint matrices (Oper. Res. 1986), which applies only to explicitly given programs.

Setting

For $x \in \mathbb{R}^n$ write $\|x\|_\infty = \max_j |x(j)|$ and $\|x\|_1 = \sum_j |x(j)|$; $\operatorname{sign}$ takes the values $-1, 0, +1$.

Decomposition. Fix a positive integer $N$. A decomposition of $w \in \mathbb{R}^n$ is an expression

$$w = \sum_{i=1}^k \lambda_i v_i, \qquad \lambda_i > 0,\ v_i \in \mathbb{Z}^n.$$

It satisfies condition (iii) if for $i = 2, \dots, k$ the vector $v_i$ is nonzero and $\lambda_i/\lambda_{i-1} \le 1/(N\|v_i\|_\infty)$: the coefficients decrease so quickly that each term is negligible against the previous one.

Preprocessing. Given a rational $w$ and $N$, the paper's preprocessing algorithm finds a decomposition with $k \le n$, condition (iii), and the size bound (ii)' $\|v_i\|_\infty \le 2^{n^2+n}N^n$, and outputs

$$\tilde w = \sum_{i=1}^k M^{k-i} v_i, \qquad M = 2^{n^2+n} N^{n+1}.$$

Linear programs. Let $A$ be an $m \times n$ matrix with entries in $\{0, \pm 1\}$ and $b \in \mathbb{R}^m$. The primal program is $\max\{wx : Ax \le b\}$ and the dual program is $\min\{yb : yA = w,\ y \ge 0\}$. A point $\bar x \in P$ is $w$-maximal if $w\bar x = \max(wx : x \in P)$. A dual basis is a maximal set of row indices of $A$ whose rows are linearly independent; it determines at most one $y$ with $yA = w$ supported on it (the basic dual solution), and it is an optimal dual basis if that $y$ exists and is optimal for the dual program.

Formalization targets

Goal — Theorem 4.2 (p. 58)

For every $w \in \mathbb{Q}^n$, with $N = (n+1)! + 1$, there is $\tilde w \in \mathbb{Z}^n$ with

$$\|\tilde w\|_\infty \le 2^{4n^3} N^{n(n+2)}$$

such that for every $0, \pm1$ matrix $A$ with $n$ columns and every $b$: (i) $x \in P$ is $w$-maximal if and only if it is $\tilde w$-maximal; (ii) a set of rows of $A$ is an optimal dual basis for $w$ if and only if it is one for $\tilde w$. The vector $\tilde w$ depends on $w$ only, not on $A$ or $b$.

Milestones

1. Dirichlet's theorem (p. 52): for $N \ge 1$ and $\alpha \in \mathbb{R}^n$ there are $p \in \mathbb{Z}^n$ and $1 \le q \le N^n$ with $|q\alpha(i) - p(i)| < 1/N$ for all $i$.
2. Theorem 3.1 (p. 53): every $w \in \mathbb{R}^n$ has a decomposition with $k \le n$, $\|v_i\|_\infty \le N^n$ and condition (iii).
3. Lemma 3.2 (pp. 54–55): under condition (iii), for integral $b$ with $\|b\|_1 \le N - 1$, $\operatorname{sign}(b \cdot w) = \operatorname{sign}(b \cdot v_j)$ for the smallest $j$ with $b \cdot v_j \ne 0$, and $b \cdot w = 0$ if there is no such $j$.
4. Theorem 3.3 (p. 56): the preprocessed $\tilde w$ satisfies $\|\tilde w\|_\infty \le 2^{4n^3}N^{n(n+2)}$ and $\operatorname{sign}(w \cdot b) = \operatorname{sign}(\tilde w \cdot b)$ for all integral $b$ with $\|b\|_1 \le N-1$.
5. The case $N = n+1$ (p. 55): an integral $\tilde w$ with $\|\tilde w\|_\infty \le 2^{4n^3}(n+1)^{n(n+2)}$ and $\tilde w(X) \le \tilde w(Y) \iff w(X) \le w(Y)$ for all subsets $X, Y$ of coordinates.
6. Lemma 4.1 (i) (p. 57): if $\operatorname{sign}(w' \cdot h) = \operatorname{sign}(w'' \cdot h)$ for all integral $h$ with $\|h\|_1 \le (n+1)!$, then $w'$ and $w''$ have the same maximizers over $\{Ax \le b\}$ for every $0, \pm1$ matrix $A$.
7. Lemma 4.1 (ii) (p. 57): under the same hypothesis, a dual basis is optimal for $w'$ if and only if it is optimal for $w''$.

Significance

The result gives a general reduction: whenever a class of polyhedra with $0, \pm1$ constraint matrices admits an optimization algorithm that is polynomial in $n$ and in the length of the objective, it admits a strongly polynomial one. The paper applies this to maximum-weight cliques in perfect graphs, optimization over submodular flow polyhedra, and matroid polyhedra membership, and its Section 5 applies the same rounding to the integer programming algorithms of Lenstra and Kannan. The subset-sum corollary (milestone 5) is independently useful: every rational weight function on a finite set can be replaced by an integral one with $O(n^3)$-bit entries that orders all subset sums identically.

All statements of this mission have been proved on paper since 1987. None is formalized on Prove2Me, and Mathlib contains only the one-dimensional Dirichlet approximation theorem. The mission produces a machine-checked version of the exact statements, with the explicit constants of the paper; the complexity claims (operation counts, strong polynomiality) are not part of it.

Difficulty

The goal combines two independent parts. The number-theoretic part (milestones 1–5) needs a multidimensional Dirichlet theorem, an induction producing the decomposition, and exact inequality chains with the constants $2^{n^2+n}N^n$ and $2^{4n^3}N^{n(n+2)}$. The linear-programming part (milestones 6–7) needs bounds on the entries of inverses of nonsingular $0, \pm1$ submatrices, the existence of optimal dual solutions supported on a dual basis, LP duality and complementary slackness. The obvious first idea, scaling $w$ to an integer vector by a common denominator, preserves every sign but gives no bound on $\|\tilde w\|_\infty$ in terms of $n$; the bound is the content of the theorem. Likewise, rounding each coordinate of $w$ separately to a fixed precision does not preserve the sign of $w \cdot b$ when $w \cdot b$ is tiny but nonzero.

Formalization scope

Vectors are functions on Fin n: the input $w$ is rational (Fin n → ℚ) in the goal, in Theorem 3.3 and in the subset-sum corollary, as in the algorithm's input line; it is real in Theorem 3.1, Lemma 3.2 and Lemma 4.1, as on the page. Integral vectors are Fin n → ℤ, and $A$ is a Matrix (Fin m) (Fin n) ℤ with every entry in $\{-1, 0, 1\}$, cast to $\mathbb{R}$; $b \in \mathbb{R}^m$ is unrestricted. Decompositions are indexed by $i \in \{1, \dots, k\} \subseteq \mathbb{N}$ as in the paper. $\|b\|_1$ is always the explicit sum $\sum_j |b(j)|$, compared with $N - 1$ in $\mathbb{Z}$; $\|v\|_\infty$ of an integer vector is a natural number (supNorm). Sign equality uses SignType.sign and includes the zero case. Condition (iii) is stated multiplicatively together with $v_i \ne 0$, which the paper's quotient presupposes; without $v_i \ne 0$ Lemma 3.2 fails. An optimal dual basis is a maximal linearly independent set of row indices together with an optimal dual solution supported on it.

Two formalizations would make the goal trivial and are excluded: dropping the bound on $\|\tilde w\|_\infty$ (a multiple of $w$ then works), and letting $\tilde w$ depend on $A$ and $b$ (the goal states $\exists \tilde w$ before $\forall A, b$). The $0, \pm1$ assumption on $A$ is part of every Section 4 statement.

A complete development needs a multidimensional pigeonhole argument, determinant and adjugate bounds for $0, \pm 1$ matrices, and basic LP duality (strong duality, complementary slackness, basic optimal dual solutions); the last two are reusable across linear-programming missions. Proofs of individual milestones, reusable lemmas on LP duality, and alternative proofs of Dirichlet's theorem are all welcome.

Selected references

• A. Frank and É. Tardos, An application of simultaneous diophantine approximation in combinatorial optimization, Combinatorica 7(1) (1987) 49–65. https://doi.org/10.1007/BF02579200
• A. K. Lenstra, H. W. Lenstra Jr. and L. Lovász, Factoring polynomials with rational coefficients, Math. Ann. 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Operations Research 34(2) (1986) 250–256. https://doi.org/10.1287/opre.34.2.250
• M. Grötschel, L. Lovász and A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981) 169–197. https://doi.org/10.1007/BF02579273
• J. W. S. Cassels, An Introduction to the Theory of Numbers (title as printed in the paper's reference [2]), Springer, Berlin, 1971; cited in the paper as [2, Sect. 1.10] for Dirichlet's theorem.

Motivation

Paging is the problem of managing a fast memory that holds $k$ pages out of $n$: when a requested page is not in fast memory (a page fault), some resident page must be evicted, and the cost of an algorithm is its number of faults. Practitioners have many eviction rules. Least-recently-used (LRU) performs well on real workloads but can be $k$ times worse than the optimal off-line schedule; the randomized marking algorithm of the same paper is $2H_k$-competitive and so has better worst-case guarantees. Fiat, Karp, Luby, McGeoch, Sleator and Young asked in 1991 whether one on-line algorithm can combine the advantages of several given ones, and answered the question exactly: the attainable combinations of ratios are characterized by one inequality (arXiv:cs/0205038, §6).

The question of combining on-line algorithms has since become a theme of its own: combining heuristics with worst-case-safe algorithms, and, more recently, combining machine-learned predictions with robust fallbacks, both ask for the same kind of guarantee against several reference algorithms at once.

Setting

A type $(k,n)$ consists of $k$ servers and a finite set $M$ of $n$ vertices with the uniform metric: two distinct vertices are at distance $1$. This is paging: vertices are pages, the vertices covered by servers are the pages in fast memory, and a server move is a page fault.

A deterministic on-line algorithm $A$ of type $(k,n)$ has an initial configuration of its $k$ servers and, after each request $r\in M$, moves servers so that some server covers $r$; its configuration after a request sequence depends only on that sequence. Its cost $C_A(\sigma)$ on a request sequence $\sigma$ is the total distance its servers travel, i.e. the number of server moves.

For algorithms $A$ and $B$ of the same type and a constant $c$, $A$ is $c$-competitive against $B$ if there is a constant $a$ such that for every request sequence $\sigma$

$$C_A(\sigma)\le c\cdot C_B(\sigma)+a .$$

A sequence $c^*=(c(1),\dots,c(m))$ of positive reals is realizable if for every type $(k,n)$ and every $m$ deterministic on-line algorithms $B(1),\dots,B(m)$ of that type there is a deterministic on-line algorithm $A$ of the same type that is $c(i)$-competitive against $B(i)$ for every $i$.

Formalization targets

Goal: Theorem 6

For $m\ge1$ and positive reals $c(1),\dots,c(m)$,

$$c^*\ \text{is realizable}\iff \sum_{1\le i\le m}\frac1{c(i)}\le 1 .$$

Milestones

In the order of the paper's proof:

1. Punishments are paid for. If $A$ punishes $B$ at a time step (an $A$-interval on a vertex $v$ ends at that step and contains the end of a $B$-interval on $v$ that began no later), then $B$ has moved a server; the number of such steps is at most $C_B(\sigma)$.
2. A fault leaves room to punish. If $|S_A|=k$, $|S_B|\le k$, $x\in S_B$ and $x\notin S_A$, then some $u\in S_A$ is not in $S_B$.
3. The greedy quota claim. If $\sum_i 1/c(i)\le 1$ and each unit of cost punishes the $B(i)$ minimizing $c(i)(\mathrm{PUN}(i)+1)$ (other algorithms may be punished incidentally), then after cost $r$ every $B(i)$ has been punished at least $\lfloor r/c(i)\rfloor$ times.
4. Shuttle algorithms. With $2m-1$ servers on $2m$ vertices there are $m$ algorithms, each keeping all vertices outside its own pair covered, no two of which move at the same step; in particular their total cost on any $\sigma$ is at most $|\sigma|$.
5. A forcing adversary. With $2m-1$ servers on $2m$ vertices every algorithm can be forced to move at each of $N$ steps, so $C_A(\tau(N))\ge N$.

Significance

The result. Theorem 6 is an exact characterization, not a bound: the region of simultaneously attainable ratios against arbitrary deterministic paging algorithms is $\{c:\sum 1/c(i)\le 1\}$. For example, any two paging algorithms can be combined into one that is $2$-competitive against each, and no better symmetric pair is possible in general. Combined with Theorem 7 of the same paper (not part of this mission), the same region is attainable against randomized algorithms, which is how LRU's practical behaviour and the marking algorithm's $2H_k$ worst-case guarantee can be obtained within constant factors by one algorithm.

Formalizing it. The theorem has been proved since 1991; no machine-checked proof is known. A formal proof produces a reusable notion of competitiveness of one on-line algorithm against another, built on the published KServer_model definitions, and a formal account of the scheduling fact at the core of the sufficiency proof.

Difficulty

Sufficiency looks like an averaging argument, but the combined algorithm cannot simulate the $B(i)$ and follow one of them: switching between their configurations costs up to $k$ per switch, which no additive constant absorbs. The accounting has to charge each of $A$'s faults to a specific move of a specific $B(i)$, and the charge must be injective; the paper's claim that $C_B(\sigma)$ is at least the number of punishments is where this happens, and it depends on how server intervals are matched. The allocation of faults to algorithms is then a deadline-scheduling problem whose feasibility is exactly $\sum 1/c(i)\le 1$, and the floor functions make the counting delicate at the boundary. The paper's own definition of punishment only counts intervals that start with a move, so the first $k$ faults of $A$ (servers on their initial vertices) need separate treatment; they are absorbed by the additive constant.

Necessity needs the right family of hard instances: the $m$ algorithms must never move at the same step, which pins the type to $(2m-1,2m)$.

Formalization scope

The Lean development works in the namespace CompetitivePaging.Combining and imports the published KServer_model definitions: KServer.OnlineAlgorithm k M (a configuration map from request prefixes to Fin k → M with a serving condition) and OnlineAlgorithm.cost. Committed conventions:

• a type $(k,n)$ is any k : ℕ and any finite M : Type with a metric in which distinct points are at distance $1$; realizability quantifies over all of them, never over one fixed type;
• servers are labelled; each algorithm has its own initial configuration, and the additive constant $a$ is chosen before the request sequence;
• $c(i)>0$ and $m\ge1$ are hypotheses of the goal, as in the paper; without positivity, $1/0=0$ in Lean would make a zero ratio free;
• time $t$ is the step processing the $t$-th request; the paper's $\mathrm{PUN}$ counts time steps.

Trivializing encodings are ruled out: realizability is not stated for a single fixed type, the metric is not the metric of Fin n, and the competitive constant is not allowed to depend on the request sequence.

A complete proof needs the construction of the punishing algorithm as a KServer.OnlineAlgorithm (a lazy, injective algorithm whose moves depend on the prefix and on the $B(i)$'s configurations), the injective charging argument, the scheduling lemma, and the explicit shuttle algorithms. The scheduling lemma and the charging lemma are independent of paging and reusable. Proofs of any milestone are welcome, as are alternative statements of the sufficiency construction.

Selected references

• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. doi:10.1016/0196-6774(91)90041-V; preprint arXiv:cs/0205038.
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2):202–208, 1985. doi:10.1145/2786.2793
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, J. Algorithms 11(2):208–230, 1990. doi:10.1016/0196-6774(90)90003-W

Motivation

The Hitchcock transportation problem asks how to ship a commodity from $m$ supply points to $n$ demand points at minimum total cost. It was posed by Hitchcock in 1941 and is one of the founding problems of linear programming and network optimization; it is solved routinely in logistics, and its structure (a bipartite network with supplies, demands and per-unit costs) recurs in assignment, optimal transport and matching.

The classical algorithms for it, the Ford–Fulkerson primal–dual method among them, augment flow one path at a time. With integral data their number of augmentations is bounded only by the total supply $\sum_i a_i$, which is exponential in the number of binary digits used to write the data. Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems (J. ACM 19(2), 1972, doi:10.1145/321694.321699), introduced capacity scaling: solve a coarse version of the problem first, then refine one binary digit at a time. Their Theorem 9 (p. 260) bounds the total number of augmentations by a quantity proportional to $\max(m,n)$ times the number of bits of the data, which made the transportation problem, and through standard reductions the minimum-cost flow problem, one of the first network problems with a polynomial-time ("good") algorithm in the sense of Edmonds.

Timeline. Hitchcock (1941) posed the problem; Ford and Fulkerson (1956–1962) gave the primal–dual labeling method and the optimality conditions by node potentials; Edmonds and Karp (1972) gave the scaling method and the bound formalized here. Strongly polynomial algorithms, independent of the size of the numbers, came later (Tardos 1985; Orlin 1988).

Setting

The network of Figure 1 (p. 259) has a source $s$, a sink $t$, supply nodes $s_1,\dots,s_m$ and demand nodes $t_1,\dots,t_n$, with $m,n\ge 1$. Its arcs are $(s,s_i)$ with capacity $a_i$ and cost $0$; $(s_i,t_j)$ with capacity $+\infty$ and cost $d_{ij}\ge 0$; $(t_j,t)$ with capacity $b_j$ and cost $0$; and the return arc $(t,s)$ with capacity $+\infty$ and cost $0$. The supplies $a_i$ and demands $b_j$ are positive integers with $\sum_i a_i=\sum_j b_j=:B$.

A flow assigns a nonnegative number to every arc, at most the capacity, with inflow equal to outflow at every node. Write $f_{0i}=f(s,s_i)$, $f_{ij}=f(s_i,t_j)$, $f_{j0}=f(t_j,t)$; the value of $f$ is $f(t,s)$, and a maximum flow is one of largest value. Its cost is $\sum_{i,j} d_{ij} f_{ij}$; a flow is extreme if no flow of the same value is cheaper. A flow is pseudo-extreme if there are real $u_i, v_j$ with $u_i-v_j+d_{ij}\ge 0$ for all $i,j$ and $f_{ij}=0$ whenever $u_i-v_j+d_{ij}>0$.

An augmenting path relative to $f$ is a sequence of distinct nodes from $s$ to $t$ in which each step either follows an arc with spare capacity or traverses backwards an arc carrying positive flow; augmenting pushes the minimum spare amount $\varepsilon$ along it and raises $f(t,s)$ by $\varepsilon$.

For $p\ge 0$, Problem $p$ has the same network and costs, with capacities $\lfloor a_i/2^p\rfloor$ and $\lfloor b_j/2^p\rfloor$. Choose $l$ with every $a_i,b_j<2^l$. The scaling method solves Problems $l-1,l-2,\dots,0$ in turn. Each phase performs augmentations keeping every flow pseudo-extreme, until no augmenting path is left. Problem $l-1$ starts from the zero flow, and Problem $p-1$ starts from twice the final flow of Problem $p$.

Formalization targets

Goal: Theorem 9

For every run of the scaling method, the total number $\sum_{p<l} K_p$ of flow augmentations satisfies

$$\sum_{p=0}^{l-1} K_p \;\le\; \max(m,n)\left(2+\left\lfloor \log_2\frac{\sum_{i=1}^m a_i}{\max(m,n)}\right\rfloor\right).$$

The bound holds for every $l$ admissible for the data and every choice of costs, and is stated with the paper's constant exactly.

Milestones

1. §1.1: augmentation preserves feasibility and raises the value by $\varepsilon>0$; a flow is maximum iff no augmenting path exists.
2. Theorem 8: a maximum flow is extreme iff there are potentials $u_0,\dots,u_m$, $v_0,\dots,v_n$ with (5a)–(5f).
3. §2.2: a pseudo-extreme maximum flow is extreme.
4. Lemma 3: if $f$ is pseudo-extreme in Problem $p$, then $2f$ is pseudo-extreme in Problem $p-1$.
5. The maximum-flow value of Problem $p$ is $f_p^*=\min\big(\sum_i\lfloor a_i/2^p\rfloor,\sum_j\lfloor b_j/2^p\rfloor\big)$.
6. Eq. (6): $\sum_p K_p\le f_0^*-\sum_{p=1}^{l-1} f_p^*$.
7. $f_p^*\ge\max\big(0,\,B/2^p-\max(m,n)\big)$.

Significance

The result. Theorem 9 shows that scaling reduces the number of augmentations from order $B$ to order $\max(m,n)\log_2(B/\max(m,n))$, which is roughly the length of the binary encoding of the data. Combined with the $O(mn)$ cost of one augmentation it gives a polynomial-time algorithm for the transportation problem; through the reduction of minimum-cost flow to transportation (p. 261) it gives one for minimum-cost flow. Capacity and cost scaling became standard techniques in network optimization and in combinatorial optimization generally. Theorem 8 and the pseudo-extreme criterion are the optimality certificates for transportation, a special case of linear-programming complementary slackness.

Formalizing it. The theorem has been proved since 1972. This mission produces a machine-checked version of the bound, of the exact counting argument (eq. (6)) and of the arithmetic estimate that turns it into the stated constant, together with the potential-based optimality conditions for the transportation network. To our knowledge no machine-checked bound on the number of augmentations of a flow algorithm exists on the platform.

Difficulty

The obvious argument bounds the number of augmentations by the increase in flow value, since each augmentation raises the value by a positive integer. Applied to Problem 0 directly this gives only $B$. The scaling bound needs three things that the naive count does not supply. First, doubling the final flow of Problem $p$ must give a feasible, still pseudo-extreme, starting flow for Problem $p-1$ (Lemma 3). Second, the gap between that start and the optimum of Problem $p-1$ must be small, which requires the exact maximum-flow value $f_p^*$ of each scaled problem. Third, the telescoping sum of the gaps must be estimated against $\log_2(B/\max(m,n))$ with the floors handled exactly. Integrality of every intermediate flow is not assumed; it has to be carried along the run from the integral capacities and the zero start.

Formalization scope

Everything lives in the namespace EdmondsKarp.Scaling. Nodes form an inductive type (s, t, src i, dst j). A flow is a structure with components f0, fx, fz, ret for the four arc families, real valued; the infinite capacities are encoded by the absence of an upper bound. IsMaxFlow is a predicate comparing values with every flow, not a supremum. Problem $p$ uses natural-number division for $\lfloor a_i/2^p\rfloor$. Augmenting paths are lists of distinct nodes from s to t whose consecutive pairs have positive residual amount (resCap, valued in WithTop ℝ); they never use the return arc.

A run of the scaling method (IsScalingRun) is a family of phases $F\,p\,0,\dots,F\,p\,(K\,p)$ for $p<l$. It starts from $0$ in Problem $l-1$, restarts from $2F\,p\,(K\,p)$ in Problem $p-1$, and advances by one augmentation per step. Every flow is pseudo-extreme, and each phase ends with no augmenting path left. The paper's path-selection rule (minimum weight for the modified reduced costs $\bar\Delta$) is abstracted to this invariant, which the paper states for it, so every run of the paper's method is covered.

The goal compares the count, cast to $\mathbb{Z}$, with $\max(m,n)\,(2+\lfloor\log_2(B/\max(m,n))\rfloor)$, using Real.logb 2 and Int.floor. The constant is the printed one; neither $O(\cdot)$ nor a weaker constant is acceptable. Positivity of all $a_i,b_j$ is a hypothesis, because without it the printed bound is false (for $m=5$, $n=1$, $a=(1,0,0,0,0)$, $b=(1)$ one augmentation is needed and the bound is negative). A formalization in which runs could be empty or never reach a maximum flow would trivialize the goal; the run predicate forbids this, and it is satisfiable (for instance with $m=n=1$, $a=b=(1)$, $l=1$ and one augmentation).

A complete development needs max-flow/min-cut for the bipartite network, integrality of flows along a run, the exact value of $f_p^*$, the telescoping identity and floor/logarithm estimates. LP duality or complementary slackness is needed only for Theorem 8. The augmenting-path and max-flow lemmas are reusable for other bipartite flow problems. Contributions welcome: proofs of any milestone, and a formalization of the paper's exact $\bar\Delta$ path rule showing that it satisfies the invariant.

Selected references

• J. Edmonds, R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699
• F. L. Hitchcock, The Distribution of a Product from Several Sources to Numerous Localities, Journal of Mathematics and Physics 20:224–230, 1941. https://doi.org/10.1002/sapm1941201224
• L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
• É. Tardos, A strongly polynomial minimum cost circulation algorithm, Combinatorica 5:247–255, 1985. https://doi.org/10.1007/BF02579369
• J. B. Orlin, A faster strongly polynomial minimum cost flow algorithm, Proc. STOC 1988, 377–387. https://doi.org/10.1145/62212.62249

Motivation

The economic order quantity (EOQ) is the most widely used formula in inventory management. It assumes that demand is a deterministic constant stream. Real demand is random, and the model that accounts for this, the continuous-review $(Q, r)$ policy with stochastic demand, has no closed-form optimum: for decades its optimal parameters were computed numerically, one instance at a time, which gave little insight into how the stochastic system behaves. Practitioners nevertheless kept using the EOQ quantity in stochastic systems and observed that the cost penalty was small (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), without an analytical explanation.

Zheng (Management Science 38(1), 1992) supplied that explanation. By minimising the average cost first over the reorder point and then over the order quantity, he obtained two simple optimality equations and compared the stochastic model with the EOQ model under the same cost structure. One of the results is the goal of this mission: for every leadtime-demand distribution, using the EOQ order quantity in the stochastic system raises the average cost by at most one eighth. The paper extends Federgruen and Zheng (1988), who treated the discrete-demand version of the cost function.

Setting

A single item faces demand at rate $\lambda > 0$. Orders are delivered after a fixed leadtime $L > 0$, and stockouts are backordered. Each order costs a fixed $K > 0$. Inventory is held at cost rate $h > 0$ per unit and backorders are penalised at cost rate $p > 0$ per unit. Let $D \ge 0$ be the demand during a leadtime, with mean $E(D) = \lambda L$. The newsvendor cost

$$G(y) = E\big[h(y - D)^+ + p(D - y)^+\big]$$

is the rate at which expected inventory costs accrue at time $t + L$ when the inventory position at time $t$ is $y$. It is convex, and it is assumed, as in the paper, to attain its minimum at a unique point $y^0$.

A $(Q, r)$ policy orders $Q$ units whenever the inventory position falls to the reorder point $r$. Its long-run average cost is

$$c(Q, r) = \frac{\lambda K + \int_r^{r+Q} G(y)\,dy}{Q}. \qquad (1)$$

For a fixed $Q > 0$ let $r(Q)$ be an optimal reorder point, and set

$$H(Q) = G(r(Q)) \ (Q > 0),\quad H(0) = G(y^0),\quad C(Q) = c(Q, r(Q)),\quad A(Q) = Q H(Q) - \int_0^Q H(y)\,dy .$$

$C(Q)$ is the average cost when the reorder point is chosen optimally for $Q$; an order quantity $Q^* > 0$ minimising $C$ over $Q > 0$ is the optimal order quantity, and $C^* = C(Q^*)$ is the optimal cost.

The EOQ model is the special case in which the leadtime demand is the constant $\lambda L$. Its cost rate is $G_d(y) = h(y - \lambda L)^+ + p(\lambda L - y)^+$, and its optimal order quantity is

$$Q^*_d = \sqrt{\frac{2\lambda K(h+p)}{hp}} .$$

The subscript $d$ marks every object of the EOQ model ($r_d$, $H_d$, $A_d$).

Formalization targets

Goal: Theorem 5

$$R = \frac{C(Q^*_d) - C^*}{C^*} \;\le\; \frac18 - \frac12\left(\frac12 - \frac{Q^*_d}{Q^*}\right)^2 \;\le\; \frac18 .$$

$C(Q^*_d)$ is the stochastic cost at the EOQ quantity with the reorder point re-optimised for it. The bound holds for every leadtime-demand distribution and every value of the parameters.

Milestones

In the order the goal's proof uses them:

• Lemma 1 (joint convexity of $c$), Lemma 2 ($r = r(Q) \iff G(r) = G(r+Q)$), Lemma 3 (properties of $r(Q)$), Corollary 1 ($G(r(Q)) \le \max(G(r), G(r+Q))$);
• Eq. (7) ($C(Q) = (\lambda K + \int_0^Q H)/Q$), Lemma 4 ($H$ increasing, convex, asymptotic slope $hp/(h+p)$), Lemma 5 ($C$ convex), Eq. (8) ($H(Q^*) = C(Q^*)$), Theorem 1 ($(Q, r)$ optimal iff $c(Q,r) = G(r) = G(r+Q)$), Lemma 6 ($A$ increasing convex, $Q = Q^* \iff A(Q) = \lambda K$, comparative statics in $K$);
• Eqs. (18), (20) (the EOQ model: $H_d(Q) = hpQ/(h+p)$ and the formula for $Q^*_d$), Eq. (22) ($G_d \le G$), Lemma 7 ($H_0 \le H_d \le H$, $A \le A_d$), and the first inequality of Theorem 2, $Q^*_d \le Q^*$.

Significance

The theorem is a distribution-free worst-case guarantee for the most common heuristic in inventory practice. It says that the EOQ formula, which needs only the mean demand rate and three cost parameters, loses at most $12.5\%$ against the true optimum, and that the loss is smaller when $Q^*_d/Q^*$ is close to $\frac12$ or to $1$. Combined with the paper's Theorem 2 (the gap $Q^* - Q^*_d$ is bounded as $K$ grows), it implies that the relative loss vanishes as the fixed ordering cost grows. The milestones along the way (the optimality conditions of Theorem 1, the monotonicity of the optimal reorder point, the comparison of $H$ with its EOQ counterpart) are the standard structural facts about continuous $(Q, r)$ systems and are reused throughout the inventory literature.

The result is proved in the paper. No machine-checked version of it, or of the $(Q, r)$ optimality conditions for the continuous cost (1), is known to exist. The platform has related but different formalizations: the discrete cost function with integer $Q$ (InventoryControl_rqDiscrete), the $(R, Q)$ cost under normal demand (InventoryControl_rq), and the EOQ without backorders (InventoryControl_eoq). A complete development here provides the continuous $(Q, r)$ machinery for an arbitrary leadtime-demand distribution.

Difficulty

The paper's proofs differentiate $r(Q)$ and $H(Q)$ twice (Eqs. (4), (5)), which presupposes a leadtime demand with a smooth density. The formalization does not assume one, so that discrete demand, such as the Poisson demand of the paper's own numerical study, is covered. Every step that the paper takes through derivatives, in particular the convexity of $H$ and the slope bound $H' \le hp/(h+p)$, has to be established by other means: through one-sided derivatives or chord arguments for the convex function $G$, whose kinks are where the derivative-based argument breaks. The definition of $r(Q)$ as a minimiser also means its existence and uniqueness must be proved before any property of $H$, $C$ or $A$ can be used.

Formalization scope

• The model is a probability measure $\mu$ on $\mathbb{R}$ (the law of $D$), concentrated on $[0,\infty)$, integrable, with mean $\lambda L$; $G$ is the integral of $h\max(y-x,0) + p\max(x-y,0)$ against $\mu$. The standing assumptions are bundled in IsQRModel: $\lambda, L, h, p > 0$, the conditions on $\mu$, and the unique minimiser of $G$ (paper, p. 90). $K > 0$ is a separate hypothesis. No density is assumed.
• $c$, $r(Q)$, $y^0$, $H$, $H_0$, $C$, $A$ and optimality of an order quantity are defined for an arbitrary cost rate $G$ and applied both to the newsvendor cost and to $G_d$; the EOQ objects $r_d$, $H_d$, $A_d$ are these definitions at $G_d$, and Eqs. (18), (20) are theorems.
• $r(Q)$ is a chosen minimiser of $c(Q,\cdot)$ (never defined by $G(r) = G(r+Q)$, which is Lemma 2). $H(0) := G(y^0)$; right-continuity of $H$ at $0$ is part of the Lemma 4 milestone. Order quantities range over $(0,\infty)$ for $c$ and $C$ and over $[0,\infty)$ for $H$, $H_0$, $A$.
• $Q^*$ in the goal is any $Q > 0$ with $C(Q) \le C(Q')$ for all $Q' > 0$; Lemma 6 asserts that exactly one exists, so the goal is not vacuous. $Q^*_d$ is the explicit square-root formula.
• Readings of informal words: "increasing" in Lemmas 4 and 6 means strictly increasing on $[0,\infty)$; "$Q^*$ increasing, $r^*$ decreasing in $K$" means strictly; "asymptotic slope $hp/(h+p)$" means that every chord of $H$ on $[0,\infty)$ has slope at most $hp/(h+p)$ and $H(Q)/Q \to hp/(h+p)$; Lemma 3 part 3 is stated as strict monotonicity of $r(Q)$ and $r(Q) + Q$, and its derivative clause $-1 < r'(Q) < 0$ is omitted because $r$ need not be differentiable without a density; "the optimal order quantity" means existence and uniqueness; Lemma 7 is stated for $Q \ge 0$.
• A trivializing formalization is ruled out: $C(Q^*_d)$ is the stochastic cost with the reorder point re-optimised in the stochastic model (not the EOQ reorder point $r^*_d$), and no positivity of $C^*$ is assumed (it follows from the model).
• Out of scope: the discrete cost (2), the §4 numerical study, and the unnumbered remarks after Theorem 5.
• Needed infrastructure: interval integrals of convex functions, partial minimisation of jointly convex functions, Jensen's inequality for $\mu$, and one-sided derivatives of convex functions. The generic $(Q, r)$ machinery (optimality conditions for arbitrary convex $G$) is reusable for other continuous-review models. Proofs of any milestone, and alternative proofs that avoid the paper's differentiability assumptions, are welcome.

Selected references

• Yu-Sheng Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• Awi Federgruen and Yu-Sheng Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808
• Paul H. Zipkin, Inventory Service-Level Measures: Convexity and Approximation, Management Science 32(8):975–981, 1986. https://doi.org/10.1287/mnsc.32.8.975
• George Hadley and Thomson M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• Daniel P. Heyman and Matthew J. Sobel, Stochastic Models in Operations Research, Vol. II, McGraw-Hill, 1984.

Motivation

In stochastic optimization the law of a random return $r$ is rarely known exactly, while its mean and variance can be estimated. A robust mean-covariance decision maker therefore evaluates a utility $u$ by its worst case

$$U=\inf\{\,E_\nu[u(r)] : \nu \text{ a law on } \mathbb R \text{ with mean } \mu \text{ and variance } \sigma^2\,\}.$$

Popescu (Operations Research 55(1), 2007) shows that for large classes of utilities this infinite-dimensional problem collapses to a one-dimensional one. The paper projects multivariate problems to a single dimension (the subject of the first mission of this series) and then asks for which $u$ the univariate worst case sits on laws with two support points. This mission formalizes the answer the paper gives for utilities whose marginal utility $u'$ is decreasing and changes curvature once, with finite limits: log-logistic utilities $C+\log\frac{1}{1+e^{-ax}}$ used in statistics and classification, and catenary-type utilities $C-b\cosh(ax)$, each plus a concave quadratic.

The result has a bounded-support precursor: Birge and Dulá (Annals of Operations Research 30, 1991, Theorem 5.1, as cited on p. 102 of Popescu 2007) proved an analogous two-point statement for functions on a bounded interval. Popescu's Proposition 5 is the unbounded version on the whole real line.

Setting

Let $u:\mathbb R\to\mathbb R$.

• The family $\mathcal Q$ collects the coefficient triples of quadratics lying below $u$: $\mathcal Q=\{(A,B,C) \mid q(y)=Ay^2+By+C\le u(y)\ \forall y\in\mathbb R\}$.
• A two-point law with support $\{a,b\}$, $a<b$, puts mass $p\in(0,1)$ on $a$ and $1-p$ on $b$. It has mean $\mu$ and variance $\sigma^2$ when $pa+(1-p)b=\mu$ and $p(a-\mu)^2+(1-p)(b-\mu)^2=\sigma^2$.
• Two-point support property (Definition 1). $u$ has it with respect to $(\mu,\sigma^2)$ if some quadratic $q$ with coefficients in $\mathcal Q$ meets $u$ at two points $a<b$, i.e. $q(a)=u(a)$, $q(b)=u(b)$, and a two-point law with support $\{a,b\}$, mean $\mu$ and variance $\sigma^2$ exists. $u$ has the two-point support property if this holds for every $\mu\in\mathbb R$ and every $\sigma>0$.
• Shapes (Definition 2). $f:\mathbb R\to\mathbb R$ is convex-concave if for some $x_0$ it is convex on $(-\infty,x_0)$ and concave on $(x_0,\infty)$; concave-convex if $-f$ is convex-concave; S-shaped if increasing and convex-concave; inverse S-shaped if $-f$ is S-shaped. So an inverse S-shaped $f$ is decreasing, concave on $(-\infty,x_0)$ and convex on $(x_0,\infty)$.
• Lemma 1's quadratic. For $a<b$ and slopes $q_a,q_b$, set

$$A=\frac{q_b-q_a}{2(b-a)},\quad B=\frac{bq_a-aq_b}{b-a},\quad C=\frac{bu(a)-au(b)}{b-a}-ab\,\frac{q_a-q_b}{2(b-a)},$$

and $q(y)=Ay^2+By+C$ (lemma1Quad).

• The function $g$. For $\mu\in\mathbb R$, $\sigma>0$ and $y<\mu$ let $z=\mu+\sigma^2/(\mu-y)$ (partnerPoint) and $g(y)=\frac{u(z)-u(y)}{z-y}-\frac{u'(y)+u'(z)}{2}$ (prop5Gap).

Formalization targets

Goal: Proposition 5 (p. 102)

If $u$ is differentiable, $u'$ is inverse S-shaped, and the limits $\lim_{y\to-\infty}u'(y)$ and $\lim_{y\to+\infty}u'(y)$ exist and are finite, then

$$u \text{ satisfies the two-point support property.}$$

Milestones

1. Proof of Lemma 1, first sentence. If $a<b$ and $\frac{u(b)-u(a)}{b-a}=\frac{q_a+q_b}{2}$, then $q(a)=u(a)$ and $q(b)=u(b)$.
2. Tangency (p. 110). $q'(a)=q_a$ and $q'(b)=q_b$.
3. Lemma 1. $u$ has two-point support if and only if for all $\mu$ and $\sigma>0$ there are $a<b$ and $q_a,q_b$ with

$$(b-\mu)(\mu-a)=\sigma^2,\qquad \frac{u(b)-u(a)}{b-a}=\frac{q_a+q_b}{2},\qquad q\le u \text{ on } \mathbb R.$$

4. Limits of $g$ (p. 110). Under the goal's hypotheses, with $\ell_\pm=\lim_{y\to\pm\infty}u'(y)$,

$$\lim_{y\to-\infty}g(y)=\frac{\ell_--u'(\mu)}{2}>0,\qquad \lim_{y\to\mu^-}g(y)=\frac{\ell_+-u'(\mu)}{2}<0 .$$

5. A zero of $g$ (p. 110). There is $a<\mu$ with $g(a)=0$; with $b=\mu+\sigma^2/(\mu-a)$ one has $a<b$, $(b-\mu)(\mu-a)=\sigma^2$ and $\frac{u(b)-u(a)}{b-a}=\frac{u'(a)+u'(b)}{2}$.

Significance

The result. Through the paper's Proposition 4, two-point support turns the worst-case expected utility over all laws with mean $\mu$ and variance $\sigma^2$ into a minimization over a single parameter $p\in(0,1)$ of $pu(\mu+\sqrt{(1-p)/p}\,\sigma)+(1-p)u(\mu-\sqrt{p/(1-p)}\,\sigma)$. Combined with the projection property of the paper's Section 2, this gives tractable robust counterparts of multivariate stochastic programs whose objective depends on a linear combination $x'R$ of random returns. Proposition 5 is the paper's sufficient condition that places a concrete class of utilities in this regime; it is also closed under adding any quadratic.

Formalizing it. The result is proved on paper; no machine-checked version is known. The formalization produces a checked characterization of two-point support (Lemma 1), a reusable encoding of convex-concave and S-shaped functions, and a proof of Proposition 5. The printed final step of the paper's proof is incomplete (see Difficulty), so a complete formal proof requires an argument the paper does not spell out.

Difficulty

Conditions (a) and (b) of Lemma 1 come from a sign change of $g$ on $(-\infty,\mu)$: the two limits in milestone 4 need a l'Hôpital-type argument and the continuity of a monotone derivative. The central difficulty is condition (c): showing that the quadratic built from a pair $(a,b)$ lies below $u$ on the whole line. The obvious argument takes any zero $a$ of $g$ and counts the intersections of the linear $q'$ with the inverse S-shaped $u'$. This fails when $u'$ is affine on an interval: a zero of $g$ can then produce a quadratic that coincides with $u$ on $[a,b]$ but crosses above $u$ just left of $a$. A proof must therefore choose the zero of $g$, or the pair $(a,b)$, with care, and the curvature hypotheses are not strict.

Formalization scope

• Functions are ℝ → ℝ; $u'$ is deriv u, and the goal assumes Differentiable ℝ u. Finite limits are Tendsto (deriv u) atBot (𝓝 l) and Tendsto (deriv u) atTop (𝓝 l) for some real l; the one-sided limit at $\mu$ is along 𝓝[<] μ.
• "Increasing" in Definition 2 is strict (StrictMono); the paper writes "nondecreasing" for the weak notion. Convexity and concavity are ConvexOn/ConcaveOn on the open half-lines Set.Iio x₀, Set.Ioi x₀, as printed.
• A two-point law is encoded by its mass $p\in(0,1)$ on $a$, with $a<b$; this is equivalent to a probability measure on $\mathbb R$ with support $\{a,b\}$, mean $\mu$ and variance $\sigma^2$.
• "Intersects it at two points $a,b$" is read as $q(a)=u(a)$ and $q(b)=u(b)$ for some $a<b$ (at least two contact points). This is the reading under which Lemma 1 is an equivalence.
• The two-point support property quantifies over $\sigma>0$: no two-point law has variance $0$, so including $\sigma=0$ would make the property false for every $u$.
• The two-point support property is defined from Definition 1 (supporting quadratic plus feasible law), not from Lemma 1's conditions, so Lemma 1 is not a tautology. Every division by $b-a$, $z-y$ or $\mu-y$ occurs under $a<b$ or $y<\mu$.

Useful infrastructure: l'Hôpital's rule at infinity (Analysis/Calculus/LHopital), Darboux's theorem for derivatives, the intermediate value theorem, and one-sided limits of monotone functions. The shape definitions of Definition 2 are reusable for S-shaped value functions elsewhere (prospect theory, sigmoidal utilities). Proofs of the milestones, of the goal, and alternative arguments for condition (c) are all welcome. Related platform work: Wasserstein Distributionally Robust Optimization II.

Selected references

• I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30:277–298, 1991 (cited in Popescu 2007, reference list)