Operations Research

Motivation

Scheduling jobs with release dates on one machine to minimize the total weighted completion time, written $1|r_j|\sum w_jC_j$, is strongly NP-hard even with unit weights (Lenstra, Rinnooy Kan & Brucker, 1977). It is a basic model of scheduling theory and a standard testbed for approximation algorithms built on linear programming relaxations. Several LP relaxations give lower bounds for it (Dyer & Wolsey, 1990; Queyranne, 1993), and the question how far these bounds can be from the optimum is also a question about the quality of branch-and-bound methods that use them.

Timeline, as surveyed in Table 1 of Goemans, Queyranne, Schulz, Skutella & Wang (2002):

• Phillips, Stein & Wein (Math. Programming, 1998) introduce converting a preemptive schedule into a nonpreemptive one by list scheduling, and the notion of $\alpha$-points; for the weighted problem their bound is $16+\epsilon$.
• Hall, Shmoys & Wein (SODA 1996) obtain 4; Schulz (IPCO 1996) and Hall, Schulz, Shmoys & Wein (Math. Oper. Res., 1997) obtain 3; Chakrabarti et al. obtain $2.8854+\epsilon$, and a combination of methods gives $2.4427+\epsilon$.
• Goemans (SODA 1997) orders jobs by $\alpha$-points of the LP schedule: $\alpha=1/\sqrt2$ gives $1+\sqrt2\approx2.4143$, a uniformly random $\alpha$ gives 2.
• Chekuri, Motwani, Natarajan & Stein (SIAM J. Comput., 2001) use random $\alpha$-points of an arbitrary preemptive schedule and obtain $e/(e-1)$ for unit weights, relative to the preemptive optimum rather than an LP value.
• Goemans, Queyranne, Schulz, Skutella & Wang (2002) prove $1.7451$ for the best common $\alpha$ and $1.6853$ for job-dependent random $\alpha_j$, both relative to the LP value $Z_R$. Afrati et al. (FOCS 1999) later give a polynomial-time approximation scheme, which does not bound the LP relaxations.

This mission formalizes the $1.6853$ result, the paper's main theorem.

Setting

There are $n$ jobs $N=\{0,\dots,n-1\}$. Job $j$ has an integral processing time $p_j>0$, an integral release date $r_j\ge0$ and a weight $w_j>0$. The jobs are indexed so that $w_0/p_0\ge w_1/p_1\ge\dots\ge w_{n-1}/p_{n-1}$.

The LP schedule is the preemptive schedule that at every moment processes the available (released, unfinished) job of smallest index. Since the data are integral, it is determined slot by slot: in $[\tau,\tau+1)$ it runs the smallest-index job $j$ with $r_j\le\tau$ and work left, or idles. Let $A^{LP}_j\subseteq\mathbb R$ be the set of times at which it processes $j$. The mean busy time of $j$ is

$$M^{LP}_j=\frac1{p_j}\int_{A^{LP}_j}t\,dt .$$

The mean busy time relaxation (R) has a variable $M_j$ per job:

$$Z_R=\min\Bigl\{\sum_j w_j\bigl(M_j+\tfrac12p_j\bigr)\ :\ \sum_{j\in S}p_jM_j\ge p(S)\bigl(r_{\min}(S)+\tfrac12p(S)\bigr)\ \text{for all nonempty }S\subseteq N\Bigr\},$$

with $p(S)=\sum_{j\in S}p_j$ and $r_{\min}(S)=\min_{j\in S}r_j$. $Z_R$ is a lower bound on the optimum of $1|r_j|\sum w_jC_j$.

For $0<\alpha\le1$ the $\alpha$-point $t_j(\alpha)$ is the first time at which $j$ has been processed for $\alpha p_j$ units in the LP schedule; $t_j(0^+)$ is the start time of $j$. For a vector $\boldsymbol\alpha\in(0,1]^n$, the $(\alpha_j)$-schedule processes the jobs nonpreemptively, as early as possible, in nondecreasing order of $t_j(\alpha_j)$; $C^{\boldsymbol\alpha}_j$ is the completion time of $j$ in it.

Let $\gamma\approx0.4835$ be the solution in $(0,1)$ of $\gamma+\ln(2-\gamma)=e^{-\gamma}\bigl((2-\gamma)e^{\gamma}-1\bigr)$, and set

$$\delta=\gamma+\ln(2-\gamma)\approx0.8999,\qquad c=1+\frac{e^{-\gamma}}{\delta},\qquad g(\alpha)=\begin{cases}(c-1)e^\alpha&0<\alpha\le\delta,\\0&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 3.9 (p. 185)

$c<1.6853$, and if $\alpha_1,\dots,\alpha_n$ each have density $g$ and are pairwise independent, then $\sum_j w_jC^{\boldsymbol\alpha}_j$ is integrable and

$$\mathbb E\Bigl[\sum_j w_jC^{\boldsymbol\alpha}_j\Bigr]\le c\cdot Z_R .$$

The bound is against the constant $c$ defined by the formula; the decimal $1.6853$ appears only in the separate inequality $c<1.6853$.

Milestones

1. Theorem 2.5 (p. 173): $M^{LP}$ is an optimal solution of (R), so $Z_R=\sum_jw_j(M^{LP}_j+\tfrac12p_j)$.
2. Eq. (3.1) (p. 176): $M^{LP}_j=\int_0^1t_j(\alpha)\,d\alpha$.
3. Corollary 3.2 (p. 179): $C^{\boldsymbol\alpha}_j\le t_j(\alpha_j)+\sum_{k:\alpha_k\le\eta_k(\alpha_j)}(1+\alpha_k-\eta_k(\alpha_j))p_k$, where $\eta_k(\alpha_j)$ is the fraction of $k$ processed by $t_j(\alpha_j)$.
4. Eq. (3.10) (p. 182): $M^{LP}_j=t_j(0^+)+\sum_{k\in N_2}(1-\mu_k)p_k+\tfrac12p_j$, where $N_2$ is the set of jobs processed between the start and completion of $j$ and $\mu_k$ is the fraction of $j$ processed before $k$ starts.
5. Eq. (3.11) (p. 183): the bound of Corollary 3.2 split over $N_1=N\setminus(N_2\cup\{j\})$ and $N_2$.
6. Lemma 3.11 (p. 185): $g$ is a probability density on $(0,1]$, and (i) $\int_0^\eta g(\alpha)(1+\alpha-\eta)\,d\alpha\le(c-1)\eta$, (ii) $(1+E_g[\alpha])\int_\mu^1g(\alpha)\,d\alpha\le c(1-\mu)$ for $\eta,\mu\in[0,1]$.

Significance

Theorem 3.9 gives a randomized algorithm for $1|r_j|\sum w_jC_j$ whose expected cost is at most $1.6853$ times the optimum, and a variant of it runs on-line (Theorem 3.14). Since $Z_R$ is a lower bound, it also shows that the relaxation (R), and the preemptive time-indexed relaxation (D), which has the same value, is within a factor $1.6853$ of the optimum (Corollary 3.10). The paper's Section 3.6 shows the gap of these relaxations can approach $e/(e-1)\approx1.5819$, so the bound is not far from what this relaxation can give.

The result is proved on paper; no machine-checked proof exists, and no part of this theory (LP schedule, $\alpha$-points, list scheduling from a preemptive schedule) is on the platform. The mission produces, besides the goal, a reusable formal account of $\alpha$-point scheduling: the LP schedule as a concrete object, the identity between mean busy times and average $\alpha$-points, and the deterministic completion-time bound of Corollary 3.2, which underlies many later $\alpha$-point analyses.

Difficulty

The obvious argument, bounding $C^{\boldsymbol\alpha}_j$ by Corollary 3.2 and integrating each $\alpha_k$ independently against $g$, does not work directly: the set of jobs $k$ with $\alpha_k\le\eta_k(\alpha_j)$ depends on $\alpha_j$, and the two effects of the random $\alpha_k$ pull in opposite directions (a small $\alpha_k$ shrinks the terms $1+\alpha_k-\eta_k$, a large one removes terms from the sum). The analysis needs the structure of the LP schedule around job $j$ (equations (3.9)–(3.11)) to separate the jobs whose $\eta_k$ is constant in $\alpha_j$ from those for which it jumps from $0$ to $1$, and then a density tuned to both at once. The claim is made under pairwise independence only, so no product structure of the random vector is available. On the formal side, the LP schedule, $\alpha$-points and list scheduling are defined from scratch, and the measure-theoretic content (integrability of a piecewise-constant function of $\boldsymbol\alpha$, conditioning under pairwise independence) is real work.

Formalization scope

Jobs are Fin n (0-based), $p$ and $r$ are natural numbers and $w$ is real. The ordering by $w_j/p_j$ is a hypothesis of every statement about the LP schedule, which is defined by the smallest-index rule; under that hypothesis the two coincide. The LP schedule is defined slot by slot, which is exact for integral data. Processing is represented by sets of times, not indicator functions. $t_j(\alpha)$ is an infimum over times, $t_j(0^+)=\inf A^{LP}_j$, and the $(\alpha_j)$-schedule is the closed form $C^{\boldsymbol\alpha}_j=\max_{k\preceq j}\bigl(r_k+\sum_{k\preceq i\preceq j}p_i\bigr)$ of list scheduling in lexicographic (α-point, index) order. $Z_R$ is the real infimum of the objective over the feasible set of (R), which is nonempty and bounded below for $w\ge0$. The random vector is any probability measure on $\mathbb R^n$ whose coordinate laws all equal the law with density $g$ and whose coordinates are pairwise independent; the product measure is one example, but the theorem is for all of them. $\gamma$ is any solution in $(0,1)$ of its equation.

A trivializing formalization is ruled out: the expectation is asserted together with integrability (a non-integrable integrand would have Bochner integral $0$), $g$ is supported on $(0,\delta]$ so every $\alpha_j$ lies in $(0,1]$ almost surely, and the bound is against $Z_R$ defined from (R), not against an expression that already contains Theorem 2.5.

Running times ($O(n\log n)$, $O(n^2)$), derandomization, the counting results (Proposition 3.8, Lemma 3.12) and the on-line variant are not formalized. Lemma 3.1 on the auxiliary $(\alpha_j)$-Conversion schedule is not a milestone; Corollary 3.2 is stated directly for the $(\alpha_j)$-schedule.

Contributions welcome: proofs of the milestones in any order; general lemmas on list scheduling and $\alpha$-points of preemptive schedules, which are reusable beyond this mission; and the measure-theoretic step from pairwise independence to the conditional bound on $\mathbb E[C^{\boldsymbol\alpha}_j\mid\alpha_j]$.

Selected references

• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single machine scheduling with release dates, SIAM J. Discrete Math. 15(2):165–192, 2002. https://doi.org/10.1137/S089548019936223X
• C. Phillips, C. Stein, J. Wein, Minimizing average completion time in the presence of release dates, Math. Programming 82:199–223, 1998.
• L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Math. Oper. Res. 22:513–544, 1997. https://doi.org/10.1287/moor.22.3.513
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM–SIAM SODA, 591–598, 1997.
• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31:146–166, 2001. https://doi.org/10.1137/S0097539797327180
• M. E. Dyer, L. A. Wolsey, Formulating the single machine sequencing problem with release dates as a mixed integer program, Discrete Appl. Math. 26:255–270, 1990.
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Ann. Discrete Math. 1:343–362, 1977.

Motivation

Minimizing the total weighted completion time $\sum_j w_j C_j$ of jobs with release dates on a single machine, written $1\,|\,r_j\,|\,\sum w_j C_j$ in scheduling notation, is strongly NP-hard. It is one of the basic models of machine scheduling, and it has served as a test case for a general technique in approximation algorithms: solve a linear programming relaxation, read off a preemptive schedule, and convert it into a nonpreemptive one using $\alpha$-points, the times at which a given fraction of each job has been processed. Phillips, Stein and Wein (doi:10.1007/BF01585872) introduced ordering jobs by points of a preemptive schedule; Goemans (SODA 1997, reference [11] of the paper below) and Chekuri, Motwani, Natarajan and Stein (doi:10.1137/S0097539797327180) showed that choosing $\alpha$ at random improves the guarantee.

Goemans, Queyranne, Schulz, Skutella and Wang (doi:10.1137/S089548019936223X) combine two LP relaxations, shown to have equal value, with carefully chosen random $\alpha$. This mission formalizes their Theorem 3.5: when a single $\alpha$ is drawn from a truncated exponential density, the resulting schedule costs in expectation at most $c < 1.7451$ times the LP lower bound.

Timeline:

• 1998: Phillips, Stein and Wein give the first constant-factor approximation (ratio $2$) for the unit-weight problem $1\,|\,r_j\,|\,\sum C_j$ by converting a preemptive schedule.
• 1997: Goemans (SODA) introduces randomly chosen $\alpha$-points for the weighted problem, the conference precursor of the paper formalized here.
• 2001: Chekuri, Motwani, Natarajan and Stein give a randomized $e/(e-1) \approx 1.58$-approximation for the unit-weight problem.
• 2002: Goemans, Queyranne, Schulz, Skutella and Wang give $1.7451$ for a single random $\alpha$ (Theorem 3.5) and $1.6853$ for job-dependent random $\alpha_j$ (Theorem 3.9), both against the same LP bound.
• 1999: Afrati et al. (doi:10.1109/SFFCS.1999.814574) give a polynomial-time approximation scheme for the problem. It is not LP-based, so the LP-relative factors of Theorems 3.5 and 3.9 remain of interest as bounds on the relaxations' integrality gaps.

Setting

There are $n$ jobs $N = \{1, \dots, n\}$. Job $j$ has an integral processing time $p_j > 0$, an integral release date $r_j \ge 0$ and a weight $w_j > 0$. The jobs are indexed so that $w_1/p_1 \ge w_2/p_2 \ge \cdots \ge w_n/p_n$.

A preemptive schedule gives each job a set $A_j \subseteq [r_j, \infty)$ of processing times of measure $p_j$, the sets pairwise disjoint. The mean busy time of $j$ is $M_j = \frac{1}{p_j}\int_{A_j} t\,dt$.

The LP schedule is the preemptive schedule that always processes the available job of smallest index, which under the indexing above is the available job of largest ratio $w_j/p_j$. Its mean busy times are $M^{LP}_j$.

The mean busy time relaxation (R) minimizes $\sum_j w_j (M_j + \tfrac12 p_j)$ subject to $\sum_{j \in S} p_j M_j \ge p(S)\big(r_{\min}(S) + \tfrac12 p(S)\big)$ for every nonempty $S \subseteq N$, where $p(S) = \sum_{j\in S} p_j$ and $r_{\min}(S) = \min_{j\in S} r_j$. Its optimal value is $Z_R$, a lower bound on the optimum of $1\,|\,r_j\,|\,\sum w_j C_j$.

For $0 < \alpha \le 1$, the $\alpha$-point $t_j(\alpha)$ is the first time at which $j$ has received $\alpha p_j$ units of processing in the LP schedule, and $t_j(0^+)$ is its start time. The $\alpha$-schedule processes the jobs nonpreemptively, each as early as possible, in nondecreasing order of $t_j(\alpha)$; $C^\alpha_j$ is the completion time of $j$ in it. More generally, the $(\alpha_j)$-schedule orders the jobs by $t_j(\alpha_j)$ for a vector $\boldsymbol\alpha = (\alpha_j)$.

Let $0 < \gamma < 1$ solve $1 - \frac{\gamma^2}{1+\gamma} = \gamma + \ln(1+\gamma)$ ($\gamma \approx 0.4675$), and set

$$c = \frac{1+\gamma}{1+\gamma-e^{-\gamma}}, \qquad \delta = 1 - \frac{\gamma^2}{1+\gamma}, \qquad f(\alpha) = \begin{cases}(c-1)e^{\alpha} & 0 < \alpha \le \delta,\\ 0 & \text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 3.5

If $\alpha$ is drawn with density $f$, then $c < 1.7451$, the expectation below is finite, and

$$\mathbb E_f\Big[\sum_{j} w_j C^\alpha_j\Big] \le c \cdot Z_R .$$

Milestones

1. Theorem 2.5: $M^{LP}$ is an optimal solution to (R), so $Z_R = \sum_j w_j (M^{LP}_j + \tfrac12 p_j)$.
2. Eq. (3.1): $M^{LP}_j = \int_0^1 t_j(\alpha)\,d\alpha$.
3. Corollary 3.2: $C^{\boldsymbol\alpha}_j \le t_j(\alpha_j) + \sum_{k:\,\alpha_k\le\eta_k(\alpha_j)} (1+\alpha_k-\eta_k(\alpha_j))\,p_k$, where $\eta_k(\alpha_j)$ is the fraction of $k$ processed by $t_j(\alpha_j)$ in the LP schedule.
4. Eq. (3.10): $M^{LP}_j = t_j(0^+) + \sum_{k\in N_2}(1-\mu_k)p_k + \tfrac12 p_j$, where $N_2$ is the set of jobs processed between the start and the completion of $j$ and $\mu_k$ the fraction of $j$ done before $k$ starts.
5. Eq. (3.11): the bound of Corollary 3.2 rewritten in terms of $N_1$, $N_2$ and $\mu_k$.
6. Lemma 3.6: $f$ is a density on $[0,1]$ with $\int_0^\eta f(\alpha)(1+\alpha-\eta)\,d\alpha \le (c-1)\eta$ and $\int_\mu^1 f(\alpha)(1+\alpha)\,d\alpha \le c(1-\mu)$ for $\eta, \mu \in [0,1]$.

Significance

Theorem 3.5 is a randomized $1.7451$-approximation for $1\,|\,r_j\,|\,\sum w_j C_j$, and simultaneously a bound on the integrality gap of (R): every instance has $\mathrm{OPT} \le 1.7451\, Z_R$. The paper also derandomizes it: there are at most $n$ distinct $\alpha$-schedules (its Proposition 3.8), and the best of them can be found in $O(n^2)$ time. The paper remarks that the truncated exponential density is optimal for its analysis and that the factor is tight for it.

On the formal side, the mission produces a reusable model of single-machine preemptive schedules, the LP schedule, $\alpha$-points and list scheduling, and the first machine-checked instance of the $\alpha$-point rounding technique that recurs across scheduling approximation. The result itself is proved in the paper; no machine-checked proof of it or of the LP-schedule identities (3.1), (3.10) is known to exist.

Difficulty

The obvious approach, bounding each $C^\alpha_j$ separately by a multiple of $t_j(\alpha)$, gives only the factor $\max\{1 + 1/\alpha, 1 + 2\alpha\}$ for fixed $\alpha$ (Theorem 3.3 of the paper), which is at least $1+\sqrt2$. The improvement needs the precise structure of the LP schedule around each job: which jobs interrupt $j$ ($N_2$) and which do not ($N_1$), and how the fraction $\eta_k(\alpha)$ of each other job depends on $\alpha$. Turning this structure into exact identities for piecewise-constant, piecewise-linear functions of $\alpha$ defined through a recursively built schedule is the bulk of the formal work. The analytic part (Lemma 3.6) is elementary but depends on the specific equation that defines $\gamma$.

Formalization scope

Jobs are Fin n (0-based) with $p, r : \texttt{Fin } n \to \mathbb N$ and real weights. The sortedness $w_j/p_j \ge w_k/p_k$ for $j \le k$, positivity $p_j > 0$ and $w_j > 0$ are hypotheses of every theorem about the LP schedule. Because the data are integral, the LP schedule is defined slot by slot on unit intervals $[\tau, \tau+1)$; a job's processing set is a finite union of such intervals. $\alpha$-points are infima over reals, and every statement restricts $\alpha$ to $(0,1]$. The $(\alpha_j)$-schedule's completion times are given by the closed form of list scheduling, $C_j = \max_{k \preceq j}(r_k + \sum_{k \preceq i \preceq j} p_i)$, with ties of $\alpha$-points broken by index (they do not occur for $\alpha \in (0,1]$). $Z_R$ is the infimum of the objective of (R) over its feasible set. The random $\alpha$ has law $f(\alpha)\,d\alpha$ on $\mathbb R$, and the expectation is a Lebesgue integral.

The goal asserts integrability of $\alpha \mapsto \sum_j w_j C^\alpha_j$ together with the bound, so the inequality cannot hold through the convention that a non-integrable function has integral $0$. The bound is against $Z_R$ defined from (R), not against $\sum_j w_j (M^{LP}_j + \tfrac12 p_j)$, which would build Theorem 2.5 into the goal; and the density's support $(0,\delta]$ is written out, so no mass is placed outside $(0,1]$. The running-time claims are not formalized, and the uniqueness of $\gamma$ is not asserted: the statements hold for every solution in $(0,1)$.

Useful infrastructure: finite unions of intervals and their measures, monotone piecewise-linear functions and their integrals, and list-scheduling identities. Contributions to any milestone, and general lemmas about the LP schedule (it is a preemptive schedule, has no idle time inside a job's span, processes interrupting jobs completely), are welcome.

Selected references

• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single Machine Scheduling with Release Dates, SIAM J. Discrete Math. 15(2):165–192, 2002. doi:10.1137/S089548019936223X
• C. Phillips, C. Stein, J. Wein, Minimizing average completion time in the presence of release dates, Math. Programming 82:199–223, 1998. doi:10.1007/BF01585872
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM-SIAM SODA, 591–598, 1997 (no DOI; reference [11] of Goemans et al. 2002).
• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31(1):146–166, 2001. doi:10.1137/S0097539797327180
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, Proc. 40th IEEE FOCS, 32–43, 1999. doi:10.1109/SFFCS.1999.814574

Motivation

In network revenue management a firm sells $n$ products that consume $m$ capacitated resources over $T$ periods, and in each period it chooses which offer set of products to make available. When customers choose among the offered products according to a choice model, the standard planning tool is the choice-based linear program, which assigns a frequency $u_S\ge 0$ to every offer set $S\subseteq N$ (Liu and van Ryzin 2008). It has $2^n$ variables. Its optimal solution is what the firm actually implements: a randomization over offer sets.

For the Markov chain choice model of Blanchet, Gallego and Goyal (2016), Feldman and Topaloglu (2017) show that the choice-based program is equivalent to a reduced linear program with only $2n$ variables. The reduced program can be solved directly, but its solution is a pair of vectors $(\hat x,\hat z)$, not a randomization over offer sets. This mission formalizes the paper's Section 7, which converts the reduced solution back into a randomization over offer sets: the Dimension Reduction algorithm, and Theorem 9, which says that the algorithm produces at most $n+1$ offer sets and that these sets are nested.

Setting

Products are indexed by $N=\{1,\dots,n\}$. A customer arrives wanting product $j$ with probability $\lambda_j$. If the product she visits is offered, she buys it. Otherwise she moves to product $i$ with probability $\rho_{j,i}$, and leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$. Throughout, $\lambda_j>0$, $\rho_{j,i}\ge0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j,i$.

For an offer set $S\subseteq N$, the (Balance) equations

$$P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S$$

have a unique solution. $P_{j,S}$ is the probability that product $j$ is purchased, and $R_{j,S}$ is the expected number of visits to $j$ while it is not offered. Write $P_S=(P_{j,S})_j$ and $R_S=(R_{j,S})_j$.

The set $\mathcal H$ consists of all pairs $(x,z)\in\mathbb R^n\times\mathbb R^n$ with $x,z\ge0$ and $x_j+z_j=\lambda_j+\sum_{i}\rho_{i,j}z_i$ for all $j$. The (Reduced) linear program maximizes $\sum_j T r_j x_j$ over $(x,z)\in\mathcal H$ subject to the capacity rows $\sum_j T a_{q,j}x_j\le c_q$ for each resource $q$.

The Dimension Reduction algorithm starts from the optimal solution $(\hat x,\hat z)$ of (Reduced) and sets $(x^1,z^1)=(\hat x,\hat z)$. At iteration $k$ it forms $S^k=\{j: x^k_j>0\}$. It stops with $\alpha^k=1$ if $S^k=\emptyset$. Otherwise it sets $\alpha^k=\min\{x^k_j/P_{j,S^k}: j\in S^k\}$, stops if $\alpha^k=1$, and if not updates

$$x^{k+1}_j=\frac{x^k_j-\alpha^kP_{j,S^k}}{1-\alpha^k},\qquad z^{k+1}_j=\frac{z^k_j-\alpha^kR_{j,S^k}}{1-\alpha^k}.$$

The weights are $\gamma^k=(1-\alpha^1)\cdots(1-\alpha^{k-1})\alpha^k$.

Formalization targets

Goal: Theorem 9

Let $(\hat x,\hat z)$ be optimal for (Reduced). The algorithm stops at some first iteration $K$ with $1\le K\le n+1$. At that $K$,

$$\hat x=\sum_{k=1}^K\gamma^kP_{S^k},\qquad \hat z=\sum_{k=1}^K\gamma^kR_{S^k},\qquad \sum_{k=1}^K\gamma^k=1,\qquad S^1\supseteq S^2\supseteq\cdots\supseteq S^K .$$

Milestones

In the order the proof uses them:

1. (Balance) has a unique, nonnegative solution for every $S$ (p. 1325).
2. $P_{j,S}>0$ for $j\in S$ (p. 1325).
3. For $(\hat x,\hat z)\in\mathcal H$: $\hat z_j\ge R_{j,S_{\hat x}}$. This is Lemma 11 of the online appendix, as quoted on p. 1332.
4. For $(\hat x,\hat z)\in\mathcal H$ with nonempty support: $\alpha_{\hat x}\le1$ (p. 1332).
5. The two stopping configurations are (Balance) solutions: $S_{\hat x}=\emptyset$ gives $(P_\emptyset,R_\emptyset)$, and $\alpha_{\hat x}=1$ gives $(P_{S_{\hat x}},R_{S_{\hat x}})$ (p. 1332).
6. Lemma 8: one step of the algorithm maps $\mathcal H$ into $\mathcal H$ and removes a minimizing index from the support (p. 1333).
7. The iterates stay in $\mathcal H$, and $S^{k+1}\subseteq S^k\setminus\{j^k\}$ (pp. 1333–1334).

Significance

Theorem 9 makes the reduced program usable. Together with the equivalence of (Reduced) and the choice-based program, it produces an optimal choice-based solution that offers at most $n+1$ sets. By a basic-solution count the choice-based program has an optimal solution with at most $m+1$ nonzero offer sets. Theorem 9 bounds the number by the number of products instead, and adds a structural property: the offered sets form a chain. Each set is contained in the previous one, so the implemented policy offers a single nested sequence of assortments. The algorithm needs at most $n+1$ solutions of linear systems of size $n$. It never enumerates offer sets.

The result is proved in the paper. As far as a search of the platform and of Mathlib shows, it has not been formalized. Mathlib's Carathéodory theorem (Analysis/Convex/Caratheodory) bounds the number of points in a convex combination. It does not construct this decomposition, and it does not give nestedness. Formalizing Theorem 9 therefore requires the paper's argument: a verified, terminating peeling procedure on the polyhedron $\mathcal H$ whose output is a convex combination of (Balance) solutions indexed by a chain of sets.

Difficulty

The algorithm divides twice. Step 2 divides by $P_{j,S^k}$, which must be positive on $S^k$. Step 3 divides by $1-\alpha^k$, which must be nonzero whenever the algorithm continues. Both rest on nontrivial facts: the positivity of purchase probabilities, and the bound $\alpha\le1$ on $\mathcal H$. That bound in turn requires the comparison $\hat z\ge R_{S_{\hat x}}$. The paper proves this comparison only in its online appendix; it is a monotonicity property of the inverse of $I-\rho^\top$ restricted to the unoffered products. The update of Step 3 can make coordinates of $z$ negative unless this comparison holds, so the naive observation that "$(x^k,z^k)$ is a combination of points of $\mathcal H$" does not by itself keep the iterates in $\mathcal H$.

Termination is not a consequence of $\alpha^k<1$ alone. It needs the strict decrease of the support, which comes from choosing a minimizing index. The weights $\gamma^k$ are defined by products of the $(1-\alpha^l)$. Their sum telescopes to $1$ only because the last step has $\alpha^K=1$.

Formalization scope

Everything lives in the namespace MarkovChainChoice.DimReduction. Products are Fin n and offer sets are Finset (Fin n). The model is a structure carrying $\lambda_j>0$, $\sum_i\rho_{j,i}<1$ and, as a disclosed implicit hypothesis, $\rho_{j,i}\ge0$. The pair $(P_S,R_S)$ is chosen by Classical.epsilon among the solutions of (Balance); milestone 1 is what identifies it with the paper's unique solution. Revenues, capacities and consumptions carry no sign conditions. "Optimal for (Reduced)" means feasible and at least as good as every feasible point.

The iterates are indexed from $k=1$ as in the paper. The value at index $0$ is an unused copy of the input. "The algorithm stops at iteration $K$" is the first $K\ge1$ with $S^K=\emptyset$ or $\alpha^K=1$. Iterates after the first stop involve a division by zero, which Lean evaluates to $0$, and no statement refers to them. The termination bound $K\le n+1$ is a conclusion of the goal, not a hypothesis. The goal is about the algorithm's actual iterates, not about an arbitrary sequence that satisfies the invariants. The paper's $\subset$ and $\supset$ denote non-strict inclusion and are rendered as $\subseteq$ and $\supseteq$.

Two milestones are stated more generally than the page. The paper states the iteration invariants for the (Reduced) optimum; the Lean requires only $(\hat x,\hat z)\in\mathcal H$, which every feasible (Reduced) solution satisfies. Lemma 8's $\arg\min$ may be a set; the statement holds for every minimizer. The page contains printed slips: on p. 1332, $\hat v_j$ has numerator $\hat x_j-\alpha R_{j,S}$, and the paper writes $R_{\hat x}$ for $R_{S_{\hat x}}$. The Lean uses the correct forms, as in Lemma 8 and Step 3. None of these slips appears in a milestone quotation.

A complete development needs a small theory of M-matrices, in the form of nonnegativity of $(I-Q)^{-1}$ for substochastic $Q$, together with finite induction on supports. The comparison lemma (milestone 3) and the (Balance) existence and uniqueness result (milestone 1) are reusable across the other missions on this paper. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
• J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
• Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0169

Motivation

A buyer and a seller negotiate over a single indivisible good. Each knows what the good is worth to them but not what it is worth to the other side, and each shades their offer to exploit the other's uncertainty. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this as a one-shot game in which both parties submit sealed offers simultaneously and a sale takes place at a weighted average of the two offers whenever the buyer's offer is at least the seller's.

The weight $k$ is a design parameter: $k = 1$ lets the buyer set the price, $k = 0$ the seller, and $k = 1/2$ splits the difference. For values uniform on a common interval the paper computes an explicit equilibrium for every $k$ (its Example 1) and then asks the questions a designer of the rule cares about: how often does trade happen, who gains when $k$ moves, and which $k$ maximises the expected gains of the two parties together. The answers are the subject of this mission.

The example became a benchmark for bilateral trade. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) proved that no mechanism can guarantee efficient trade with two-sided private information, and that for uniform values the split-the-difference equilibrium of this game attains the largest expected gains from trade of any mechanism. The numbers $9/32$ and $\tfrac{9}{64}\bar v$ below are therefore the second-best benchmarks against which later work on the $k$-double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) measures inefficiency.

Setting

A seller with reservation price $v_s$ and a buyer with reservation price $v_b$ each know their own value. The two values are drawn independently and uniformly on $[0, \bar v]$, with $\bar v > 0$; this law, written $\mathrm{unif}(\bar v)$, is also each player's belief about the other's value ($F_s(v) = F_b(v) = v/\bar v$ in the paper).

Under the Bargaining Rule with parameter $k \in [0,1]$, the seller asks $s$ and the buyer offers $b$. If $b \ge s$ the good is sold at price $P = kb + (1-k)s$, the seller earns $P - v_s$ and the buyer earns $v_b - P$; otherwise both earn zero. Ties trade.

An offer strategy maps a value to an offer. The strategies of Example 1(a) are

$$S(v_s) = \frac{v_s}{2-k} + \frac{1-k}{2}\bar v \quad\text{for } 0 \le v_s \le \tfrac{2-k}{2}\bar v, \qquad S(v_s) \ge \text{the same expression for } \tfrac{2-k}{2}\bar v < v_s \le \bar v,$$ $$B(v_b) = \frac{v_b}{1+k} + \frac{k(1-k)}{2(1+k)}\bar v \quad\text{for } \tfrac{1-k}{2}\bar v \le v_b \le \bar v, \qquad B(v_b) \le \text{the same expression for } 0 \le v_b < \tfrac{1-k}{2}\bar v.$$

A pair $(S, B)$ with these four properties is said to have the shape of Example 1(a) (IsExample1Pair k v̄ S B). On the two inequality ranges a seller asks too much, or a buyer bids too little, for any trade to occur, so the strategy there is free apart from the bound.

For such a pair, with $(v_s, v_b) \sim \mathrm{unif}(\bar v) \otimes \mathrm{unif}(\bar v)$, the trade probability is $\Pr[S(v_s) \le B(v_b)]$ (tradeProb), and the ex ante expected profits — taken before either value is drawn, as the paper specifies on p. 843 — are

$$\pi_s = \mathbb E\bigl[\mathbf 1\{S(v_s) \le B(v_b)\}\,(kB(v_b) + (1-k)S(v_s) - v_s)\bigr],\qquad \pi_b = \mathbb E\bigl[\mathbf 1\{S(v_s) \le B(v_b)\}\,(v_b - kB(v_b) - (1-k)S(v_s))\bigr]$$

(sellerExAnte, buyerExAnte).

Formalization targets

Goal: Example 1(c)(iii), total expected profit

For $0 \le k \le 1$, $\bar v > 0$ and every pair of the shape of Example 1(a),

$$\pi_s + \pi_b = \frac{\bar v}{16}(1+k)(2-k),$$

and as a function of $k \in [0,1]$ this total attains its maximum $\tfrac{9}{64}\bar v$ at $k = 1/2$. The goal is the paper's efficiency statement: among these equilibria, splitting the difference maximises expected group profit.

Milestones

1. Example 1(b). $\Pr[S(v_s) \le B(v_b)] = \dfrac{-k^2 + k + 2}{8}$, with maximum $9/32$ at $k = 1/2$.
2. Example 1(c)(i). $\pi_s(k) = \dfrac{\bar v}{48}(2-k)^2(1+k)$, strictly decreasing in $k$ on $[0,1]$.
3. Example 1(c)(ii). $\pi_b(k) = \dfrac{\bar v}{48}(1+k)^2(2-k)$, strictly increasing in $k$ on $[0,1]$.

The goal is the sum of milestones 2 and 3 together with a one-variable maximisation; milestone 1 describes the trade region over which both profits are integrated.

Significance

The formulas answer the design question for the rule. Moving $k$ toward the buyer's offer makes the price rule look more favourable to the seller, yet milestone 2 shows the seller's equilibrium profit falls and milestone 3 shows the buyer's rises: the paper (p. 844) uses this to show that an intuition which ignores the players' strategic response is mistaken. The comparison with truthful offers, which would trade with probability $1/2$ and earn expected group profit $\bar v/6$, quantifies the cost of strategic misrepresentation: at best $9/32$ and $\tfrac{9}{64}\bar v$.

The paper states these results as "straightforward computations" and prints no derivation. As far as is known, none of them has a machine-checked proof. A formalization settles the constants against the exact strategies of Example 1(a), including the non-linear no-trade branches the paper allows, and provides a worked example of computing trade probabilities and expected payoffs under a product of uniform laws, reusable for other double-auction and bilateral-trade examples.

Difficulty

The computation is elementary on paper, but the equilibrium strategies are only partly specified: on the seller's high range and the buyer's low range the offers are arbitrary functions subject to a bound, and need not be measurable. The obvious approach — substitute the linear formulas and integrate — is valid only after showing that these free branches never trade, so that the trade event and both integrands agree almost everywhere with their linear versions. The resulting integrals are over a product of two conditioned Lebesgue measures, not over Lebesgue measure on the plane, and the trade region depends on $k$ through both strategies. The monotonicity claims hold only on $[0,1]$ (the seller's cubic is not monotone on $\mathbb R$), and the derivative of each profit vanishes at an endpoint of the interval.

Formalization scope

Values are real numbers; the uniform law on $[0, \bar v]$ is Lebesgue measure conditioned on the interval (volume[|Icc 0 v̄]), and the joint law of $(v_s, v_b)$ is the product measure, with pairs ordered $(v_s, v_b)$. The trade probability is the real number (P {p | S p.1 ≤ B p.2}).toReal; the profits are Bochner integrals over the product. Ties trade. The results are ex ante, not conditional on a player's own value. Every theorem assumes $0 \le k \le 1$ and $\bar v > 0$. Maxima are stated with IsMaxOn on $[0,1]$ plus the value at $k = 1/2$; monotonicity with StrictAntiOn/StrictMonoOn on $[0,1]$.

The statements do not assume that $(S, B)$ is an equilibrium; they are computations about any pair of the shape of Example 1(a). That this pair is an equilibrium is Example 1(a) itself, the goal of a companion mission. No measurability of $S$ or $B$ is assumed: the free branches never trade, so each integrand agrees almost everywhere with a bounded measurable function and the integrals are the paper's expectations. A formalization that assumes $S$ and $B$ linear everywhere, or that integrates over a single uniform variable, proves a different statement.

A complete development needs: the reduction of the trade event and the integrands to their linear versions on $[0,\bar v]^2$; Fubini for the product of conditioned measures; evaluation of polynomial integrals over a triangle; and elementary calculus on cubics. Lemmas on integrating over products of uniform laws are reusable. Contributions of intermediate lemmas, such as the explicit trade region, are welcome.

Selected references

• K. Chatterjee and W. Samuelson, Bargaining under Incomplete Information, Operations Research 31(5):835–851, 1983. https://doi.org/10.1287/opre.31.5.835
• R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• M. A. Satterthwaite and S. R. Williams, Bilateral Trade with the Sealed Bid k-Double Auction: Existence and Efficiency, Journal of Economic Theory 48(1):107–133, 1989. https://doi.org/10.1016/0022-0531(89)90120-8
• W. Leininger, P. B. Linhart and R. Radner, Equilibria of the Sealed-Bid Mechanism for Bargaining with Incomplete Information, Journal of Economic Theory 48(1):63–106, 1989. https://doi.org/10.1016/0022-0531(89)90121-X

Motivation

The traveling-salesman problem (TSP) asks for a cheapest cycle through all vertices of a weighted complete graph. Exact algorithms for it are branch-and-bound searches, and their size depends almost entirely on the quality of the lower bounds used to prune the search. In 1970 Held and Karp introduced the 1-tree bound: a Lagrangian relaxation of the degree-2 constraints of a tour, whose value can be evaluated by one minimum-spanning-tree computation (Held & Karp, Part I, 1970). Part II (Held & Karp, 1971) replaces the ascent procedure of Part I by an iterative method related to the relaxation method for linear inequalities of Agmon and of Motzkin and Schoenberg (1954), and with it solved to proven optimality every instance presented to it, up to 64 cities. The iteration is the prototype of what is now called the subgradient method with Polyak-type step sizes, and the 1-tree bound remains a standard lower bound in exact TSP codes.

Timeline:

• 1954 — Agmon; Motzkin and Schoenberg: the relaxation method for systems of linear inequalities, and convergence of Féjer-monotone sequences relative to full-dimensional sets.
• 1970 — Held and Karp (Part I): the 1-tree bound $\max_\pi w(\pi)$ and a column-generation / ascent method for it.
• 1971 — Held and Karp (Part II): the iteration $\pi^{m+1} = \pi^m + t_m v_{k(\pi^m)}$, its relaxation-method analysis (Lemmas 1–3) and the constant-step guarantee (Theorem 1).
• 1974 — Held, Wolfe and Crowder validate the method as general subgradient optimization.

Setting

Let $n \ge 3$ and let $(c_{ij})$ be a symmetric real $n\times n$ matrix of weights on the edges of the complete graph $K_n$ with vertex set $\{1,\dots,n\}$; weights may be negative and need not satisfy the triangle inequality. A subgraph has weight equal to the sum of its edge weights. A tour is a cycle through every vertex exactly once; $C^*$ is the weight of a minimum tour.

A 1-tree is a tree on the vertex set $\{2,\dots,n\}$ together with two distinct edges at vertex $1$. Index the 1-trees by $k$; let $c_k$ be the weight of the $k$-th 1-tree, $d_{ik}$ the degree of vertex $i$ in it, and $v_k \in \mathbb R^n$ the degree-excess vector with components $d_{ik}-2$. For $\pi \in \mathbb R^n$ define

$$w(\pi) = \min_k\,[c_k + \pi\cdot v_k].$$

A tour is a 1-tree with $v_k = 0$, so $C^* \ge w(\pi)$ for every $\pi$ (Eq. (2)); the best bound is $\max_\pi w(\pi)$. For a point $\pi$, $k(\pi)$ denotes a minimum-weight 1-tree at $\pi$, a 1-tree attaining the minimum defining $w(\pi)$. The ascent iteration (3) is

$$\pi^{m+1} = \pi^m + t_m\,v_{k(\pi^m)}.$$

For a target value $\bar w$, $P_{\bar w}$ is the polyhedron of solutions of $\bar w \le c_k + \pi\cdot v_k$ for all $k$ (system (5)). All norms $\|\cdot\|$ are Euclidean.

Formalization targets

Goal: Theorem 1

With constant step $t_m = \bar t > 0$, any starting point and any choice of minimum-weight 1-trees,

$$\sup_m w(\pi^m) \;\ge\; \max_\pi w(\pi) - \tfrac12\,\bar t\,\limsup_{m\to\infty}\|v_{k(\pi^m)}\|^2 .$$

Milestones

1. Eq. (2): $C^* \ge w(\pi)$ for every $\pi$.
2. Lemma 1: if $w(\bar\pi) \ge w(\pi)$ then $(\bar\pi-\pi)\cdot v_{k(\pi)} \ge w(\bar\pi) - w(\pi) \ge 0$.
3. Lemma 2: if $0 < t < 2(w(\bar\pi)-w(\pi))/\|v_{k(\pi)}\|^2$ then $\|\bar\pi - (\pi + t v_{k(\pi)})\| < \|\bar\pi-\pi\|$.
4. Féjer-monotone convergence (Motzkin–Schoenberg, quoted in the proof of Lemma 3): a sequence whose distance to every point of a set with nonempty interior is nonincreasing converges.
5. Lemma 3, Case 1: for $\bar w < \max_\pi w$ and the relaxation iteration

$$\pi^{m+1} = \pi^m + \lambda_m\,\frac{\bar w - w(\pi^m)}{\|v_{k(\pi^m)}\|^2}\,v_{k(\pi^m)} \qquad (6)$$

with $0<\varepsilon<\lambda_m\le 2$, the iterates enter $P_{\bar w}$ or converge to a boundary point of $P_{\bar w}$. 6. Lemma 3, Case 2: with $\lambda_m = 2$ the iterates enter $P_{\bar w}$. 7. §3 bound: the restricted minimum $w_{X,Y}(\pi)$ over 1-trees containing the edges $X$ and avoiding the edges $Y$ is a lower bound on every tour of the derived problem.

Milestones 1–5 are the steps of the paper's proof of Theorem 1; 6 and 7 are further results of the paper on the same objects.

Significance

Theorem 1 is the paper's justification of the step rule actually used in its computations: a fixed step $\bar t$ loses at most $\tfrac12\bar t$ times the asymptotic squared deviation of the generated 1-trees from being tours. Since $\|v_k\|^2$ is an even integer that vanishes exactly on tours, and the paper observes it is typically small in practice, the bound explains why the constant-step ascent reaches bounds sharp enough for branch-and-bound. Lemmas 1–3 are the first analysis of a subgradient-type method for a nonsmooth concave function, cast as the relaxation method for the (exponentially large) system (5).

All results are proved in the paper (except the Féjer-monotone convergence and Case 2 of Lemma 3, which it cites from Motzkin and Schoenberg). None is formalized: the platform has the 1-tree lower bound only under a metric assumption on the weights (SupplyChainTheory.held_karp_bound, SupplyChainTheory.one_tree_lower_bound), and the subtour-LP bound MetricTSP.held_karp_le_opt, a different object. This mission produces the bound for arbitrary real weights, the supergradient property of $v_{k(\pi)}$, and a machine-checked convergence analysis of the relaxation iteration.

Difficulty

Lemmas 1 and 2 and Eq. (2) are short once the finite minimum defining $w$ is handled. The difficulty is in Lemma 3 and Theorem 1. The iteration is not monotone in $w$, so no descent argument applies; progress is measured by the Euclidean distance to the target polyhedron $P_{\bar w}$, and turning distance decrease into convergence requires the Féjer-monotonicity theorem, which in turn needs $P_{\bar w}$ to have nonempty interior (from $\bar w < \max_\pi w$). In Theorem 1 the step is constant rather than of the relaxation form (6), and the target polyhedron is not given in advance: the relevant relaxation parameters are admissible only eventually and must be kept away from zero, which requires controlling degenerate directions $v_{k(\pi^m)} = 0$ and the behaviour of $w$ along an iteration that is not known a priori to stay bounded. A direct argument that $w(\pi^m)$ increases fails, since single steps can decrease $w$.

Formalization scope

Vertices are Fin n, the paper's vertex 1 is 0 : Fin n, and graphs are SimpleGraph (Fin n). Weights are c : Sym2 (Fin n) → ℝ, arbitrary reals. A 1-tree is a graph whose restriction to the vertices other than 0 is a tree and in which 0 has degree 2; a tour is a connected graph with all degrees 2. w(π) is the minimum of weight c G + ∑ i, π i * (deg G i − 2) over 1-trees, written as an sInf over a finite set that is nonempty for n ≥ 3; every theorem assumes 3 ≤ n. Euclidean norms and inner products are written as coordinate sums of squares and products, never Mathlib's sup norm on Fin n → ℝ. The minimum-weight 1-tree $k(\pi^m)$ is a hypothesis at every step, and ties may be broken arbitrarily. The goal is stated as "for every $\pi^*$ and $\delta>0$ some iterate has $w(\pi^m) > w(\pi^*) - \tfrac12\bar t L - \delta$", which is equivalent to the printed inequality; $L$ is the limsup of a sequence with finitely many values, a genuine real.

The statements exclude trivializing readings: the 1-tree predicate rejects graphs without exactly two edges at vertex 1; w is never a minimum over an empty set under the standing hypothesis 3 ≤ n; no ⨆ of a possibly unbounded family is used; the step size $\bar t$ and the parameter $\varepsilon$ are strictly positive.

A complete development needs finite minima of affine functions (concavity, attainment), 1-tree and tour combinatorics on simple graphs, and Féjer-monotone sequences in $\mathbb R^n$; the last two are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 3, are welcome.

Selected references

• M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
• M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees, Operations Research 18 (1970) 1138–1162. https://doi.org/10.1287/opre.18.6.1138
• T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 393–404. https://doi.org/10.4153/CJM-1954-038-x
• S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 382–392. https://doi.org/10.4153/CJM-1954-037-2
• M. Held, P. Wolfe and H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223

Motivation

This mission continues chapter 11's account of the M♮-concave/M♮-convex exchange-economy model begun in mission 14-economic-equilibrium, placing seven of that chunk's own results that were previously left out-of-cone: the two gross-substitutes-style characterizations of M♮-concavity (§11.3), the transfer theorem that lifts an equilibrium of the continuous relaxation to one for indivisible commodities (§11.4), and the explicit polyhedral description of the equilibrium price set together with its feasibility criterion (§11.5).

Setting

Mission 14-economic-equilibrium built the exchange-economy vocabulary this mission redeclares in full (UDom, ArgMaxBot/ArgMinTop, PriceShift/PriceShiftConvex, DemandSet/SupplySet, IsEquilibrium, MNaturalConcave, IsMNaturalConvexSet, the concave/convex closures ConcaveClosureR/ConvexClosureR and their continuous analogues ContDemandSet/ContSupplySet/ IsContEquilibrium) and placed the qualitative structural theorems (Theorems 11.1-11.3, 11.4, 11.16-11.18, 11.23-11.24). This mission adds the gross-substitutes axioms (−M♮-GS[Z], the price-monotonicity property NegGS, and −M♮-SWGS[Z], its one-price-at-a-time refinement NegSWGS), the M♮-convex-set transfer machinery connecting a continuous equilibrium to a discrete one, and the equilibrium price polyhedron built from the three bound families ℓ(j), u(j), u(i,j) (Eqs. (11.40)-(11.42)) that make Theorem 11.16's qualitative L♮-convex-polyhedron fact concrete and linear-programming-checkable.

Formalization targets

Goal: The equilibrium price set is the explicit L♮-convex polyhedron (11.43) (Theorem 11.21)

For a fixed allocation (x,y), the set P* of all equilibrium price vectors is an L♮-convex polyhedron and equals the polyhedron cut out by max{0,ℓ(j)} ≤ p(j) ≤ u(j) and p(j)-p(i) ≤ u(i,j). Chosen as goal: it is the sharpest structural result of chapter 11's computation section, upgrading Theorem 11.16's qualitative fact to a concrete description, and is what Theorem 11.22 (also placed) builds on directly.

Supporting structural targets

Theorem 11.5 and Theorem 11.6 characterize M♮-concavity via the gross-substitutes and stepwise gross-substitutes properties, completing chapter 11's suite of M♮-concavity characterizations begun with Theorem 11.4 (mission 14). Theorem 11.15 is the general transfer theorem (continuous equilibrium ⟹ discrete equilibrium) that mission 14's own Theorem 11.14 invokes as a special case. Theorem 11.22 gives the feasibility criterion for the existence of an equilibrium price vector, the mission's second theorem built on the equilibrium price polyhedron.

Significance

Together with mission 14-economic-equilibrium, this mission completes the book's account of how M♮-concavity/convexity — a purely combinatorial exchange condition — reproduces, and sharpens, the classical gross-substitutes theory of competitive equilibrium for economies with indivisible goods: existence transfers from the continuous relaxation, and the equilibrium price set itself has a description exact enough to reduce to a linear feasibility question. None of these results are open — they are Murota's own account (attributed in the book's own notes to Danilov-Koshevoy- Lang and Murota-Tamura for the gross-substitutes theorems, and to Murota-Tamura for the equilibrium price polyhedron); this mission contributes a faithful, machine-checked formal statement of each (see Formalization scope).

Difficulty

Two of this chunk's seven BRIEF.md results are not drafted this pass, for a disclosed time- budget reason rather than any faithfulness failure: Proposition 11.19 and Theorem 11.20 require the H,L-indexed bipartite MSFP2 flow-network vocabulary (separate vertex sets V+_e, V+_l, V-_h, an M-convex/M-concave-combining flow objective) that neither this mission nor mission 14 builds, and building it in proportion to placing exactly these two results was judged disproportionate to the remaining time in this pass; see HARD.md and STATUS.md. This is explicitly not a hard exclusion — both results are well-posed and provable from the book's own complete proofs — and is recorded as an honest scope limitation for a future pass. Theorem 11.22's own trailing algorithmic remark (that equilibrium prices can be found via a shortest-path computation, yielding a polynomial-time equilibrium-checking algorithm) is a computational/ complexity claim outside this series' propositional-formalization methodology and is omitted; the mathematical "iff feasibility" content is placed in full. See HARD.md.

Formalization scope

Ground set K is a Fintype with DecidableEq; consumer/producer index sets H, L are Fintypes (Nonempty where the price-bound formulas (11.40)-(11.42) need a nonempty sup'/inf' range). All base vocabulary is redeclared fresh from mission 14-economic-equilibrium's own definitions, since this draft cannot import that sibling mission. The gross-substitutes axioms are formalized directly from their defining inequalities (Eqs. preceding (11.19) and following, and p.331); the equilibrium price polyhedron's bound families ℓ(j)/u(j)/u(i,j) are formalized literally from Eqs. (11.40)-(11.42), extracting each WithBot ℝ/WithTop ℝ operand to ℝ before subtracting (since WithBot ℝ carries no subtraction instance). Two results (Proposition 11.19, Theorem 11.20) are not drafted this pass for the disclosed time-budget reason above; one result (Theorem 11.22's trailing algorithmic remark) is scoped out as computational content. Contributions completing any of the five sorrys, or building the MSFP2 vocabulary to place Proposition 11.19/Theorem 11.20 in a follow-up mission, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• V. Danilov, G. Koshevoy, K. Murota, "Discrete convexity and equilibria in economies with indivisible goods and money," Mathematical Social Sciences, 41 (2001), pp. 251-273 [33] (origin of the gross-substitutes characterization, Theorem 11.6).
• K. Murota, A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [160] (origin of the equilibrium price polyhedron, Theorems 11.20-11.22).

Motivation

Competitive-equilibrium theory for economies of divisible commodities — where consumption and production are real vectors — has rested on a rigorous mathematical foundation since around 1960, built from convexity, compactness, and fixed-point theorems (Debreu 1959; Arrow–Hahn 1971; McKenzie 2002). A large share of real markets, however, trade goods that cannot be split: houses, cars, aircraft, job assignments, radio spectrum licenses. For such economies, no comparably general existence theory existed before the framework this mission formalizes. Kelso and Crawford (1982) and Gul and Stacchetti (1999) had identified the gross substitutes property as the right condition on preferences for equilibrium to exist in labor-market and assignment models; Danilov, Koshevoy, and Murota (1998, 2001) showed that gross substitutes, and several other conditions proposed independently in the economics literature, all coincide with a single combinatorial notion from discrete convex analysis: M-natural-concavity. This mission formalizes the resulting existence theorem for economies with indivisible goods, together with the definitional results that pin down exactly what M-natural-concavity of a utility function means and how it connects to the classical demand-set language of general equilibrium theory.

Setting

Fix a finite set $K$ of indivisible commodity types and a finite set $H$ of consumers ("she"). A consumption bundle is an integer vector $x \in \mathbb Z^K$, one coordinate per commodity. Consumer $h$'s preferences over bundles, net of a perfectly divisible numeraire ("money"), are summarized by a utility function $U_h : \mathbb Z^K \to \mathbb R \cup \{-\infty\}$, where $-\infty$ marks bundles outside her feasible range (her effective domain, $\operatorname{dom} U_h = \{x : U_h(x) \ne -\infty\}$). Given a price vector $p \in \mathbb R^K$ (one real price per commodity), consumer $h$ chooses a bundle from her demand set

$$D_h(p) = \arg\max_{x \in \mathbb Z^K} \big(U_h(x) - \langle p, x\rangle\big),$$

the bundles that maximize utility net of expenditure; the shorthand $U_h[-p](x) := U_h(x) - \langle p,x\rangle$ is used throughout. For the notion this mission is built around, write $\chi_i \in \mathbb Z^K$ for the $i$-th unit vector, and for $x, y \in \mathbb Z^K$ let $\operatorname{supp}^+(x-y) = \{k : x(k) > y(k)\}$ and $\operatorname{supp}^-(x-y) = \{k : x(k) < y(k)\}$. A function $U$ with nonempty effective domain is M-natural-concave if it satisfies the exchange axiom: for $x, y \in \operatorname{dom} U$ and $i \in \operatorname{supp}^+(x-y)$,

$$U(x) + U(y) \le \max\Big(U(x-\chi_i)+U(y+\chi_i),\ \max_{j \in \operatorname{supp}^-(x-y)} \big[U(x-\chi_i+\chi_j) + U(y+\chi_i-\chi_j)\big]\Big),$$

with the convention that a maximum over the empty set is $-\infty$. A producer $l$ from a finite set $L$ is symmetric, described by a cost function $C_l : \mathbb Z^K \to \mathbb R \cup \{+\infty\}$ that is M-natural-convex — the mirror-image exchange axiom with $\min$ in place of $\max$ and the inequality reversed — and a supply set $S_l(p) = \arg\max_y(\langle p,y \rangle - C_l(y))$. An equilibrium for a total initial endowment $x^\circ \in \mathbb Z^K$ is a tuple $((x_h \mid h \in H), (y_l \mid l \in L), p)$ with $x_h \in D_h(p)$, $y_l \in S_l(p)$, market clearing $\sum_h x_h = x^\circ + \sum_l y_l$, and $p \ge 0$.

Formalization targets

$$\textbf{Theorem 11.13 (goal).}\quad \text{If every } U_h \text{ is nondecreasing and M-natural-concave with bounded domain, an equilibrium exists for every } x^\circ \in \bigcap_h \operatorname{dom} U_h \text{ in the exchange economy } (L = \emptyset).$$

This is the weakest form of the existence claim the mission proves in full — no producers, so no interaction between two different M-natural-convexity classes is needed — and is the natural target because it isolates exactly what M-natural-concavity buys on the consumer side alone. Two companion results sharpen the picture: Theorem 11.4 pins down M-natural-concavity through an equivalent single-step ascent property, and Theorem 11.7 restates it through the combinatorial structure (M-natural-convexity) of the demand sets themselves, connecting the definition to the gross-substitutes literature. Proposition 11.12 supplies the structural fact the existence proof turns on (the aggregate excess-cost function inherits M-natural-convexity and has a nonempty subdifferential), Theorem 11.14 extends existence to the general economy with producers by transporting an equilibrium down from a continuous relaxation, and Theorem 11.16 establishes that the set of all equilibrium prices is not merely nonempty but a lattice-structured polyhedron.

Significance

The result itself. Theorem 11.13 is a genuine existence theorem for a discrete general- equilibrium model — not an approximation or a relaxation of the continuous theory, but a free-standing result about the integer lattice. Its consequence set is also constructive by consequence: Theorem 11.16's lattice structure and section 11.5's reduction to submodular-flow computation (not part of this mission) together show that finding an extreme equilibrium price is a polynomial-time problem, not merely a nonempty-existence claim. Before this line of work, economists working with indivisible goods either restricted to special two-sided matching structures or worked with sufficient conditions (such as gross substitutes) whose relationship to each other and to any unifying combinatorial property was not understood; Fujishige–Yang (2003) and Murota–Tamura independently identified the M-natural-concavity connection cited here.

Formalizing it. All of the results in this mission are proved in the source text; nothing here is open. What formalization adds is a machine-checked confirmation that the demand/supply-set and equilibrium definitions, and the exchange-axiom characterization of M-natural-concavity, compose exactly as the informal statements claim — a nontrivial check, since the definitions involve several layers of arg-max/arg-min over integer lattices and price-shifted objectives that are easy to state slightly wrong (e.g. conflating $\arg\max$ and $\arg\min$, or omitting the extended index $0$ in the single-improvement axiom).

Difficulty

The obvious approach to existence — relax the discrete problem to $\mathbb R^K$, apply a classical fixed-point argument, and round the resulting continuous equilibrium to the nearest integer point — fails outright, and the book devotes section 11.2 to a two-agent, two-good example that demonstrates this concretely: at certain initial endowments, every candidate integer allocation leaves an unclaimed unit of surplus, so no equilibrium price exists at all, even though the continuous relaxation of the same economy has one. The gap is a failure of convexity in the Minkowski sum $D_1(p) + D_2(p)$: ordinary discrete demand sets can be "hole-free" individually and still sum to a set with a hole. M-natural-concavity is precisely the condition under which Minkowski sums of demand sets stay hole-free (a consequence of the parallel discrete-convex-set theory this book develops earlier), which is what makes the round-down argument valid after all — but only under this specific hypothesis, not under plain concavity or submodularity.

Formalization scope

Commodities and prices live on a general finite type $K$ (Fintype, DecidableEq), not a fixed $\mathrm{Fin}\ n$; consumers and producers are indexed by general finite types $H$, $L$, with the pure exchange economy realized as the special case $L = \mathrm{PEmpty}$. Utility values lie in WithBot ℝ ($\mathbb R \cup \{-\infty\}$) and cost values in WithTop ℝ ($\mathbb R \cup \{+\infty\}$), matching the book's asymmetric conventions for the two families exactly; no constant appears anywhere in this mission's statements (all hypotheses and conclusions are qualitative), so there is no explicit-constant obligation to record. The one hypothesis that must never be silently dropped is "nondecreasing" in Theorem 11.13: it is a real, separate condition from M-natural-concavity (more of a good is always weakly preferred), stated as its own conjunct rather than folded into the concavity predicate. A formalization that replaced M-natural-concavity with ordinary real-valued concavity, or dropped the boundedness hypothesis on the domains, would be a different — and for indivisible goods, false — statement; section 11.2's example is a concrete witness that discreteness together with a weaker structural hypothesis than M-natural-concavity is not enough. This mission's "M-natural-convex set" (used in Theorem 11.7) and "L-natural-convex polyhedron" (used in Theorem 11.16) are each formalized via one of the book's own stated equivalent characterizations (projection of an M-convex set on an extended ground set, and the (SBS-natural[R]) lattice-translation property respectively) rather than reintroduced as new primitives. Reusable beyond this mission: the general subdifferential SubdiffR and the EReal-valued concave/convex closure constructions apply to any discrete convex/concave function, not only to the aggregate cost function of this chapter. Contributions welcome on the sorry'd proofs, and on formalizing section 11.5's computational reduction to the M-convex submodular flow problem (deferred here — see HARD.md — pending chunk 12's flow vocabulary).

Selected references

• Murota, K. Discrete Convex Analysis. SIAM, 2003. DOI: 10.1137/1.9780898718508. (Chapter 11.)
• Kelso, A. S., Crawford, V. P. "Job Matching, Coalition Formation, and Gross Substitutes." Econometrica 50(6), 1982, 1483–1504.
• Gul, F., Stacchetti, E. "Walrasian Equilibrium with Gross Substitutes." Journal of Economic Theory 87(1), 1999, 95–124.
• Danilov, V., Koshevoy, G., Murota, K. "Discrete Convexity and Equilibria in Economies with Indivisible Goods and Money." Mathematical Social Sciences 41(3), 2001, 251–273.
• Fujishige, S., Yang, Z. "A Note on Kelso and Crawford's Gross Substitutes Condition." Mathematics of Operations Research 28(3), 2003, 463–469.
• Debreu, G. Theory of Value: An Axiomatic Analysis of Economic Equilibrium. Yale University Press, 1959.