All missions

Motivation

Insertion heuristics build a traveling salesman tour one city at a time: start from a single city, and at each step choose a city not yet on the subtour and splice it into the subtour where it lengthens the subtour least. Local search heuristics start from a tour and repeatedly replace a few of its edges by others while this shortens the tour. Both families are standard in practice, and a natural engineering idea is to combine them: run an insertion heuristic, then polish the result by local search. The question this mission formalizes is whether local optimality of the insertion tour certifies anything about its quality.

Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) answered this for graphs satisfying the triangle inequality. Their §4 proves that nearest and cheapest insertion always return a tour of length at most $2(1-1/n)$ times the optimal length, and their Theorem 5 shows this bound is attained. Their §7 then shows that the very tour attaining the bound is $k$-optimal for every $k\le n/4$: no exchange of $k$ edges shortens it. So the insertion bound is tight even for tours that local search with $k$-changes cannot improve.

Timeline, as far as this mission is concerned:

• 1965: Lin (Bell System Tech. J. 44) defines $k$-optimal tours and uses 3-optimal local search.
• 1973: Lin and Kernighan (Oper. Res. 21) generalize the edge-exchange neighbourhoods.
• 1977: Rosenkrantz, Stearns and Lewis prove the $2(1-1/n)$ upper bound for nearest and cheapest insertion (Theorem 4 and its corollary), its tightness for $n\ge 6$ (Theorem 5), the existence of $k$-optimal tours with the same ratio (Theorem 6, stated for $n\ge 8$), and the Corollary combining the two.

Setting

A traveling salesman graph on $n$ nodes is the node set $N=\{1,\dots,n\}$ with a distance $d(i,j)\ge 0$ that is symmetric and satisfies the triangle inequality $d(i,k)\le d(i,j)+d(j,k)$. A tour is a Hamiltonian circuit; its length is the sum of its edge lengths; OPTIMAL is the least length of a tour. As in the paper, the identically zero distance is excluded, so OPTIMAL $>0$.

A subtour is a circuit on a subset of the nodes (a single node is a subtour without edges). For a subtour $T$ and a node $k\notin T$, TOUR$(T,k)$ is obtained by deleting an edge $(x,y)$ of $T$ minimizing $d(x,k)+d(k,y)-d(x,y)$ and adding $(x,k)$ and $(k,y)$; COST$(T,k)$ is the resulting increase in length. An insertion method chooses nodes $a_0,a_1,\dots,a_{n-1}$, starts from $T_1=\{a_0\}$ and sets $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$; INSERT is the length of $T_n$. Nearest insertion chooses $a_i$ minimizing $d(T_i,x)=\min_{y\in T_i}d(y,x)$ over $x\notin T_i$; cheapest insertion chooses $a_i$ minimizing COST$(T_i,x)$. Ties are broken arbitrarily.

A $k$-change of a tour deletes $k$ of its edges and adds $k$ other edges so that another tour is obtained. A tour is $k$-optimal if no $k$-change produces a strictly shorter tour.

The extremal instance is the circle $(N_n,d_n)$: $n$ cities equally spaced on a circular road, with $d_n(i,j)$ the smallest $m\ge 0$ with $i-j\equiv m$ or $j-i\equiv m \pmod n$. The insertion run of Theorem 5 inserts the cities in the order $1,2,\dots,n$ and produces the zig-zag tour $T_n$: city 1, then the even cities in increasing order, then the odd cities in decreasing order.

Formalization targets

Goal: the Corollary to Theorem 6

For $n\ge 6$ and $4k\le n$ there is a traveling salesman graph with OPTIMAL $>0$ on which some run of nearest insertion, and some run of cheapest insertion, return a $k$-optimal tour with

$$\frac{\mathrm{INSERT}}{\mathrm{OPTIMAL}}=2\left(1-\frac1n\right).$$

Milestones

1. The insertion run on the circle: the subtours $T_i$ and nodes $a_i=i+1$ form an insertion run that obeys both the nearest and the cheapest rule (proof of Theorem 5).
2. On the circle, $T_n$ has length $2(n-1)$ and OPTIMAL $=n$ (proof of Theorem 5).
3. Theorem 5: for $n\ge 6$ there is a graph with INSERT/OPTIMAL $=2(1-1/n)$ for both methods.
4. Equation (7.4): the length of a tour of the circle is the sum over unit edges $e$ of COUNT$(e,T)$, the number of times $e$ is traversed when each tour edge is replaced by a shortest arc.
5. Every tour of the circle is odd or even (all counts of one parity), eq. (7.5).
6. $T_n$ is the shortest even tour, so every tour shorter than $T_n$ is odd.
7. $T_n$ is $k$-optimal for every $k\le n/4$.
8. Theorem 6: for $n\ge 8$ there is a graph with a tour that is $k$-optimal for all $k\le n/4$ and has LOCALOPT/OPTIMAL $=2(1-1/n)$.

Significance

The result. The Corollary shows that the $2(1-1/n)$ worst-case guarantee of nearest and cheapest insertion cannot be improved by requiring that the returned tour survive $k$-change local search, for $k$ up to a quarter of the number of cities. Theorem 6 says more generally that $k$-optimality with $k\le n/4$ does not bound the ratio to the optimum below $2(1-1/n)$. Together with the paper's upper bound, the insertion guarantee is exact, and it stays exact after local polishing with small neighbourhoods.

Formalizing it. All statements are proved in the paper; none, to our knowledge, has been machine-checked. The platform has an upper bound for nearest insertion (SupplyChainTheory, Theorem 10.7, ratio at most 2) but no tightness example and no notion of $k$-optimality. This mission produces a reusable definition of $k$-changes against arbitrary tours, the circle metric, and the parity-counting argument on a cycle, and it supplies the calculations the paper omits ("We omit these calculations but note that they require the assumption $n\ge 6$").

Difficulty

Two steps carry the weight. First, the omitted calculations for the insertion run: at each stage one must show that inserting $a_i$ between $i-1$ and $i$ minimizes the insertion increase over every edge of the zig-zag subtour, and that no other outside city can be inserted for less than 2; the claim fails for $n=4$ and $n=5$, so the verification must use $n\ge 6$ in an essential way. Second, $k$-optimality is a statement about every tour at edge difference $k$, not about 2-opt segment reversals or any specific move family. A search over moves of a special form does not establish it; the argument must bound the length of an arbitrary tour at edge difference $k$ from below.

Formalization scope

Nodes are Fin n, so the paper's node $m$ is index $m-1$ and $a_i=i+1$ is index $i$; subtour indices stay 1-based ($T_1=[a_0]$, approximation $T_n$). A distance is d : Fin n → Fin n → ℝ with the structure IsTSPDist (symmetric, nonnegative, triangle inequality, and $d(i,i)=0$; the last is a normalization absent from the paper that changes no length). A tour is an Equiv.Perm (Fin n), a subtour a list read cyclically; OPTIMAL is Finset.univ.inf' over permutations, the true minimum. TOUR$(T,k)$ is insertion at a position minimizing the new length; COST is a minimum over positions; the nearest-insertion distance (4.1) takes values in WithTop ℝ, so no junk value arises. $k$-optimality compares the tour with every permutation whose edge set (unordered pairs) misses exactly $k$ of the tour's edges. Ratios are multiplied out.

COUNT$(e,T)$ needs a choice of shortest arc for antipodal pairs when $n$ is even; the formalization takes the arc through $\min(x,y),\dots,\max(x,y)$. The paper's argument does not depend on this choice.

Deviations from the printed text: the Corollary is stated for $n\ge 6$ (the printed statement says only $4k\le n$, but its proof uses the example of Theorem 5, which exists for $n\ge 6$; for $k=0$, $n=3$ the printed statement is false). Theorem 6 keeps its printed $n\ge 8$. In the proof of Theorem 5 the paper writes "(4.2) holds" where the cheapest-insertion condition (4.3) is meant; the formal statement uses (4.3).

The existence statements carry OPTIMAL $>0$, the paper's standing assumption (1.1). Without it, the zero distance would make every length zero and every tour $k$-optimal, which would satisfy the ratio equations trivially; that formalization is ruled out.

Contributions welcome: proofs of any milestone, in particular the omitted insertion calculations and the parity lemma, and reusable lemmas on cyclic lists and edge sets of permutations.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM J. Comput. 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• S. Lin, Computer solutions of the traveling salesman problem, Bell System Tech. J. 44:2245–2269, 1965. https://doi.org/10.1002/j.1538-7305.1965.tb04146.x
• S. Lin, B. W. Kernighan, An effective heuristic algorithm for the traveling-salesman problem, Oper. Res. 21(2):498–516, 1973. https://doi.org/10.1287/opre.21.2.498

Motivation

In a combinatorial auction a set of $m$ items is sold to $n$ bidders who value bundles of items rather than single items. Spectrum auctions, procurement of transportation lanes and the allocation of cloud resources all have this form, and the central algorithmic question is how to allocate the items so as to maximize the social welfare, the sum of the bidders' values for what they receive. Even to describe a general valuation takes $2^m$ numbers, so algorithms access the bidders through queries, and the achievable approximation depends on the class of valuations allowed.

Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010) study bidders without complementarities. For the class of XOS valuations, maxima of additive valuations, which strictly contains the submodular valuations, they give LP-based algorithms and, in §3.3, a purely combinatorial algorithm: bidders arrive one at a time, take their demanded bundle at the current item prices, and raise the prices of what they took. Its analysis charges the welfare of any allocation to the item prices the algorithm sets, an argument that uses only the demand and XOS oracles.

Setting

The items are $M=\{1,\dots,m\}$ and the bidders $1,\dots,n$.

• An additive valuation (a clause) $w$ assigns nonnegative values $w(1),\dots,w(m)$ to the items and $w(S)=\sum_{j\in S}w(j)$ to a bundle $S\subseteq M$.
• An XOS valuation $v$ is given by a nonempty finite set of clauses $\{w_1,\dots,w_t\}$ (its XOS expression) through $v(S)=\max_k w_k(S)$. A clause $w_k$ with $w_k(S)=v(S)$ is a maximizing clause for $S$. Every XOS valuation is normalized, $v(\emptyset)=0$, and monotone.
• An allocation is a tuple of pairwise disjoint bundles $O_1,\dots,O_n$; items may stay unallocated. Its welfare is $\sum_i v_i(O_i)$.
• A demand oracle for bidder $i$ answers, given item prices $p\in\mathbb R^m$, a bundle maximizing $v_i(T)-\sum_{j\in T}p_j$. An XOS oracle answers, given a bundle $S$, a maximizing clause for $S$ in $v_i$.

The greedy price-update algorithm. Start with all bundles empty and all prices $p_j=0$. For $i=1,\dots,n$: let $S_i$ be bidder $i$'s demand at the current prices; remove the items of $S_i$ from the bundles of the earlier bidders; let $q^i$ be the maximizing clause for $S_i$ in $v_i$; set $p_j=q^i_j$ for $j\in S_i$. Write $p^k$ for the prices after stage $k$ ($p^0=0$), $p^k(T)=\sum_{j\in T}p^k_j$, and $A_1,\dots,A_n$ for the final bundles.

In the Lean development these objects are XOSExpr, XOSExpr.val, IsAllocation, welfare, IsDemandOracle, IsXOSOracle, greedyState, greedyPrices and greedyAlloc in the namespace ComplementFreeCA.XOSGreedy.

Formalization targets

Goal: Theorem 3.3

For XOS valuations $v_1,\dots,v_n$, every demand oracle and every XOS oracle, and every allocation $O_1,\dots,O_n$,

$$\sum_{i=1}^n v_i(O_i)\;\le\;2\sum_{i=1}^n v_i(A_i).$$

The comparison with every allocation is the paper's comparison with the optimal allocation.

Milestones

1. Lemma 3.4. The final prices are paid for by the algorithm's welfare:

$$p^n(M)\le\sum_i v_i(A_i).$$

2. Lemma 3.5. Prices never decrease: $p^k_j\le p^{k'}_j$ for all items $j$ and stages $k\le k'$.
3. Lemma 3.6. For every allocation $O$,

$$\sum_i v_i(O_i)\le 2\,p^n(M).$$

Three further statements are included without being milestones: the output $A_1,\dots,A_n$ is an allocation (used implicitly by the paper); the first sentence of the proof of Lemma 3.6, that with $\Delta^i=p^i(M)-p^{i-1}(M)$ one has $\Delta^i=\max_{T\subseteq M}\bigl(v_i(T)-p^{i-1}(T)\bigr)$; and the factor $2$ is attained on the paper's two-item, two-bidder example (p. 9).

Significance

Theorem 3.3 shows that a factor-2 approximation of the optimal welfare for XOS bidders needs no linear program: one pass over the bidders, one demand query and one XOS query each. The paper's LP-based algorithm of §3.2 attains the better ratio $e/(e-1)$, and Theorem 4.1 of the paper shows that for the larger class of complement-free bidders no $(2-\epsilon)$-approximation is possible with polynomial communication.

The result is proved in the paper; to the best of our knowledge it has no machine-checked proof. This mission produces a formal model of XOS valuations, demand and XOS oracles and the greedy run that is reusable for other price-based arguments, and a formal proof of the guarantee for every tie-breaking in both oracles.

Difficulty

The argument is elementary, but its bookkeeping is where a formal proof can go wrong. Items move between bidders: an item taken from an earlier bidder in step (b) is re-priced in step (d), and every priced item lies in exactly one final bundle. Lemma 3.4 needs this invariant across all $n$ stages, together with the fact that a maximizing clause for the demanded set bounds $v_i$ on every subset, which holds because it is a clause of $v_i$ itself, not merely an additive function agreeing with $v_i$ on $S_i$. Lemma 3.5 is a contradiction argument using optimality of the demand; Lemma 3.6 telescopes the price increases and needs prices to stay nonnegative. The argument must hold for arbitrary oracle answers, so no canonical demand can be assumed.

Formalization scope

• Bidders are Fin n, items Fin m, bundles Finset (Fin m), values in ℝ. An XOS valuation is represented by its expression: a nonempty Finset (Fin m → ℝ) of clauses with nonnegative entries, evaluated with Finset.sup'. The paper's standing assumptions, normalized and monotone valuations (p. 1), hold automatically in this representation.
• The oracles are function parameters dem : Fin n → (Fin m → ℝ) → Finset (Fin m) and cl : Fin n → Finset (Fin m) → (Fin m → ℝ) with hypotheses IsDemandOracle and IsXOSOracle; every theorem holds for every such pair, so no tie-breaking rule is fixed.
• The run is a recursion on the stage: stage $k+1$ processes the 0-based bidder $k$, i.e. the paper's bidder $k+1$; after stage $n$ the state is constant.
• The paper's goal compares with the optimal allocation; the Lean goal compares with every allocation, which is equivalent and avoids an argmax. Stating the bound against one particular allocation, or against the algorithm's own output, would be trivial and is excluded.
• There are no $O(\cdot)$ constants: the factor $2$ is the paper's.
• Printed slip: the model on p. 1 writes an allocation as $S_1,\dots,S_m$; it is one bundle per bidder, $S_1,\dots,S_n$.
• Out of scope: running time, the cost of simulating oracles (Proposition 2.1), and communication lower bounds.

Contributions welcome: proofs of the three milestones and of the goal, and reusable lemmas on the invariant that every priced item lies in exactly one final bundle.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• B. Lehmann, D. Lehmann, N. Nisan, Combinatorial auctions with decreasing marginal utilities, Games and Economic Behavior 55(2):270–296, 2006. https://doi.org/10.1016/j.geb.2005.02.006

Motivation

In a combinatorial auction a seller offers $m$ indivisible items to $n$ bidders, each of whom values bundles of items rather than single items. Allocating the items so as to maximize the total value (the social welfare) is the central optimization problem of the area: it models spectrum auctions, procurement and resource allocation, and it is NP-hard and hard to approximate for general valuations. A large literature therefore studies restricted classes of valuations without complementarities. Among them the class XOS (valuations that are a maximum of additive valuations, also called fractionally subadditive) sits strictly between submodular and subadditive valuations and has become a standard benchmark class in algorithmic game theory.

Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010) gave, among other results, a randomized algorithm that approximates the optimal welfare for XOS bidders within a factor $1/(1-(1-1/n)^n)$, which is at most $e/(e-1)\approx 1.582$. The algorithm rounds the standard LP relaxation and resolves conflicts between bidders using the XOS structure. This mission formalizes that guarantee (Theorem 3.2 of the paper).

A short timeline: Lehmann, Lehmann and Nisan (EC 2001) introduced the XOS terminology and a 2-approximation for submodular bidders; the conference version of the present paper (STOC 2005) gave the $e/(e-1)$ bound for XOS with demand and XOS oracles; Feige (STOC 2006) extended the $e/(e-1)$ ratio to XOS bidders with demand oracles only and gave a 2-approximation for subadditive bidders.

Setting

Items are $M=\{1,\dots,m\}$ and bidders are $N=\{1,\dots,n\}$ with $n\ge1$. Bidder $i$ has a valuation $v_i$ assigning a real number $v_i(S)$ to every bundle $S\subseteq M$. An allocation is a tuple $(O_1,\dots,O_n)$ of pairwise disjoint bundles; its welfare is $\sum_i v_i(O_i)$.

A clause is an additive valuation $w$ given by nonnegative item values $w_1,\dots,w_m$, with $w(S)=\sum_{j\in S}w_j$. A valuation $v$ is XOS if there is a nonempty finite set $W$ of clauses with

$$v(S)=\max_{w\in W}\ \sum_{j\in S}w_j\qquad(S\subseteq M).$$

A clause of $W$ attaining the maximum for $S$ is a maximizing clause for $S$ in $v$; an XOS oracle returns one (arbitrarily, if several attain it).

The LP relaxation has a variable $x_{i,S}$ for every bidder $i$ and bundle $S$ and asks to maximize $\mathrm{OPT}^*=\sum_{i,S}x_{i,S}v_i(S)$ subject to $\sum_{i}\sum_{S\ni j}x_{i,S}\le1$ for each item $j$, $\sum_S x_{i,S}\le1$ for each bidder $i$, and $x_{i,S}\ge0$.

Randomized rounding draws a preallocation $S_1,\dots,S_n$: independently for each bidder $i$, bundle $S$ is chosen with probability $x_{i,S}$ and the empty bundle with the remaining probability $1-\sum_S x_{i,S}$. The preallocation can give an item to several bidders.

The algorithm of §3.2: (i) draw a preallocation from an optimal LP solution $x$; (ii) let $p^i=(p^i_1,\dots,p^i_m)$ be the maximizing clause for $S_i$ in $v_i$; (iii) give each item $j$ to a bidder $i$ with $p^i_j\ge p^{i'}_j$ for all $i'$. Write $\mathrm{ALG}$ for the welfare of the resulting allocation.

Formalization targets

Goal: Theorem 3.2

For every XOS profile, every optimal LP solution $x$, every choice of maximizing clauses, every tie-breaking in step (iii) and every allocation $O$,

$$\Big(1-\Big(1-\frac1n\Big)^n\Big)\sum_i v_i(O_i)\ \le\ \mathbb E[\mathrm{ALG}].$$

Milestones

1. $\sum_i v_i(O_i)\le\mathrm{OPT}^*$ for an optimal LP solution (step (i) of the proof of Theorem 3.1).
2. Pointwise, $\mathrm{ALG}\ge\sum_j Q_j$ with $Q_j=\max_i p^i_j$.
3. Eq. (1): for $1\le k\le n$ and $X_1,\dots,X_k\in[0,1]$ with $\sum X_i\le1$,

$$1-\prod_{i\le k}(1-X_i)\ \ge\ 1-\Big(1-\tfrac{\sum X_i}{k}\Big)^k\ \ge\ \Big(1-\big(1-\tfrac1k\big)^k\Big)\sum X_i\ \ge\ \Big(1-\big(1-\tfrac1n\big)^n\Big)\sum X_i .$$

4. Lemma 3.3: $\mathbb E[Q_j]\ge(1-(1-1/n)^n)\sum_i\sum_{S\ni j}x_{i,S}\,p^{(i,S)}_j$ for every feasible $x$.
5. $\mathbb E[\mathrm{ALG}]\ge(1-(1-1/n)^n)\,\mathrm{OPT}^*(x)$ for every feasible $x$.

Milestone 5 is stronger than the goal (it compares with the fractional value); the goal is stated against the integral optimum because that is what Theorem 3.2 asserts.

Significance

The bound $1-(1-1/n)^n\ge1-1/e$ is a constant-factor guarantee for a class that includes every submodular valuation, obtained from nothing more than the LP relaxation and the clause structure of XOS. It shows that the integrality gap of the configuration LP for XOS bidders is at most $1/(1-(1-1/n)^n)$, a fact reused in later work on welfare maximization, online allocation and posted-price mechanisms. The per-item analysis (Lemma 3.3 and Eq. (1)) is the same "$1-1/e$" correlation-gap argument that recurs in submodular maximization and prophet-inequality proofs.

The result is proved in the paper. To our knowledge it has no machine-checked proof. This mission produces a Lean statement and proof of the guarantee with the randomness made explicit, a reusable model of the configuration LP and of randomized rounding over bundles, and a formal version of the inequality in Eq. (1), which is independently useful.

Difficulty

Each piece of the argument is short; the work is in the bookkeeping. The preallocation is infeasible, so welfare cannot be read off from the rounding directly; the proof reduces it to per-item quantities $Q_j$ and then lower-bounds $\mathbb E[Q_j]$ by comparing with a different assignment of item $j$ that is not the algorithm's. The expectation of that auxiliary assignment involves a product of probabilities over bidders ordered by a conditional expectation, and the final bound needs the calculus inequality of Eq. (1) together with a summation by parts. A naive attempt to bound $\mathbb E[\mathrm{ALG}]$ bidder by bidder fails, because a bidder's received bundle is not contained in its preallocated bundle, and the clause values of other bidders decide what it receives.

Formalization scope

• Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. XOS is stated through its expression: each $v_i$ comes with a nonempty finite clause set $W_i$ of nonnegative clauses, and $v_i(S)$ is attained by a clause of $W_i$ and bounded by all of them. Normalization and monotonicity, the paper's standing assumptions (p. 1), follow from this.
• The LP has a variable for every bundle, including $\emptyset$. "Optimal" is stated as feasible and not beaten by any feasible solution; existence of an optimum is not asserted.
• The rounding is a finite product distribution over profiles $\sigma:\mathrm{Fin}\,n\to$ bundles, with bidder $i$'s law $q_i(S)=x_{i,S}+\mathbf 1[S=\emptyset](1-\sum_T x_{i,T})$; expectations are finite sums.
• The XOS oracle is a function parameter with its specification, and step (iii) is any rule selecting a bidder with maximal clause value; every statement quantifies over all of them.
• "Approximation" in Theorem 3.2 is read in expectation, as its proof establishes. There are no $O(\cdot)$ constants in this mission.
• Printed slip: the display of Lemma 3.3 (and the identity for $\mathrm{OPT}^*$ before it) sums $x_{i,S}p^{(i,S)}_j$ over all $(i,S)$; the proof's final line restricts to $S\ni j$, and the printed version is false. The Lean states Lemma 3.3 with $S\ni j$.
• Running time, the ellipsoid method and oracle complexity are out of scope.
• Ruled out as trivializing: dropping the LP constraints on $x$ (the item constraint is what makes Eq. (1) apply), stating the bound for a fixed preallocation instead of the expectation, or allowing negative clause values.

A complete development needs finite product distributions over bundles, the AM–GM inequality, monotonicity of $(1-1/k)^k$, and a summation-by-parts argument. The LP and rounding model are reusable for the other randomized-rounding results of the paper; proofs of any milestone are welcome.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• S. Dobzinski, N. Nisan, M. Schapira, Approximation algorithms for combinatorial auctions with complement-free bidders, STOC 2005. https://doi.org/10.1145/1060590.1060681
• B. Lehmann, D. Lehmann, N. Nisan, Combinatorial auctions with decreasing marginal utilities, EC 2001. https://doi.org/10.1145/501158.501161
• U. Feige, On maximizing welfare when utility functions are subadditive, STOC 2006. https://doi.org/10.1145/1132516.1132540

Motivation

In a combinatorial auction a seller offers $m$ indivisible items to $n$ bidders, each of whom values bundles of items rather than single items. Allocating the items to maximize total value is the basic welfare problem of spectrum auctions, procurement and resource allocation, and it is the running example of algorithmic mechanism design. For general valuations no polynomial-time algorithm achieves a ratio polynomially better than $\sqrt m$ under standard assumptions, so positive results require restricting the valuations. The most natural restriction is complement freeness (subadditivity): a bundle is never worth more than the sum of its parts.

Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010; conference version STOC 2005) gave the first polynomial-time algorithms with sub-polynomial approximation ratios for complement-free bidders given demand oracles. This mission formalizes their Section 3.1 algorithm, which rounds the linear-programming relaxation of the auction and splits the resulting infeasible solution into feasible ones.

Timeline. Lehmann, Lehmann and Nisan (2001) introduced the complement-free hierarchy and treated submodular bidders. The original version of the algorithm formalized here claimed an $O(\log m)$ ratio; Feige observed that the same algorithm achieves $O(\log m/\log\log m)$ and that its ratio is at least $\Omega(\sqrt{\log m/\log\log m})$ (Feige, SIAM J. Comput. 39(1), 2009). Feige then obtained a constant ratio ($2$) for subadditive bidders by a different rounding.

Setting

Items are $M=\{1,\dots,m\}$ and bidders $N=\{1,\dots,n\}$. Bidder $i$ has a valuation $v_i$ assigning a real value $v_i(S)$ to each bundle $S\subseteq M$. Every valuation is normalized, $v_i(\emptyset)=0$, and monotone, $S\subseteq T\Rightarrow v_i(S)\le v_i(T)$. A valuation is complement free if $v(S\cup T)\le v(S)+v(T)$ for all $S,T$. An allocation is a tuple $(S_1,\dots,S_n)$ of pairwise disjoint bundles; its welfare is $\sum_i v_i(S_i)$, and $OPT$ denotes the largest welfare.

The LP relaxation has a variable $x_{i,S}\ge0$ for each bidder and bundle, with $\sum_{i,S\ni j}x_{i,S}\le1$ for each item $j$ and $\sum_S x_{i,S}\le1$ for each bidder $i$; its objective is $\sum_{i,S}x_{i,S}v_i(S)$, with optimum $OPT^*\ge OPT$. Randomized rounding lets each bidder independently draw bundle $S$ with probability $x_{i,S}$ and $\emptyset$ with the remaining probability. The result, a preallocation, has expected welfare $OPT^*$ but may give an item to several bidders.

The algorithm takes $k=\lfloor 3\log m/\log\log m\rfloor$ and:

1. rounds until the preallocation $(S_1,\dots,S_n)$ has every item in at most $k$ bundles and $\sum_i v_i(S_i)\ge OPT^*/3$;
2. splits each $S_i$ into layers $S_i^r$, $r=1,\dots,k$, where $S_i^r$ holds the items of $S_i$ that appear in exactly $r-1$ of $S_1,\dots,S_{i-1}$;
3. picks the layer index $r$ maximizing $\sum_i v_i(S_i^r)$ and sets $T_i=S_i^r$;
4. if some bidder has $v_i(M)\ge\sum_{i'}v_{i'}(T_{i'})$, gives that bidder everything instead.

Formalization targets

Goal: Theorem 3.1, with the explicit ratio

For all sufficiently large $m$, for normalized, monotone, complement-free valuations and an optimal LP solution $x$ with value $OPT^*$:

1. if $OPT^*>3\max_i v_i(M)$, one rounding meets the two conditions of step 1 with probability $>1/6$;
2. from any preallocation meeting them, every admissible run of steps 2–4 outputs an allocation with

$$\sum_i v_i(\text{output}_i)\ \ge\ \frac{OPT}{3k},\qquad k=\Big\lfloor\frac{3\log m}{\log\log m}\Big\rfloor;$$

3. if $OPT^*\le3\max_i v_i(M)$, the bidder maximizing $v_i(M)$ alone achieves $OPT/3$.

Milestones

• $OPT\le OPT^*$ (proof, step (i)).
• The layers of each index form an allocation and partition each $S_i$ (proof, step (ii)).
• Complement freeness gives $\sum_r v_i(S_i^r)\ge v_i(S_i)$, and the best layer has welfare $\ge OPT^*/(3k)$ (proof, step (iii)).
• Lemma 3.1: independent Bernoulli variables with $\sum_i p_i\le1$ exceed $3\log m/\log\log m$ with probability $\le1/m^2$.
• Lemma 3.2: for $X$ a sum of independent $[0,1]$ variables with mean $\mu$, $\Pr[|X-\mu|\ge\alpha]\le\mu/\alpha^2$.
• §3.1.1: some item appears more than $3\log m/\log\log m$ times with probability $\le1/m$; the preallocation's welfare falls below $OPT^*/3$ with probability $<3/4$.

Significance

Theorem 3.1 was among the first polynomial-time approximation guarantees for welfare maximization with general subadditive bidders, and its layering argument is the standard way to turn an LP solution that is feasible up to a factor $k$ into a feasible allocation losing only a factor $k$ for subadditive objectives. The same argument applies to the $k$-duplicates auction and reappears in later rounding schemes. Lemma 3.1 is the standard balls-in-bins tail bound behind every $\log m/\log\log m$ load estimate.

The results are proved in the paper; none of them is formalized, on this platform or in Mathlib, as far as searches show. The mission produces a machine-checked version of the algorithm's guarantee with an explicit constant $3k$ in place of $O(\cdot)$, a precise statement of the probabilistic step, and reusable statements of two concentration inequalities for sums of independent bounded variables.

Difficulty

The combinatorial part (steps (ii) and (iii)) is short. The difficulty is in step (i). The rounding is a product distribution over bundles, while the count of an item is a sum over bidders of indicators that depend on each bidder's whole bundle; connecting the finite product law to independent Bernoulli variables, and then to Lemma 3.1, requires building the independence structure explicitly. Lemma 3.1 itself does not follow from a Chernoff bound with a fixed relative deviation: the threshold $3\log m/\log\log m$ grows with $m$ while the mean stays at most $1$, and the bound must hold uniformly in the number of variables, which a fixed-deviation Chernoff statement does not give. Finally, the event-$B$ bound needs the preallocation's welfare as a sum of independent variables in $[0,1]$, which requires rescaling by $\max_i v_i(M)$ and monotonicity.

Formalization scope

Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity, the paper's standing assumptions (p. 1), are hypotheses of the goal. $\log$ is the natural logarithm; the paper does not fix a base. The rounding law is written as explicit finite sums over profiles $\sigma:\texttt{Fin } n\to\texttt{Finset (Fin } m)$ with product weights, so independence across bidders is literal; Lemmas 3.1 and 3.2 are stated measure-theoretically with Mathlib's iIndepFun.

Explicit constants and conventions that replace the paper's notation:

• The ratio $O(k)=O(\log m/\log\log m)$ is stated as $3k$ with $k=\lfloor3\log m/\log\log m\rfloor$, the constant the proof establishes (step (iii), p. 6). "Sufficiently large $m$" is an existential $m_0$.
• The w.l.o.g. scaling $\max_i v_i(M)=1$ and the split at $OPT^*=3$ become the scale-free split at $OPT^*=3\max_i v_i(M)$.
• The choice of $r$ in step (iii) and of the bidder in step (iv) are universally quantified over all admissible choices.

Printed slips resolved in the statements:

• Lemma 3.1 mixes $n$ and $m$. Here the number of variables is arbitrary, "sufficiently large" refers to $m$, and $\sum_ip_i=1$ is relaxed to $\sum_ip_i\le1$, which is what the application uses.
• The display after Lemma 3.1 writes the threshold $\log m/(3\log\log m)$; the lemma's $3\log m/\log\log m$ is used.
• "$\Pr[\vee_jE_j]<1/n$" and "$\le 1/n+3/4$" should read $1/m$.
• The event $B$ is defined without its sum; it means $\sum_iv_i(S_i)<OPT^*/3$.

Trivializing formalizations are ruled out: the guarantee assumes the item-count bound (without it the layers do not cover the bundles), the probability statements assume an LP-feasible $x$, neither the layer index nor the step-(iv) bidder is fixed, and the ratio is the explicit $3k$ rather than an unspecified constant. Running time, the ellipsoid method and oracle complexity are out of scope. Contributions of general concentration lemmas for sums of independent bounded variables are welcome and reusable beyond this mission.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• U. Feige, On Maximizing Welfare When Utility Functions Are Subadditive, SIAM Journal on Computing 39(1):122–142, 2009. https://doi.org/10.1137/070680977
• B. Lehmann, D. Lehmann, N. Nisan, Combinatorial Auctions with Decreasing Marginal Utilities, Games and Economic Behavior 55(2):270–296, 2006. https://doi.org/10.1016/j.geb.2005.02.006
• M. Mitzenmacher, E. Upfal, Probability and Computing, Cambridge University Press, 2005. https://doi.org/10.1017/CBO9780511813603

Motivation

Submodularity — the diminishing-returns property $g(p) + g(q) \ge g(p \vee q) + g(p \wedge q)$ on a lattice — is one of the most useful structural hypotheses in combinatorial optimization, underlying efficient algorithms for network flows, matroid theory, and set-function minimization. Chapter 7 studies L-convex functions: functions on the integer lattice $\mathbb Z^V$ that are submodular and linear along the all-ones direction. This is the "dual" notion, under the conjugacy developed later in the book, to chunk 06's M-convex functions, and it inherits the same strong minimization theory — a purely local optimality criterion and a proximity theorem with an explicit distance bound — while additionally supporting a genuinely new characterization with no M-convex counterpart: discrete midpoint convexity, the direct lattice analogue of the classical real-valued midpoint convexity condition. This mission formalizes the chapter's definitional theorem, its midpoint-convexity characterization, the L-optimality criterion, and the L-proximity theorem itself.

Setting

Let $V$ be a finite ground set. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain is an L-convex function if it satisfies (SBF[Z]): $g(p) + g(q) \ge g(p \vee q) + g(p \wedge q)$ for all $p, q$ ($\vee, \wedge$ componentwise max/min), and (TRF[Z]): there is $r \in \mathbb R$ with $g(p + \mathbf 1) = g(p) + r$ for all $p$, where $\mathbf 1$ is the all-ones vector. An L$^\natural$-convex function is one whose lift to the extended ground set $\{0\} \cup V$ is L-convex; equivalently (Theorem 7.1), $g$ satisfies the translation-submodularity axiom (SBF$^\natural$[Z]): $g(p) + g(q) \ge g((p - \alpha\mathbf 1) \vee q) + g(p \wedge (q + \alpha\mathbf 1))$ for all $p, q$ and all nonnegative integers $\alpha$. Discrete midpoint convexity asks $g(p) + g(q) \ge g(\lceil (p+q)/2 \rceil) + g(\lfloor (p+q)/2 \rfloor)$ componentwise. For $\alpha$ a positive integer, a point satisfies scaled local optimality if $g(p_\alpha) \le g(p_\alpha \pm \alpha \chi_Y)$ for every $Y \subseteq V$.

Formalization targets

Goal: Theorem 7.18 (the L-proximity theorem)

Assume $\alpha$ is a positive integer and $n = |V|$. (1) If $g$ is L-convex with $g(p) = g(p+\mathbf 1)$ for all $p$, and $p_\alpha \in \operatorname{dom} g$ satisfies $g(p_\alpha) \le g(p_\alpha + \alpha\chi_Y)$ for all $Y \subseteq V$, then $\arg\min g \ne \emptyset$ and there is $p^* \in \arg\min g$ with the componentwise bound

$$p_\alpha \le p^* \le p_\alpha + (n-1)(\alpha-1)\mathbf 1.$$

(2) If $g$ is L$^\natural$-convex and $p_\alpha$ satisfies the two-sided version, then there is $p^*$ with $p_\alpha - n(\alpha-1)\mathbf 1 \le p^* \le p_\alpha + n(\alpha-1)\mathbf 1$. The bound is a genuine vector (lattice-order) inequality, not an $\ell^\infty$-norm bound — the form later chapters' applications need.

Milestones: Theorems 7.1, 7.7, 7.14

Theorem 7.1: L$^\natural$-convexity (defined via the lift) is equivalent to the direct translation-submodularity axiom. Theorem 7.7: this same class is also characterized by discrete midpoint convexity — a three-way equivalence with the approach property (L$^\natural$-APR[Z]) as a bridge — giving L-convexity a genuinely different, more geometric face than anything available on the M-convex side. Theorem 7.14 (the L-optimality criterion): global optimality reduces to a purely local check against the sign-pattern neighbors $p \pm \chi_Y$, mirroring chunk 06's Theorem 6.26 but with the plain L-convex case additionally requiring the periodicity condition $g(p) = g(p+\mathbf 1)$.

Significance

The result itself. Discrete midpoint convexity (Theorem 7.7) is philosophically important: it shows the lattice-submodularity definition of L-convexity is not an arbitrary discretization choice but coincides exactly with the most direct discrete analogue of ordinary midpoint convexity, the classical characterization of convex functions via $f((p+q)/2) \le (f(p)+f(q))/2$. The L-optimality criterion and L-proximity theorem give L-convex minimization the same algorithmic footing as M-convex minimization (chunk 06): scaling algorithms for L-convex objectives — which arise naturally from network flow and submodular-function duality — inherit a provable, dimension-and-scale-explicit distance guarantee between a coarse-scale local optimum and the true minimizer.

Formalizing it. No matching item exists on the platform for L-convex functions, discrete midpoint convexity, or the L-optimality/proximity theorems. This mission gives the first formal statement of these results, completing (alongside chunk 06's M-convex-function results) both halves of the exchange-axiom-based theory that chapter 8's conjugacy duality later unifies.

Difficulty

A natural shortcut, given the structural parallel to chunk 06, is to assume the L-proximity theorem's proof is a mechanical relabeling of the M-proximity theorem's proof. It is not: the M-convex proof (chunk 06) crucially uses the exchange axiom's additive four-term inequality to build a chain of strictly improving points, whereas the L-convex proof instead exploits (TRF[Z])'s periodicity directly — it reduces to the case $p_\alpha = 0$ using translation invariance, then constructs a minimal (with respect to the lattice order) point among all sufficiently good solutions and shows this minimality, combined with submodularity (SBF[Z]), forces the componentwise bound. The vector (rather than norm) form of the conclusion is not cosmetic: it is exactly what this lattice-order argument naturally produces, and is the form needed by later chapters' applications.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is (V → ℤ) → WithTop ℝ. Unlike chunk 06's M-convex axiom, (SBF[Z]), (TRF[Z]), and (SBF$^\natural$[Z]) are stated for all of $\mathbb Z^V$, not restricted to $\operatorname{dom} g$, so no explicit import of chunk 05's L-convex-set vocabulary was needed for dom g's structure (unlike the corresponding note in chunk 06's BRIEF.md, which flagged the same concern for dom f). L$^\natural$-convexity is represented via an explicit lift to Option V, matching the book's own primary definition, with the direct axiom (SBF$^\natural$[Z]) kept as a separate object related to it by Theorem 7.1.

A trivializing formalization of the goal would convert its componentwise vector bound into an $\ell^\infty$-norm bound (losing the direction-of-approach information the vector form carries) or drop Part (1)'s periodicity hypothesis $g(p) = g(p+\mathbf 1)$; neither is done here. Propositions establishing dom g as an L-convex set, the L/L$^\natural$ relationship (Theorem 7.3), the submodular-set-function embedding (Proposition 7.4), and several structural closure properties are cut from this mission's scope (see MODERATION_NOTES.md) but are natural targets for a follow-on mission or for chunk 09, which builds directly on this chunk's exchange-axiom vocabulary, mirroring chunks 06→07.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

Motivation

The relaxation method for a system of linear inequalities, introduced by Agmon and by Motzkin and Schoenberg in back-to-back papers of the Canadian Journal of Mathematics (1954), solves $\sum_j a_{ij}x_j + b_i \ge 0$ by repeatedly moving a point towards, or across, the most violated half-space. It is the ancestor of the perceptron algorithm, of Kaczmarz-type projection methods, and of the method of alternating projections, all of which are still used in feasibility problems, tomography and machine learning.

Motzkin and Schoenberg's paper ends (Part IV, §§9–10) by asking whether the behaviour of the reflexion process — the relaxation step with factor $\lambda = 2$ — survives when the finite family of half-spaces is replaced by an infinite one. They answer this for one natural infinite family: all supporting half-spaces of a closed bounded convex set. This mission formalizes that answer, Theorem 3 of the paper.

Timeline of the thread this mission belongs to:

• 1922 — Fejér observes that a sequence approaching every point of a set monotonically has useful convergence properties (Fejér, Math. Annalen 85, 1922).
• 1954 — Agmon proves convergence of the relaxation method for $0 < \lambda < 2$ (Agmon, Canad. J. Math. 6, 1954, pp. 382–392); Motzkin and Schoenberg prove finite termination of the reflexion method ($\lambda = 2$) for full-dimensional solution polytopes (Theorem 1), the oscillation behaviour in lower dimension (Theorem 2), and the convex-body version (Theorem 3) (Motzkin–Schoenberg 1954).

Setting

Let $E_n$ be $n$-dimensional Euclidean space and let $A \subseteq E_n$ be a nonempty, closed, bounded, convex set. Its dimension $r$ is the dimension of its affine span $L_r$, the smallest flat containing $A$.

For $p \notin A$ let $q$ be the point of $A$ nearest to $p$; it exists and is unique. The image of $p$ with respect to $A$ is

$$p_1 = F(p) = p + 2(q - p), \qquad (3.1)$$

the reflexion of $p$ through $q$. The reflexion process starts at $p_0 \notin A$ and sets $p_{\nu+1} = F(p_\nu)$ as long as $p_\nu \notin A$ (3.2). Either the process terminates with some $p_N \in A$, or it produces an infinite sequence of points outside $A$.

The family $F$ of supporting half-spaces of $A$ consists of the closed half-spaces $H \supseteq A$ whose bounding hyperplane touches $A$. The paper observes that the half-space $H_0$ through $q$ normal to $pq$ is the member of $F$ farthest from $p$, so (3.1) is exactly the reflexion step of the relaxation method applied to the infinite family $F$.

A sequence $\{q_\nu\}$ of points outside $A$ is Fejér-monotone with respect to $A$ if $q_\nu \ne q_{\nu+1}$ and $|q_{\nu+1} - a| \le |q_\nu - a|$ for all $a \in A$. Two points $u, v$ are symmetric with respect to a flat $L$ if their midpoint lies in $L$ and $u - v$ is orthogonal to $L$.

Formalization targets

Goal: Theorem 3 (p. 402)

For every nonempty closed bounded convex $A \subseteq E_n$ with affine span $L_r$, every $p_0 \notin A$ and every run $\{p_\nu\}$ of the reflexion process:

$$\textbf{Case 1: } r = n \implies \exists N,\ p_N \in A.$$ $$\textbf{Case 2: } r < n \implies \begin{cases} p_0 \in L_r \implies \exists N,\ p_N \in A,\\[2pt] p_0 \notin L_r \implies p_\nu \notin A\ \forall \nu, \text{ and } \exists \nu_0, u \ne v \text{ symmetric w.r.t. } L_r:\ \{p_\nu, p_{\nu+1}\} = \{u, v\}\ \forall \nu > \nu_0. \end{cases}$$

No number of steps is fixed: termination is finite but not uniformly bounded.

Milestones (attack order)

1. §9 — the half-space $H_0$ belongs to $F$, maximizes $\operatorname{dist}(p, H)$ over $F$, and every farthest member of $F$ yields the step (3.1).
2. §10 — an infinite run of the reflexion process is Fejér-monotone with respect to $A$.
3. Lemma 1, Case 1 — a sequence Fejér-monotone with respect to a set of dimension $n$ converges to a point.
4. §10 — the limit of an infinite run lies in $A$ and on its boundary.
5. Theorem 3, Case 1 — if $r = n$ the process always terminates.
6. §10 — orthogonal projection on a flat $L \supseteq A$ commutes with the image map, and each step keeps the distance to $L$ while switching sides.

Significance

The result. Theorem 3 shows that the dichotomy proved in the paper for finitely many half-spaces — finite termination when the target is full-dimensional, eventual oscillation otherwise — holds for the infinite family of all supporting half-spaces of a convex body. Case 1 says that reflecting through the nearest point, a method that uses no information about $A$ beyond metric projection, reaches a full-dimensional convex body in finitely many steps from any start. Case 2 says that for a lower-dimensional body the process detects this: the iterates settle into a two-cycle whose midpoint is a point of $A$, so a solution can be read off.

Formalizing it. The theorem is proved in the paper (1954), with a short proof of Case 1 that relies on geometric intuition about normal cones near a boundary point. To our knowledge no machine-checked proof exists. A complete development produces a verified finite-termination theorem for a projection method on general convex bodies, together with reusable facts about Fejér-monotone sequences and metric projections that recur throughout the analysis of projection algorithms.

Difficulty

The obvious argument for Case 1 is: the run is Fejér-monotone, hence converges (Lemma 1), and its limit $a$ lies on the boundary of $A$; then derive a contradiction. For a polytope (Theorem 1) the contradiction comes from finiteness: eventually every reflexion is in one of finitely many hyperplanes through $a$, which keeps the iterates on a sphere around $a$. For a convex body there are infinitely many supporting hyperplanes near $a$, and the iterates are reflected in a different one at every step; no finiteness argument is available. What replaces finiteness is an argument about how the supporting hyperplanes of $A$ at boundary points near $a$ are oriented, and the paper gives it only as an informal geometric sketch. Making this step rigorous is the main work of the mission.

Numerical experiments show that termination can take tens of thousands of steps near sharp corners of a polygon, so no bound on the number of steps in terms of the distance of $p_0$ to $A$ alone can be expected.

Formalization scope

• Space. $E_n$ is EuclideanSpace ℝ (Fin n). $A$ is a Set with four explicit hypotheses: A.Nonempty, IsClosed A, Convex ℝ A, Bornology.IsBounded A. Nonemptiness is implicit in the paper ("of dimension $r$", "the point of $A$ nearest to $p$").
• The image as a relation. IsImage A p p₁ holds when $p_1 = p + 2(q - p)$ for a nearest point $q$ of $A$; the nearest point is not chosen by a function. For closed convex nonempty $A$ this relation is a function on $E_n$. A run is any sequence with IsImage A (p ν) (p (ν+1)) whenever p ν ∉ A; values after entering $A$ are unconstrained. Every statement quantifies over every run from every $p_0 \notin A$; a formalization that only asserts the existence of some terminating run is ruled out.
• Dimension. $L_r$ is affineSpan ℝ A; $r = n$ is affineSpan ℝ A = ⊤, $r < n$ is affineSpan ℝ A ≠ ⊤. No separate natural number $r$ is introduced.
• Symmetry. IsSymmetricWrt L u v: midpoint ℝ u v ∈ L and u - v orthogonal to L.direction. For $r < n - 1$ this is a point reflection through the foot of the perpendicular, not a reflection in a hyperplane. The goal also requires $u \ne v$ and strict alternation $p_\nu \leftrightarrow p_{\nu+1}$ for $\nu > \nu_0$ (strict inequality, as printed).
• Boundary is frontier A; distances to sets are Metric.infDist.
• Generalizations recorded. Lemma 1, Case 1 is stated for an arbitrary set $A \subseteq E_n$ with full affine span (the paper states it for the polytope of (1.4) and applies it in §10 to a convex body). The projection milestone is stated for any flat $L \supseteq A$, not only after the paper's reduction to $r = n - 1$. The §9 milestone expresses "the reflexion process with respect to $F$ amounts to (3.1)" as: every farthest member of $F$, with any nearest point on it, gives the same step.
• Duplication. Case 1 appears both as a milestone and inside the goal, because the paper's proof of Case 2 cites Case 1. Solvers will need to transfer Case 1 from $E_n$ to the flat $L_r$ (an isometric copy of $E_r$).
• Infrastructure. Mathlib's metric projection onto complete convex sets (exists_norm_eq_iInf_of_complete_convex, norm_eq_iInf_iff_real_inner_le_zero) and EuclideanGeometry.orthogonalProjection cover the basic geometry. Normal cones of convex sets and their upper semicontinuity are not in Mathlib; a contribution there is reusable well beyond this mission. Proofs of any milestone, and alternative proofs of Case 1, are welcome.

Selected references

• 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 (the companion paper in the same issue).
• L. Fejér, Über die Lage der Nullstellen von Polynomen, die aus Minimumforderungen gewisser Art entspringen, Mathematische Annalen 85 (1922), 41–48.

Motivation

Heavy-traffic and fluid approximations for open queueing networks are obtained by writing the queue-content process as a deterministic function of a simpler netput process (arrivals minus potential service, corrected for routing) and then transferring a functional limit theorem for the netput through that function. The function is the multidimensional reflection map of Harrison and Reiman (Harrison and Reiman 1981), extended from continuous paths to paths with jumps by Reiman (Reiman 1984). The transfer works only if the map is continuous, and quantitative bounds on the approximation error require it to be Lipschitz with a known modulus.

Chen and Whitt (Chen and Whitt 1993) use this map to derive diffusion approximations for networks whose servers are subject to interruptions. Before doing so, Section 2 of the paper supplies "explicit Lipschitz bounds" for the map in the uniform topology: a bound in the Harrison–Reiman scaling (Proposition 2.1) and a new bound that depends on the routing matrix only through its powers (Proposition 2.3).

Timeline. Harrison and Reiman (1981) proved existence, uniqueness and continuity of the map on continuous paths for a routing matrix of spectral radius less than one. Reiman (1984) extended it to paths with jumps. Chen and Mandelbaum (Leontief systems, RBV's and RBM's, 1991, cited in the paper as [4]) noted that a minor extension of the argument makes the map Lipschitz on $D([0,T],\mathbb R^n)$ with the uniform topology. Chen and Whitt (1993, Section 2) made the Lipschitz constants explicit.

Setting

Fix a dimension $n$ and an $n\times n$ matrix $Q$ whose transpose $Q^{\mathsf t}$ is substochastic: all entries of $Q$ are nonnegative and every column sum of $Q$ is at most $1$. Assume also $Q^k \to 0$ as $k\to\infty$. With Markovian routing, $Q^{\mathsf t}$ is the routing matrix of an open network of $n$ queues.

Vectors $c\in\mathbb R^n$ carry the norm $\|c\| = \sum_j |c_j|$, and matrices carry the maximum absolute column sum $\|P\| = \max_j \sum_i |P_{ij}|$ (Eq. (2.5)). $D([0,T],\mathbb R^n)$ is the space of paths that are right-continuous with left limits on $[0,T]$. For a path $x$, $|x|\in\mathbb R^n$ is the vector of coordinatewise sup norms, $|x|_j = \sup_{0\le t\le T}|x_j(t)|$, and $\|x\| = \big\||x|\big\| = \sum_j \sup_{t}|x_j(t)|$.

The reflection of $x \in D$ is the pair $(y,z) = (\psi(x),\phi(x))$ with $y \in D$ and

$$z = x + (I-Q)\,y \ge 0, \qquad y_j \text{ nondecreasing},\ y_j(0) = 0, \qquad \int_0^T z_j(t)\,dy_j(t) = 0 \quad (1\le j\le n).$$

The last condition says that $y_j$ increases only when $z_j = 0$. In queueing terms, $z$ is the vector of queue contents and $y$ the cumulative idleness. The operator $\pi_x(y) = (Qy - x)^{\uparrow}\vee 0$, where $f^{\uparrow}(t) = \sup_{0\le s\le t} f(s)$ coordinatewise, has the reflection as its fixed point (Eq. (2.4)). Write $\gamma = \|Q^n\|$.

Formalization targets

Goal: Proposition 2.3

For all $x_1,x_2\in D$ with reflections $(\psi(x_i),\phi(x_i))$,

$$|\psi(x_1)-\psi(x_2)| \le (I-Q)^{-1}|x_1-x_2| \quad\text{componentwise},\tag{2.9}$$ $$\|\psi(x_1)-\psi(x_2)\| \le \|(I-Q)^{-1}\|\,\|x_1-x_2\| \le \sum_{k=0}^\infty \|Q^k\|\,\|x_1-x_2\| \le \frac{n}{1-\gamma}\|x_1-x_2\|,\tag{2.10}$$ $$\|\phi(x_1)-\phi(x_2)\| \le \big(1+\|I-Q\|\,\|(I-Q)^{-1}\|\big)\|x_1-x_2\| \le \Big(1+\frac{2n}{1-\gamma}\Big)\|x_1-x_2\|.\tag{2.11}$$

The constants are those of the paper. The goal fixes nothing beyond the standing assumptions on $Q$.

Milestones

1. Existence and uniqueness of the reflection for $x\in D$ with $x(0)\ge0$ (Section 2, p. 337).
2. Eq. (2.4): given (2.1)–(2.2), the complementarity condition (2.3) is equivalent to $y = \pi_x(y)$.
3. $\gamma = \|Q^n\| < 1$ (p. 338).
4. Proposition 2.2: $\|\pi_x^k(y_1)-\pi_x^k(y_2)\| \le \|Q^k|y_1-y_2|\| \le \|y_1-y_2\|$ for $k\ge1$, the factor $\gamma$ for $k\ge n$, and $\pi_x^k(y_1)\to\psi(x)$.
5. Proposition 2.1: for $Q^* = \Lambda^{-1}Q\Lambda$ with $\Lambda$ diagonal and $\|Q^*\| = \alpha<1$, the moduli $\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\psi$ and $1 + \|I-Q\|\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\phi$.
6. Remark (2.1): for $n=1$, $Q=0$ the bounds are attained.
7. Remark (2.2): for two queues in series, (2.10) gives modulus $2$, while (2.7) gives at best $4$ (every modulus $\ge 4$ is attained, $4$ at $z = 1/2$).

Significance

Proposition 2.3 makes the queue-content and idleness processes of an open network Lipschitz functions of the netput, in the uniform norm, with a modulus computed from the routing matrix alone. Combined with the fact that Lipschitz continuity in the uniform topology passes to the Skorohod $J_1$ and $M_1$ topologies (Section 2 of the paper), it is what turns a functional central limit theorem for arrival and service processes into a heavy-traffic limit for the network. The paper uses it in exactly this way in Sections 3–4. Explicit moduli also yield rates: an error of order $\varepsilon$ in the netput produces an error of at most $n\varepsilon/(1-\gamma)$ in the idleness process.

On the formal side, the results are proved in the paper, but neither the reflection map nor $D([0,T],\mathbb R^n)$ has a machine-checked development in Mathlib or on this platform. The mission would provide a reusable definition of the oblique reflection map with a Lebesgue–Stieltjes complementarity condition, its fixed-point characterization, and certified Lipschitz constants, as a foundation for any later formal heavy-traffic limit.

Difficulty

The componentwise bound (2.9) is short once the fixed-point form of the map is available. The difficulty lies in the infrastructure beneath it. The fixed-point characterization (2.4) is a one-dimensional Skorokhod-problem argument carried out coordinatewise for paths with jumps, where the complementarity condition must be handled through Lebesgue–Stieltjes measures. A jump of $y_j$ is allowed at a time where $z_j = 0$ even if $z_j$ was positive just before. Existence needs the iterates $\pi_x^k(0)$ to converge in $D$ and the limit to satisfy (2.1)–(2.3). The explicit constants involve $(I-Q)^{-1}$, $\sum_k\|Q^k\|$ and $\gamma = \|Q^n\|<1$. The last inequality is a combinatorial fact about transient substochastic matrices. It does not follow from $\|Q\|\le1$.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and $\|P\|$ is the maximum absolute column sum. Paths are functions ℝ → Fin n → ℝ, of which only the restriction to $[0,T]$ matters. Membership in $D([0,T],\mathbb R^n)$ is the predicate IsCadlagOn T x: right-continuous on $[0,T)$, left limits on $(0,T]$, and (redundantly) bounded on $[0,T]$. The reflection is the predicate IsReflection Q T x y z. Every theorem is stated for all pairs satisfying it, so no choice function and no junk value are involved. Condition (2.3) is encoded as "the Lebesgue–Stieltjes measure $dy_j$ of $\{t\in[0,T]: z_j(t)>0\}$ is zero". For $z\ge0$ this is equivalent to $\int_0^T z_j\,dy_j=0$. $\pi_x^k$ is Nat.iterate, $(I-Q)^{-1}$ is Mathlib's matrix inverse (invertible under the standing assumptions), and $\sum_k\|Q^k\|$ is a tsum stated together with its summability.

Corrections and conventions, each disclosed in the item concerned:

• The norm (2.6). The page prints $\|x\| = \sup_t\sum_j|x_j(t)|$. Under that norm Propositions 2.1 and 2.3 are false for $n\ge2$. With $Q=0$, $n=2$, $T=1$, $x_1\equiv0$ and $x_2 = (-\mathbf 1_{[0.1,0.2)}, -\mathbf 1_{[0.3,0.4)})$, one gets $\|x_1-x_2\|=1$ but $\psi(x_2) = (\mathbf 1_{[0.1,1]},\mathbf 1_{[0.3,1]})$ has norm $2$. The paper's proofs are valid for $\|x\| = \sum_j\sup_t|x_j(t)|$, which is used throughout. In dimension one the two norms coincide.
• (2.8) prints $\phi(x_1)-\phi(x_1)$. The formalization states $\phi(x_1)-\phi(x_2)$.
• (2.2)–(2.3) print the index range $1\le j\le J$. The dimension is $n$.
• $x(0)\ge0$ is added to the existence item. Conditions (2.1)–(2.2) force $z(0)=x(0)$, so no reflection exists otherwise. The Lipschitz bounds are stated for all solution pairs and are vacuous exactly when some $x_i(0)$ has a negative coordinate.
• Proposition 2.1 assumes only that $\Lambda$ is diagonal with nonzero entries. All quantities depend on $|\Lambda|$, so this covers the positive scaling of Harrison and Reiman.
• Eq. (2.4) keeps the standing assumptions on $Q$ as on the page, although the equivalence does not use them.

A trivializing formalization would read (2.3) through a Bochner integral, which is $0$ for non-integrable integrands, or take suprema over unbounded families. The measure-zero encoding and the boundedness built into IsCadlagOn rule both out. A sorry-free check shows that Remark (2.1)'s jump example satisfies IsReflection.

Welcome contributions: a general API for càdlàg paths on $[0,T]$ (boundedness, measurability, running suprema), the one-dimensional Skorokhod lemma for càdlàg paths, and the Neumann series for transient substochastic matrices. All of these are reusable beyond this mission.

Selected references

• H. Chen and W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
• J. M. Harrison and M. I. Reiman, Reflected Brownian motion on an orthant, Annals of Probability 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994428
• M. I. Reiman, Open queueing networks in heavy traffic, Mathematics of Operations Research 9 (1984) 441–458. https://doi.org/10.1287/moor.9.3.441
• H. Chen and A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Annals of Probability 19 (1991) 1463–1519. https://doi.org/10.1214/aop/1176990220