Operations Research

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

An M-convex function is defined on the integer lattice, but chapter 6's earlier results (companion missions 06-mconvex-functions-i, 22-ch06b-mconvexfunctions, 23-ch06c-mconvexfunctions) show it always extends to a genuine convex function on real space. Once that extension exists, every tool of classical convex analysis — directional derivatives, subdifferentials, positive homogeneity — becomes available, and the natural question is whether these classical objects remain combinatorially special when applied to an M-convex function's extension. This mission answers that question at its sharpest: the directional derivative of an M-convex function at any point is again a positively homogeneous M-convex function, its subdifferential is exactly the admissible-potential set of a distance function satisfying the triangle inequality, and this correspondence between positively homogeneous M-convex functions and triangle-inequality distance functions is itself a clean one-to-one correspondence. This closes the loop between chapters 4-5 (M-convex and L-convex sets, distance functions) and the continuous convex-analytic machinery chapter 8 needs for its duality theory.

Companion missions 06-mconvex-functions-i, 22-ch06b-mconvexfunctions, and 23-ch06c-mconvexfunctions cover this chapter's optimality theory, algebraic toolkit, and convex-extensibility characterization. This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the chapter's real-variable capstones: the transfer of M-convexity's basic operations, optimality criterion, and supermodularity to the polyhedral (real-variable) setting, the identification of positively homogeneous M-convex functions with distance functions satisfying the triangle inequality, and — this mission's goal — the full directional-derivative/subdifferential correspondence.

Setting

Fix a finite ground set $V$. A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for $x,y \in \operatorname{dom}_{\mathbb R} g$ and $u \in \operatorname{supp}^+(x-y)$, some $v \in \operatorname{supp}^-(x-y)$ and $\alpha_0 > 0$ make the exchange inequality hold on $\alpha \in [0,\alpha_0]$; M♮-convex if its lift to one extra coordinate is M-convex. The directional derivative of $g$ at $x \in \operatorname{dom}_{\mathbb R} g$ in direction $d$ is $g'(x;d) = \inf_{t>0} (g(x+td) - g(x))/t$. A function is positively homogeneous if $g(tx) = t \cdot g(x)$ for all $t > 0$; write $0M[\mathbb R \to \mathbb R]$ for the positively homogeneous polyhedral M-convex functions. A distance function $\gamma$ satisfying the triangle inequality and its set of admissible potentials $D(\gamma)$ were introduced in chapter 5; the subdifferential $\partial_{\mathbb R} f(x) = \{p : f(y) - f(x) \ge \langle p, y-x \rangle\ \forall y\}$ generalizes this to any function $f$ at a point $x$ in its domain.

Formalization targets

Goal: the directional-derivative/subdifferential correspondence

For $f \in M[\mathbb R \to \mathbb R]$ and $x \in \operatorname{dom}_{\mathbb R} f$, setting $\gamma_{f,x}(u,v) = f'(x;-\chi_u+\chi_v)$:

$$\gamma_{f,x} \text{ satisfies the triangle inequality}, \quad \partial_{\mathbb R} f(x) = D(\gamma_{f,x}) \ne \emptyset, \quad f'(x;\cdot) = \widehat{\gamma_{f,x}}(\cdot),$$

with the analogous statement for $f \in M[\mathbb Z \to \mathbb R]$ at an integer point $x$, using $\gamma_{f,x}(u,v) = f(x-\chi_u+\chi_v)-f(x)$ (Theorem 6.61). This is the weakest stable form: it identifies the subdifferential exactly, as a set, rather than bounding its size or complexity, and holds at every point of the domain uniformly.

Supporting structural targets

Ten further results build the real-variable toolkit and the positive-homogeneity correspondence this goal completes: the transfer of M♮-convexity, the basic operations, the optimality criterion, supermodularity, and weighted-minimizer polyhedrality to the real-variable setting (Theorems 6.48-6.52, Proposition 6.53), the identification of the classes $0M[\mathbb Z|\mathbb R \to \mathbb R]$ and $0M[\mathbb R \to \mathbb R]$ and the compatibility of convex extension with positive homogeneity (Proposition 6.56), the two directions of the correspondence between positively homogeneous M-convex functions and triangle-inequality distance functions (Propositions 6.57-6.58, Theorem 6.59), and the fact that a directional derivative of an M-convex function is itself positively homogeneous and M-convex (Proposition 6.60).

Significance

Theorem 6.61 is the technical bridge that lets discrete convex analysis borrow the entire apparatus of classical convex duality: because the subdifferential of an M-convex function is always the admissible-potential set of a chapter-5 distance function, every fact already proved about $D(\gamma)$ (its polyhedral structure, its own L-convexity, its relationship to shortest paths) transfers immediately to subdifferentials of M-convex functions. This is exactly the mechanism the book calls out as essential for Chapter 8's separation theorem for M♮-convex functions. The $0M \leftrightarrow T$ correspondence (Theorem 6.59) is independently significant: it says the positively homogeneous special case of M-convex function theory — which is what directional derivatives of any M-convex function reduce to, by Proposition 6.60 — is exactly as rich as ordinary shortest-path distance function theory, no more and no less, so nothing new needs to be built to understand local behavior at a point.

None of these results are open — they are Murota's account of how the discrete exchange axiom interacts with directional differentiation and subgradients, a bridge chapter between the purely combinatorial theory of chapters 4-6 and the duality theory of chapter 8. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (MExchangeAxiomR, DirDeriv, GammaHat) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to Theorem 6.61 would try to compute $\partial_{\mathbb R} f(x)$ directly from the definition of subgradient and separately verify it happens to equal some $D(\gamma)$; the book's actual proof instead derives the equality of sets from the M-optimality criterion (Theorem 6.52) applied pointwise: $p \in \partial_{\mathbb R} f(x)$ is shown, via a chain of logical equivalences, to be exactly the condition defining $D(\gamma_{f,x})$, so no separate verification of polyhedrality or nonemptiness is needed beyond what Theorem 6.52 and Proposition 6.60 already supply. The genuine difficulty is upstream, in Proposition 6.60 itself: showing a directional derivative is M-convex requires exploiting the local validity of the identity $f(x+d)-f(x) = f'(x;d)$ for small $\|d\|_1$ (Eq. (6.85)) and then extending the exchange property from that neighborhood to all of $\mathbb R^V$ using positive homogeneity — a two-step argument with no single-step shortcut, since the exchange axiom's defining inequality is not obviously homogeneous-invariant on its own.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; real-domain functions are (V→ℝ)→WithTop ℝ. The directional derivative is built directly as an infimum of difference quotients over $t>0$, matching the book's own local characterization (Eq. (6.85)) without a separate limit construction. Positive homogeneity and the classes 0M[R→R]/0M[Z→R] are stated exactly as the book defines them (the latter via positive homogeneity of the convex extension, not of f itself, since f is undefined off Zⱽ). Theorems 6.49-6.50 restate 4 of their 8 operations (matching the identical scope decision for chunk 22-ch06b-mconvexfunctions's Theorem 6.13); Theorem 6.61 omits the dual-integral refinement clauses for the M[R→R|Z]/ M[Z→Z] sub-classes. Both reductions are documented, not trivializing omissions — see Difficulty above and HARD.md/MODERATION_NOTES.md. No numeric constants are hard-coded anywhere in this mission. This mission's definitions are redeclared from chunks 06-mconvex-functions-i, 21-ch05b-lconvexsets (for the distance-function/admissible-potential vocabulary), 22-ch06b-mconvexfunctions, and 23-ch06c-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal and Proposition 6.60 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota and A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 (the polyhedral M-convex function theory this mission's real-variable results are drawn from).

Motivation

An American option may be exercised at any moment up to maturity, so pricing one is not an integration problem but a stopping problem: the holder must decide, at each date and in each state of the market, whether the payoff available now beats the option value of waiting. A perpetual American put pushes this to its limit — there is no maturity at all, so the horizon is unbounded and the problem has no terminal condition to induct backwards from. What replaces the terminal condition is a fixed point characterization, and the classical answer, going back to McKean (1965) and Merton (1973) in continuous time and to Cox, Ross and Rubinstein (1979) in the binomial model, is that the price is the smallest superharmonic majorant of the payoff.

Bäuerle and Rieder's Chapter 11 (Markov Decision Processes with Applications to Finance, Springer, 2011) derives this from their own general unbounded-horizon stopping theory rather than from stochastic analysis, and in the same chapter applies the bounded-horizon version to a problem from banking rather than trading: when should a bank cancel a credit line? The two halves share one mathematical shape — a stopping problem whose optimal policy turns out to be of threshold type — and this mission formalizes both, with the perpetual put as the goal.

Setting

The binomial model (§11.1). A stock moves from price $x$ to $xu$ with risk-neutral probability $q$ and to $xd$ with $1-q$, where $0 < d < u$, and the discount factor is $\beta \in (0,1]$. The defining relation of the risk-neutral measure,

$$\beta q u + \beta(1-q)d = 1,$$

is carried as a hypothesis of the model: it is what makes the discounted stock price a martingale, and the proofs use it directly.

The American put with strike $K$ pays $(K-x)^+$ when exercised. With $n$ periods to maturity its price satisfies the recursion $J_0(x) = (K-x)^+$ and

$$J_n(x) = \max\Big\{(K-x)^+,\ \beta\big(q J_{n-1}(xu) + (1-q)J_{n-1}(xd)\big)\Big\} =: \mathcal{T}J_{n-1}(x),$$

the maximum being "exercise now" against "hold". Proposition 11.1.2 describes the price $\pi_n(x) := J_{N-n}(x)$ at time $n$ of an option maturing at $N$: it is continuous in $x$, decreasing in $n$, and — the part that carries the argument — $x \mapsto \pi_n(x) + x$ is increasing, even though $\pi_n$ itself decreases in $x$. That single reformulation, obtained by adding $x$ to both sides of the recursion and using the risk-neutral relation, is what yields the threshold structure: there are exercise boundaries $K =: x_N^* \ge x_{N-1}^* \ge \dots \ge x_0^* \ge 0$ with $\tau^* = \inf\{n \le N \mid X_n \le x_n^*\}$ optimal. Exercise when the stock falls far enough, and the boundary rises as maturity approaches.

The perpetual put (Theorem 11.1.3, the goal). With no expiration date the price at time zero is a supremum over all stopping times, $\tau \le \infty$ included:

$$P(x) := \sup_{\tau \le \infty} \mathbb{E}^{\mathbb{Q}}_x\big[\beta^\tau (K - S_\tau)\big],$$

with the stopping reward set to zero on $\{\tau = \infty\}$. The theorem says four things: $P$ is the limit of the finite-maturity prices $J_n$; $P$ solves $\mathcal{T}P = P$ and satisfies $0 \le P \le K$; $P$ is the smallest superharmonic function majorizing $(K-x)^+$; and, if the value $J_{f^*}$ of the exercise-region policy dominates $\mathcal{T}J_{f^*}$, then $P$ equals that value and $\tau^* = \inf\{n \mid X_n \in E^*\}$, the hitting time of $E^* = \{x \mid P(x) = (K-x)^+\}$, is optimal.

The conditional in part d) is the book's own and is not decoration: without it the exercise region need not deliver an optimal stopping time, and the unconditional version is a different, false statement. The boundedness $0 \le P \le K$ in b) is likewise a genuine claim rather than a side remark — the fixed point equation alone admits other solutions, and it is boundedness together with minimality that pins $P$ down among them.

Credit granting (§11.2). A bank holds a credit contract of maximal duration $N$. Each period it observes a rating class $x_n$ evolving as a Markov process $Q^X$, and chooses to extend — earning $c(x)$ — or to cancel, ending the contract. The value iteration is $J_n(x) = \max\{0,\ c(x) + \beta\int J_{n-1}\,dQ^X(\cdot|x)\}$. Under two structural assumptions — $c$ increasing, and $Q^X$ stochastically monotone, so that a better-rated borrower stays better-rated — Theorem 11.2.1 gives the same shape of answer as the option: cancel exactly when the rating falls below a threshold $x_n^*$, and those thresholds rise as the remaining duration shortens, since a marginal borrower is no longer worth keeping when there is little time left to recover.

Theorem 11.2.2 repeats this when the borrower is not rated at all. The bank has only a prior $\mu_0$ on the repayment probability and one signal per period; the state $(s,n)$ records $s$ positive signals out of $n$, and the expected repayment probability is the posterior mean $q(s,n)$. Monotonicity here is for the order of p. 342 — more positive signals and fewer negative ones — and not the coordinatewise order, under which the claim would be false: an extra signal that is negative makes the state worse.

What is being asked

Formalize Theorem 11.1.3 in full, all four parts: the limit identification, the fixed point equation with its bounds, the minimality among superharmonic majorants, and the conditional optimality of the exercise-region stopping time. The three milestones are Proposition 11.1.2, the finite-horizon put whose threshold structure the perpetual case specializes, and the two credit granting theorems, which run the same bounded-horizon argument on a different model.

The stopping-time apparatus is built rather than assumed: the stock path, the law $\mathbb{Q}$ pinned by its finite-dimensional distributions, stopping times valued in $\mathbb{N}\cup\{\infty\}$, and the reward vanishing at $\infty$. Part a) of the goal is the identification of the supremum with $\lim_n J_n$, so carrying $P$ as an abstract function would make the theorem vacuous.

Motivation

MAXIMUM SATISFIABILITY asks for a truth assignment satisfying as many clauses of a given set as possible. It was among the first NP-hard optimization problems for which an approximation algorithm came with a proven worst-case guarantee. In Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 1974, doi:10.1016/S0022-0000(74)80044-9), David S. Johnson set up a framework for measuring such guarantees and analyzed two heuristics for the problem. The second of these, algorithm B2, weights each clause by $2^{-|C|}$ and repeatedly sets a literal so that the heavier side is satisfied. On inputs whose clauses all have at least $k$ literals, it satisfies at least a $1 - 2^{-k}$ fraction of the optimum.

B2 is the ancestor of a line of work on MAX-SAT approximation:

• 1974. Johnson proves the $2^k/(2^k-1)$ bound for B2 on MS(k) and the $(k+1)/k$ bound for the unweighted greedy algorithm B1.
• 1994. Goemans and Williamson (SIAM J. Discrete Math. 7) present Johnson's algorithm as the derandomization, by conditional expectations, of the uniformly random assignment, and combine it with LP rounding to obtain a $3/4$-approximation.
• 1999. Chen, Friesen and Zheng (JCSS 58) show that B2 is a $2/3$-approximation on general inputs, sharper than the $1/2$ that Johnson's bound gives at $k = 1$.

Setting

A literal is a variable $x_i$ or its negation $\bar x_i$. A clause is a finite set of literals. A truth assignment is a set $T$ of literals containing no pair $\{x_i, \bar x_i\}$; it satisfies a clause $C$ when $C \cap T \ne \emptyset$. An input is a finite set $S$ of clauses, and $S^*$ is the largest $|S'|$ over subsets $S' \subseteq S$ satisfied by one truth assignment. MS(k) is the restriction to inputs in which every clause contains at least $k$ distinct literals.

Algorithm B2 keeps a set SUB of satisfied clauses, a set LEFT of unsettled clauses, the literals LIT still available, and a weight $w(C)$ per clause, starting from $w(C) = 2^{-|C|}$, $\mathrm{SUB} = \emptyset$, $\mathrm{LEFT} = S$. While some literal of LIT occurs in a clause of LEFT, it picks any such literal $y$. Let YT be the clauses of LEFT containing $y$ and YF those containing $\bar y$. If $\sum_{\mathrm{YT}} w \ge \sum_{\mathrm{YF}} w$, it makes $y$ true, moves YT to SUB and doubles the weight of each clause of YF; otherwise it does the symmetric move with $\bar y$. Finally it removes $y, \bar y$ from LIT. When no literal of LIT remains in LEFT it returns SUB.

The choice of $y$ is free, so several outputs may be choosable on one input. Johnson measures the algorithm by its worst choosable output, through the ratio $r(B2, S) = S^*/|\mathrm{SUB}|$ and its maximum $R[B2, \mathrm{MS}(k)](n)$ over inputs of size at most $n$.

Formalization targets

Goal: Theorem 3, with the equality range corrected

For every $k \ge 1$, every $S$ in MS(k) and every SUB choosable by B2 on $S$,

$$(2^k - 1)\,S^* \le 2^k\,|\mathrm{SUB}|,$$

and for every $k \ge 2$ there are $S$ in MS(k) and a choosable SUB with $|\mathrm{SUB}| > 0$ and

$$(2^k - 1)\,S^* = 2^k\,|\mathrm{SUB}|.$$

The paper states equality "for all sufficiently large $n$" for every $k \ge 1$. At $k = 1$ this is false: the ratio 2 would require every clause to be a unit clause and all clauses to be jointly satisfiable, and on such inputs B2 satisfies everything. The goal therefore asserts tightness for $k \ge 2$. A separate item states that at $k = 1$ the ratio is never attained.

Milestones

1. Initially, the total weight of LEFT is at most $|S|/2^k$.
2. No iteration increases the total weight of LEFT, so at halting it is still at most $|S|/2^k$.
3. At halting, every clause left in LEFT has weight exactly $1$.
4. At halting, $|\mathrm{LEFT}| \le |S|/2^k$ and $|\mathrm{SUB}| \ge |S|(1 - 2^{-k})$.
5. The eight-clause instance for $k = 3$ has $S^* = 8$ and admits a choosable output of size $7$.

Significance

The bound $1 - 2^{-k}$ is exactly the expected fraction of clauses a uniformly random assignment satisfies on MS(k). B2 attains it deterministically, and the proof bounds $|\mathrm{SUB}|$ against $|S|$ rather than against $S^*$, a feature the paper points out. For $k = 3$ the constant $8/7$ was later shown by Håstad (2001) to be optimal among polynomial-time algorithms unless P = NP, so the guarantee of this 1974 algorithm is best possible for MAX-E3-SAT.

Formalizing the result produces a machine-checked potential-function argument for a nondeterministic algorithm: the invariant links each clause's weight to how many of its literals have been removed. The mission also records a correction to the printed statement at $k = 1$. The paper's proof is complete; to our knowledge no machine-checked version exists.

Difficulty

The obvious argument follows the counting proof for algorithm B1 and compares clauses saved with clauses wounded in each step. It fails here: B2 can wound more clauses than it saves in a step, and the bound holds only in the weighted sense. The weight of a clause is not a static quantity. It is $2^{-|C|}$ times $2$ to the number of its literals already discarded, and this invariant must be carried through every step, including clauses that contain both $y$ and $\bar y$. Tightness needs an explicit input and an explicit adversarial run that exploits the tie in Step 4, and then a proof that every assignment of the remaining variables kills exactly one clause.

Formalization scope

• Literals and clauses. A literal is a pair (variable index in $\mathbb N$, sign). Clauses are Finsets of literals, and an input is a Finset of clauses, so there are no duplicate clauses. Truth assignments are partial and consistent. $S^*$ is a maximum over the finite, nonempty family of satisfiable subsets.
• B2 as a relation. B2 is a nondeterministic run relation, and "choosable" means reachable by finitely many steps from the initial state and halting. Step 3 allows a literal of either sign. The tie in Step 4 goes to $y$, and the comparison and doublings use the weights before the update. Weights are rationals.
• Size-free ratios. The size-dependent $R[B2, \mathrm{MS}(k)](n)$ is replaced by statements about every input (upper bound) and one attaining input (tightness). The two forms are equivalent because $R$ is a maximum over finitely many inputs and nondecreasing in $n$.
• No division. All ratios are multiplied out, so no division by zero can make a bound vacuous.
• Trivializations ruled out. A deterministic tie-break in Step 3 or 4, or tightness at a single fixed $k$, would be a weaker theorem and is not acceptable. So is stating only the upper bound.

The definitions (the MS layer, the run relation) can be reused by other MAX-SAT approximation results, and an identical MS layer appears in the companion mission on algorithm B1. Contributions welcome: proofs of the milestones, of the $k \ge 2$ tightness family, and of the $k = 1$ correction.

Selected references

• D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9 (1974) 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• J. Chen, D. K. Friesen, H. Zheng, Tight bound on Johnson's algorithm for maximum satisfiability, J. Comput. System Sci. 58 (1999) 622–640. https://doi.org/10.1006/jcss.1998.1610
• M. X. Goemans, D. P. Williamson, New 3/4-approximation algorithms for the maximum satisfiability problem, SIAM J. Discrete Math. 7 (1994) 656–666. https://doi.org/10.1137/S0895480192243516
• J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001) 798–859. https://doi.org/10.1145/502090.502098

Motivation

An insurance company collects premia and pays claims each period; the difference is a random, signed quantity that can push the company's risk reserve up or down. At the start of every period, before that period's premia and claims are realized, the company's owners may pay themselves a dividend out of the current reserve — but once the reserve goes negative the company is ruined and stops operating for good. How should the owners time and size these payments to maximize the total expected discounted dividend paid out before ruin? This is the classical De Finetti dividend problem, one of risk theory's oldest optimization questions, and Chapter 9 §9.2 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) solves its fully discrete-time version by identifying the exact combinatorial shape of the optimal policy — not just proving one exists. This mission also covers §9.1, a different application of Chapter 7's contracting theory to a consumption-investment problem whose planning horizon is itself random rather than fixed or infinite.

Setting

The dividend model is a stationary Markov Decision Model on the integers: the state $x \in \mathbb Z$ is the current risk reserve, the action $a \in \{0,1,\dots,x\}$ (for $x \ge 0$; only $a=0$ is available once ruined) is the dividend paid, the reward is $r(x,a):=a$, and the reserve evolves by i.i.d. increments $Z_n$ (premia minus claims) after the dividend is deducted. Because the reward is bounded by an explicit function of the state (Lemma 9.2.2), Chapter 7's general existence theory applies directly, and the value function $J_\infty$ satisfies a genuine Bellman equation. The chapter's real content begins once existence is established: Theorem 9.2.3 pins down enough analytic structure of $J_\infty$ and its largest-maximizing policy $f^*$ (monotonicity, a Lipschitz-type inequality, and a self-consistency identity) to drive a purely combinatorial argument that $f^*$'s shape is a finite alternation of "pay nothing" and "pay down to a fixed level" intervals — a band-policy (Definition 9.2.5). Section 9.1's random-horizon consumption-investment model reuses the same Chapter 7 machinery in a different setting: the usual $(c,a)$ (consumption, portfolio) decision each period, but where the horizon itself ends after each period with probability $1-p$, making the effective one-period discount $\beta p$ rather than $\beta$.

Formalization targets

The goal, Theorem 9.2.9, states the section's main claim in one sentence: the stationary policy $(f^*,f^*,\dots)$ is optimal and is a band-policy. Short as it is stated, its proof assembles every earlier result of the section. The milestones supply that assembly, in order: Lemma 9.2.2 gives the model's bounding function and the resulting integrability/convergence facts; Theorem 9.2.3 gives the value-function bounds and the self-consistency identity $f^*(x-f^*(x))=0$; Corollary 9.2.4 checks the two sign-definite degenerate cases directly from Theorem 9.2.3; Proposition 9.2.6 proves the top threshold $\xi := \sup\{x \mid f^*(x)=0\}$ is finite (not merely well-defined) and that $f^*$ is a simple barrier above it; Proposition 9.2.8 proves the increment property below $\xi$ that forces each band's shape; and Theorem 9.2.10 (a postscript refinement, stated after the goal) shows the wave lengths are bounded once the reserve's downward jumps are themselves bounded, collapsing to a single barrier-policy in the extreme case. Theorem 9.1.1, the random-horizon consumption-investment verification theorem, is included as a full item but is not a milestone of this goal, since its content and proof belong to a different, disjoint model — see Difficulty.

Significance

Band-policies and the discrete-time De Finetti dividend problem have no substrate anywhere in Mathlib or on the platform, and the result is a genuinely deep, classical one: a discrete-time analogue of the continuous-time De Finetti barrier-strategy theory, obtained here by pure dynamic-programming argument rather than the stochastic-calculus techniques the continuous-time theory usually relies on. The mission is explicit that the goal's conclusion is the general band-policy structure, not the strictly weaker barrier-policy special case that Theorem 9.2.10 b) proves only under an extra hypothesis (bounded downward jumps) — stating the goal with a barrier-policy conclusion instead would understate what Theorem 9.2.9 actually proves.

Difficulty

The central formalization challenge is Definition 9.2.5's own combinatorial intricacy: a band-policy is specified by an alternating chain of thresholds $0 \le c_0 < d_1 \le c_1 < d_2 \le \dots \le d_n \le c_n$ with a positive-width gap condition on every wave, and the policy's four piecewise branches case-split on which wave (if any) the current state falls into. This mission renders it existentially over the witnessing $(n,c,d)$ rather than as one closed-form function, a faithful but more verbose transcription that avoids conflating the different branch conditions. A second difficulty is Proposition 9.2.6's own finiteness claim: $\xi$ is a supremum over a subset of $\mathbb N_0$ that could, in principle, be unbounded, and Mathlib's convention for sSup over the naturals returns a finite junk value ($0$) even for an unbounded set — using it directly would silently trivialize "$\xi<\infty$" into a claim that is true regardless of the proposition's actual mathematical content. This mission instead states the proposition by exhibiting the finite value of $\xi$ directly, so that "$\xi$ is finite" survives as genuine content that the theorem's proof must establish. A third difficulty is scope: Theorem 9.1.1's random-horizon consumption-investment model shares no state space, action space, or definitions with the dividend model of the goal, despite both appearing in this chunk's assigned page range; it is formalized as a genuine application of a locally-restated copy of Chapter 7's contracting theory, but is excluded from the milestone list proper since it plays no role in the goal's own proof.

Formalization scope

The dividend model's transition law is built from Mathlib's PMF (probability mass function) type on $\mathbb Z$, which supplies the "probabilities sum to one" fact automatically rather than as a separate hypothesis. J_\infty, \delta, and every finite-horizon value function throughout this mission use this whole book series' Filter.limsup-of-truncations convention for infinite-horizon reward, restated locally (own namespace copy, per this series' file-ownership boundary) from chunk 07a's identical apparatus rather than imported. The consumption-investment model of §9.1 is formalized with the number of risky assets $d$ as an explicit type parameter and its admissible-portfolio and domain restrictions as separate, citable fields rather than folded silently into the reward or transition definitions.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• B. De Finetti, "Su un'impostazione alternativa della teoria collettiva del rischio", Transactions of the XVth International Congress of Actuaries, 1957 (the original continuous-time dividend problem this chapter's discrete-time analogue is modeled on).
• H. Schmidli, Stochastic Control in Insurance, Springer, 2008 (cited by Remark 9.2.1 for the reduction from a continuous dividend-payout action space to the integer setting used throughout this section).
• H. U. Gerber, "Games of economic survival with discrete- and continuous-income processes", Operations Research, 1972 (an early discrete-time treatment of the same class of problems, in the spirit this chapter's own model follows).

Motivation

Every mission in this series so far has treated a control problem that already lives in discrete time: a decision maker observes a state, chooses an action, and the process moves to a new state at the next integer time step. Many real systems evolve in continuous time instead — a machine that runs deterministically until it randomly breaks down and is repaired into a new condition, an inventory that drains continuously until a random demand arrives, a population that grows deterministically between random catastrophic events. Chapter 8 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) shows that an entire class of such continuous-time control problems — Piecewise Deterministic Markov Decision Processes, where the state moves along a deterministic, controlled flow between randomly-timed jumps to a new state — can be solved by exactly the discrete-time machinery this book's series has already built, once the problem is re-expressed as a Markov Decision Model at the jump times themselves. This mission covers that embedding and its consequences (§8.2), and a simpler, discrete-state special case, the continuous-time Markov Decision Chain, treated with both an infinite and a finite time horizon (§8.3).

Setting

A Piecewise Deterministic Markov Decision Model (Definition 8.1.1) consists of a Borel state space $E$, a Borel control space $U$, a deterministic drift $\mu(x,u)$ governing the flow $\varphi^\alpha_t(x)$ between jumps, a Poisson jump clock of rate $\lambda$, a kernel $Q$ giving the distribution of the post-jump state, a reward rate $r$, and a discount rate $\beta$. A control is a whole measurable function $\alpha : \mathbb R_{\ge0} \to U$ fixed at each jump time and applied until the next one — so the "action space" of the embedded discrete-time problem is itself a function space, a genuinely new technical wrinkle this book's earlier chapters never face. Embedding at the jump times produces a discrete-time Markov Decision Model $(E,A,Q',r')$ whose reward and kernel are themselves integrals of the original data against the flow (Eqs. (8.4)-(8.5)); Chapter 7's infinite-horizon existence theory, already developed for a general Borel state space, applies directly to this embedded model once its own compactness and semicontinuity hypotheses are checked. Checking them forces a further enlargement of the control space to the relaxed controls $R$ — measurable functions into probability measures on $U$ rather than $U$ itself — which is compact in a suitable topology where the space of literal control functions is not.

Formalization targets

The goal, Theorem 8.2.6, is the chapter's central existence result: given a continuous upper bounding function with the discrete embedded model's own contraction-type condition and a package of continuity/compactness assumptions, the value function of the model embedded with relaxed controls is bounded, upper semicontinuous, and a genuine fixed point of the maximal- reward operator, and an optimal relaxed Markov policy exists. The milestones build up to it and extend past it: Theorem 8.2.1 establishes the foundational fact that the continuous-time expected reward of the original process equals the discrete-time embedded model's own value — the correspondence every other result in the chapter relies on; Lemma 8.2.5 is the technical semicontinuity-preservation step the goal's proof needs; Theorem 8.2.7 upgrades the goal's relaxed optimal policy to a genuine, nonrelaxed one under an uncontrolled-flow or convexity condition; Theorem 8.2.8 gives the classical Hamilton-Jacobi-Bellman verification technique as an alternative, differential route to the same value function. Section 8.3's continuous-time Markov Decision Chain — the same theory specialized to a countable state space, transition rates in place of a kernel, and an uncontrolled flow — is covered for both an infinite horizon (Theorem 8.3.1) and, the more finance-relevant case, a finite horizon with a terminal reward (Theorems 8.3.2-8.3.3).

Significance

Piecewise Deterministic Markov Processes have no substrate anywhere in Mathlib or on the platform, and this mission's content is a genuine method, not just a specialization of existing results: it shows how to reduce an entire continuous-time control problem to the discrete-time theory already available, at the cost of enlarging the state of the discrete embedded problem's own data (which becomes an integral against a whole flow, not a pointwise value) and enlarging the control space when compactness is needed for existence. This mission is careful to keep two distinctions the book itself insists on separate: relaxed versus nonrelaxed controls (Theorem 8.2.6 produces only the former; recovering the latter is Theorem 8.2.7's own, harder, conditional content), and the general Piecewise Deterministic model of §8.1-8.2 versus the simpler, discrete-state Markov Decision Chain of §8.3, which is a genuinely different structure (sums over a countable state space rather than integrals against a controlled flow), not an instance of the general model specialized after the fact.

Difficulty

The central formalization challenge is representing the continuous-time expected reward $V^\pi(x)$ (Eq. (8.2)) faithfully, since the book itself only asserts the existence of a probability space carrying the jump-time/post-jump-state process with a specified conditional law, citing general marked-point-process theory rather than constructing it. This mission builds that probability-space data directly — via Mathlib's conditional expectation, conditioning on the current post-jump state — rather than treating $V^\pi$ as a bare hypothesis-only quantity, so that Theorem 8.2.1's value-equality claim is a genuine, non-vacuous correspondence between two independently-defined objects (a continuous-time path functional and a discrete-time recursion) rather than true by definitional fiat. A second, compounding difficulty is that the same correspondence must be built twice — once for the general flow-driven process (§8.2) and again, independently, for the discrete-state jump process of the finite-horizon chain (§8.3) — since the two models share no state-space structure. A third difficulty specific to Theorem 8.2.8 is that its Hamilton-Jacobi-Bellman verification argument is genuinely differential (a process generator built from a gradient, a self-referential closed-loop control solving its own ODE), unlike every other result in this chapter, which works through the discrete-time embedding alone.

Formalization scope

The book's own topology on the control-function space $A$ (the coarsest making certain integrals measurable) and the Young topology on the relaxed-control space $R$ (which the book cites as making $R$ separable, metric and compact, without reconstructing it) are not rebuilt from scratch; continuity/compactness hypotheses that need a topology on these spaces are stated directly against the pointwise/product topology on the underlying function types, a faithful but representationally simpler stand-in documented in MODERATION_NOTES.md. The embedded kernel $Q'$ (Eqs. (8.4), (8.7)) is bundled as data satisfying its own defining integral identity rather than literally constructed as a mixture of pushforward measures — a routine but heavy argument that would add no mathematical content beyond the formula itself. This mission's own goal (Theorem 8.2.6) explicitly produces a relaxed-control optimal policy, not a nonrelaxed one: stating it with a $U$-valued policy instead would silently substitute Theorem 8.2.7's strictly harder, conditionally-true conclusion for Theorem 8.2.6's own unconditional one, exactly the trivializing formalization this chapter's own structure warns against.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• M. H. A. Davis, Markov Models and Optimization, Chapman & Hall, 1993 (the standard reference for Piecewise Deterministic Markov Processes, cited by the book for extensions of this chapter's basic model).
• A. A. Yushkevich, "On reducing a jump controllable Markov model to a model with discrete time", Theory of Probability and its Applications, 1980 (the topology on the control-function space $A$ cited by Definition 8.1.1's own construction).
• H. J. Kushner and P. G. Dupuis, Numerical Methods for Stochastic Control Problems in Continuous Time, 2nd ed., Springer, 2001 (the Young topology and the Chattering Theorem, cited by Remark 8.2.3).
• N. Bäuerle and U. Rieder, "Optimal control of piecewise deterministic Markov processes with finite time horizon", in Modern Trends of Controlled Stochastic Processes: Theory and Applications, 2010 (cited for the finite-horizon extension of this chapter's model, applied in chunk 09b's Sections 9.3-9.4).

Motivation

Scaling algorithms are one of the standard techniques for solving discrete optimization problems efficiently: instead of searching a huge integer domain directly, an algorithm first solves a coarsened version of the problem — checking optimality only against neighbors reached by a large step size $\alpha$ — and then refines the resulting approximate solution down to the true optimum. This strategy is only as good as the guarantee that a coarse-scale local optimum is provably close to a true, fine-scale global optimum; without such a guarantee, refinement could require an unbounded number of steps. Results providing this guarantee are called proximity theorems, and they are a standard tool across combinatorial optimization, from network flow scaling algorithms to submodular function minimization.

M-convex functions, the subject of this chapter, are exactly the class of discrete convex functions for which the classical local-optimality test of chapter 3 (checking a full neighborhood of up to $3^n-1$ sign patterns) sharpens to a much smaller, purely pairwise test: checking $f(x) \le f(x - \chi_u + \chi_v)$ for every pair of coordinates $u, v$. This mission formalizes the chapter's central definitional equivalence (Theorem 6.2), this pairwise optimality criterion (Theorem 6.26), a structural minimizer-cut lemma (Theorem 6.28), and the chapter's capstone, the M-proximity theorem (Theorem 6.37) — the result that makes M-convex scaling algorithms provably correct, with an explicit, dimension-and-scale-only distance bound between a coarse-scale local optimum and a true global minimizer.

Setting

Let $V$ be a finite ground set. A function $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain $\operatorname{dom} f$ is an M-convex function if it satisfies the exchange axiom (M-EXC[Z]): for $x, y \in \operatorname{dom} f$ and $u$ in the positive support of $x - y$, there is $v$ in the negative support of $x-y$ with

$$f(x) + f(y) \ge f(x - \chi_u + \chi_v) + f(y + \chi_u - \chi_v).$$

An M$^\natural$-convex function is one whose lift $\tilde f$ to the extended ground set $\tilde V = \{0\} \cup V$ — defined by $\tilde f(x_0, x) = f(x)$ when $x_0 = -x(V)$, and $+\infty$ otherwise — is M-convex; equivalently (Theorem 6.2, below) $f$ satisfies the axiom (M$^\natural$-EXC[Z]), a variant of (M-EXC[Z]) that additionally allows a single-coordinate move ($u$ alone, with no compensating $v$). Every M-convex function is M$^\natural$-convex, but not conversely. For $\alpha$ a positive integer, a point satisfies the scaled local optimality condition at scale $\alpha$ if $f(x_\alpha) \le f(x_\alpha + \alpha(\chi_v - \chi_u))$ for all relevant $u, v$ — a check against neighbors $\alpha$ steps away rather than adjacent ones.

Formalization targets

Goal: Theorem 6.37 (the M-proximity theorem)

Assume $\alpha$ is a positive integer and $n = |V|$.

$$\text{(1) } f \text{ M-convex, } f(x_\alpha) \le f(x_\alpha + \alpha(\chi_v-\chi_u))\ \forall u,v \implies \exists x^* \in \arg\min f,\ \|x_\alpha - x^*\|_\infty \le (n-1)(\alpha-1),$$ $$\text{(2) } f \text{ M}^\natural\text{-convex, same hypothesis over } u,v \in V \cup \{0\} \implies \exists x^* \in \arg\min f,\ \|x_\alpha - x^*\|_\infty \le n(\alpha-1).$$

Both bounds are exact and specific to their hypothesis class; replacing either with an unspecified function of $n$ and $\alpha$ would discard exactly the content chapter 10's algorithms rely on.

Milestones: Theorems 6.2, 6.26, 6.28

Theorem 6.2: M$^\natural$-convexity (defined via the lift) is equivalent to the direct exchange axiom (M$^\natural$-EXC[Z]) — the chapter's central definitional theorem, needed to work with M$^\natural$-convex functions without repeatedly invoking the lift construction. Theorem 6.26 (the M-optimality criterion): global optimality of $f$ at $x$ is equivalent to a purely pairwise local check, $f(x) \le f(x-\chi_u+\chi_v)$ for all $u,v$ (plus, in the M$^\natural$ case, $f(x) \le f(x\pm\chi_v)$). Theorem 6.28 (the M-minimizer cut): from any point and any coordinate pair minimizing a one-step exchange, one can certify a coordinate-wise bound that some global minimizer must satisfy — the structural fact underlying both the domain-reduction algorithm and, via the same proof technique, the proximity theorem itself.

Significance

The result itself. Theorem 6.26 already sharpens chapter 3's local-to-global criterion (checking a full $3^n-1$-point neighborhood) to an $O(n^2)$-size pairwise check — the minimum spanning tree optimality criterion is a direct special case. The proximity theorem builds on this to control what happens when the local check is only performed at a coarse scale $\alpha$: it guarantees that scaling-based algorithms, which alternate between coarse-scale local search and scale reduction, terminate with a guaranteed-close approximation at every stage, with an explicit linear-in-$n$, linear-in-$\alpha$ error bound rather than a qualitative "eventually converges" guarantee.

Formalizing it. No matching item exists on the platform for M-convex functions, the exchange axiom, or a discrete proximity theorem of this kind. This mission gives the first formal statement of the M-optimality criterion and the M-proximity theorem, together with the exchange-axiom / lift-based-definition equivalence (Theorem 6.2) that the rest of the M-convex function theory (chunks 07, and indirectly 10–14) is built on.

Difficulty

The natural first attempt at Theorem 6.37 is to try a direct coordinatewise argument: since the scaled hypothesis holds for every pair $u, v$, one might hope to bound $|x_\alpha(v) - x^*(v)|$ coordinate by coordinate independently. This does not work, because a single application of the exchange axiom only ever improves $f$ by trading one coordinate down and one other coordinate up simultaneously — there is no way to move a single coordinate toward a minimizer in isolation without accounting for where the compensating mass goes. The actual proof instead fixes a target coordinate $v$, constructs a chain of strictly decreasing function values $y_0 = x_\alpha, y_1, \ldots, y_k$ by repeatedly applying (M-EXC[Z]) against a fixed near-optimal point $x^*$ (exactly the technique of Theorem 6.28's proof), and then bounds how far each other coordinate can move along this chain using the scaled hypothesis itself, before summing those bounds via the M-convex domain's hyperplane constraint $x(V) =$ constant to recover the bound on $v$. The chain construction, not a per-coordinate estimate, is what makes the linear-in-$n$ bound provable at all.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is (V → ℤ) → WithTop ℝ. M$^\natural$-convexity is represented via an explicit lift to Option V (none standing for the extended ground set's new element $0$), matching the book's own primary definition; the direct exchange-axiom form is a separate predicate related to it by Theorem 6.2, not conflated with it. `‖x_\alpha - x^*|_\infty \le c$ is stated pointwise.

A trivializing formalization of the goal would replace either exact bound, $(n-1)(\alpha-1)$ or $n(\alpha-1)$, with an unspecified asymptotic bound, or merge the two hypothesis classes into a single weaker statement; neither is done here. Propositions establishing dom f as an M-convex set, the M/M$^\natural$ relationship (Theorem 6.3), and several structural closure properties are cut from this mission's scope (not needed by the chosen items' statements — see MODERATION_NOTES.md) but are natural targets for a follow-on mission or for chunk 07, which builds directly on this chunk's exchange-axiom vocabulary. Contributions building the arg min f M-convexity corollary (Proposition 6.29) or the scaled minimizer cut (Theorem 6.39, the direct generalization of Theorem 6.28 drafted here) are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• D. S. Hochbaum, "Lower and upper bounds for the allocation problem and other nonlinear optimization problems," Mathematics of Operations Research, 19(2), 1994, pp. 390–409.