Operations Research

Motivation

The $k$-server problem was introduced by Manasse, McGeoch, and Sleator (STOC 1988 / J. Algorithms 1990) as a common generalization of paging, weighted caching, and related sequential decision problems, and their $k$-server conjecture has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly $k$ — governs deterministic online server management on every metric space.

Timeline

• 1985. Sleator and Tarjan introduce competitive analysis — an online algorithm judged against the offline optimum on every input — for list update and paging, and ask for a theory of such guarantees.
• 1988–1990. Manasse, McGeoch, and Sleator introduce the $k$-server problem (STOC 1988; J. Algorithms 1990) and settle its extremes: no deterministic algorithm beats ratio $k$ on any space with more than $k$ points (Corollary 7), two servers admit a $2$-competitive algorithm (Theorem 5, algorithm RES), and $k$ servers on $k+1$ points admit a $k$-competitive one (Theorem 4, algorithm BAL). Section 8 poses the $k$-server conjecture, in the symmetric finite setting of the paper.
• 1990. Fiat, Rabani, and Ravid (FOCS 1990) give the first competitive ratio depending on $k$ alone — exponential in $k$, but finite on every metric space.
• 1991. Chrobak, Karloff, Payne, and Vishwanathan (SIAM J. Discrete Math.) prove the conjecture on the real line via Double Coverage; Chrobak and Larmore (SIAM J. Comput.) extend it to all tree metrics.
• 1995. Koutsoupias and Papadimitriou (J. ACM) prove the Work Function Algorithm is $(2k-1)$-competitive on every metric space — the breakthrough, and still the best general bound. Their Conjecture 1.1 fixes the conjecture's modern form: for every metric space there is an online algorithm with competitive ratio $k$.
• 1996. The same authors verify the conjecture on spaces of $k+2$ points via the dual 2-evader problem (Inf. Process. Lett. 57).
• 2004. Bartal and Koutsoupias prove the WFA itself is $k$-competitive on the line, weighted stars, and all spaces of $k+2$ points.
• 2021. Coester and Koutsoupias (ICALP) give a unifying potential for all known WFA analyses and push the frontier to the circle.
• 2023. Bubeck, Coester, and Rabani (STOC) refute the randomized analogue: no $o(\log^2 k)$-competitive randomized algorithm exists in general. The deterministic conjecture — this mission's goal — survives as the central open question, with the gap between $k$ and $2k-1$ unmoved since 1995.
• 2026. Coester, Koutsoupias, and Zbysiński post The $k$-server conjecture is true (arXiv:2609.15979), a claimed proof of the full conjecture: the Work Function Algorithm itself is $k$-competitive on every metric space, via a matrix representation of work functions and a potential function built on it. The preprint is not yet peer-reviewed; this mission's goal stays open until a machine-checked proof exists.

Setting

Fix a metric space $M$ with distance function $d$, and a number of servers $k \ge 1$. A configuration records where the $k$ servers stand: it is a function $C$ assigning to each server $i \in \{1, \dots, k\}$ a point $C(i) \in M$. Moving the servers from configuration $C$ to configuration $C'$ means server $i$ travels from $C(i)$ to $C'(i)$; the movement cost is the total distance traveled,

$$\mathrm{moveCost}(C, C') \;=\; \sum_{i=1}^{k} d\bigl(C(i),\, C'(i)\bigr).$$

A request sequence is a finite list $\sigma = (r_1, \dots, r_n)$ of points of $M$, presented one at a time; write $\sigma_{\le j} = (r_1, \dots, r_j)$ for the list of the first $j$ requests (so $\sigma_{\le 0}$ is the empty list).

A deterministic online algorithm $A$ is a rule that, for every finite request sequence $\ell$, specifies a configuration $A(\ell)$ — where the servers stand after serving the requests of $\ell$ in order. In particular $A(\text{empty list})$ is the initial configuration, before any request arrives. Two points about this way of modeling an algorithm:

• Online and deterministic, by construction. The configuration after $j$ requests is $A(\sigma_{\le j})$, a function of those first $j$ requests only — the algorithm cannot see the future, and makes no random choices.
• The service constraint. Whenever a request sequence ends with a request $r$, some server must stand at $r$ immediately after: for every list $\ell$ and every point $r$, the configuration reached after serving $\ell$ followed by $r$ places at least one server at the point $r$.

Running $A$ on $\sigma = (r_1, \dots, r_n)$ produces the configurations $A(\sigma_{\le 0}),\, A(\sigma_{\le 1}),\, \dots,\, A(\sigma_{\le n})$, and its cost is the total movement along this trajectory:

$$\mathrm{cost}_A(\sigma) \;=\; \sum_{j=1}^{n} \mathrm{moveCost}\bigl(A(\sigma_{\le j-1}),\, A(\sigma_{\le j})\bigr).$$

For comparison, an offline schedule for $\sigma$ starting at a configuration $C_0$ is any sequence of configurations $S_0 = C_0, S_1, \dots, S_n$ in which $S_j$ places a server at the request $r_j$, for each $j$ — chosen with the whole of $\sigma$ known in advance. The optimal offline cost $\mathrm{OPT}(C_0, \sigma)$ is the infimum, over all such schedules, of the total movement $\sum_{j=1}^{n} \mathrm{moveCost}(S_{j-1}, S_j)$.

Finally, $A$ is $c$-competitive if there is a constant $a$ — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with

$$\mathrm{cost}_A(\sigma) \;\le\; c \cdot \mathrm{OPT}\bigl(A(\text{empty list}),\, \sigma\bigr) + a \qquad \text{for every request sequence } \sigma.$$

Formalization targets

Goal — the $k$-server conjecture

$$\text{For every } k \ge 1,\ \text{every metric space } M,\ \text{and every initial configuration } C_0:\ \exists\, A \text{ starting at } C_0 \text{ that is } k\text{-competitive.}$$

The goal fixes no algorithm: any $k$-competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof.

Milestones — the known ladder

The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound $c \ge k$ on any space with at least $k+1$ points; the conjecture for $k = 2$; for spaces of exactly $k+1$ points; for the real line; the $(2k-1)$ upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly $k+2$ points; the conjecture for three servers in the Manhattan plane $(\mathbb{R}^2, \ell^1)$ — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm itself — not just some algorithm — is $3$-competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the randomized analogue: there are $(k+1)$-point spaces on which every randomized algorithm is $\Omega(\log^2 k)$-competitive, stated over a mixed-strategy model of randomized online algorithms.

Significance

A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio $k$ is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences.

None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized $k$-server problem.

Difficulty

The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server other than the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds $k$.

Formalization scope

The Lean model commits to: configurations as functions Fin k → M (labeled servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions List M → (Fin k → M) with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in ℝ via Metric.dist; the offline optimum as an sInf over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as ∃ a, ∀ σ.

Two conventions guard against trivialization. The additive constant is quantified before the request sequence — allowing it to depend on $\sigma$ would make every algorithm $1$-competitive. And the lower-bound milestone requires $k+1$ distinct points (Finset.card = k + 1); on spaces with at most $k$ points the conjecture is trivially true and the lower bound false.

Three further definitional layers extend the model. The work function workFunction C₀ σ C is the sInf of (schedule cost + final move to C) over schedules serving σ from C₀, and the Work Function Algorithm WFA is defined on finite spaces with k ≥ 1 servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A tree is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A randomized algorithm is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in $[0,\infty]$, and $c$-competitiveness from $C_0$ demands every outcome start at $C_0$ and one additive constant work for all request sequences.

Welcome contributions: proofs of any milestone in any order (the lower bound and the $(k+1)$-point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about moveCost, schedules, and work functions published as reusable platform theorems.

Selected references

• M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11 (1990). doi:10.1016/0196-6774(90)90003-W
• A. Fiat, Y. Rabani, Y. Ravid, Competitive k-server algorithms, FOCS 1990. doi:10.1109/FSCS.1990.89566
• M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, New results on server problems, SIAM J. Discrete Math. 4 (1991). doi:10.1137/0404017
• M. Chrobak, L. Larmore, An optimal on-line algorithm for k servers on trees, SIAM J. Comput. 20 (1991). doi:10.1137/0220008
• E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42 (1995). doi:10.1145/210118.210128
• E. Koutsoupias, C. Papadimitriou, The 2-evader problem, Inf. Process. Lett. 57(5) (1996), 249–252.
• C. Coester, E. Koutsoupias, Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle, ICALP 2021. arXiv:2102.10474
• S. Bubeck, C. Coester, Y. Rabani, The randomized k-server conjecture is false!, STOC 2023. arXiv:2211.05753
• E. Koutsoupias, The k-server problem (survey), Computer Science Review 3 (2009). doi:10.1016/j.cosrev.2009.04.002

Motivation

Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed $\pm 1$ so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.

Timeline

• 1963. Steinitz-type vector balancing questions circulate; Bárány and Grinberg later (1981) show any norm admits a dimension-dependent bound $2d$, setting the theme: how much of the dependence on dimension is real?
• 1981. Beck and Fiala (Discrete Appl. Math.) prove degree-$t$ set systems have discrepancy at most $2t - 1$, by the floating-colors argument, and conjecture $O(\sqrt{t})$.
• 1980s. Komlós poses the vector form — unit $\ell^2$-norm columns, constant $\ell^\infty$ discrepancy — which implies the Beck–Fiala conjecture; it circulates through Spencer's Ten Lectures (1987) as the central open problem of the area.
• 1985. Spencer (Trans. AMS) proves "six standard deviations suffice": discrepancy $6\sqrt{n}$ for $n$ sets on $n$ points, beating random signing via the partial-coloring method.
• 1998. Banaszczyk (Random Struct. Algorithms) proves the Komlós bound $O(\sqrt{\log n})$ by a recursive Gaussian-measure argument over convex bodies.
• 2010–2016. The constructive era: Bansal (2010) makes Spencer algorithmic by SDP random walks, Lovett and Meka (2012) simplify, and Bansal, Dadush, and Garg (STOC 2016) give a polynomial-time algorithm matching Banaszczyk's bound.
• 2023. Kunisky (SIAM J. Discrete Math.) constructs instances from unsatisfiable formulas with discrepancy approaching $1+\sqrt{2}$ — the strongest lower bound on the conjectured constant.
• 2025. Bansal and Jiang (arXiv:2508.03961) break the Banaszczyk barrier: $\tilde{O}((\log n)^{1/4})$ for Komlós, and the Beck–Fiala conjecture resolved for $t \ge \log^2 n$ — the first movement in nearly thirty years. The gap between $2.414\ldots$ and $\tilde{O}((\log n)^{1/4})$ is the conjecture.

Setting

Fix $n$ vectors $v_1, \dots, v_n \in \mathbb{R}^m$ with Euclidean norm $\lVert v_i \rVert_2 \le 1$. A sign vector is an $\varepsilon \in \{-1, +1\}^n$: one sign $\varepsilon_i \in \{\pm 1\}$ per vector. Writing $v_{ij}$ for the $j$-th coordinate of the vector $v_i$, the discrepancy of the family under $\varepsilon$ is the largest coordinate, in absolute value, of the signed sum $\sum_i \varepsilon_i v_i$ — that is, $\max_{j \le m} \lvert \sum_{i \le n} \varepsilon_i v_{ij} \rvert$, the $\ell^\infty$ norm of the signed sum. The Komlós property at constant $K$ — KomlosBound K — says that every such family, in every $n$ and every $m$, admits a sign vector with every coordinate of the signed sum at most $K$ in absolute value.

Set systems embed as the special case of $0/1$-incidence matrices: if $A$ is an $m \times n$ matrix of $0$s and $1$s in which every column has at most $t$ ones (every element lies in at most $t$ sets), the columns scaled by $1/\sqrt{t}$ have norm at most one, so the Komlós property gives discrepancy $K\sqrt{t}$ — the Beck–Fiala conjecture.

Formalization targets

Goal — the Komlós conjecture

$$\exists\, K \in \mathbb{R}: \quad \text{every } v_1, \dots, v_n \in \mathbb{R}^m \text{ with } \lVert v_i\rVert_2 \le 1 \text{ admits } \varepsilon \in \{\pm 1\}^n \text{ with } \max_j \Big|\sum_i \varepsilon_i v_{ij}\Big| \le K.$$

The goal fixes no value of $K$: any finite universal constant settles it, so the statement survives every improvement in the constant.

Milestones — the known ladder

Eight results over the same definitions: Beck–Fiala's $2t - 1$ for degree-$t$ set systems; Spencer's $6\sqrt{n}$ for $n$ sets on $n$ points; Banaszczyk's $O(\sqrt{\log n})$ for the Komlós setting; its corollary $O(\sqrt{t \log n})$ for set systems; the reduction "Komlós at $K$ implies Beck–Fiala at $K\sqrt{t}$"; Kunisky's lower bound $K \ge 1 + \sqrt{2}$; and the two 2025 Bansal–Jiang breakthroughs — $\tilde{O}((\log n)^{1/4})$ for the Komlós setting, and the Beck–Fiala conjecture's bound $O(\sqrt{t})$ in the regime $t = \Omega(\log^2 n)$.

Significance

The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.

None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.

Difficulty

Random signs lose: they give $\Theta(\sqrt{n})$, not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below $2t - O(1)$ by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at $\sqrt{\log n}$ by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least $1 + \sqrt{2}$ — so any proof must handle instances strictly harder than the set-system case.

Formalization scope

The Lean model commits to: vectors as EuclideanSpace ℝ (Fin m), whose norm is the $\ell^2$ norm (the hypothesis $\lVert v_i \rVert \le 1$ reads ‖v i‖ ≤ 1); the $\ell^\infty$ conclusion written coordinatewise as ∀ j, |∑ i, ε i * v i j| ≤ K, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with ε i = 1 ∨ ε i = -1; and set systems as matrices A : Fin m → Fin n → ℝ with an entrywise $0/1$ hypothesis and column-degree counted by Set.ncard. Quantifier order matters everywhere: in KomlosBound K the constant is fixed before $n$ and $m$ — a $K$ depending on $n$ would make the statement the trivial $\sqrt{n}$ bound. In beck_fiala the hypothesis $t \ge 1$ is required (the degree-$0$ system has discrepancy $0 > 2t-1$ otherwise); the Banaszczyk-form bounds use $\log(n+2)$ so that the bound is positive already at $n \le 1$. In the Bansal–Jiang milestones the asymptotic $\tilde{O}$ and $\Omega$ are rendered by existential constants quantified before all instances: the hidden $\mathrm{poly}(\log\log n)$ factor becomes $(\log\log(n+8))^{\gamma}$ for some fixed $\gamma > 0$ (the inner shift $+8$ keeps the iterated logarithm positive), and the threshold $t = \Omega(\log^2 n)$ becomes $C_0 \log^2(n+2) \le t$ for some fixed $C_0 > 0$.

Welcome contributions: any milestone in any order — beck_fiala and komlos_implies_beck_fiala are self-contained finite arguments and the natural entry points; spencer_six_deviations and banaszczyk_bound each import a major technique; komlos_lower_bound needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.

Selected references

• J. Beck, T. Fiala, "Integer-making" theorems, Discrete Applied Mathematics 3 (1981). doi:10.1016/0166-218X(81)90022-6
• J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985). doi:10.1090/S0002-9947-1985-0784009-0
• W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures & Algorithms 12 (1998). doi link
• N. Bansal, D. Dadush, S. Garg, An algorithm for Komlós conjecture matching Banaszczyk's bound, FOCS 2016 / SIAM J. Comput. arXiv:1605.02882
• N. Bansal, H. Jiang, Decoupling via affine spectral-independence: Beck–Fiala and Komlós bounds beyond Banaszczyk, 2025. arXiv:2508.03961
• D. Kunisky, The discrepancy of unsatisfiable matrices and a lower bound for the Komlós conjecture constant, SIAM J. Discrete Math. 37 (2023). arXiv:2111.02974
• B. Chazelle, The Discrepancy Method, Cambridge University Press, 2000. author's page

Motivation

Matroids and their integral generalizations, integral base polytopes, are the combinatorial structures on which the greedy algorithm is exact. Edmonds' theory relates them to submodular and supermodular set functions: a polytope is a base polytope exactly when its support function, restricted to $0/1$ vectors, is supermodular and the greedy formula evaluates it everywhere. Dress and Wenzel's valuated matroids (1990) and Murota's M-concave functions carry the exchange axiom from sets to functions on sets. This paper (Adv. Math. 124, 1996) sets up the resulting theory of discrete concave functions on base sets, later developed into discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003).

The question behind this mission is how the set-level correspondence between exchange and supermodularity extends to functions. Section 5 of the paper answers it with the Local Supermodularity Theorem: the exchange property of a function is a supermodularity property of its concave conjugate, holding locally at every point.

Setting

Let $V$ be a finite nonempty set, $n=|V|$. For $u\in V$ let $\chi_u\in\mathbb Z^V$ be the unit vector, for $X\subseteq V$ let $\chi_X$ be its characteristic vector, $x(X)=\sum_{v\in X}x(v)$, and $\langle p,x\rangle=\sum_v p(v)x(v)$. For a finite $B\subseteq\mathbb Z^V$, $\overline B$ is its convex hull.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that

$$\text{(B1)}\quad x,y\in B,\ u\in\operatorname{supp}^+(x-y)\ \Rightarrow\ \exists v\in\operatorname{supp}^-(x-y):\ x-\chi_u+\chi_v\in B.$$

A function $\omega:B\to\mathbb R$ satisfies the exchange property (EXC) (is M-concave) if for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ there is $v\in\operatorname{supp}^-(x-y)$ with $x-\chi_u+\chi_v,\ y+\chi_u-\chi_v\in B$ and $\omega(x)+\omega(y)\le\omega(x-\chi_u+\chi_v)+\omega(y+\chi_u-\chi_v)$. Write $\omega[p](x)=\omega(x)+\langle p,x\rangle$ and $\operatorname{argmax}(g)$ for the maximizers of $g$ on $B$.

The support function of $B$ is $\psi^\circ(p)=\min\{\langle p,x\rangle\mid x\in B\}$. A positively homogeneous $h:\mathbb R^V\to\mathbb R$ is "matroidal" if

• (C1) $X\mapsto h(\chi_X)$ is supermodular, and
• (C2) $h(p)=\sum_{j=1}^n(p_j-p_{j+1})\,h(\chi_{V_j})$ whenever $V=\{v_1,\dots,v_n\}$ with $p(v_1)\ge\dots\ge p(v_n)$, $p_j=p(v_j)$, $V_j=\{v_1,\dots,v_j\}$, $p_{n+1}=0$.

The concave conjugate is $\omega^\circ(p)=\min\{\langle p,x\rangle-\omega(x)\mid x\in B\}$, the concave closure is $\hat\omega(b)=\inf_p\{\langle p,b\rangle-\omega^\circ(p)\}$, the subdifferential is $\partial\omega^\circ(p_0)=\{b\mid\omega^\circ(p)-\omega^\circ(p_0)\le\langle p-p_0,b\rangle\ \forall p\}$, and the localization of $\omega^\circ$ at $p_0$ is $\hat L(\omega^\circ,p_0)(p)=\inf\{\langle p,b\rangle\mid b\in\partial\omega^\circ(p_0)\}$.

Formalization targets

Goal: the Local Supermodularity Theorem (Theorem 5.3, corrected)

For $\omega$ on a finite integral base set $B$,

$$\omega\ \text{satisfies (EXC)}\iff\Big(\omega=\hat\omega\ \text{on}\ B\Big)\ \text{and}\ \Big(\hat L(\omega^\circ,p_0)\ \text{is "matroidal" for every}\ p_0\in\mathbb R^V\Big).$$

The printed Theorem 5.3 has only the second condition on the right. Its "only if" direction holds as printed; its "if" direction is false without the first condition, and a separate item of the mission states the counterexample: $B=\{(2,0),(1,1),(0,2)\}$, $\omega=(0,-10,0)$.

Milestones

1. Theorem 2.1: (B1) is equivalent to $B$ being the integer points of an integral submodular (equivalently, supermodular) system, whose defining function is determined by $B$.
2. Theorem 5.1: if $B=\mathbb Z^V\cap\overline B$, then $B$ satisfies (B1) iff $\psi^\circ$ is "matroidal".
3. Lemma 5.2: sums of "matroidal" functions are "matroidal".
4. Theorem 4.4: (EXC) holds iff every $\operatorname{argmax}(\omega[p])$ satisfies (B1).
5. Eq. (5.12): $\hat L(\omega^\circ,p_0)(p)=\min\{\langle p,x\rangle\mid x\in\operatorname{argmax}(\omega[-p_0])\}$.

Significance

The result. Theorem 5.3 is the function-level version of Theorem 5.1. Condition (C1) is a supermodularity condition, so the theorem expresses (EXC) as "a collection of local supermodularity" properties of $\omega^\circ$, in the same way that (B1) corresponds to supermodularity of a support function. In the paper this characterization of the conjugate side underlies the Fenchel-type duality of Section 6, and more generally the conjugacy between M-concave and L-convex functions in discrete convex analysis.

The formalization. No part of this theory is formalized in Lean or on this platform: base sets, (EXC), "matroidal" functions and concave conjugates of functions on base sets are all new. The mission also corrects the published statement: the reduction from localizations to base sets needs every integer point of $\operatorname{conv}(\operatorname{argmax}\,\omega[-p_0])$ to be a maximizer, and the concave-closure condition supplies this. A machine-checked proof would settle both the corrected theorem and the counterexample. Theorem 2.1 and Lemma 5.2 are classical but have no formal proof either.

Difficulty

$\omega^\circ$ depends only on the concave closure $\hat\omega$, so any characterization of (EXC) through $\omega^\circ$ alone cannot see values of $\omega$ below $\hat\omega$. That is why the goal needs the extra clause. The "only if" direction needs the full theory of Section 4: M-concave functions coincide with their concave closure, and all their maximizer sets are base sets. Theorem 5.1 needs the greedy algorithm on integral base polytopes, together with the fact that the base polytope of an integral supermodular function has integral vertices. Theorem 2.1 is the folklore statement that polyhedral and exchange descriptions agree, and the paper does not prove it. Eq. (5.12) needs the subdifferential of a finite minimum of affine functions to be the convex hull of the active gradients, stated globally rather than only near $p_0$.

Formalization scope

Integer vectors are V → ℤ, real vectors V → ℝ, with [Fintype V] [DecidableEq V] [Nonempty V]. A finite subset of $\mathbb Z^V$ is a Finset (V → ℤ). A function on $B$ is a total function (V → ℤ) → ℝ whose values off $B$ are never used. The mission commits to the following readings:

• Minima. $\psi^\circ$, $\omega^\circ$ are real infima over the finite set $B$, hence minima for nonempty $B$ (every statement has $B$ nonempty). $\hat\omega$ is a real infimum used only at points of $B$, where it is bounded below.
• Localization. $\hat L$ is a real sInf over the subdifferential, defined by (5.8)–(5.9) exactly, not by the formula (5.12). Eq. (5.12) is stated with IsLeast, so it asserts attainment, not just the value.
• (C2). It is required for every bijection Fin n ≃ V along which $p$ is non-increasing. This is equivalent to "for some" such indexing. "Matroidal" includes positive homogeneity but not concavity.
• Theorem 2.1. The page's "$\forall X\subset V$" is read as all $X\subseteq V$. The set functions are integer-valued, and "Moreover" is read strongly: every $f$ (resp. $g$) as in (b) (resp. (c)) equals the displayed max (resp. min).
• Theorem 4.4. "$\overline{\operatorname{argmax}(\omega[p])}$ is an integral base polytope" is read as "$\operatorname{argmax}(\omega[p])$ satisfies (B1)", following Lemma 4.3 and the proof of Theorem 5.3. The literal convex-hull reading makes the "if" direction false (same counterexample).
• Theorem 5.1 keeps the page's hypothesis $B=\mathbb Z^V\cap\overline B$.

Trivializing formalizations are ruled out. Defining $\hat L$ by (5.12) would reduce the goal to Theorems 4.4 and 5.1. A "matroidal" without (C2) would be satisfied by support functions of non-base sets. An $\omega^\circ$ taken as a supremum would reverse the sign conventions.

The development needs: the greedy algorithm and integrality for integral base polytopes, supergradients of polyhedral concave functions, and the Section 4 results of the paper (concave closure of M-concave functions, Lemma 4.3). The base-set and "matroidal" layers can be reused beyond this mission. Proofs of any milestone, of the counterexample, and a proof of the "only if" direction on its own are all welcome.

Selected references

• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996), 272–311. https://doi.org/10.1006/aima.1996.0084
• A. W. M. Dress, W. Wenzel, Valuated matroids: a new look at the greedy algorithm, Applied Mathematics Letters 3 (1990), 33–35.
• S. Fujishige, Submodular Functions and Optimization, 2nd ed., Annals of Discrete Mathematics 58, Elsevier, 2005.
• L. Lovász, Submodular functions and convexity, in Mathematical Programming: The State of the Art, Springer, 1983, 235–257. https://doi.org/10.1007/978-3-642-68874-4_10
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

The problem of solving linear inequalities

The linear feasibility problem takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns

$$\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset$$

has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.

What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$. In the real-number model the input is a list of $mn + m$ exact real numbers, each arithmetic operation ($+, -, \times, \div$), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$. An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every $m$, $n$, and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.

Why it matters

For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$, covering network flows and all $\{0,\pm1\}$-constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).

For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.

The question and what is known

$$\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}$$

The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).

Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.

Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of $A$ alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.

The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).

A hierarchy of formalization targets

The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.

Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:

$$\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.$$

It fixes nothing about $n \ge 2$; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.

Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of

$$2^n - 1 \text{ pivots}$$

from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.

Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$, every admissible ellipsoid run decides feasibility within

$$t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.$$

The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$.

Level 3 — the goal (open). A uniform program with data-independent polynomial cost:

$$\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.$$

The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.

Formalization scope

Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with $\{x \mid Ax \ge b\}$ as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$; both are benign for the class of programs quantified over.

The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.

Selected references

• L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers, Bull. AMS 21(1):1–46, 1989. DOI
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2):7–15, 1998. DOI
• V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, pp. 159–175.
• L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20:53–72, 1980. DOI
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4:373–395, 1984. DOI
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40:59–93, 1988. DOI
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res. 34(2):250–256, 1986. DOI
• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. DOI
• G. Kalai, A subexponential randomized simplex algorithm, STOC 1992. DOI
• O. Friedmann, T. D. Hansen, U. Zwick, Subexponential lower bounds for randomized pivoting rules for the simplex algorithm, STOC 2011. DOI
• D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. DOI
• S. A. Vavasis, Y. Ye, A primal-dual interior point method whose running time depends only on the constraint matrix, Math. Programming 74:79–120, 1996. DOI
• Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Math. Oper. Res. 36(4):593–603, 2011. DOI
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. DOI
• X. Allamigeon, S. Gaubert, N. Vandame, No self-concordant barrier interior point method is strongly polynomial, STOC 2022. arXiv
• D. Dadush, S. Huiberts, B. Natura, L. A. Végh, A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix, STOC 2020. arXiv
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the Introduction to Linear Optimization mission series).
• B. Korte, J. Vygen, Combinatorial Optimization: Theory and Algorithms, 6th ed., Springer, 2018, §4.1–4.5.

Motivation

A linear program asks for a point $x\in\mathbb{R}^d$ minimizing $c^Tx$ subject to $n$ linear inequalities $\sum_{j=1}^d a_{ij}x_j\ge b_i$. Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev ($L_\infty$) norm, finding the smallest disk or ball containing a point set (a related convex problem). For these problems the number of variables $d$ is a small constant, and what matters is how the running time grows with $n$.

Nimrod Megiddo showed that for every fixed $d$ the problem can be solved in time $C(d)\cdot n$ (J. ACM 31(1), 1984).

Timeline.

• 1983. Megiddo (SIAM J. Comput. 12) and, independently, Dyer (SIAM J. Comput. 13 (1984)) give linear-time algorithms for $d=2$ and $d=3$.
• 1984. Megiddo extends the method to every fixed $d$, with $C(d)<2^{2^{d+2}}$ (the paper formalized here).
• 1988–1991. Clarkson (J. ACM 42 (1995), conference version 1988) gives a randomized algorithm with expected time $O(d^2n)+d^{O(\sqrt d)}\log n$. Seidel (Discrete Comput. Geom. 6 (1991)) gives a simple randomized $O(d!\,n)$ algorithm.
• 1992–1996. Matoušek, Sharir and Welzl and, independently, Kalai give subexponential randomized bounds. Chazelle and Matoušek derandomize the linear dependence with $C(d)=d^{O(d)}$ (J. Algorithms 21 (1996)).

Setting

Fix $d$. An instance is a matrix $A\in\mathbb{R}^{n\times d}$ and a vector $b\in\mathbb{R}^n$, and its feasible region is the polyhedron $P(A,b)=\{x\in\mathbb{R}^d: Ax\ge b\}$. Here $n$ is the number of constraints and $d$ the number of variables.

The model of computation is the real RAM. A program is a finite list of instructions acting on real registers, integer pointer registers and a memory $\mathbb{Z}\to\mathbb{R}$. It performs exact $+,-,\times,/$ on reals at unit cost, tests the sign of a real, sets, copies, increments, decrements and compares pointers, and loads and stores through pointers. The input is the standard encoding of $(A,b)$ in memory: the numbers $n$ and $d$, then $A$ row by row, then $b$. A program decides an instance within $T$ steps with output $\beta\in\{\text{accept},\text{reject}\}$ if it halts on that output after at most $T$ steps.

Megiddo's method rests on multidimensional search. There is an unknown point $x^*\in\mathbb{R}^d$ and an oracle that, for any hyperplane $\{x: a^Tx=b\}$, answers whether $a^Tx^*<b$, $=b$ or $>b$. Given hyperplanes $H_i=\{a_i^Tx=b_i\}$ with $a_i\ne0$, the question is how many oracle calls determine the position of $x^*$ relative to all of them. A search strategy is a ternary decision tree: inner nodes are hyperplane queries, leaves carry outputs, and the tree is built from the data alone. For linear programming, $x^*$ is an optimal solution, or a minimizer of the infeasibility function $f(x)=\max_i(b_i-a_i^Tx)$ when the system is infeasible. The oracle is implemented by solving problems in $d-1$ variables.

Formalization targets

Goal: linear-time feasibility on the real RAM

$$\forall d\ \exists R\ \exists C\ \forall n\ \forall A\in\mathbb{R}^{n\times d},\,b\in\mathbb{R}^n:\quad R\text{ decides within }C\,(n+1)\text{ steps whether } \{x: Ax\ge b\}\neq\emptyset.$$

The program and the constant depend on $d$ only. No explicit form of $C(d)$ is fixed.

Milestones

1. One query settles half of $n$ hyperplanes on the line ($A(1)=1$, $B(1)=\tfrac12$).
2. $v(\epsilon)=(1,\epsilon,\dots,\epsilon^{d-1})$ is orthogonal to some $a_i$ for at most $n(d-1)$ values of $\epsilon$, so there is a basis in which all $a_{ij}\ne0$.
3. For hyperplanes of opposite slopes in the $(x_1,x_2)$ plane, the answers for $H^{(1)}_{ik}$ and $H^{(2)}_{ik}$ settle one of $H_i$, $H_k$.
4. A linearly dependent pair of opposite slopes has $a_{i1}=a_{k1}=0$, and the middle hyperplane settles one of them.
5. Approach I: $2^{d-1}$ queries settle at least $\lfloor 2^{1-2^d}n\rfloor$ hyperplanes.
6. $C(d)\log n$ queries settle all $n$ hyperplanes.
7. If a hyperplane contains no optimal point, all optimal points lie on one side of it.
8. The oracle, Case I: at an optimum relative to $\{x_d=0\}$, two auxiliary systems decide the side or certify global optimality.
9. The oracle, Case II: at a minimizer of $f$ on $\{x_d=0\}$, systems (1) and (2) decide the side or certify infeasibility.

Significance

The result. For every fixed dimension, linear programming is solvable in time linear in the number of constraints. The algorithm is also strongly polynomial in fixed dimension: its operation count does not depend on the bit size of the data. Deciding whether the optimum is at most $t$ is feasibility of $Ax\ge b$ together with $-c^Tx\ge-t$, so the goal also covers the decision form of optimization. The prune-and-search technique of the paper, which discards a constant fraction of the constraints per round, became a standard tool of computational geometry.

Formalizing it. The result is proved and classical. The platform already has the cases $d=1$ (linear time) and $d=2$ (quadratic time, by Fourier–Motzkin elimination) on the same machine and input encoding (SmaleNinth.real_ram_decides_one_variable_lp_linear, SmaleNinth.real_ram_decides_two_variable_lp_quadratic). No machine-checked proof of the general statement is known. The work consists of the query-complexity layer (milestones 1–6), the convex-analytic correctness of the oracle (milestones 7–9), and a real-RAM implementation with a step count linear in $n$, including linear-time median selection. Alternative proofs, for example through Clarkson's or Seidel's algorithms made deterministic, are welcome for the goal.

Difficulty

The obvious approach is to find the optimum by testing constraints one by one or by eliminating variables. Fourier–Motzkin elimination produces $\Theta(n^2)$ constraints after one step. Pivoting methods have no known bound linear in $n$. The key difficulty is to discard a constant fraction of the constraints using only a constant number of recursive calls in dimension $d-1$, when no single hyperplane test gives information about more than one constraint. The multidimensional search layer gives this, and it is where the pairing of hyperplanes by slope and the degenerate cases (dependent pairs, zero coefficients) have to be handled exactly. At the machine level, the step count must stay linear in $n$ for a fixed program, so every median selection and every recursive call must be implemented within the budget, with the recursion depth depending on $d$ only.

Formalization scope

• Machine and input. The machine is the platform's real RAM SmaleNinth.RAMProgram with RAMDecidesInTime, and the input convention is SmaleNinth.encodeLP (published definitions, reused unchanged). No instruction is added: there is no LP, median, floor or sort primitive. Time is the number of machine steps.
• Quantifier order. $\forall d\ \exists R\ \exists C\ \forall n, A, b$. The bound is $C(n+1)$ in the number $n$ of constraints, so that the machine can halt at $n=0$. The paper's $C(d)<2^{2^{d+2}}$ counts unspecified units of "effort" with an unquantified $\theta(nd)$ term, and it is not transferred to machine steps. Where a milestone's proof fixes a constant exactly, the constant is stated: $2^{d-1}$ queries and $\lfloor n/2^{2^d-1}\rfloor$ settled hyperplanes in milestone 5.
• Feasibility only. The machine outputs accept or reject. Returning an optimizer, "unbounded", or a minimizer of $f$ is not part of the goal. The case $d=0$ is included.
• Query trees. Nodes are queries compare (a ⬝ᵥ x) b and nothing else, leaves hold fixed values, and correctness is required for every $x$. A tree over arbitrary tests of $x$ would make milestones 5 and 6 empty, and it is excluded by the definition.
• Indices. The paper's $x_1,x_2$ are indices 0, 1 of Fin (d + 2), and its $x_d$ is Fin.last d of Fin (d + 1).
• Corrections. Two passages of §4 are stated in corrected form. The Case I auxiliary objective includes the $\pm c_d$ term of the direction. In Case II, feasibility of (1) puts improvement in $\{x_d>0\}$, where the page's last sentence says $\{x_d<0\}$. The pairing claim carries $a_{k1}a_{i2}-a_{k2}a_{i1}\ne0$, the hypothesis its argument uses, since linear independence alone does not give it.
• Not included. Approach II and its bound $O(n(\log n)^{d^2})$, the remarks on slowly growing $d$, the randomized variants, and the applications of §1.
• Reusable parts. The query-tree definition and milestones 1–6 apply to any prune-and-search problem with a hyperplane oracle. The oracle lemmas (7–9) are statements about convex piecewise-linear functions and polyhedra.

Selected references

• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. https://doi.org/10.1145/2422.322418
• N. Megiddo, Linear-time algorithms for linear programming in $R^3$ and related problems, SIAM J. Comput. 12(4):759–776, 1983. https://doi.org/10.1137/0212052
• M. E. Dyer, Linear time algorithms for two- and three-variable linear programs, SIAM J. Comput. 13(1):31–45, 1984. https://doi.org/10.1137/0213003
• K. L. Clarkson, Las Vegas algorithms for linear and integer programming when the dimension is small, J. ACM 42(2):488–499, 1995. https://doi.org/10.1145/201019.201036
• R. Seidel, Small-dimensional linear programming and convex hulls made easy, Discrete Comput. Geom. 6:423–434, 1991. https://doi.org/10.1007/BF02574699
• B. Chazelle, J. Matoušek, On linear-time deterministic algorithms for optimization problems in fixed dimension, J. Algorithms 21(3):579–597, 1996. https://doi.org/10.1006/jagm.1996.0046

Motivation

Many engineering and economic planning problems must meet random requirements with a prescribed reliability: a reservoir must satisfy demand with probability at least $0.95$, a power system must cover load except on rare days, an inventory must avoid shortage with high probability. Probabilistic constrained programming (also called chance-constrained programming) models this by requiring that a system of random inequalities hold jointly with probability at least $p$.

The first obstacle to solving such problems is structural. The probability that random constraints are satisfied is, in general, neither concave nor convex in the decision, so the feasible set need not be convex and local search can stall. Prékopa's theory of logarithmically concave measures (1971–1973) removed that obstacle for a large class of distributions, and it is the basis of the numerical methods of Chapter 5 of Ermoliev and Wets, Numerical Techniques for Stochastic Optimization (Springer 1988). This mission formalizes the structural theorems of that chapter.

Timeline:

• 1959: Charnes and Cooper, individual chance constraints.
• 1971: Prékopa, logarithmic concave measures with application to stochastic programming (Acta Sci. Math. Szeged 32).
• 1973: Prékopa, logarithmic concave measures and functions (Acta Sci. Math. Szeged 34), containing the marginal theorem: marginals of log-concave functions are log-concave.
• 1970s–1980s: nonlinear programming methods for (5.1) (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) combined with Monte Carlo evaluation of $h_0$; the chapter surveys them.

Setting

Let $\xi$ be a random vector in $\mathbb R^q$ on a probability space $(\Omega, \mathcal F, P)$ and let $g_1, \dots, g_r : \mathbb R^n \times \mathbb R^q \to \mathbb R$. The chapter studies problem (5.1):

$$\min h(x) \quad \text{s.t.} \quad h_0(x) = P\bigl(g_1(x,\xi) \ge 0, \dots, g_r(x,\xi) \ge 0\bigr) \ge p, \quad h_1(x) \ge p_1, \dots, h_m(x) \ge p_m .$$

The function $h_0$ is the probability function (chanceProb in Lean). In the special case $g_i(x,y) = T_i x - y_i$ it equals $F(Tx)$, where $F$ is the joint distribution function of $\xi$.

A function $f \ge 0$ is logarithmically concave on a convex set $S$ if

$$f(\lambda u + (1-\lambda) v) \ge f(u)^{\lambda} f(v)^{1-\lambda}, \qquad u, v \in S,\ 0 < \lambda < 1 .$$

Where $f > 0$ this is concavity of $\log f$; the power form also makes sense where $f = 0$. Nondegenerate normal densities, uniform densities on convex bodies and exponential densities are log-concave.

Section 5.7 introduces the polynomial distribution (5.19) on the cube $0 < z_j \le 1$:

$$F(z_1, \dots, z_n) = \frac{1}{\sum_{i=1}^{N} c_i z_1^{\alpha_{i1}} \cdots z_n^{\alpha_{in}}}, \qquad c_i > 0,\ \alpha_{ij} \le 0,\ \textstyle\sum_j \alpha_{ij} < 0$$

(polyDistF in Lean).

Formalization targets

Goal: Theorem 5.1

If $g_1, \dots, g_r$ are jointly concave on $\mathbb R^{n+q}$ and $\xi$ has a log-concave density $f$ on $\mathbb R^q$, then

$$h_0 \text{ is logarithmically concave on } \mathbb R^n .$$

Its immediate consequence is that the feasible set $\{x : h_0(x) \ge p\}$ is convex for every $p$.

Milestones

1. Theorem 5.2.1: if $h$ is log-concave on the convex set $H = \{h \ge p\}$, $0 < p < 1$, then $h - p$ is log-concave on $H$. This makes the logarithmic penalty function (5.5) of the SUMT method convex.
2. Theorem 5.2.2: under the standing assumptions of §5.2, every interior point $z$ of the feasible set of (5.1) satisfies $h_i(z) > p_i$, $i = 0, \dots, m$.
3. Theorem 5.7.1 (proved content, (5.21)): for $n = 2$ and oppositely ordered exponents, $\partial^2 F / \partial z_1 \partial z_2 \ge 0$ on $(0,1)^2$.
4. Theorem 5.7.2: the polynomial distribution function is log-concave on $(0,1]^n$.

The platform theorem ConvexOptimization.prekopa_marginal_log_concave (Prékopa's marginal theorem, proved) is included as a reference item.

Significance

Theorem 5.1 turns a probabilistic constraint into a convex constraint after taking logarithms. This is what makes convergence proofs for nonlinear programming methods (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) applicable to (5.1) and to the reliability maximization problem (5.4); without it, those methods have no guarantee of finding a global optimum. Theorems 5.2.1 and 5.2.2 are the two facts that make the SUMT method of §5.2 well defined and convex on the interior of the feasible set. Theorem 5.7.2 shows that probabilistic constraints under the polynomial distribution define convex sets, so they can be added to geometric programmes.

On status: Theorem 5.1 is a classical result, proved in Prékopa's papers (the chapter itself refers to Prékopa's survey for the proof). Prékopa's marginal theorem and the Prékopa–Leindler inequality are already machine-checked on this platform; Theorem 5.1 and the §5.2 and §5.7 theorems are, as far as a search of the platform shows, not formalized. The work is formalizing known proofs, in the log-concavity predicate the platform already uses.

Difficulty

The obvious argument for Theorem 5.1, "the constraint set is convex and the density is log-concave, so the probability is log-concave", hides the real content: log-concavity of a probability as a function of a parameter is a statement about integrals, and it does not follow from pointwise properties of the integrand without a Prékopa–Leindler-type inequality. Concavity of each $g_i$ separately in $x$ and in $y$ is not enough; joint concavity in $(x, y)$ is used essentially. The probability function vanishes on large regions in typical examples, so any argument that takes logarithms pointwise fails at the boundary of its support.

For Theorem 5.2.2 the naive argument fails at the index $i = 0$: nothing about $h_0$ is assumed directly, and log-concavity of $h_0$ is exactly Theorem 5.1. For Theorem 5.7.1 the difficulty is a sign condition on a covariance; without the ordering hypothesis the mixed derivative can be negative.

Formalization scope

$\mathbb R^n$ and $\mathbb R^q$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin q); the constraint functions take pairs $(x, y)$ in the product, and concavity is ConcaveOn ℝ Set.univ on that product (joint concavity). A "continuous probability distribution with density $f$" is stated as P.map ξ = volume.withDensity (ENNReal.ofReal ∘ f) with $\xi$ and $f$ measurable and $P$ a probability measure. Log-concavity is the platform definition ConvexOptimization.LogConcaveOn (nonnegativity plus the power inequality), imported as a reference item; concavity of Real.log ∘ h₀ would be a different, wrong property because Lean's Real.log 0 = 0. Indices are 0-based (Fin r, Fin m, Fin N, Fin n); the probabilistic constraint $i = 0$ of Theorem 5.2.2 is stated separately from $h_1, \dots, h_m$. The polynomial distribution is a formula on Fin n → ℝ with real powers, used only on the cube.

No constant of the book is replaced by an explicit value: every result of this chapter is qualitative.

Corrections of the printed text, recorded in each item's Formalization Note:

• Theorem 5.1 states the density condition "for every $x_1, x_2 \in \mathbb R^n$"; the density lives on $\mathbb R^q$ and the condition is imposed there.
• (5.19) prints the first factor as $z_i^{\alpha_{i1}}$ and the domain index as $i = 1, \dots, N$; they are read as $z_1^{\alpha_{i1}}$ and $j = 1, \dots, n$.
• Theorem 5.7.1 prints its ordering hypothesis with transposed indices ($\alpha_{11} \le \alpha_{12} \le \dots \le \alpha_{1n}$); following the proof, it is read as: across the $N$ terms the $z_1$-exponents increase and the $z_2$-exponents decrease.
• Theorem 5.7.1 claims "is a probability distribution function"; the book proves only (5.21), and normalization would need $\sum_i c_i = 1$, which is not assumed. The formal statement is (5.21), the mixed derivative as an iterated deriv.

Theorem 5.2.2 carries all six assumptions of §5.2, including compactness of the feasible set and the Slater point; it does not assume log-concavity of $h_0$, which must be derived from the density and concavity hypotheses. A trivializing formalization, such as one with a density hypothesis that no probability law satisfies or a log-concavity predicate that holds for every function vanishing somewhere, is ruled out: the density hypotheses are satisfiable (checked locally) and LogConcaveOn is the multiplicative inequality at every pair of points.

Needed infrastructure: Prékopa's marginal theorem (available), log-concavity of indicators of convex sets and of products, measurability of the constraint set, and Artin's theorem that a sum of log-convex functions is log-convex (for Theorem 5.7.2). Artin's theorem and closure properties of LogConcaveOn are reusable beyond this mission, and contributions of them are welcome.

Selected references

• A. Prékopa, "Numerical Solution of Probabilistic Constrained Programming Problems", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 5, pp. 123–139. https://doi.org/10.1007/978-3-642-61370-8
• A. Prékopa, "Logarithmic concave measures with application to stochastic programming", Acta Sci. Math. (Szeged) 32 (1971), 301–316.
• A. Prékopa, "On logarithmic concave measures and functions", Acta Sci. Math. (Szeged) 34 (1973), 335–343.
• A. Charnes and W. W. Cooper, "Chance-constrained programming", Management Science 6 (1959), 73–79. https://doi.org/10.1287/mnsc.6.1.73
• B. L. Miller and H. M. Wagner, "Chance constrained programming with joint constraints", Operations Research 13 (1965), 930–945. https://doi.org/10.1287/opre.13.6.930
• A. Prékopa, Stochastic Programming, Kluwer 1995. https://doi.org/10.1007/978-94-017-3087-7

Motivation

Many design problems in control, finance and operations research are convex programs with uncertain constraints: a decision $\theta$ must satisfy $\theta\in\Theta_\delta$ for a parameter $\delta$ that is not known in advance. Enforcing the constraint for every possible $\delta$ (robust optimization) is often intractable or too conservative, and a chance-constrained formulation needs the distribution of $\delta$, which in practice is rarely known. The scenario approach replaces the uncertain constraint by the constraints of $N$ observed samples $\delta_1,\dots,\delta_N$ and solves the resulting ordinary convex program. The question it answers is how much of the unseen uncertainty the resulting decision still violates.

The answer, the generalization theorem of the scenario approach, is distribution-free: the probability that the scenario solution violates more than a fraction $\varepsilon$ of the uncertainty is bounded by a binomial tail that depends only on $N$ and on the number $d$ of decision variables. This mission formalizes that theorem as it is presented in Chapters 3 and 5 of Campi and Garatti's textbook Introduction to the Scenario Approach (SIAM/MOS 2018), the first mission of a series on the book.

Timeline. Calafiore and Campi introduced scenario programs and bounded the violation of their solutions through the count of support constraints (Math. Program. 2005; IEEE TAC 2006). Campi and Garatti proved in 2008 that the binomial-tail bound of Theorem 3.7 holds for every convex scenario program under existence and uniqueness of the solution, and that it is attained with equality by fully supported problems (SIAM J. Optim. 2008), which settled the tightness question. The textbook (DOI 10.1137/1.9781611975444) presents the theorem with a complete proof for fully supported problems in the plane.

Setting

Fix a cost vector $c\in\mathbb R^d$, a domain $\Theta\subseteq\mathbb R^d$, a measurable space $\Delta$ of uncertainty instances with a probability $\mathbb P$, and a constraint set $\Theta_\delta\subseteq\mathbb R^d$ for each $\delta\in\Delta$.

• The violation of a decision $\theta$ (Definition 3.1) is $V(\theta)=\mathbb P\{\delta\in\Delta:\theta\notin\Theta_\delta\}$, the probability that $\theta$ fails the constraint of a fresh instance.
• For a sample $(\delta_1,\dots,\delta_m)$, the scenario program is

$$\min_{\theta\in\Theta}c^T\theta\quad\text{subject to}\quad\theta\in\bigcap_{i=1}^{m}\Theta_{\delta_i}.$$

A solution is a feasible point of least cost. With $m=N$ i.i.d. samples its solution is denoted $\theta^*$; it is a random vector, a function of the sample, and $V(\theta^*)$ is a random variable in $[0,1]$.

• Assumption 3.4 (convexity): $\Theta$ and every $\Theta_\delta$ are convex and closed. Assumption 3.6 (existence and uniqueness): for every $m$ and every sample, the program with $m$ constraints has exactly one solution.
• A constraint is a support constraint (Definition 5.1) if its removal improves the solution. A problem is fully supported (Definition 5.4) if for every $m\ge d$ the program with $m$ constraints has, with probability 1, exactly $d$ support constraints.

Formalization targets

Goal: Theorem 3.7

For $1\le d\le N$ and every $\varepsilon\in[0,1]$, under Assumptions 3.4 and 3.6,

$$\mathbb P^N\{V(\theta^*)>\varepsilon\}\le\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}.$$

The right-hand side is the upper tail of a Beta$(d,N-d+1)$ distribution. The statement leaves $\mathbb P$, $\Theta$ and the constraint family completely unspecified beyond the two assumptions.

Milestones

1. Helly's lemma (Lemma 5.3), referenced from the platform in its $d$-dimensional form.
2. Theorem 5.2: for every $m$ and every sample, a convex scenario program has at most $d$ support constraints.
3. Eq. (5.3): for a fully supported problem with $d=N=2$, $\mathbb P^2\{V(\theta^*)>\varepsilon\}=1-\varepsilon^2$.
4. Eq. (5.2): for fully supported problems, Theorem 3.7 holds with equality.
5. Eqs. (3.5)–(3.6): the bound is the Beta$(d,N-d+1)$ distribution function (a published incomplete-beta identity).
6. Eq. (3.9): $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}\le 2^{d-1}(1-\varepsilon/2)^N\le2^{d-1}e^{-\varepsilon N/2}$.
7. Theorem 3.8: $\mathbb E[V(\theta^*)]\le d/(N+1)$.
8. Theorem 1.3: if $N\ge\frac2\varepsilon(\ln\frac1\beta+d-1)$, then $V(\theta^*)\le\varepsilon$ with probability at least $1-\beta$.

Significance

Theorem 3.7 is what makes the scenario approach usable as a design method: it certifies the reliability of a decision computed from data without any knowledge of the data-generating distribution, requiring only independence of the samples. Theorems 3.8 and 1.3 are its two most used consequences, an expected-violation bound and an explicit sample size, and later chapters of the book (constraint removal, the FAST algorithm, empirical-cost results) build on the same statement. Equality for fully supported problems shows that the bound cannot be improved for any $d$ and $N$.

The theorem is proved in the literature; it has no machine-checked proof. A formalization produces, beyond the result itself, a reusable library of scenario programs, violation probabilities and support constraints on which the rest of the series (constraint removal, nonconvex support sets) can be stated, and it checks the measure-theoretic content that the book deliberately leaves aside ("measurability issues are glossed over throughout", p. 33).

Difficulty

The deterministic part, at most $d$ support constraints, is a short consequence of Helly's theorem. The probabilistic part is where the obvious approach fails. A uniform-convergence argument over all $\theta$ (Vapnik–Chervonenkis theory, footnote 11 of the book) gives bounds of the wrong order and can be vacuous, because it ignores that only the solution matters. The sharp bound is an exact statement about the law of $V(\theta^*)$, not a union bound, and problems with fewer than $d$ support constraints, or with degenerate configurations of constraints, must be shown to be no worse than fully supported ones; the book treats the general case only in the plane and refers to Campi & Garatti 2008 for general $d$. Handling the null sets and the exchangeability of the samples under the product measure is a substantial part of the work.

Formalization scope

• Decisions live in EuclideanSpace ℝ (Fin d); the cost is inner ℝ c θ. A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ : Fin m => P), and P is a probability measure.
• The violation is the real number (P {δ | θ ∉ Θδ δ}).toReal; probabilities of events over the sample are compared in $[0,\infty]$ through ENNReal.ofReal.
• The solution $\theta^*$ is a function θstar : (Fin N → Δ) → EuclideanSpace ℝ (Fin d) together with the hypothesis that θstar ω solves the program for every sample; it is never an arbitrary map.
• Assumption 3.6 is stated for every $m$ including $m=0$ (a unique minimizer on $\Theta$ itself) and for every sample, as on the page.
• Hypotheses the page leaves implicit are explicit: the constraint relation $\{(\theta,\delta):\theta\in\Theta_\delta\}$ is jointly measurable and θstar is measurable (the book's p. 33 convention); $\varepsilon\in[0,1]$; $d\ge1$.
• A support constraint is one whose removal leaves a feasible point of strictly smaller cost than the solution; the count is a Finset.card over Fin m.
• Theorem 3.8 asserts integrability of $V(\theta^*)$ together with the bound, so it cannot hold through the convention that a non-integrable function integrates to $0$. Theorem 1.3's own sentence omits the assumptions; they are added as in §3.2.1, where it is derived from Theorem 3.7.

A statement in which $\theta^*$ is any feasible point of the program, or merely a measurable function of the sample, is false and does not count as a formalization of Theorem 3.7; nor does one in which Assumption 3.6 is weakened to almost every sample. Contributions of general infrastructure are welcome: exchangeability arguments for product measures, the binomial–beta identity, and Helly-type counting lemmas are reusable well beyond this mission.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 2008. https://doi.org/10.1137/07069821X
• G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102, 2005. https://doi.org/10.1007/s10107-003-0499-y
• G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 2006. https://doi.org/10.1109/TAC.2006.875041
• E. Helly, Über Mengen konvexer Körper mit gemeinschaftlichen Punkten, Jahresbericht der DMV 32, 1923.

Motivation

A discrete function defined only on the integer lattice cannot, by itself, be minimized by the tools of continuous optimization — gradients and convexity in the classical sense simply do not apply. Murota's theory of M-convex functions closes this gap by showing that the exchange axiom alone, a purely combinatorial condition, is enough to guarantee that a discrete function behaves exactly like a convex one: its minimizers form a well-structured (M-convex) set, it can be extended to a genuine convex function on real space without gaining any new local minima, and its behavior under a change of price vector (in the economic interpretation where the function is a cost and its argument a bundle of goods) satisfies the same gross substitutes law economists have studied since Kelso and Crawford's matching-market models. This mission develops the second half of that connection: from local optimality (established in the companion mission) to the full structural picture — minimizer sets, price-substitution laws, and the extension of M-convex functions to genuine convex functions in real variables.

Companion mission 06-mconvex-functions-i (Discrete Convex Analysis V) and sibling mission 22-ch06b-mconvexfunctions (Discrete Convex Analysis XXI) cover this chapter's optimality theory (the M-optimality criterion, the exchange axiom as sequential improvement) and its algebraic toolkit (domain operations, worked examples). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results on minimizer structure, gross substitutability, and convex extension that this chapter's remaining sections develop: the M-convexity of minimizer sets, the gross substitutes and stepwise gross substitutes properties and their characterizing role, a minimizer-cut theorem with scaling, integral convexity of M♮-convex functions, and — this mission's goal — the theorem characterizing M-convexity entirely through the polyhedral structure of a function's convex extension.

Setting

Fix a finite ground set $V$. For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain, write $f[p](x) = f(x) - \langle p,x \rangle$ for the linear reweighting by $p \in \mathbb R^V$, and $\arg\min g = \{x : g(x) \le g(y)\ \forall y\}$ for the minimizer set of any function $g$. The convex closure $\bar f(x)$ of $f$ at a real point $x$ is the infimum, over finite convex combinations of points of $\operatorname{dom} f$ representing $x$, of the corresponding combination of function values; $f$ is convex extensible if $\bar f$ agrees with $f$ on $\mathbb Z^V$, and integrally convex if $\bar f(x)$ can always be computed using only points from $x$'s own integral neighborhood $N(x)$ (the integer vectors within one unit of $x$ in every coordinate). 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 for every $\alpha \in [0,\alpha_0]$.

Formalization targets

Goal: convex extensibility characterizes M-convexity

For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain,

$$f \text{ is M-convex} \iff \bigl(f \text{ is convex extensible}\bigr) \wedge \bigl(\forall p \in \mathbb R^V,\ \arg\min \bar f[-p] \text{ is an M-convex polyhedron, if nonempty}\bigr),$$

with the M♮-analogue using M♮-convex polyhedra (Theorem 6.43). This is the weakest stable form: it characterizes M-convexity purely by properties of the (unique) convex closure, without reference to any specific algorithm for computing it or any bound on the polyhedron's complexity.

Supporting structural targets

Ten further results build the toolkit this goal draws on and the picture it completes: the M-convexity of minimizer sets (Proposition 6.29), the gross substitutes and stepwise gross substitutes properties and the theorems showing they characterize M-convexity and M♮-convexity among convex-extensible functions (Propositions 6.32-6.33, 6.35, Theorems 6.34, 6.36), a minimizer-cut theorem with scaling used algorithmically in Chapter 10 (Theorem 6.39), integral convexity of M♮-convex functions (Theorem 6.42), a shared-coefficient convex-combination theorem for pairs of M♮-convex functions used in Chapter 8's separation theorem (Theorem 6.44), and the polyhedral-M-convexity of an M-convex function's convex extension together with the correspondence between polyhedral M♮-convexity and the real exchange axiom (Theorems 6.45, 6.47).

Significance

Theorem 6.43 is what makes the whole edifice of M-convex function theory a genuine extension of M-convex set theory (chapters 4-5) rather than a separate parallel development: it says that knowing a function's convex extension is polyhedral, with every price-weighted minimizer set an M-convex polyhedron, is not merely a consequence of M-convexity but an exact characterization of it. This is the theorem that lets later results (the discrete conjugacy theorem of Chapter 8, the separation theorems for M♮-convex functions) move freely between the discrete and continuous pictures. The gross substitutes property (Propositions 6.32-6.36) is independently significant outside this book: it is the exact condition, discovered independently in mathematical economics (Kelso-Crawford, Gul-Stacchetti), under which competitive equilibria with indivisible goods are guaranteed to exist — Murota's theorem that gross substitutability characterizes M-convexity (among convex-extensible functions) is what unifies the economic and combinatorial literatures on this question, taken up again in Chapter 11.

None of these results are open — they are Murota's systematic account of a theory with roots in matroid theory, submodular optimization, and mathematical economics. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (MExchangeAxiom, ConvexClosureVal, ArgMinOn) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The forward direction of Theorem 6.43 (M-convex $\implies$ convex extensible with polyhedral minimizers) is comparatively direct given Theorem 6.42 and Proposition 6.29. The converse is substantial: it must show that a function whose weighted minimizer sets are all M-convex polyhedra — a purely global, polyhedral condition — satisfies the local exchange axiom (M-EXCloc[Z]), and the book's proof does this by an edge-direction argument on the polyhedron $B = \arg\min f$: every edge of an M-convex polyhedron must be parallel to some $\chi_u - \chi_v$, a fact borrowed from the combinatorial structure of chapter 4's base polyhedra applied to a carefully perturbed weight vector. No shortcut through convex analysis alone succeeds, because ordinary polyhedral theory says nothing about which combinatorial directions a polyhedron's edges must follow — that content comes entirely from the M-convexity of the minimizer sets, not from convexity of the closure by itself.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; functions are (V→ℤ)→WithTop ℝ (integer domain) or (V→ℝ)→WithTop ℝ (real domain, for the polyhedral theorems). The convex closure is built directly from finite convex-combination representations rather than an abstract closure operator, and integral convexity compares it against the same construction restricted to each point's integral neighborhood (Fintype.piFinset of per-coordinate Finset.Icc). Real M-convex/M♮-convex polyhedra are defined as convex hulls of M-convex/M♮-convex integer sets, reusing chapters 4-5's own characterization. The real-variable exchange axioms (Theorems 6.45, 6.47) are formalized from the book's primal (interval-of-$\alpha$) definition, not the directional-derivative reformulation (M-EXC'[R]); Theorem 6.47's own three-way equivalence is correspondingly stated with only its first two legs (see Difficulty and MODERATION_NOTES.md/HARD.md — this is a documented scope choice, not a trivializing omission, since the six results using the primal axiom already exercise the chapter's real- variable machinery in full). No numeric constants are hard-coded anywhere in this mission beyond the book's own literal coefficients in Theorem 6.39's cut bound ((n-1)(α-1)). This mission's definitions are redeclared from chunks 06-mconvex-functions-i and 22-ch06b-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's converse direction and Theorem 6.44's shared-coefficient construction carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• A. S. Kelso Jr. and V. P. Crawford, "Job matching, coalition formation, and gross substitutes," Econometrica, 50 (1982), pp. 1483-1504.
• F. Gul and E. Stacchetti, "Walrasian equilibrium with gross substitutes," Journal of Economic Theory, 87 (1999), pp. 95-124.