All missions

Motivation

Many operations decisions are made after observing side information: an inventory manager sees weather, search trends and calendar effects before ordering; a supply-chain planner sees market signals before shipping. Bertsimas and Kallus, in From Predictive to Prescriptive Analytics (arXiv:1402.5481v4, Management Science 2020), study how to turn such data into decisions. Besides their local, weight-based prescriptions (the subject of mission 1 of this series), their §8 analyses a second approach: choose a decision rule $z(\cdot)$ from a structured class, such as norm-bounded linear rules, by empirical risk minimization — minimizing the average historical cost of the rule.

The question this mission formalizes is the one any practitioner of that approach must answer: how far can the true expected cost of the chosen rule exceed its in-sample cost? Classical statistical learning answers it with Rademacher complexity (Bartlett and Mendelson, JMLR 2002), but only for real-valued predictors. Operations decisions are vectors (order quantities for several products, shipments to several locations), so the paper extends the theory to multivariate decision rules.

Setting

Covariates $x$ take values in a measurable space $\mathcal X$, the uncertain quantity $y$ in a measurable space $\mathcal Y$, and decisions $z$ in $\mathbb R^{d}$, unconstrained. Data are an i.i.d. sample $S_N=((x^1,y^1),\dots,(x^N,y^N))$ from a probability measure $\mu$ on $\mathcal X\times\mathcal Y$, and $S_N^x=(x^1,\dots,x^N)$ is its covariate part. A cost $c(z;y)$ is incurred when decision $z$ meets outcome $y$. A decision rule is a measurable map $z(\cdot):\mathcal X\to\mathbb R^d$; $\mathcal F$ is a class of decision rules. Its expected cost is $\mathbb E[c(z(X);Y)]$, and its empirical cost is $\frac1N\sum_{i=1}^N c(z(x^i);y^i)$, the objective of problem (4).

The empirical multivariate Rademacher complexity of $\mathcal F$ (Definition 3) on a sample $s_1,\dots,s_N$ is

$$\widehat{\mathfrak R}_N(\mathcal F;S_N)=\mathbb E_\sigma\Big[\frac2N\sup_{g\in\mathcal F}\sum_{i=1}^N\sum_{k=1}^d\sigma_{ik}\,g_k(s_i)\Big],$$

with $\sigma_{ik}$ independent uniform signs, and the marginal complexity $\mathfrak R_N(\mathcal F)$ is its expectation over the sample. For real-valued classes ($d=1$) these are the usual Rademacher complexities with factor $2/N$ and no absolute value. Lean notation: empRademacher, margRademacher, expCost, empCost, costClass in PrescAnalytics.ERM.

Formalization targets

Goal: Theorem 13 (out-of-sample guarantees)

If $0\le c(z;y)\le\bar c$ and $|c(z;y)-c(z';y)|\le L\|z-z'\|_\infty$, then for any $\delta>0$ each of the following holds with probability at least $1-\delta$:

$$\mathbb E[c(z(X);Y)]\le\frac1N\sum_{i=1}^N c(z(x^i);y^i)+\bar c\sqrt{\frac{\log(1/\delta)}{2N}}+L\,\mathfrak R_N(\mathcal F)\quad\forall z\in\mathcal F,\tag{26}$$ $$\mathbb E[c(z(X);Y)]\le\frac1N\sum_{i=1}^N c(z(x^i);y^i)+3\bar c\sqrt{\frac{\log(2/\delta)}{2N}}+L\,\widehat{\mathfrak R}_N(\mathcal F;S_N^x)\quad\forall z\in\mathcal F.\tag{27}$$

In particular they hold for the empirical risk minimizer. The goal is stated for a general class $\mathcal F$, not only the linear rules (25).

Milestones

1. Lemma 1 (comparison): for $\mathcal G=\{(x,y)\mapsto c(f(x);y):f\in\mathcal F\}$, $\widehat{\mathfrak R}_N(\mathcal G;S_N)\le L\,\widehat{\mathfrak R}_N(\mathcal F;S_N^x)$ and $\mathfrak R_N(\mathcal G)\le L\,\mathfrak R_N(\mathcal F)$.
2. Theorem 14 (29): for a class $\mathcal G$ of functions with values in $[0,\bar g]$, with probability at least $1-\delta$, $\mathbb E g\le\frac1N\sum_i g(u^i)+\bar g\sqrt{\log(1/\delta)/(2N)}+\mathfrak R_N(\mathcal G)$ for all $g\in\mathcal G$.
3. Theorem 14 (30): the data-dependent version with $3\bar g\sqrt{\log(2/\delta)/(2N)}+\widehat{\mathfrak R}_N(\mathcal G;S_N)$.

Significance

Theorem 13 says that the quantity empirical risk minimization optimizes is, up to confidence terms that do not depend on the rule, an upper bound on the true expected cost of every rule in the class, uniformly. Bound (27) is computable from data, so it certifies a learned policy without a holdout set. Combined with complexity bounds for norm-restricted linear rules (the paper's Lemmas 2 and 3, not part of this mission), it shows the confidence terms vanish as $N\to\infty$.

The results are known: (29) and (30) for $[0,\bar g]$-valued classes are the standard Rademacher bounds (Mohri, Rostamizadeh and Talwalkar, Foundations of Machine Learning, Thm 3.3, after rescaling). What is new in the paper is the $\infty$-norm vector comparison inequality of Lemma 1 with constant $1$. None of these statements has a machine-checked proof on the platform. A formal development would supply a reusable symmetrization-plus-McDiarmid pipeline and a vector contraction lemma. Related items posed in this repository are Bartlett–Mendelson's Theorem 8 (RadGauss.RiskBound.theorem_8, with an absolute value in the complexity and constant $\sqrt{8\ln(2/\delta)/n}$), Maurer's Euclidean vector contraction with constant $\sqrt2$ (SPOBounds.Margin.maurer_vector_contraction), and the open uniform law HighDimStat.UniformLaws.uniform_law_rademacher_complexity; none is the same statement as a target here.

Difficulty

The uniform bound needs three ingredients: a concentration inequality for the supremum of the deviation over the class (bounded differences), a symmetrization step relating the expected supremum to the Rademacher complexity, and a comparison inequality to pass from the cost class to the decision rules. The scalar contraction principle of Ledoux and Talagrand does not apply directly, since each cost depends on a $d$-dimensional output; applying it coordinatewise loses a factor of $d$, and Euclidean vector contraction loses $\sqrt2$ and uses the wrong norm. Lemma 1 needs an argument specific to the $\infty$-norm. Measure theory adds its own difficulty: the supremum over an uncountable class must be shown measurable before its expectation or probability means anything.

Formalization scope

Decisions are Fin d → ℝ, whose Lean norm is the $\infty$-norm; $\mathcal X$, $\mathcal Y$ are general measurable spaces. Samples are drawn from the product measure Measure.pi (fun _ : Fin N => μ), with $N\ge1$. The following readings are explicit:

• Each "with probability at least $1-\delta$, … for all $z\in\mathcal F$" is a bound $\le\delta$ on the outer measure of the set of samples where the inequality fails for some $z$; the quantifier over the class is inside the event.
• Empirical complexities are in EReal (an unbounded class gives $+\infty$), marginal ones are lower Lebesgue integrals in $[0,\infty]$; $0\cdot\infty=0$.
• The paper assumes only $\sup c\le\bar c$ (resp. $|g|\le\bar g$). With that alone (26) and (29) are false — a two-point outcome with a constant rule violates them with probability $1/2$ — so the costs are assumed to take values in $[0,\bar c]$, keeping every printed constant.
• The undefined $\delta',\delta''$ are $\delta$ (the i.i.d. case of the paper's Theorem 21); the Lipschitz denominator printed as $\|z_k-z'_k\|_\infty$ is $\|z-z'\|_\infty$.
• Decision rules and the cost are measurable and the class is pointwise separable (a countable subclass approximates every member pointwise). The paper takes probabilities and expectations of suprema over the class without comment; without such a convention the statement fails for pathological classes.

A trivializing formalization is ruled out: the quantifier over the class sits inside the probability, the complexity has no absolute value and is never a junk $0$ for unbounded classes, and the hypotheses are satisfied by a clipped newsvendor cost. Solvers will need McDiarmid's inequality, symmetrization with a ghost sample, and the comparison lemma; each is reusable for any Rademacher-based generalization bound. Formalizations of these tools as separate lemmas are welcome.

Selected references

• D. Bertsimas, N. Kallus, From Predictive to Prescriptive Analytics, arXiv:1402.5481v4, 2018; Management Science 66(3), 2020. https://arxiv.org/abs/1402.5481 , https://doi.org/10.1287/mnsc.2018.3253
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, JMLR 3, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• M. Ledoux, M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4
• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018. https://mitpress.mit.edu/9780262039406/
• A. Maurer, A Vector-Contraction Inequality for Rademacher Complexities, ALT 2016. https://arxiv.org/abs/1605.00251

Motivation: curvature of the central path as a complexity measure

Path-following interior point methods solve a linear program by tracking its central path, a smooth curve that runs through the interior of the feasible set and ends at an optimal solution. Their number of iterations is polynomial in the bit size of the input, and whether some interior point method is strongly polynomial (bounded by a polynomial in the number of variables and constraints alone) is open. Bayer and Lagarias called the central path "a fundamental mathematical object underlying Karmarkar's algorithm". Dedieu and Shub proposed its total curvature as an informal complexity measure: a path that turns little should be easy to follow with straight steps. Several results bound that curvature:

• 2005. Dedieu and Shub conjecture that the total curvature of the central path is bounded linearly in the dimension. Dedieu, Malajovich and Shub prove an $O(n)$ bound on average over the regions of a hyperplane arrangement. De Loera, Sturmfels and Vinzant later obtain the same averaged bound with matroid methods (arXiv:1012.3978).
• 2008–2009. Deza, Terlaky and Zinchenko build redundant Klee–Minty cubes and "snakes" with curvature $\Omega(m)$ for $m$ inequalities, which refutes the dimension version. They then conjecture the continuous analogue of the Hirsch conjecture: the total curvature is bounded linearly in the number of constraints.
• 2014–2017. Allamigeon, Benchimol, Gaubert and Joswig disprove that conjecture with a family of linear programs whose central paths have curvature exponential in the number of constraints. The bound first appeared in arXiv:1405.4161 and was given an elementary tropical proof in arXiv:1708.01544v2, Theorem 25, which is the result of this mission.

Setting

A linear program in slack form has a real $m\times n$ matrix $A$, $b\in\mathbb R^m$, $c\in\mathbb R^n$ and $N:=n+m$:

$$\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. } Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .$$

For $\mu>0$ the point of the central path $(x^\mu,w^\mu,s^\mu,y^\mu)\in\mathbb R^{2N}$ is the unique solution of

$$Ax+w=b,\quad s-A^\top y=c,\quad x_js_j=\mu,\quad w_iy_i=\mu,\quad x,w,s,y>0. \tag{1}$$

The primal central path is $\mu\mapsto(x^\mu,w^\mu)\in\mathbb R^N$.

For $r\ge1$ and $t>0$, the program $\mathbf{LW}_r(t)$ minimizes $x_1$ over $x\in\mathbb R^{2r}$ subject to

$$x_1\le t^2,\quad x_2\le t,\quad x_{2j+1}\le t\,x_{2j-1},\quad x_{2j+1}\le t\,x_{2j},\quad x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ \ (1\le j<r),\quad x\ge0 .$$

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$, $m=3r-1$, $N=5r-1$.

For points $U,V,W$ of Euclidean space with $U\ne V\ne W$, the turning angle $\angle UVW\in[0,\pi]$ is the angle between the vectors $V-U$ and $W-V$. For a curve $\sigma$ parameterized over $I\subseteq\mathbb R$, the total curvature is

$$\kappa(\sigma,I)=\sup\Big\{\sum_{k=1}^{p-1}\angle\,\sigma(\mu_{k-1})\sigma(\mu_k)\sigma(\mu_{k+1})\ :\ \mu_0<\dots<\mu_p\ \text{in } I\Big\}\in[0,+\infty].$$

The milestones also use the field $\mathbb K$ of absolutely convergent generalized real Puiseux series $\sum_{\alpha\in\mathbb R}a_\alpha t^\alpha$. Such a series can be evaluated at large real $t$, and it has a valuation $\mathrm{val}\in\mathbb T=\mathbb R\cup\{-\infty\}$, its leading exponent. Read over $\mathbb K$, $\mathbf{LW}_r$ is one linear program. The valuation of its central path at $\mu=t^\lambda$ is the tropical central path $\mathcal C^{\mathrm{trop}}(\lambda)\in\mathbb R^{2N}$, a piecewise-linear curve with an explicit recursive description (Propositions 20–21 of the paper).

Formalization targets

Goal: Theorem 25

For every $r\ge1$ and $\epsilon>0$ there is $t_0$ such that for all $t>t_0$,

$$\kappa\big(\mu\mapsto(x^\mu,w^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon\quad\text{and}\quad\kappa\big(\mu\mapsto(x^\mu,w^\mu,s^\mu,y^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon$$

for the central path of $\mathbf{LW}^=_r(t)$. Here $t_0$ may depend on $r$ and $\epsilon$. Both the primal and the primal-dual curves are part of the goal, as in the paper.

Milestones, in the order of the paper's argument

1. Lemma 22: for non-null $\mathbf x,\mathbf y\in\mathbb K^d$, the angle $\angle\mathbf x(t)\mathbf y(t)$ has a limit, which is $\pi/2$ when the arg maxes of $\mathrm{val}\,\mathbf x$ and $\mathrm{val}\,\mathbf y$ are disjoint.
2. Lemma 23: the turning angle $\angle\mathbf U(t)\mathbf V(t)\mathbf W(t)\to\pi/2$ when $\max\mathrm{val}\,\mathbf U<\max\mathrm{val}\,\mathbf V<\max\mathrm{val}\,\mathbf W$ and the arg maxes of $\mathrm{val}\,\mathbf V$ and $\mathrm{val}\,\mathbf W$ are disjoint.
3. Proposition 24: $\liminf_{t}\kappa(\mathcal C_t,[t^{\lambda_0},t^{\lambda_p}])\ge\sum_{k=1}^{p-1}\angle^*\mathcal C^{\mathrm{trop}}(\lambda_{k-1})\mathcal C^{\mathrm{trop}}(\lambda_k)\mathcal C^{\mathrm{trop}}(\lambda_{k+1})$, where $\angle^*$ is the weak tropical angle ($\pi/2$ under the conditions of Lemma 23, else $0$).
4. Table 1: the coordinates of the tropical central path of $\mathbf{LW}_r$ at $\lambda=(4k+2c)/2^j$.
5. Claims in the proof of Theorem 25 (p. 23): on $[0,2]$ the dual coordinates of $\mathcal C^{\mathrm{trop}}$ are at most $\max(0,\lambda-1)$. At $\lambda_k=4k/2^{r-1}$ the largest coordinate is $r-1+(2k+2)/2^{r-1}$, attained only by $w_{3(r-1)}$ or $w_{3(r-1)+1}$. Hence $\angle^*=\pi/2$ at each interior subdivision point.

Significance

The theorem shows that the total curvature of the central path is not bounded by any polynomial in the number of constraints: $\mathbf{LW}_r$ has $3r+1$ constraints and curvature at least about $2^{r-2}\pi/2$. This settles the conjecture of Deza, Terlaky and Zinchenko in the negative. It also shows that the averaged upper bounds of Dedieu–Malajovich–Shub and De Loera–Sturmfels–Vinzant cannot hold for every region. A companion mission of this series formalizes the paper's second main result, an exponential lower bound on the number of iterations of log-barrier path-following methods on the same family.

The result is proved on paper. As far as is known, it has not been formalized in any proof assistant, and Mathlib has no notion of the total curvature of a curve, of Puiseux-series evaluation and valuation, or of the tropical central path. Formalizing the theorem would give a machine-checked reference point for a much-cited negative result in interior point theory. The Lean definitions of total curvature and of the turning angle are general and reusable.

Difficulty

The total curvature is a supremum over inscribed polygons, and a lower bound needs explicit polygons whose angles can be estimated for every large $t$. The central path of $\mathbf{LW}^=_r(t)$ has no closed form, so its points cannot be written down at given parameters $\mu$. Numerical evidence at a fixed $t$ says nothing uniform in $r$. The natural first idea, to compute the path's angles directly from system (1) for a fixed instance, gives no handle on how the number of turns grows with $r$. What is needed is control of the path's geometry uniformly over the whole scale of $t$, with $2^{r-2}$ turns located at once, and the threshold $t_0$ is not explicit.

Formalization scope

Vectors in which angles are measured are EuclideanSpace ℝ (Fin d). The turning angle is InnerProductGeometry.angle (V - U) (W - V), not Mathlib's vertex angle ∠ U V W, which is $\pi$ minus it. A degenerate triple ($U=V$ or $V=W$) contributes angle $0$. Total curvature is an EReal-valued supremum over strictly increasing parameter sequences in the parameter set, and the goal uses the set $(0,\infty)$. The primal and primal-dual curves are the vectors $(x,w)\in\mathbb R^{5r-1}$ and $(x,w,s,y)\in\mathbb R^{2(5r-1)}$. System (1) is the published Vanderbei central-path system with objective $-c$. The goal quantifies over every curve solving (1) for all $\mu>0$. Existence and uniqueness of that curve is the referenced platform statement VanderbeiLP.CentralPath.central_path_exists_unique and is not posed again. Indices are the paper's, 1-based, mapped to Fin by subtracting one. Powers $2^{r-2}$ use integer exponents of the real number $2$.

A trivializing formalization is ruled out explicitly: the curvature is a supremum in EReal (a real sSup of an unbounded set would be $0$), the turning angle is not the vertex angle, and degenerate polygons cannot add spurious right angles.

Lemmas 22–24 are stated over a model of $\mathbb K$ by coefficient functions with the paper's support and absolute-convergence conditions. Equalities, products and order in $\mathbb K$ are expressed through evaluation at all sufficiently large $t$, which is how the paper characterizes them. Table 1 and the claims of the proof are stated for the explicit tropical central path of $\mathbf{LW}_r$ given by Propositions 20–21 (milestones of the companion mission), written as a definition here. One repair: the paper's "uniquely attained" claim fails at $r=2$, $k=0$, where $w_1=w_4=2$. It is stated with that case excluded, which the proof does not use.

Welcome contributions: a general theory of total curvature of curves (monotonicity under refinement, behaviour under limits), asymptotics of evaluated Puiseux series, and the comparison between the central path over $\mathbb K$ and its real specializations.

Selected references

• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-Barrier Interior Point Methods Are Not Strongly Polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; preprint v2 (cited throughout) arXiv:1708.01544, doi:10.1137/17M1142132.
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Long and winding central paths, preprint, 2014. arXiv:1405.4161
• J. A. De Loera, B. Sturmfels, C. Vinzant, The central curve in linear programming, Found. Comput. Math. 12(4), 2012. arXiv:1012.3978
• J.-P. Dedieu, G. Malajovich, M. Shub, On the curvature of the central path of linear programming theory, Found. Comput. Math. 5(2), 2005.
• J.-P. Dedieu, M. Shub, Newton flow and interior point methods in linear programming, Int. J. Bifurcation and Chaos 15(3), 2005.
• A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Springer, 2009.
• L. van den Dries, P. Speissegger, The real field with convergent generalized power series, Trans. Amer. Math. Soc. 350(11), 1998.

Motivation

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

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

Setting

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

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

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

Formalization targets

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

Expected utility theory explains a single attitude toward risk by the curvature of a utility function of final wealth: a concave utility makes a decision maker risk averse, a convex one risk seeking. Several well documented patterns of behaviour do not fit this picture. The same people buy insurance against small-probability losses and buy lottery tickets with small-probability gains (Friedman and Savage, 1948, doi:10.1086/256692); subjects who are risk averse for gains are risk seeking for the mirrored losses, the reflection effect; and subjects who are indifferent between full insurance and bearing a risk reject half-price insurance that pays only half the time, probabilistic insurance (Kahneman and Tversky, 1979, doi:10.2307/1914185).

David E. Bell's 1982 paper Regret in Decision Making under Uncertainty (doi:10.1287/opre.30.5.961) proposes that a decision maker cares not only about what she obtains but also about what she would have obtained had she chosen differently. Its first part (the companion mission of this series) derives the representation $u(x,y)=\alpha v(x)+f(v(x)-v(y))$; its Section 2 shows that the single additive form with linear $v$ explains all of the patterns above at once, provided the regret function $f$ is decreasingly concave. Regret theory, developed at the same time by Loomes and Sugden (1982, doi:10.2307/2232669), remains one of the standard alternatives to expected utility in decision analysis and behavioural economics.

Setting

A decision maker chooses between two alternatives $a$ and $b$. Uncertainty is described by finitely many states $i$ with probabilities $\pi_i$; in state $i$ alternative $a$ gives final assets $a_i$ and $b$ gives $b_i$. Choosing $a$ means forgoing $b$, and an outcome is valued by the regret utility

$$u(x,y)=x+f(x-y),$$

where $x$ is the final assets received, $y$ the assets the foregone alternative would have given in the same state, and $f:\mathbb R\to\mathbb R$ the regret function. The expected utility of selecting $a$ when $b$ is foregone is

$$\mathrm{EU}_\pi(a\,|\,b)=\sum_i \pi_i\,u(a_i,b_i),$$

and $a$ is strictly preferred to $b$ when $\mathrm{EU}_\pi(b\,|\,a)<\mathrm{EU}_\pi(a\,|\,b)$ (the paper's inequality (1)); $a$ and $b$ are indifferent when the two expected utilities are equal.

The comparisons are given by three payoff tables. Table II: a horse wins with probability $p$; betting \p$gives$1-p$if it wins and$-p$if it loses, not betting gives$0$. Table III: a car is damaged with probability$p$at a cost of$1$; insuring gives$-p$in both states, not insuring gives$-1$or$0$. Table IV: an accident has probability$q$; self insurance gives$-1$or$0$, full insurance$-p$always, and probabilistic insurance, which charges half the premium and pays with probability one half given an accident, gives$-p$,$-1$or$-p/2$.

The regret function $f$ is decreasingly concave if it is twice differentiable with strictly increasing second derivative $f''$. Section 3 also uses $g(r)=r+f(r)-f(-r)$ and the negative exponential $f(r)=1-e^{-\gamma r}$, $\gamma>0$.

Formalization targets

Goal: coexistence of insurance and gambling

If $f$ is decreasingly concave and $0<p<\tfrac12$, then the bet of Table II is strictly preferred to not betting and insuring in Table III is strictly preferred to not insuring:

$$p\,[f(1-p)-f(p-1)]>(1-p)\,[f(p)-f(-p)].$$

Both comparisons have equal expected values, so the statement is a pure regret effect. The goal fixes no constants and assumes nothing about $f$ beyond decreasing concavity; it is the weakest hypothesis the page offers.

Milestones

1. Display (5): the bet is preferred iff the inequality above; display (6): insurance is preferred iff the same inequality, so the two preferences coincide.
2. The inequality holds for $0<p<\tfrac12$ whenever $(f(x)-f(-x))/x$ is strictly increasing on $x>0$; and that ratio is strictly increasing whenever $f''(x)>f''(-x)$ for $x>0$.
3. The reflection effect (Sec. 2(ii)): $x_2$ for sure is indifferent to the lottery $(p:x_1;\,1-p:x_3)$ iff $-x_2$ for sure is indifferent to $(p:-x_1;\,1-p:-x_3)$.
4. Probabilistic insurance (Sec. 2(iii)): display (9) characterises indifference between full and self insurance; under (9) and $0\le q<1$,

$$f(p/2)-f(-p/2)<\tfrac12\,[f(p)-f(-p)]\qquad(11)$$

holds iff full insurance is strictly preferred to probabilistic insurance, iff probabilistic insurance is strictly preferred to self insurance; and (11) follows from the same ratio condition. 5. The negative exponential (Sec. 3): $f$ concave, $g$ convex on $r\ge0$, $g(r)/r$ strictly increasing on $r>0$, and $f$ decreasingly concave.

Significance

The goal is the paper's central behavioural claim: one regret function explains why the same decision maker gambles on long odds and buys insurance at fair prices, behaviour that a single concave or convex utility of wealth cannot produce. The milestones show that the reflection effect and the rejection of probabilistic insurance follow from the same model, and two of them reduce to the same inequality on the odd part $f(x)-f(-x)$ of the regret function. The negative exponential example shows the hypotheses are met by a concrete, commonly used function, so the explanation is not vacuous.

The results are proved in the paper by short calculations, and none of them has been machine-checked before. The mission produces a formal statement of the regret model of Section 2 with its payoff tables, which pins down several points the printed text leaves loose: the meaning of "decreasingly concave", the domain on which "increasing" and "convex" are meant, and three misprinted intermediate displays.

Difficulty

The comparisons (5), (6), (9) and the reflection identity are algebraic once the payoff tables are expanded; the work is in expanding them correctly, since the foregone argument of $u$ changes with the alternative selected and three printed expansions are wrong. The substance lies in the analytic step: passing from a pointwise condition on $f''$ to strict monotonicity of $(f(x)-f(-x))/x$ on $(0,\infty)$, with strict inequalities throughout and through a quotient that is undefined at $0$. The naive reading of the page's condition, "$f''(x)>f''(-x)$ for all $x$", is unsatisfiable and cannot be used as a hypothesis.

Formalization scope

All quantities are real numbers. The utility is regretU f x y = x + f (x - y), i.e. form (4) with $v(x)=x$ exactly; the page assumes $v$ only "approximately linear" but computes every display with $v(x)=x$. A comparison is a finite state space Fin n with a real weight vector; the theorems instantiate it with $(p,1-p)$ for Tables II–III and with $(q/2,q/2,1-q)$ for Table IV, the accident state split by whether the insurer pays. Strict preference is strict inequality of expected regret utilities; indifference is equality.

Conventions and corrections, each disclosed in the item concerned:

• "Decreasingly concave" is not defined in the paper; it is read as Differentiable ℝ f, Differentiable ℝ (deriv f) and StrictMono (deriv (deriv f)). The page's presumption that $f$ is increasing and concave is not assumed.
• "Increasing" is read strictly, because the conclusions (5), (6), (11) are strict, and on $x>0$, because $(f(x)-f(-x))/x$ is undefined at $0$ and even.
• "$f''(x)>f''(-x)$ for all $x$" is read for $x>0$.
• The convexity of $g$ in the exponential example is stated on $r\ge0$: $g(r)=r+2\sinh(\gamma r)$ is concave for $r<0$, as the paper itself notes on p. 977.
• Misprints corrected: the last bracket of the second reflection equality on p. 973; $f(p/2)$ for $f(-p/2)$ in the expansion before (10) and in the probabilistic-versus-self display on p. 975, which also lacks a factor $q$. The normalisation $f(0)=0$ is not needed.
• The equivalences (5), (6), (9) and the reflection identity hold for every real probability and are stated without a range; the goal keeps $0<p<\tfrac12$ and the probabilistic-insurance statement keeps $0\le q<1$.

The goal cannot be satisfied vacuously: the negative exponential milestone exhibits a decreasingly concave $f$, and the conclusion is a strict preference between two alternatives of equal expected value. Section 2(iv) (preference reversals) is not formalized: its printed rewriting of (12) in terms of $h$ drops a linear term and its conclusion is unquantified ("for sufficiently small units of money").

Contributions welcome: proofs of the algebraic reductions, the slope argument for $(f(x)-f(-x))/x$, and the convexity facts for $\sinh$; the latter two are reusable beyond this mission.

Selected references

• D. E. Bell, Regret in Decision Making under Uncertainty, Operations Research 30(5), 961–981, 1982. doi:10.1287/opre.30.5.961
• D. Kahneman and A. Tversky, Prospect Theory: An Analysis of Decision under Risk, Econometrica 47(2), 263–291, 1979. doi:10.2307/1914185
• G. Loomes and R. Sugden, Regret Theory: An Alternative Theory of Rational Choice under Uncertainty, The Economic Journal 92(368), 805–824, 1982. doi:10.2307/2232669
• M. Friedman and L. J. Savage, The Utility Analysis of Choices Involving Risk, Journal of Political Economy 56(4), 279–304, 1948. doi:10.1086/256692

Motivation

Many planning problems are made in two stages: a first decision $x$ is fixed before an uncertain parameter is revealed, and a second decision $y$ is taken afterwards. Two models compete for such problems. Two-stage stochastic optimization assumes a probability distribution over the scenarios and minimizes the expected cost, letting the second-stage decision depend on the scenario. Robust optimization asks for one solution that is feasible in every scenario and minimizes the worst-case cost. The robust problem is usually far easier to solve: it is a single deterministic problem, while the stochastic problem optimizes over policies. The question is how much cost one gives up by solving the easy problem instead of the hard one.

Bertsimas and Goyal (Math. Oper. Res. 2010) measure this loss by the stochasticity gap, the ratio of the robust optimum to the stochastic optimum. Their Theorem 2.1 shows that when only the right-hand side of the constraints is uncertain, the uncertainty set is symmetric and the distribution is centred at the point of symmetry, the robust optimum is at most twice the stochastic one. Section 3 asks whether the same holds when the second-stage costs are uncertain as well, and answers no with an explicit instance: Theorem 3.1. This mission formalizes that instance.

Setting

There are no first-stage variables. The second-stage decision is a vector $y\in\mathbb R^n_+$ with $n\ge1$ continuous coordinates, subject to the single covering constraint

$$y_1+y_2+\dots+y_n\ \ge\ 1 ,$$

the constraint $By\ge b$ with $B=[1,1,\dots,1]\in\mathbb R^{1\times n}$ and $b=1$. A set $\Omega$ of scenarios carries a cost map $d:\Omega\to\mathbb R^n$; in scenario $\omega$ the second-stage cost is $d(\omega)^{\mathsf T}y$. The uncertainty set is $I_{(b,d)}(\Omega)=\{(b(\omega),d(\omega)) : \omega\in\Omega\}$, here $\{1\}\times[0,1]^n$: the range of $d$ is the whole cube $[0,1]^n$. A probability measure $\mu$ on $\Omega$ makes the coordinates $d_1,\dots,d_n$ independent, each uniformly distributed on $[0,1]$.

The stochastic problem $\Pi_{\mathrm{Stoch}}(b,d)$, display (1.4) of the paper, chooses a policy $\omega\mapsto y(\omega)\ge0$ satisfying the constraint in every scenario and minimizes $\mathbb E_\mu[d(\omega)^{\mathsf T}y(\omega)]$; its optimal value is $z_{\mathrm{Stoch}}(b,d)$. The robust problem $\Pi_{\mathrm{Rob}}(b,d)$, display (1.5), chooses one $y\ge0$ satisfying the constraint and minimizes $\max_{\omega\in\Omega} d(\omega)^{\mathsf T}y$; its optimal value is $z_{\mathrm{Rob}}(b,d)$. A set $P$ is symmetric (Definition 1.2) if there is $u^0\in P$ with $u^0+z\in P\iff u^0-z\in P$ for every $z$.

The Lean development names these zStochBD and zRobBD (the general problems (1.4) and (1.5) with data $A$, $B$, $b$, $c$, $d$ and integer coordinate sets), and IsSymmetricAbout (Definition 1.2).

Formalization targets

Goal: Theorem 3.1 (p. 22)

$$z_{\mathrm{Rob}}(b,d)\ \ge\ (n+1)\cdot z_{\mathrm{Stoch}}(b,d).$$

The constant $n+1$ is the paper's. Both sides are pinned down separately by the milestones, so the goal cannot be satisfied by a degenerate value of either side.

Milestones

1. Symmetry of the instance (proof of Theorem 3.1, pp. 22–23): the uncertainty set is symmetric about $(1,(\tfrac12,\dots,\tfrac12))$ and $\mathbb E_\mu[d(\omega)]=(\tfrac12,\dots,\tfrac12)$, so the hypotheses of the symmetric theory hold.
2. Robust side (p. 23): $z_{\mathrm{Rob}}(b,d)\ge1$.
3. Eq. (3.1) (p. 23): $z_{\mathrm{Stoch}}(b,d)\le\mathbb E_\mu[\min(d_1(\omega),\dots,d_n(\omega))]$.
4. Eq. (3.2) (p. 23): $\mathbb E_\mu[\min(d_1(\omega),\dots,d_n(\omega))]=\dfrac1{n+1}$.

Significance

Theorem 3.1 marks the boundary of the paper's positive results. The bound $z_{\mathrm{Rob}}\le2\,z_{\mathrm{Stoch}}$ of Theorem 2.1 needs only symmetry of the uncertainty set and a centred distribution. The instance here has both, has no integer variables and a single constraint, and still has a gap that grows linearly in the dimension. So symmetry alone does not make a robust solution a good approximation of the stochastic optimum when costs are uncertain. The paper's abstract states this as one of its main conclusions, and it is why Sections 4 and 5 compare the robust problem with the adaptive problem, whose worst-case objective does not suffer from it.

The result is proved in the paper; to our knowledge it has no machine-checked proof. What this mission adds is a formal proof of the instance against the general definitions of the two-stage problems, including the probabilistic computation (3.2), the expected minimum of independent uniform random variables, which Mathlib does not contain. That computation is reusable wherever order statistics of uniforms appear, for example in auctions, secretary problems and random-assignment bounds.

Difficulty

The robust half is short. The stochastic half has two parts. Eq. (3.1) needs a measurable policy that selects a cheapest coordinate; the policy printed in the paper puts a unit on every minimizing coordinate, which at ties overpays, so a formal proof must choose a single minimizer measurably and use integrability on the probability space. Eq. (3.2) is the main work: it is a genuine integral over the $n$-dimensional cube against a product measure, for every $n$, and Mathlib has no lemma on the distribution or the expectation of the minimum of independent random variables.

Formalization scope

• Vectors are Fin k → ℝ with the componentwise order; $B$ is the all-ones Matrix (Fin 1) (Fin n) ℝ, $A$ and $c$ live on Fin 0, $b(\omega)=1$, and the integer coordinate sets are empty ($p_1=p_2=0$).
• Optimal values are infima in EReal, $+\infty$ when infeasible; the robust worst-case cost is an EReal supremum. No optimal solution is assumed to exist: the paper's "consider an optimal solution" is a proof device, and the statements are about the infima.
• Stochastic policies must be integrable, together with their cost $\omega\mapsto d(\omega)^{\mathsf T}y(\omega)$, and satisfy the constraint in every scenario, as on the page, not only almost surely.
• The scenario space is an arbitrary probability space $(\Omega,\mu)$ with a measurable $d$ whose range is exactly $[0,1]^n$ and whose law is the product of $n$ uniform distributions on $[0,1]$. This is the paper's "each $d_j$ is distributed uniformly at random between 0 and 1 and independent of other coefficients" together with its description of $I_{(b,d)}(\Omega)$.
• $n\ge1$ is assumed; the paper leaves it implicit.
• The paper prints $\mathbb Z^{n_2}_+$ for the second-stage integer block in (1.4)–(1.5); $\mathbb Z^{p_2}_+$ is meant, and here $p_2=0$. Eq. (3.2) is called an inequality on the page; it is formalized as the equality it is.

A real-valued infimum would assign the value $0$ to an infeasible or ill-posed problem and make the goal trivially true; the EReal infima, and the separate milestones fixing $z_{\mathrm{Rob}}\ge1$ and $z_{\mathrm{Stoch}}\le\mathbb E[\min_j d_j]=1/(n+1)$, rule that out.

Contributions are welcome on each milestone separately. The expected-minimum computation (3.2) is self-contained and of independent use; a general lemma on the law of the minimum of independent random variables would serve it and other missions.

Selected references

• D. Bertsimas, V. Goyal, On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1090.0440 (cited here from the authors' manuscript, MIT DSpace).
• J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• D. Bertsimas, M. Sim, The Price of Robustness, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0065

Why regret enters the utility function

Expected utility theory predicts that a decision maker's choice between two lotteries depends only on the distribution of final wealth under each. Observed behaviour contradicts this in systematic ways: the Allais paradox, the coexistence of insurance and gambling, and the reflection effect documented by Kahneman and Tversky (1979). David Bell's 1982 paper (Operations Research 30(5), 961–981) explains these patterns by regret: the dissatisfaction of learning that the alternative not chosen would have done better. In the same year Loomes and Sugden (1982) proposed a closely related theory; together the two papers are the origin of regret theory in decision analysis.

Bell's contribution is axiomatic. Instead of postulating a regret term, he derives the shape of a utility function that incorporates regret from three behavioural assumptions about how preferences respond to shifting all outcomes by an equal increment of value. This mission formalizes that derivation, Section 1 of the paper (pp. 965–970), culminating in Theorem 1.

Setting

An endpoint is described by two attributes: the final assets $x$ and the foregone assets $y$, the asset level the decision maker would have had under the alternative not chosen. Utility is a function $u(x,y)$, strictly increasing in $x$ and strictly decreasing in $y$.

A simple comparison is a choice between two alternatives whose uncertainties are resolved by one predetermined joint distribution. With $n$ states, a probability vector $p=(p_1,\dots,p_n)$ and alternatives $A,B\in\mathbb R^n$ ($A_i$ the final assets of $A$ in state $i$), the expected utility of selecting $A$ while $B$ is foregone is

$$\mathrm{EU}_p(A\,|\,B)=\sum_{i=1}^n p_i\,u(A_i,B_i),$$

and $A$ is preferred to $B$ when $\mathrm{EU}_p(B\,|\,A)<\mathrm{EU}_p(A\,|\,B)$ (inequality (1) of the paper).

A value function $v:\mathbb R\to\mathbb R$, strictly increasing and onto $\mathbb R$, measures incremental value: moving from $a$ to $b$ is worth $v(b)-v(a)$. An alternative $A'$ is obtained from $A$ by a shift of incremental value $\delta$ if $v(A'_i)=v(A_i)+\delta$ for every state.

• Assumption 1. Shifting every outcome of both alternatives by the same incremental value leaves the preferred alternative unchanged.
• Assumption 2. If $v(x_2)-v(x_1)=v(x_3)-v(x_2)$, the decision maker is indifferent between $x_2$ for sure and a 50-50 lottery between $x_1$ and $x_3$.
• Assumption 3. If selecting $L_1$ over $L_2$ is preferred to selecting $L_3$ over $L_4$, that is $\mathrm{EU}_p(L_3\,|\,L_4)<\mathrm{EU}_p(L_1\,|\,L_2)$, this persists after all outcomes of all four alternatives are shifted by the same incremental value.

Formalization targets

Goal: the regret form (Theorem 1, p. 969, corrected)

Under Assumptions 2 and 3, there are a constant $\alpha$ and a function $f$ with

$$u(x,y)=\alpha\,v(x)+f\big(v(x)-v(y)\big)\quad\text{for all }x,y.$$

Utility separates additively into a term in the value of final assets and a function of the regret $v(x)-v(y)$. The coefficient $\alpha$ is left free (see Formalization scope).

Milestones, in the order of the paper's argument

1. Proof of Lemma 1 (p. 967): for $v(x)=x$, $w(x+h,y+h)=k(h)\,w(x,y)$ with $k(h)>0$, where $w(x,y)=u(x,y)-u(y,x)$.
2. Lemma 1, linear $v$ (p. 967): $u(x,y)-u(y,x)=[u(0,y-x)-u(y-x,0)]\,e^{-cx}$.
3. Lemma 1 (p. 967): Assumption 1 implies $u(x,y)-u(y,x)=g(v(x)-v(y))\,e^{-c\,v(x)}$.
4. Lemma 2, linear $v$ (p. 968): $u(x,y)-u(y,x)=u(0,y-x)-u(y-x,0)$.
5. Lemma 2 (p. 968): Assumptions 1 and 2 imply $u(x,y)-u(y,x)=g(v(x)-v(y))$.
6. Assumption 1 is a special case of Assumption 3 (p. 969).
7. Proof of Theorem 1 (p. 970): for $v(x)=x$, $u(x+h,y+h)-u(x,y)=j(h)$.
8. Theorem 1 for $v(x)=x$ (p. 970): $u(x,y)=\alpha x+u(0,y-x)$.

Significance

The additive form is the basis of the rest of Bell's paper: Section 2 uses it to show that a single decision maker with $f$ decreasingly concave both buys fair insurance and takes long-odds bets, and to account for the Allais paradox and the reflection effect. The same additive structure, a value term plus a function of the regret difference, is the form in which regret theory has been used since, alongside the parallel proposal of Loomes and Sugden (1982). Lemmas 1 and 2 have independent content: simple comparisons identify only the antisymmetric part $u(x,y)-u(y,x)$, and the lemmas pin that part down to a function of the regret difference.

The results are published with proofs in prose; none has a machine-checked proof. Formalizing them checks the argument as printed, which turns out to need a correction (the coefficient of $v(x)$ in (4)), and fills in the regularity steps the paper leaves implicit: the solutions of the Cauchy equations that appear, and the passage from $v(x)=x$ to a general value function.

Difficulty

The obvious argument reads each assumption as a functional equation and solves it. Two steps resist this. First, the functional equations $k(x+h)=k(x)k(h)$ and $j(x+h)=j(x)+j(h)$ have non-measurable solutions; excluding them needs boundedness of $k$ and $j$ on intervals, which must be extracted from the monotonicity of $u$ and is never stated on the page. Second, the proof of Theorem 1 compares two 50-50 lotteries that are indifferent and requires $g(a_1-b_1)$ to take an arbitrary value $u(c_1,c_2)-u(a_2,b_2)$; when $g$ is bounded no such indifference exists, so the printed step does not cover every case. Passing from $v(x)=x$ to a general $v$ requires transporting all three assumptions along $v^{-1}$.

Formalization scope

• Assets, probabilities and utilities are real numbers; $u$ is u : ℝ → ℝ → ℝ with u x y $=u(x,y)$. Every theorem assumes $u$ strictly increasing in $x$ and strictly decreasing in $y$ (the paper's "increasing"/"decreasing", p. 965, read strictly).
• A simple comparison is a probability vector on Fin n and two alternatives on the same states. Assumption 3 quantifies over four alternatives on one common state space, the setting of the paper's own use of it.
• The value function is strictly increasing (p. 968) and, as an added reading, maps $\mathbb R$ onto $\mathbb R$: Assumptions 1 and 3 shift outcomes by arbitrary equal incremental values, which presupposes that every shifted value is attained. "$v$ linear" (Lemmas 1, 2) is read as $v(x)=ax+b$ with $a>0$.
• Indifference in Assumption 2 is "neither alternative is preferred", equivalent to the first display on p. 969.
• Corrected slip. The paper's display (4) and the end of its proof have coefficient $1$ on $v(x)$ (resp. $x$). This is false as printed: $v(x)=x$, $u(x,y)=x-y$ satisfies every hypothesis, but $x-y=x+f(x-y)$ forces $f(0)=0$ at $x=y=0$ and $f(0)=-1$ at $x=y=1$. The proof derives $j(h)=\alpha h$ and silently sets $\alpha=1$. The goal and milestone 8 keep $\alpha$ free, with no sign or normalisation imposed; milestone texts stay verbatim.
• All existential objects ($k$, $c$, $g$, $j$, $\alpha$, $f$) are chosen before the variables $x,y,h$. The assumptions are statements about preferences between lotteries, never functional equations on $u$; a formalization that states an assumption as "$u(x+h,y+h)-u(x,y)$ is independent of $(x,y)$" would put the conclusion into the hypothesis and is ruled out.
• Needed infrastructure: monotone or locally bounded solutions of the Cauchy additive and multiplicative equations on $\mathbb R$, and transport of the assumptions along an order isomorphism of $\mathbb R$. Both are reusable; contributions proving either are welcome.

Selected references

• D. E. Bell, Regret in Decision Making under Uncertainty, Operations Research 30(5), 961–981, 1982. https://doi.org/10.1287/opre.30.5.961
• G. Loomes and R. Sugden, Regret Theory: An Alternative Theory of Rational Choice under Uncertainty, The Economic Journal 92(368), 805–824, 1982. https://doi.org/10.2307/2232669
• D. Kahneman and A. Tversky, Prospect Theory: An Analysis of Decision under Risk, Econometrica 47(2), 263–291, 1979. https://doi.org/10.2307/1914185

Motivation

Online bipartite matching models a platform that must commit each arriving request to a resource immediately. The motivating application of Feldman, Mehta, Mirrokni and Muthukrishnan is display advertising: an ad server knows from past traffic how many impressions of each type (web page, audience segment) to expect, sells them to advertisers in advance, and must assign each impression to an interested advertiser the moment a user loads the page. The goal is to fill as many contracted impressions as possible.

When arrivals are chosen by an adversary, the best ratio an online algorithm can guarantee is $1 - 1/e \approx 0.632$, achieved by the RANKING algorithm of Karp, Vazirani and Vazirani (STOC 1990). The ad server, however, is not facing an adversary: it has a forecast. The i.i.d. model captures this: the graph and the distribution of impression types are known in advance, and the impressions are independent draws. The paper asks whether this knowledge allows an online algorithm to beat $1 - 1/e$, and answers yes.

Timeline.

• 1990: Karp, Vazirani and Vazirani give RANKING, with ratio $1 - 1/e$ for adversarial arrivals, and show this is optimal in that model.
• 2005: Mehta, Saberi, Vazirani and Vazirani obtain $1 - 1/e$ for the budgeted AdWords generalization.
• 2009: Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) show that in the i.i.d. model the two suggested matchings algorithm achieves about $0.670$ with high probability when OPT is linear in $n$, the first ratio above $1 - 1/e$ for this model, and that no online algorithm reaches $26/27$ in expectation.

Setting

An instance is a bipartite graph $G = (A, I, E)$ with a finite set $A$ of advertisers, a finite set $I$ of impression types, and edges $E \subseteq A \times I$ recording which advertisers want which types. The mission treats the case analysed throughout §4.2 of the paper, in which one impression of each type is expected ($e_i = 1$). So $n = |I|$ impressions arrive one at a time, with types $\omega(0), \dots, \omega(n-1)$ drawn independently and uniformly from $I$. On arrival an impression must be assigned at once and irrevocably to a still unassigned advertiser adjacent to its type, or discarded. $\mathrm{ALG}(\omega)$ is the number of impressions an algorithm assigns. $\mathrm{OPT}(\omega)$ is the size of a maximum matching of the realization graph, which has one node per arrival $t$, joined to every advertiser $a$ with $(a, \omega(t)) \in E$.

The two suggested matchings (TSM) algorithm works offline first. Its boosted flow graph $G_f$ has a source arc of capacity $2$ into every advertiser, a unit-capacity arc along every edge of $E$, and an arc of capacity $2$ from every type to a sink. The algorithm takes the edge set $E_f$ of an integral maximum flow. Every vertex then has at most two edges of $E_f$, so $E_f$ splits into vertex-disjoint paths and cycles. The algorithm colours each component blue and red:

• on cycles, the colours alternate;
• on odd paths, the colours alternate, with more blue than red;
• on even paths between advertisers, the colours alternate;
• on even paths between types, the first two edges are blue, then the colours alternate, ending in blue.

Online, the first arrival of type $i$ tries the advertiser along $i$'s blue edge, the second tries the one along its red edge, and later arrivals are discarded. A tried advertiser that is already taken is not reassigned. The advertisers fall into four classes by their coloured edges: $A_{BR}$ (one blue, one red), $A_{BB}$ (two blue), $A_B$ (one blue only) and $A_R$ (one red only).

Formalization targets

Goal: Theorem 5, first sentence, $e_i = 1$

Let

$$\alpha = \frac{1 - 2/e^2}{4/3 - 2/(3e)} \approx 0.67029 .$$

The goal has three parts. First, every maximum flow edge set admits a colouring that follows the rules. Second, for every $\varepsilon > 0$ and $c > 0$ there are $\delta > 0$ and $N$ such that, for every instance with $n \ge N$, every maximum flow edge set and every rule-following colouring,

$$\Pr_\omega\big[\ \mathrm{OPT} \ge c\,n \implies \mathrm{ALG} \ge (\alpha - \varepsilon)\,\mathrm{OPT}\ \big] \;\ge\; 1 - e^{-\delta n}.$$

Third, $\alpha > 1 - 1/e$.

Milestones

1. Facts 1 and 2: concentration for two balls-in-bins statistics.
2. The note of §4.2.1: each type has no coloured edge, one blue edge, or one blue and one red edge.
3. Equation (1): $|E_f| = 2|A_{BR}| + 2|A_{BB}| + |A_B| + |A_R|$.
4. Equation (2): with high probability, $\mathrm{ALG} \ge (1 - 1/e^2)|A_{BB}| + (1 - 2/e^2)|A_{BR}| + (1 - 3/(2e))(|A_B| + |A_R|) - 4\varepsilon n$.
5. Equation (3): $|E_f| = 2(|A_T| + |I_S|) + |E_\delta|$ for the surgered residual cut $(S,T)$ of $G_f$.
6. Equation (4): with high probability, $\mathrm{OPT} \le |A_{BR}| + |A_{BB}| + \tfrac12(|A_B| + |A_R|) + (\tfrac12 - \tfrac1e)|E_\delta| + \varepsilon n$.
7. Lemma 1: $|E_\delta| \le \tfrac23|A_{BR}| + \tfrac43|A_{BB}| + |A_B| + \tfrac13|A_R|$.

Significance

The theorem separates the i.i.d. model from the adversarial one: knowing the distribution is worth a constant factor above $1 - 1/e$. The suggested matching algorithm of the same paper (Theorem 4) shows that following a single offline matching gets exactly $1 - 1/e$, so the second, red matching is what crosses the barrier. The paper's question started a line of work on the i.i.d. and random-order models, with later improvements to the constant by other authors under further assumptions.

The result has a written proof but, as far as the platform record shows, no machine-checked one. The mission formalizes the paper's own argument: the flow-and-colouring construction, the balls-in-bins concentration facts, the cut-based bound on OPT and the combinatorial Lemma 1. It also fixes two slips in the printed statements (see Formalization scope). The pieces are reusable beyond this paper. The occupancy concentration (Fact 1) and the satisfied-sequences bound (Fact 2) recur in analyses of online algorithms with stochastic input. The degree-capped flow encoding and its path/cycle decomposition are standard tools for 2-matchings.

Difficulty

The upper bound on OPT is the delicate part. A cut of the flow graph bounds the maximum matching of the realization graph only after a second surgery that depends on the random arrivals. Its size must then be compared with the colour classes, which are defined by a different structure (the components of $E_f$). Lemma 1 bridges the two, and it depends on the exact colouring rules: a colouring that only satisfies local degree conditions can put red edges at both ends of an even advertiser path, which breaks the inequality $|A_B| \ge |A_R|$ behind (2). On the probabilistic side, the advertisers of $A_{BR}$ share impression types with each other, so the success events are dependent, and Fact 2 needs a bounded-differences argument in which one ball affects up to $d$ sequences.

Formalization scope

All declarations live in the namespace OnlineStochMatching.TSM. Advertisers and types are finite types A I : Type, and $E$ is a Finset (A × I). Probabilities are counting ratios $\#\{\omega : \mathrm{Fin}\ n \to I \mid P\,\omega\}/|I|^n$, so there are no measurability side conditions. OPT is a maximum over the finite, nonempty set of partial injective assignments. An integral flow of $G_f$ is its set of saturated middle edges, i.e. a subset of $E$ with at most two edges per vertex; $E_f$ is such a set of maximum cardinality. A colouring is given by a listing of the components of $E_f$ as vertex sequences. Every theorem quantifies over every maximum $E_f$ and every colouring the rules allow, since the paper fixes neither.

The paper's asymptotic phrases are replaced by explicit quantifiers that come from its own proofs:

• "with probability $1 - e^{-\Omega(n)}$" and "with high probability" (Theorem 5, (2), (4)) become: $\exists\, \delta > 0,\ \exists\, N$, chosen before the instance, with probability at least $1 - e^{-\delta n}$ for all $n \ge N$;
• "as long as OPT $= \Omega(n)$" becomes the event $\mathrm{OPT} \ge c\,n$ for an arbitrary $c > 0$ fixed before $\delta$ and $N$;
• the $O(1)$ term in the bound on $|A^*_\delta|$ (p. 8) is absorbed into $\varepsilon n$ for $n \ge N$.

Corrections to the printed statements:

• Theorem 5 prints $\mathrm{ALG}/\mathrm{OPT} - \epsilon \ge \alpha$; the proof concludes $\mathrm{ALG}/\mathrm{OPT} + \epsilon \ge \alpha$, so the goal states $\mathrm{ALG} \ge (\alpha - \varepsilon)\mathrm{OPT}$;
• Fact 1 prints the failure probability $2e^{-\epsilon n/2}$; its proof gives $2e^{-\epsilon^2 n/2}$, which is used;
• Fact 2 states two hypotheses its proof uses: the bins of a sequence are distinct, and $c^2 < n$.

The ratio is multiplied out, so no division by OPT occurs. A colouring condition that is unsatisfiable, or a flow set that is not maximum, would make the goal vacuous or false; part (a) of the goal rules out the first, and every statement requires maximality. Not included: the reduction to general integer $e_i$ (§4.2.4), the tightness sentence of Theorem 5 (§4.2.5), and footnote 7's variant of the algorithm.

Useful infrastructure: bounded-differences (McDiarmid/Azuma) inequalities for functions of i.i.d. uniform variables, which exist on the platform as separate theorems; path/cycle decomposition of graphs of maximum degree two; and max-flow min-cut for unit-capacity bipartite networks. Contributions are welcome on Facts 1 and 2 independently of the combinatorics, and on Lemma 1 and equations (1) and (3), which are deterministic.

Selected references

• J. Feldman, A. Mehta, V. Mirrokni, S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, FOCS 2009; arXiv:0905.4100v1. https://arxiv.org/abs/0905.4100
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
• A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized online matching, FOCS 2005; J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321