All missions

Motivation

Counting the objects that avoid every one of a list of conditions is one of the most frequent tasks in enumerative combinatorics: functions that miss no value, permutations that fix no point, integers that share no prime factor with a given number. The Principle of Inclusion-Exclusion converts such a count into an alternating sum of counts of objects that do satisfy prescribed conditions, which are usually far easier to compute. Chapter 7 of Keller and Trotter's Applied Combinatorics (2017 Edition) develops the principle in the abstract language of properties and applies it to three classical questions: the number of surjections, the number of derangements, and Euler's totient function.

This mission formalizes the first two applications, with the chapter's headline result, the closed formula for the number of surjections from an $n$-element set onto an $m$-element set, as its goal. The surjection count answers distribution questions of the form "in how many ways can $n$ distinct objects be handed to $m$ distinct recipients so that every recipient receives at least one", which the book illustrates with fifteen lottery tickets shared among four grandchildren ($S(15,4) = 1016542800$).

Setting

Let $X$ be a finite set and let $\mathcal P = \{P_1, \dots, P_m\}$ be a family of properties: for each $x \in X$ and each $i$, either $x$ satisfies $P_i$ or it does not. For a subset $S \subseteq [m] = \{1, \dots, m\}$ write

$$N(S) = \bigl|\{x \in X : x \text{ satisfies } P_i \text{ for every } i \in S\}\bigr|,$$

so that $N(\emptyset) = |X|$.

Two families of properties are used.

• Functions. $X$ is the set of all functions $f : [n] \to [m]$, and $f$ satisfies $P_i$ when $i$ is not in the range of $f$, i.e. $f(j) \ne i$ for every $j \in [n]$. The functions satisfying none of the properties are the surjections, and their number is written $S(n, m)$.
• Permutations. $X$ is the set of all permutations $\sigma$ of $[n]$, and $\sigma$ satisfies $P_i$ when $\sigma(i) = i$. The permutations satisfying none of the properties are the derangements, and their number is written $d_n$.

In Lean, $X$ is a type with [Fintype X], the properties are a decidable predicate family P : Fin m → X → Prop, and $N(S)$ is AppliedComb.InclExcl.N P S. The two families are AppliedComb.InclExcl.NotInRange n m on Fin n → Fin m and AppliedComb.InclExcl.FixesPoint n on Equiv.Perm (Fin n).

Formalization targets

Goal: Theorem 7.9 (number of surjections)

For all $n, m \ge 0$,

$$S(n, m) = \bigl|\{f : [n] \to [m] \text{ surjective}\}\bigr| = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (m-k)^n .$$

Milestones

1. Theorem 7.7 (Principle of Inclusion-Exclusion). For every finite $X$ and every family of $m$ properties,

$$\bigl|\{x \in X : x \text{ satisfies no } P_i\}\bigr| = \sum_{S \subseteq [m]} (-1)^{|S|} N(S).$$

2. Lemma 7.8. For the function properties, $N(S)$ depends only on $|S|$, and $N(S) = (m-k)^n$ when $|S| = k$.
3. Lemma 7.10. For the permutation properties, $N(S)$ depends only on $|S|$, and $N(S) = (n-k)!$ when $|S| = k$.
4. Theorem 7.11 (number of derangements). For all $n \ge 0$,

$$d_n = \sum_{k=0}^{n} (-1)^k \binom{n}{k} (n-k)! .$$

Milestones 1 and 2 are the two ingredients the book names for the goal; milestones 3 and 4 are the parallel derangement application, which shares the definition of $N(S)$ and milestone 1.

Significance

The result itself. The surjection formula is the standard closed form for $m!\,S_2(n,m)$, where $S_2$ is the Stirling number of the second kind; it gives $S(n, m) = 0$ for $n < m$ and $S(n, n) = n!$ as special cases, and it underlies counts of ordered set partitions, of onto colourings, and of occupancy problems in which every cell is filled. The derangement formula is the standard answer to the hat-check problem and leads directly to the limit $d_n/n! \to 1/e$ (Theorem 7.12 of the book). The Principle of Inclusion-Exclusion in the book's "none of the properties" form is the common tool behind both and behind Möbius inversion in general.

Formalizing it. All results are classical and fully proved in the book. Mathlib contains inclusion-exclusion for unions and intersections of finsets (Finset.inclusion_exclusion_card_biUnion, Finset.inclusion_exclusion_card_inf_compl), the derangement count via its own recurrence (numDerangements, card_derangements_eq_numDerangements, numDerangements_sum), and Stirling numbers of the second kind (Nat.stirlingSecond) with their recurrence, but no closed formula for the number of surjections. The platform has union-form inclusion-exclusion (FamousTheorems.inclusion_exclusion_card_biUnion) and the $1/e$ limit, neither in the property form used here. This mission produces the property-indexed statement of the principle, the two $N(S)$ computations, and the surjection count as a cardinality of surjective functions, in a form that downstream missions of the series (generating functions, Pólya counting) can cite.

Difficulty

The proofs are short on paper, and the work lies in the bookkeeping that the page leaves implicit. Two points stand out. First, the Principle of Inclusion-Exclusion is phrased with properties and $N(S)$ rather than with a union of sets; connecting the two forms, or proving the property form directly, requires handling sums over the power set of $[m]$ together with the sign $(-1)^{|S|}$ in $\mathbb Z$. Second, the step "the result follows immediately, as there are $\binom{m}{k}$ $k$-element subsets of $[m]$" requires regrouping a sum over all subsets $S \subseteq [m]$ by cardinality, which needs Lemma 7.8's statement that $N(S)$ depends only on $|S|$ and a count of the subsets of each size. The book's one-line arguments for Lemmas 7.8 and 7.10 ("a string of length $n$ from an alphabet of $m-k$ letters", "a permutation among the remaining $n-k$ positions") are counting identifications that have to be made precise for subtypes of Fin n → Fin m and of Equiv.Perm (Fin n).

Formalization scope

• The book's $[n] = \{1, \dots, n\}$ is represented by Fin n $= \{0, \dots, n-1\}$; this is an index shift only.
• $S(n, m)$ is Fintype.card {f : Fin n → Fin m // Function.Surjective f} and $d_n$ is Fintype.card {σ : Equiv.Perm (Fin n) // ∀ i, σ i ≠ i}. Defining $S(n, m)$ by the formula, or $d_n$ by the sum, would make the goal hold by rfl; the counts are therefore cardinalities of the sets the book describes. $S(n,m)$ is also not stated through Nat.stirlingSecond, which counts unordered partitions and differs by a factor $m!$.
• All alternating sums are identities in $\mathbb Z$; the natural-number counts are cast. The differences $m - k$ and $n - k$ are computed in $\mathbb N$ where $k$ ranges over $0, \dots, m$ (resp. $0, \dots, n$) or equals $|S|$, so they are exact.
• The book introduces $S(n,m)$ for positive $n, m$ and states Theorem 7.11 for positive $n$. The formal statements are made for all $n, m \ge 0$, where they remain true with Lean's convention $0^0 = 1$ ($S(0,0) = 1$, $S(0,m) = 0$ for $m \ge 1$, $d_0 = 1$). No explicit constants arise: the chapter contains no $O(\cdot)$ or approximate statements among the formalized results.
• The Principle of Inclusion-Exclusion is stated for an arbitrary finite type and an arbitrary decidable family of $m \ge 0$ properties; for $m = 0$ both sides equal $|X|$.

A complete development needs only Mathlib's finite-set, power-set and binomial-coefficient API. The property-form inclusion-exclusion (Theorem 7.7) and the two $N(S)$ lemmas are reusable for other sieve-type counts, for example Euler's totient function (Theorem 7.14 of the book), which is not part of this mission. Proofs of any milestone independently of the others are welcome, as are alternative proofs of the goal (for instance via exponential generating functions) that do not pass through Theorem 7.7.

Selected references

• Mitchel T. Keller and William T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 7 (Theorems 7.7, 7.9, 7.11; Lemmas 7.8, 7.10), CC BY-SA 4.0. https://www.appliedcombinatorics.org/
• Richard P. Stanley, Enumerative Combinatorics, Volume 1, 2nd ed., Cambridge University Press, 2011, Chapter 2 (sieve methods). https://doi.org/10.1017/CBO9781139058520
• The Mathlib Community, The Lean Mathematical Library, CPP 2020. https://doi.org/10.1145/3372885.3373824

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.