Closed — negative resolution of Erdős Problems 96 and 97

Adam McKenna closed this mission on 13 September 2026 following Unit distances in convex polygons, by Liam Kruer, Jensen Kohlmeyer, and Liam Price. Their construction gives strictly convex point sets with Ω(n log log n) unit-distance pairs and arbitrarily large minimum unit-distance degree, answering both questions and the general fixed-k version of Problem 97 negatively.

Paper and complete Lean source. All credit for the counterexample and its formalization belongs to those authors. Adam McKenna prepared the Prove2Me adapters.

Do not start further proof attempts or solver runs for the affirmative conjectures. Existing statements, conditional lemmas, partial proofs, and milestones remain as historical work. The owner has authorized closure assuming the external result is correct; individual theorem pages report Prove2Me verification status.

---

Historical mission description

Motivation

The mission is to prove the combined open goal

$$\text{Problem 97} \;\land\; \text{Problem 96}$$

for finite point sets in strictly convex position in the Euclidean plane.

Why Problems 97 and 96 belong together

Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every nonempty convex-independent finite set then has a vertex with at most three neighbors at each positive radius, in particular at radius $1$. Delete that vertex and preserve convex independence. Apply the same step to every subset created by deletion until no points remain. Charge each unordered unit-distance pair to the first endpoint deleted. Each deleted vertex receives at most three charges, so an $n$-point set determines at most $3n$ unordered unit-distance pairs. This gives the Problem 96 bound and therefore $O(n)$. The package uses this one-way dependency; it does not seek a reverse implication.

Setting

Let $A\subset\mathbb R^2$ be finite. Strict convex position means that every point of $A$ is an extreme point of the convex hull of $A$. For $p\in A$, the pinned multiplicity at radius $r>0$ counts points $q\in A$ with $\lVert p-q\rVert=r$. Problem 97 asks for a point where no radius has four such other points. Problem 96 counts unordered pairs at distance $1$, then takes the supremum over convex-independent $n$-point sets.

The historical progression is part of the setting. Erdős’s 1946 paper posed an earlier three-neighbor version. His 1987 account reports Danzer’s convex nonagon in which every vertex has three equidistant witnesses, and asks about four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex configuration with the same unit distance at every vertex, placing the local question beside the unit-distance problem.

Target

The Problem 97 target is the canonical statement that every nonempty finite convex-independent $A$ has no four-equidistant-point property:

$$\forall A,\quad A\ne\varnothing\;\to\;\operatorname{ConvexIndep}(A) \;\to\;\neg\operatorname{HasNEquidistantProperty}(4,A).$$

The Problem 96 target is the canonical asymptotic statement

$$U_c(n)=O(n),$$

where $U_c(n)$ is the supremum of the unordered unit-distance counts determined by convex-independent $n$-point sets. The bound is asymptotic; the Problem 97 route would give the stronger explicit bound $U_c(n)\le3n$ for every natural number $n$.

Significance

The package records a formal proof route joining a pinned geometric obstruction to a global extremal bound. A successful Problem 97 proof would immediately settle Problem 96 with the explicit constant $3$, while preserving the combinatorial meaning of the count. It also separates the historical three-neighbor constructions from the still-open four-neighbor assertion.

Difficulty

The source proof reduces Problem 97 to strong induction on $|A|$. Its counting engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib (2013). This engine forces every counterexample to have at least nine points; a finite geometric analysis excludes exactly nine points; and the remaining step must produce a removable vertex for every larger minimal counterexample. The removable-vertex statement carries the induction hypothesis that every strictly smaller nonempty convex 4-equidistant set is contradictory. That large-cardinality geometric step remains open, so both headline targets remain open. Finite computational certificates can support local cases but do not replace the universal geometric statement.

Counterexample routes

Problem 97 is open, so the mission also records the parallel negative route. The source formalization calls a nonempty convex-independent finite set with the four-equidistant property a Problem97.IsCounterexample. Constructing one such set would refute Problem 97 and therefore refute the mission's affirmative conjunction, regardless of whether Problem 96 remains true. The counterexample milestone keeps this resolution path visible beside the nonexistence proof. A successful witness must use exact coordinates or exact algebraic data from which Lean verifies both strict convex position and the four-equidistant property; a numerical approximation or a realizable incidence pattern alone is insufficient.

Problem 96 has its own negative route. Because its claim is asymptotic, one finite convex configuration cannot refute it. A counterexample must instead give convex-independent point sets at arbitrarily large cardinalities whose unit-distance counts exceed every proposed linear constant. The mission tracks this superlinear-family statement separately, together with a reduction from it to the exact negation of Problem 96. This keeps both possible outcomes visible: a direct or Problem-97-derived linear upper bound, and an explicit family proving that no such bound exists.

Formalization scope

The canonical source is pinned at commit 757d852766f377f7c1a0ffeeef6d3526bc0cb7a4. It contains the formal source statements for Problem 97 and Problem 96. The source repository reports closed proofs of the conditional bridge to the $3n$ bound (conditional three-times bound), the $|A|\ge9$ counting milestone (nine-point counting bound), and the exact nine-point exclusion (exact nine-point exclusion theorem). The remaining large-cardinality milestone is the removable-vertex step, with its minimality hypothesis retained. The current platform mission contains accepted transfers of the counting argument, the conditional bridge, and the exact nine-point exclusion, while the removable-vertex step remains open. Its definitions make convex independence and the positive-radius condition explicit; no theorem is assumed inside a definition. Singletons and two-point sets are included in Problem 97, while Problem 96's counting definitions also include the empty set. The source repository uses Lean v4.27.0; these mission statements target the platform's v4.33.1. Source-proof transfer and revalidation remain separate work. The Lean declarations and proofs are this project's own formalization. The Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical provenance; they do not indicate that a paper proof was imported or machine-checked directly.

These source results establish the intended dependency graph: the P97 universal root feeds low-unit-degree extraction, strong induction, and then the P96 supremum bound. The platform mission records those contracts and milestones; it does not claim to have transplanted their proof bodies. The milestones include the two canonical roots, their conditional bridge, the |A| ≥ 9 count, the n = 9 exclusion, the |A| > 9 removable-vertex step, the documented Danzer nine-point three-neighbor example, the parallel goal of constructing a Problem 97 counterexample, and the superlinear-family route to a counterexample to Problem 96.

References

• Erdős, On Sets of Distances of n Points (1946), DOI.
• Erdős, Some Combinatorial and Metric Problems in Geometry (1987), scan.
• Fishburn–Reeds, Unit Distances Between Vertices of a Convex Polygon (1992), publisher record.
• Dumitrescu, On Distinct Distances from a Vertex of a Convex Polygon (2006), Springer record; provenance for the source counting method.
• Nivasch–Pach–Pinchasi–Zerbib, The Number of Distinct Distances from a Vertex of a Convex Polygon (2013), arXiv:1207.1266; provenance for the cap-witness refinements used by the source formalization.

Motivation

Split Euclidean space into finitely many measurable cells and record, for each cell, its Gaussian first moment, the integral of $x$ against the standard Gaussian measure over that cell. How large can the sum of the squared lengths of these vectors be? The propeller conjecture predicts that, with at least three cells in dimension at least two, the answer is $9/(8\pi)$, attained by three planar sectors of angle $2\pi/3$ (a "propeller") times the orthogonal complement. The question arose in Khot and Naor's work on approximate kernel clustering (Mathematika 2009), where this Gaussian partition parameter determines both the approximation ratio of Gaussian rounding and the matching Unique-Games hardness threshold. The surprise is that more cells or more dimensions do not help: the optimum uses only three cells in a plane.

This mission asks for a formal proof of the propeller bound in every dimension, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1983–2003 — The Gaussian Minkowski (Ehrhard) inequality: Ehrhard for convex sets (Math. Scand. 1983), Latała when one set is convex (Studia Math. 1996), Borell for Borel sets (C. R. Acad. Sci. 2003); later van Handel's game proof (PTRF 2018).
• 2009 — Khot and Naor introduce the problem, reduce maximizers to conical partitions in the span of their centroids, and compute the three-cell value (Mathematika 2009); see also their sharp kernel-clustering paper (RSA 2013).
• 2013 — Heilman, Jagannath and Naor prove the conjecture in $\mathbb R^3$ with a computer-assisted argument (DCG 2013).
• 2022 — Heilman gives a conditional route for three or four cells in any dimension, under a stability hypothesis on noise-stability maximizers (arXiv:2209.11216).
• September 2026 — The OpenAI preprint claims the bound for every dimension and every number of cells (Theorem 1.1, p. 1).

Setting

Let $\gamma_d$ be the standard Gaussian probability measure on $\mathbb R^d$, with density $(2\pi)^{-d/2}e^{-\|x\|^2/2}$. For a measurable set $A\subseteq\mathbb R^d$, its centroid is the unnormalized vector

$$z(A)=\int_A x\,d\gamma_d(x)\in\mathbb R^d .$$

A measurable partition $(A_1,\dots,A_k)$ of $\mathbb R^d$ consists of measurable sets such that almost every point (for $\gamma_d$) lies in exactly one of them; empty cells and arbitrary cell probabilities are allowed. Its value is $F(A)=\sum_{i=1}^k\|z(A_i)\|^2$. The propeller is the partition of $\mathbb R^d$, $d\ge2$, into the three sets $S_j\times\mathbb R^{d-2}$, where $S_1,S_2,S_3$ are the planar sectors of opening $2\pi/3$ bounded by the rays at angles $\pm\pi/3$ and $\pi$, with any further cells empty.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For all positive integers $d,k$ and every measurable partition $(A_1,\dots,A_k)$ of $\mathbb R^d$,

$$\sum_{i=1}^k\Bigl\|\int_{A_i}x\,d\gamma_d(x)\Bigr\|^2\ \le\ \frac{9}{8\pi},$$

and for $d\ge2$, $k\ge3$ the propeller is a measurable partition attaining equality.

Significance

The result itself. It settles the propeller conjecture in all dimensions and for all numbers of cells, without constraints on cell masses. Through Khot and Naor's analysis, the constant $9/(8\pi)$ fixes the loss factor $\alpha_k=\frac{8\pi}{9}(1-\frac1k)$ of Gaussian rounding for identity-target kernel clustering; combined with the companion Unique Games preprint, the preprint deduces NP-hardness of any better fixed loss factor (Theorem 6.1, p. 18). The bound also gives a sharp inequality for expected Gaussian maxima (Corollary 5.1, p. 17).

Formalizing it. A formal proof needs Gaussian measures on Euclidean space (available in Mathlib as stdGaussian), a compactness argument for extremal partitions, the convex case of the Ehrhard inequality, and the three-dimensional theorem of Heilman, Jagannath and Naor, which the preprint uses as an established input and which itself relies on a finite computer verification. Each of these is a reusable component; the three-dimensional case alone would be a substantial formalization.

Difficulty

The optimization runs over all measurable partitions, with both shapes and probabilities free. Khot and Naor's reduction gives conical extremizers whose $m$ nonzero centroids span an $(m-1)$-dimensional space, so the three-dimensional theorem disposes of $m\le4$ active cells. The remaining cases $m\ge5$ cannot be handled by any fixed finite computation. The preprint constrains them in two ways: deleting one score costs a definite amount of expected maximum, via concavity from the Ehrhard inequality (Section 3), and competition against two residual scores constrains a covariance determinant (Section 4, Lemma 4.1 and Corollary 4.2, pp. 11–12). Combining these must rule out every configuration with five or more cells.

Formalization scope

• Space d is EuclideanSpace ℝ (Fin d) and the measure is stdGaussian. IsPartition A asks each cell to be measurable and almost every point to lie in exactly one cell, matching the paper's convention that partitions are taken up to null sets.
• centroid A is the Bochner integral of the identity over A; value sums squared Euclidean norms. Integrability holds because Gaussian measures have finite first moments.
• The goal is a conjunction: the bound for all $d,k\ge1$, and, for $d\ge2$, $k\ge3$, that the explicit three-sector propeller d k (cells $\ge3$ empty) is a partition with value exactly $9/(8\pi)$. The sectors are written with closed inequalities, so they overlap only on null rays.
• No hypothesis is vacuous: the case $k=1$ is included (value $0$), and the equality clause pins the constant.

Selected references

• OpenAI, The Gaussian propeller bound in every dimension, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Gaussian-Propeller-Bound-in-Every-Dimension-September-24-2026/main.pdf
• S. Khot, A. Naor, Approximate kernel clustering, Mathematika 55 (2009), 129–165. https://doi.org/10.1112/S002557930000098X
• S. Khot, A. Naor, Sharp kernel clustering algorithms and their associated Grothendieck inequalities, Random Struct. Algorithms 42 (2013), 269–300. https://doi.org/10.1002/rsa.20398
• S. Heilman, A. Jagannath, A. Naor, Solution of the Propeller Conjecture in $\mathbb R^3$, Discrete Comput. Geom. 50 (2013), 263–305. https://doi.org/10.1007/s00454-013-9530-0
• S. Heilman, Hyperstable sets with voting and algorithmic hardness applications, arXiv:2209.11216 (2022). https://arxiv.org/abs/2209.11216v1
• A. Ehrhard, Symétrisation dans l'espace de Gauss, Math. Scand. 53 (1983), 281–301. https://doi.org/10.7146/math.scand.a-12035
• R. Latała, A note on the Ehrhard inequality, Studia Math. 118 (1996), 169–174. https://doi.org/10.4064/sm-118-2-169-174
• C. Borell, The Ehrhard inequality, C. R. Acad. Sci. Paris 337 (2003), 663–666. https://doi.org/10.1016/j.crma.2003.09.031
• R. van Handel, The Borell–Ehrhard game, Probab. Theory Relat. Fields 170 (2018), 555–585. https://doi.org/10.1007/s00440-017-0762-4
• E. Mossel, R. O'Donnell, K. Oleszkiewicz, Noise stability of functions with low influences: invariance and optimality, Ann. of Math. 171 (2010), 295–341. https://doi.org/10.4007/annals.2010.171.295

Motivation

Dantzig–Wolfe decomposition and column generation solve large integer programs by replacing a set of "easy" constraints with a description of its feasible points, and then pricing out the points one at a time. For linear programs this rests on the Minkowski–Weyl representation: every point of a polyhedron is a convex combination of its extreme points plus a nonnegative combination of its extreme rays. For integer programs that representation is not enough. Imposing integrality on the convex multipliers of the extreme points of $\mathrm{conv}(X)$ does not give back the integer program, because an optimal integer point may lie in the interior of $\mathrm{conv}(X)$.

Lübbecke and Desrosiers, in their survey Selected Topics in Column Generation (Operations Research 53(6), 2005), present discretization (Johnson 1989, Vanderbeck 2000) as the true integer analogue of the decomposition principle. Its basis is their Theorem 1: the integer points of a rational polyhedron are generated by finitely many integer points and finitely many integer rays with integer multipliers. The paper states this result and refers its proof to Nemhauser and Wolsey, Integer and Combinatorial Optimization (1988). It underlies the integer master problem (25) of branch-and-price.

Setting

Let $D$ be an $m \times n$ matrix and $\mathbf d$ an $m$-vector with rational entries. The polyhedron is

$$P = \{\mathbf x \in \mathbb R^n \mid D\mathbf x \geqslant \mathbf d,\ \mathbf x \geqslant \mathbf 0\},$$

and its set of integer points is $X = P \cap \mathbb Z^n$, the points of $P$ whose coordinates are all integers. Because $P \subseteq \mathbb R^n_+$, $X = P \cap \mathbb Z^n_+$.

The recession cone of $P$ is $\{\mathbf r \in \mathbb R^n \mid D\mathbf r \geqslant \mathbf 0,\ \mathbf r \geqslant \mathbf 0\}$. An integer ray of $P$ is a nonzero vector of $\mathbb Z^n$ in this cone. Extreme rays are not required.

In Lean these are polyhedronP D d, integerPoints D d, recessionConeP D and IsIntegerRay D w in the namespace Lubbecke2005.Discretization, with integer vectors cast to real vectors by castVec.

Formalization targets

Goal: Theorem 1 (pp. 1011–1012)

If $P \neq \emptyset$, there exist a finite set of integer points $\{\mathbf p_q\}_{q \in Q} \subseteq X$ and a finite set of integer rays $\{\mathbf p_r\}_{r \in R}$ of $P$ such that

$$X = \Bigl\{\mathbf x \in \mathbb R^n_+ \ \Big|\ \mathbf x = \sum_{q \in Q} \mathbf p_q \lambda_q + \sum_{r \in R} \mathbf p_r \lambda_r,\ \sum_{q \in Q} \lambda_q = 1,\ \boldsymbol\lambda \in \mathbb Z_+^{|Q|+|R|}\Bigr\}. \qquad (24)$$

Since the multipliers are nonnegative integers summing to one over $Q$, (24) says that $X$ is the union, over $q \in Q$, of the translates $\mathbf p_q + \mathbb Z_+\{\mathbf p_r\}_{r\in R}$ of the monoid generated by the rays. No bound on $|Q|$ or $|R|$ is part of the goal.

Milestone: Remark in §3.3 (p. 1012)

If $X \subseteq [0,1]^n$, every point of $X$ is a vertex of $\mathrm{conv}(X)$. In this case convexification and discretization coincide.

Significance

The result. Theorem 1 converts an integer program $\min\{c(\mathbf x) \mid A\mathbf x \geqslant \mathbf b,\ \mathbf x \in X\}$ into the integer master program (25) over the multipliers $\boldsymbol\lambda$, with one column per generating point and per generating ray. When $X$ is bounded the rays disappear, exactly one $\lambda_q$ equals one, and (25) is a linear integer program even for a nonlinear cost $c$. The representation is what makes branching on master variables, and the passage between compact and extensive formulations, well defined in branch-and-price.

Formalizing it. The result is classical (Nemhauser–Wolsey 1988, going back to Giles and Pulleyblank and to Meyer's theorem that the integer hull of a rational polyhedron is a polyhedron). On Prove2Me, the real representation (8) is formalized as LinearOptimization.polyhedron_resolution (Bertsimas–Tsitsiklis Thm 4.15) and the integer hull theorem as LinearOptimization.integer_hull_is_polyhedron (Thm 11.3); both are included as reference items. The convexification counterpart of §3.2, that the Lagrangian dual equals the LP over $\mathrm{conv}(X)$, is LinearOptimization.lagrangean_dual_eq_lp_over_hull. No machine-checked statement of the integer representation (24), with integer multipliers and integer rays, was found on the platform. The mission produces that statement and, once solved, its proof.

Difficulty

The obvious attempt applies the real representation (8) and rounds. It fails twice. First, the extreme points of $P$ need not be integral, and an integer point written as a real combination of vertices and rays has no reason to have integer multipliers. Second, the extreme rays of $P$ generate the recession cone over $\mathbb R_+$, but the integer points of that cone are not in general nonnegative integer combinations of the (scaled) extreme rays; a generating set of the lattice points of a cone must usually contain non-extreme vectors. The finiteness of $Q$ is also not automatic: $X$ itself is typically infinite, and taking $Q = X$ trivializes the statement.

Rationality of the data is essential. For $P = \{\mathbf x \in \mathbb R^2_+ \mid \sqrt2\,x_1 - x_2 \geqslant 0\}$, every integer ray has slope below $\sqrt 2$, so finitely many base points and rays generate only points with $x_2 \leqslant \rho x_1 + C$ for some $\rho < \sqrt 2$, while $X$ contains $(k, \lfloor\sqrt2 k\rfloor)$ for every $k$.

Formalization scope

• Vectors are Fin n → ℝ; integer vectors are Fin n → ℤ cast coordinatewise. Both sides of (24) are sets of real vectors.
• $D$ and $\mathbf d$ are ℚ-valued and cast to ℝ. This is an addition: the paper names no field, and the theorem is false for irrational data (see Difficulty). The cited source, Nemhauser–Wolsey, works with rational data.
• The hypothesis $P \neq \emptyset$ is kept as on the page. $X$ may still be empty (e.g. $P = \{1/2\}$); then $Q = \emptyset$ and both sides of (24) are empty. The statement allows this.
• $Q$ and $R$ are Fin k and Fin l for existentially chosen $k, l \in \mathbb N$; the finiteness is the content of the theorem. The multiplier vector $\boldsymbol\lambda \in \mathbb Z_+^{|Q|+|R|}$ is written as a pair of ℕ-valued vectors.
• "Integer rays of $P$" is read as nonzero integer vectors in the recession cone $\{D\mathbf r \geqslant \mathbf 0, \mathbf r \geqslant \mathbf 0\}$; extremality is not required, as the page does not require it (contrast (8), which says "extreme rays").
• The constraint $\mathbf x \in \mathbb R^n_+$ on the right side of (24) is kept although it is implied.
• In the Remark, "vertices of $\mathrm{conv}(X)$" is read as extreme points of the convex hull; $X$ is finite there, so the two notions agree.

A formalization with real multipliers would be the resolution theorem (8), already on the platform, and one with $Q$ or $R$ infinite would be trivial; both are excluded by the statement.

Useful infrastructure: lattice points of rational polyhedral cones (Hilbert bases, Gordan's lemma), the integer hull theorem, and the real resolution theorem. A proof of Gordan's lemma for rational cones in this vocabulary would be reusable well beyond this mission. Contributions toward any of these are welcome.

Selected references

• M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
• G. L. Nemhauser and L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
• R. R. Meyer, On the existence of optimal solutions to integer and mixed-integer programming problems, Mathematical Programming 7:223–235, 1974. https://doi.org/10.1007/BF01585518
• F. Vanderbeck, On Dantzig–Wolfe decomposition in integer programming and ways to perform branching in a branch-and-price algorithm, Operations Research 48(1):111–128, 2000. https://doi.org/10.1287/opre.48.1.111.12453
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

Motivation: keeping partial sums of vectors small

Given vectors $v_1,\dots,v_N$ in the Euclidean unit ball of $\mathbb R^d$ that sum to zero, can they always be reordered so that every partial sum stays in a ball whose radius depends only on $d$? Steinitz's lemma, from his work on rearrangements of conditionally convergent vector series, says yes: in any norm, radius $d$ suffices (Grinberg–Sevast'yanov 1980). For the Euclidean norm, the expected answer is $O(\sqrt d)$, the Euclidean Steinitz–Bergström conjecture. A closely related prefix discrepancy problem asks for signs $\varepsilon_i\in\{\pm1\}$, chosen once and for all, such that every signed prefix $\sum_{i\le k}\varepsilon_iv_i$ is $O(\sqrt d)$, independently of $N$. Both questions are basic in discrepancy theory and combinatorial vector balancing, with applications to scheduling, rounding and the analysis of online and streaming algorithms.

Timeline

• 1913 — Steinitz proves his rearrangement lemma for conditionally convergent vector series (historical account in Ambrus–Heck 2026, Section 2).
• 1954 — Behrend discusses the expected square-root growth in Euclidean space (Canad. J. Math., p. 108).
• 1980 — Grinberg and Sevast'yanov prove that partial sums can be kept within $d$ times the unit ball, for every norm (Funct. Anal. Appl.).
• 1994–2023 — Chobanyan's transference principle relates rearrangements to signed sums (Probability in Banach Spaces 9, 1994), later in a finite positive-forward, negative-reverse form (Chobanyan et al., Bull. TICMI 2023).
• 1998 / 2012 — Banaszczyk's Gaussian-measure balancing theorem (Random Structures Algorithms 1998) and his prefix bound $O(\sqrt d+\sqrt{\log N})$ for signed series and rearrangements (Random Structures Algorithms 2012).
• 2021 — Bansal, Jiang, Meka, Singla and Sinha state the $O(\sqrt d)$ prefix-signing question explicitly (Conjecture 6.3, arXiv:2111.07049).
• 2026 — Ambrus and Heck record the conjecture and its attribution to Bergström (Conjecture 5) and reduce it to a relaxed problem (Mathematika); Dutta, Jha and Jiang give efficient bounds $O(\sqrt d+d^{1/4}\log^{7/4}N)$ (arXiv:2604.13355).
• 2026 — An OpenAI preprint, The Euclidean Steinitz–Bergström theorem (OpenAI Math Release, September 24, 2026), claims the $O(\sqrt d)$ bound for both problems with an absolute constant. It has not been peer reviewed, and its proof is not formally verified.

Setting

Work in Euclidean space $\mathbb R^d$ with norm $\|\cdot\|_2$, and let $v_1,\dots,v_N$ satisfy $\|v_i\|_2\le1$; repetitions and zero vectors are allowed. A prefix sum is $\sum_{i=1}^k$ for $0\le k\le N$ (the empty sum is $0$). For a zero-sum family, the Steinitz quantity

$$\beta(v_1,\dots,v_N)=\min_{\pi\in\mathfrak S_N}\ \max_{0\le k\le N}\Bigl\|\sum_{i=1}^kv_{\pi(i)}\Bigr\|_2$$

is the best achievable maximal prefix norm over all orderings. The Euclidean Steinitz constant $S_2(d)$ is its supremum over all such families.

Formalization targets

Goal: prescribed-order signing and Euclidean Steinitz with one absolute constant (Theorems 1.1 and 1.2)

There is an absolute constant $C$ such that for all $d,N\ge1$ and all $v_1,\dots,v_N\in\mathbb R^d$ with $\|v_i\|_2\le1$:

1. (Theorem 1.1) there are signs $\varepsilon_i\in\{-1,1\}$ with

$$\max_{0\le k\le N}\Bigl\|\sum_{i=1}^k\varepsilon_iv_i\Bigr\|_2\le C\sqrt d ;$$

2. (Theorem 1.2) if moreover $\sum_iv_i=0$, some permutation $\pi$ satisfies

$$\max_{0\le k\le N}\Bigl\|\sum_{i=1}^kv_{\pi(i)}\Bigr\|_2\le C\sqrt d .$$

The constant is not fixed. The simplex example in the source shows $S_2(d)\ge\tfrac12\sqrt d$, so the order is optimal. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.2 settles the Euclidean Steinitz–Bergström conjecture: $S_2(d)=\Theta(\sqrt d)$. Theorem 1.1 settles the $\ell_2$ prefix-discrepancy question of Bansal et al., removing the $\sqrt{\log N}$ term in Banaszczyk's bound. A single choice of signs controls all prefixes at once, unlike terminal balancing results that bound one sum. The source also derives finite-dimensional $\ell_p$ Steinitz bounds and a colorful Steinitz theorem (Corollaries 8.1–8.2). The result is existential and gives no efficient algorithm.

Formalizing it. The statement is finite and elementary. The deduction of Theorem 1.2 from Theorem 1.1 is a short transference argument (Section 1.1 of the source), suitable as a first formalization step. The proof of Theorem 1.1 uses Gaussian measures of convex bodies, Dirichlet energies, Steiner symmetrization and Brownian survival estimates, which would make substantial reusable additions to Mathlib's probability and convex-geometry libraries.

Difficulty

Signing each prefix separately is easy, by terminal balancing results, but one common signing must work for all $N$ prefixes. Union bounds over prefixes and Banaszczyk's Gaussian-measure method lose a $\sqrt{\log N}$ factor, because the probability that a random walk stays in a ball of radius $C\sqrt d$ for $N$ steps decays with $N$. The proof must therefore control a single body of coefficients enforcing all prefix constraints, with bounds independent of the number of steps.

Formalization scope

• Vectors live in EuclideanSpace ℝ (Fin d), indexed by Fin N, with $d,N\ge1$ and $\|v_i\|\le1$.
• Prefixes are sums over $\{i : i < k\}$ for every natural $k\le N$, so the empty prefix and the full sum are included.
• SignedPrefixBound C asks for signs $\varepsilon_i\in\{-1,1\}$ (as reals) with every signed prefix at most $C\sqrt d$. OrderingPrefixBound C asks, for zero-sum families, for a permutation $\pi$ with every reordered prefix at most $C\sqrt d$. The goal is $\exists C,\ \mathrm{SignedPrefixBound}\,C\wedge\mathrm{OrderingPrefixBound}\,C$; the same constant serves both, as stated in the source.
• The quantifier order is the source's: $C$ is chosen before $d$, $N$ and the vectors.
• Needed infrastructure: Gaussian measures of symmetric convex bodies, Steiner symmetrization, Dirichlet energies of densities, Ornstein–Uhlenbeck/Brownian survival estimates, and the Chobanyan transference. Contributions proving the transference step (Theorem 1.1 ⇒ Theorem 1.2) or the lower-bound example are welcome.

Selected references

• V. S. Grinberg and S. V. Sevast'yanov, Value of the Steinitz constant, Funct. Anal. Appl. (1980).
• F. A. Behrend, The Steinitz–Gross theorem on sums of vectors, Canad. J. Math. (1954).
• S. Chobanyan, Convergence a.s. of rearranged random series in Banach space and associated inequalities, Probability in Banach Spaces 9 (1994).
• W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures Algorithms (1998).
• W. Banaszczyk, On series of signed vectors and their rearrangements, Random Structures Algorithms (2012).
• N. Bansal, H. Jiang, R. Meka, S. Singla and M. Sinha, Prefix discrepancy, smoothed analysis, and combinatorial vector balancing, 2021. https://arxiv.org/abs/2111.07049
• G. Ambrus and R. Heck, A note on the Steinitz Lemma, Mathematika (2026). https://doi.org/10.1112/mtk.70085
• K. Dutta, A. V. Jha and H. Jiang, Near-optimal constructive bounds for $\ell_2$ prefix discrepancy and Steinitz problems via affine spectral independence, 2026. https://arxiv.org/abs/2604.13355
• OpenAI, The Euclidean Steinitz–Bergström theorem, OpenAI Math Release preprint, September 24, 2026 (Theorems 1.1 and 1.2, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026.pdf

Motivation

Every pure integer program $\min\{c\cdot x : Ax = b,\ x \ge 0 \text{ integer}\}$ can be relaxed, by dropping the nonnegativity of the basic variables of an optimal linear-programming basis, to a problem over a finite Abelian group: find nonnegative integers $t(g)$, one for each nonzero group element, with $\sum t(g)\cdot g = g_0$. R. E. Gomory's 1969 paper Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969) 451–558) studies the convex hulls of the solutions of these group equations, the corner polyhedra, and the master polyhedron $P(\mathcal G, g_0)$ that contains all of them as faces. These polyhedra are the source of the group-theoretic approach to cutting planes: their faces are valid inequalities for every integer program with the same group, and their vertices are the candidate optimal solutions of the group relaxation.

The paper's first section shows that every vertex of such a polyhedron is an irreducible solution, and remarks (p. 460) that the converse fails in general: a typical group has many irreducible solutions that are not vertices. Section 3F identifies a family of groups where the two notions coincide, which is what makes the vertices of these polyhedra countable in closed form.

Setting

Let $\mathcal G$ be a finite Abelian group written additively, with zero $\bar 0$, and $\mathcal G^+ = \mathcal G\setminus\{\bar 0\}$. For $g_0 \in \mathcal G$ the group equation is

$$\sum_{g\in\mathcal G^+} t(g)\cdot g = g_0, \qquad t(g) \in \{0, 1, 2, \ldots\}.$$

The master polyhedron $P(\mathcal G, g_0)$ is the convex hull in $\mathbb R^{\mathcal G^+}$ of its nonnegative integer solutions (for $g_0 = \bar 0$ the solution $t = 0$ is excluded). A vertex is an extreme point of $P(\mathcal G, g_0)$.

A nonnegative integer vector $t$ is irreducible if any two integer vectors $r, s$ with $0 \le r, s \le t$ and $\sum r(g)\cdot g = \sum s(g)\cdot g$ are equal. A finite set $S$ of group elements is independent if $\sum_{g\in S} s_g g = \bar 0$ with integers $s_g$ forces $s_g g = \bar 0$ for each $g$.

The groups of §3F are those in which every nonzero element has order 2, the groups $\mathcal G_2, \mathcal G_{2,2}, \ldots$, or every nonzero element has order 3, the groups $\mathcal G_3, \mathcal G_{3,3}, \ldots$.

Formalization targets

Goal: THEOREM 23 (p. 505)

If every nonzero element of $\mathcal G$ has order $p$, with $p = 2$ or $p = 3$, and $g_0 \ne \bar 0$, then for every nonnegative integer solution $t$ of the group equation

$$t \text{ irreducible} \iff t \in \operatorname{vert} P(\mathcal G, g_0),$$

and the support $\{g : t(g) > 0\}$ of such a vertex is an independent set.

Milestones

1. THEOREM 2 (p. 460), for $P(\mathcal G, g_0)$ with $g_0 \ne \bar 0$: every vertex is an irreducible integer solution.
2. The LEMMA of p. 505: for $p \in \{2, 3\}$, $p > t > 0$ and $p > s \ge 0$ there are $0 \le t', t'' \le t$ with $t' + s \equiv t'' \pmod p$.
3. The support of an irreducible solution is independent (p. 506).
4. A solution vanishing off the support of an irreducible $t$ agrees with $t$ modulo $p$ and dominates it (p. 506, corrected).
5. An irreducible $t$ minimizes $\pi$, the indicator of the complement of its support, every minimizer dominates $t$, and $t$ is a vertex (p. 506, corrected).
6. The vertex characterization (p. 506): a nonzero $t$ is a vertex of some $P(\mathcal G, g_0)$, $g_0 \ne \bar 0$, iff its support is independent and $t(g) < p$ for all $g$.

Significance

THEOREM 23 turns a polyhedral question into a combinatorial one for the elementary Abelian 2- and 3-groups: the vertices of $P(\mathcal G, g_0)$ are read off from independent subsets of the group and residues below $p$. Gomory uses this on pp. 506–507 to count all vertices of all $P(\mathcal G_{s^n}, g_0)$ exactly and to derive their asymptotic number. It also marks the boundary of the general picture: groups with elements of other orders have irreducible solutions that are not vertices.

The result has been proved since 1969; no machine-checked proof exists. The mission produces a Lean statement and, once solved, a verified proof of the theorem together with the general fact that vertices of the master polyhedron are irreducible, a reusable layer for the other group-polyhedron results of the same paper. Two sentences of the printed proof (p. 506) are false as written (see Formalization scope); formalization records their corrected forms.

Difficulty

The direction "vertex $\Rightarrow$ irreducible" holds in every group and is a midpoint argument. The difficulty is the converse: showing that an irreducible solution cannot be written as a proper convex combination of other solutions, which are infinitely many and unbounded. The natural route, exhibiting a linear objective that $t$ uniquely minimizes, does not work with the objective printed on the page: solutions with the same support as $t$ but larger entries are tied with it. The argument must control those solutions through the arithmetic of residues modulo $p$, and this is where the exponent 2 or 3 is used; the analogous residue statement fails for $p = 5$.

Formalization scope

• T-space vectors are functions on the subtype {g : G // g ≠ 0}; integer solutions are $\mathbb N$-valued and cast to $\mathbb R$; vertices are Set.extremePoints ℝ of the convex hull of the cast solutions.
• "All elements of $\mathcal G$ are of order 2 or all of order 3" is read as: there is $p \in \{2, 3\}$ with every nonzero element of order $p$. Groups mixing orders 2 and 3 are excluded, as on the page.
• $g_0 \ne \bar 0$ is a hypothesis of the whole of THEOREM 23 (the page attaches it to the second sentence only). At $g_0 = \bar 0$ the solution $t = 0$ is excluded (footnote p. 474) and every nonzero solution is reducible, so the first sentence would fail. THEOREM 2 is restated for $P(\mathcal G, g_0)$, $g_0 \ne \bar 0$, for the same reason.
• "Independent" is the page's definition with integer coefficients; the gloss "part of a group basis" is not formalized.
• The letter $T$ on pp. 505–506 is the support of $t$, not the solution set.
• The page's claim that $t$ is the only solution vanishing off its support, and the unique minimizer of $\pi$, fail literally (in $\mathbb Z_2$ with $g_0 = 1$, $t = (1)$ and $u = (3)$). Milestones 4 and 5 state the corrected conclusions; the goal theorem is unaffected.
• The vertex characterization adds $t \ne 0$, which the page leaves implicit.
• Ruled out: stating the order hypothesis for all elements including $\bar 0$ (unsatisfiable, so the theorem would be vacuous), dropping $g_0 \ne \bar 0$ (false statement), or replacing the master polyhedron by a bounded truncation (a different polyhedron with extra vertices).
• Needed: convex hulls of infinite sets of lattice points and their extreme points (Mathlib's convexHull, extremePoints_convexHull_subset), and finite sums in Abelian groups. Contributions welcome: any of the milestones, and a general lemma that a unique minimizer of a nonnegative linear function over the integer solutions is a vertex.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. https://doi.org/10.1016/0024-3795(69)90017-2
• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proc. Natl. Acad. Sci. USA 53 (1965), 260–265. https://doi.org/10.1073/pnas.53.2.260
• R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Mathematical Programming 3 (1972), 23–85. https://doi.org/10.1007/BF01584976

Motivation

The vertices and edges of a convex polytope form a graph, and much of polyhedral combinatorics and of the theory of the simplex method is about that graph: how far apart two vertices can be (the Hirsch question), which graphs arise (Steinitz's theorem in dimension 3), and how robust the graph is. In 1961 M. L. Balinski proved that the graph of a full-dimensional polytope in $n$-space cannot be disconnected by deleting fewer than $n$ vertices (Pacific J. Math. 11 (1961) 431–434). The result, now called Balinski's theorem, is a standard entry in textbooks on polytopes (Grünbaum, Convex Polytopes, §11.3; Ziegler, Lectures on Polytopes, Thm 3.14) and is the starting point of the study of connectivity of polytope graphs. Its proof uses only linear programming: the improving-edge step of the simplex method and the connectivity of the graph of a face.

Timeline. Steinitz (1922) characterised the graphs of 3-polytopes as the 3-connected planar graphs, so the case $n=3$ is contained in his theorem. Balinski (1961) proved $n$-connectivity in every dimension. Whitney (1932) had shown that $n$-connectivity is equivalent to the existence of $n$ disjoint paths between any two points; Balinski gives a new proof of that equivalence through max-flow min-cut and draws the corollary that any two vertices of a full-dimensional polytope in $\mathbb R^n$ are joined by $n$ disjoint edge paths.

Setting

Fix integers $n$ (the dimension of the space) and $m$ (the number of inequalities), vectors $a_1,\dots,a_m\in\mathbb R^n$ (the rows of a matrix $A$) and $b\in\mathbb R^m$. Balinski's system (1) describes

$$S=\{X\in\mathbb R^n : AX\le b\}=\{x : \langle a_i,x\rangle\le b_i,\ i=1,\dots,m\},$$

written Hirsch.Hpoly a b in Lean. The paper assumes throughout two standing assumptions (StandingAssumptions a b):

1. the only solution to $AX\le0$ is $X=0$;
2. some $X^0$ satisfies $AX^0<b$.

A vertex of $S$ is an extreme point. An edge is a segment $[u,v]$, $u\neq v$, that is an extreme subset of $S$ (Hirsch.Adj S u v). The graph $G(S)$ (polyGraph S) has the vertices as points and the edges as lines.

A graph is $n$-tuply connected (IsNTuplyConnected G n) if it has at least $n+1$ points and remains connected after dropping out any $n-1$ or fewer points. Two points are joined by $n$ disjoint paths (HasDisjointPaths G u v n) if there are $n$ distinct paths from $u$ to $v$ which share no point other than $u$ and $v$.

Formalization targets

Goal: the THEOREM (p. 432)

$$\text{(i), (ii)}\ \Longrightarrow\ G(S)\ \text{is } n\text{-tuply connected}.$$

That is, $|\operatorname{ext} S|\ge n+1$ and $G(S)-X$ is connected for every set $X$ of at most $n-1$ vertices.

Milestones, in the order the proof uses them

1. $S$ has finitely many vertices, $S=\operatorname{conv}(\operatorname{ext}S)$, and $S$ lies in no hyperplane $\{\langle c,x\rangle=d\}$, $c\neq0$ (p. 432).
2. $|\operatorname{ext}S|\ge n+1$ (p. 432).
3. Preliminary remark: every vertex has degree at least $n$ in $G(S)$ (p. 432).
4. Improving neighbour: if $\langle c,\cdot\rangle$ is not maximal on $S$ at a vertex $v$, some neighbour $w$ of $v$ has $\langle c,w\rangle>\langle c,v\rangle$ (p. 432, case (a)).
5. The graph of a face is connected (p. 433, case (a)); this is the published, proved Hirsch.face_connected.
6. Two vertices with $\langle c,\cdot\rangle>d$ are joined by a path in $G(S)$ all of whose points satisfy $\langle c,\cdot\rangle>d$ (pp. 432–433, case (a)).
7. COROLLARY (p. 434): any two distinct vertices are joined by $n$ disjoint paths:

$$u\neq v\ \Longrightarrow\ \exists\,P_1,\dots,P_n:\ P_i\cap P_j\subseteq\{u,v\}\ (i\neq j).$$

Significance

The result. Balinski's theorem says that polytope graphs are highly connected, which constrains which graphs can be graphs of $n$-polytopes and is the base case of later results on the connectivity of polytope graphs. Together with Whitney's theorem it gives $n$ vertex-disjoint edge paths between any two vertices. The improving-neighbour step is the local optimality criterion of the simplex method.

Formalizing it. The theorem is classical and proved; it has not been formalized. On this platform the case $n=1$ (the graph of a polytope is connected) is proved as Hirsch.graph_connected_general, and connectivity of the graph of each face as Hirsch.face_connected, both by Shuze Chen; LinearOptimization.polyhedron_bounded_convex_hull_extreme proves the convex-hull clause of milestone 1 for a matrix-form polyhedron under the hypotheses "nonempty and bounded", and ConnPreservingHamPath.IsKConnected.le_ncard_neighborSet proves "connectivity at most minimum degree" for its own notion of $k$-connectivity. This mission adds vertex $n$-connectivity in every dimension, the simplex improving-neighbour lemma for H-polytopes, and the corollary on disjoint paths. The corollary needs Whitney's theorem, which is the goal of the companion mission On the Graph Structure of Convex Polyhedra in n-Space II.

Difficulty

An induction on dimension through facets does not directly control where the deleted vertices lie. Balinski's argument leans on several facts the paper calls obvious or clear: that a vertex with no improving neighbour is optimal, that the graph of a face is connected, that $n$ points of $\mathbb R^n$ lie on a common hyperplane while $S$ does not, and that $S$ has at least $n+1$ vertices. Each needs its own development from the two algebraic assumptions, in particular the passage from (i)–(ii) to a bounded full-dimensional polytope with finitely many vertices, and the identification of extreme segments with edges. Deleting fewer than $n-1$ vertices, which the definition requires and the proof's text does not treat, needs a separate argument. The proof also tacitly needs the affine function to take a nonzero value at some vertex.

Formalization scope

• Space: EuclideanSpace ℝ (Fin n); rows a : Fin m → EuclideanSpace ℝ (Fin n), b : Fin m → ℝ. The published Hirsch_model names the dimension d and the number of rows n; here $n$ is the dimension, as in the paper.
• The two standing assumptions are hypotheses of every theorem, stated literally, not replaced by "bounded and full-dimensional".
• Vertices are Set.extremePoints ℝ S; edges are Hirsch.Adj (extreme segments). $G(S)$ is a SimpleGraph on the vertex subtype.
• Counts use Set.encard; "$n-1$ or fewer points" is X.encard < n. A path of the paper is a Mathlib Walk (consecutive points distinct).
• Explicit readings of loose phrases: "form a graph" includes finiteness of the vertex set (milestone 1); "lies within no hyperplane" is "for every $c\neq0$ and $d$ some point of $S$ has $\langle c,x\rangle\neq d$"; "whose graph is clearly connected" is the referenced Hirsch.face_connected; the affine function $y_0$ of the proof is an arbitrary $x\mapsto\langle c,x\rangle-d$, and only the "maximum"/"$>$" forms are stated (the others follow for $-c,-d$); "at least $n$ disjoint paths between any pair of vertices" is a family of $n$ pairwise distinct paths without repeated points, sharing only their endpoints, between two distinct vertices.
• Trivializing formalizations are ruled out: edges are not arbitrary pairs of vertices (that makes the goal nearly free), $n$-tuply connected requires both the point count and connectivity after deletion, and the disjoint paths must be pairwise distinct (otherwise $n$ copies of one edge would do).
• Welcome contributions: the passage from (i)–(ii) to a polytope (finiteness of vertices, Krein–Milman in this setting), the simplex optimality criterion for H-polytopes, and conversion between Hirsch walk vocabulary and Mathlib Walks; all are reusable beyond this mission.

Selected references

• M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific J. Math. 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
• H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150–168. https://doi.org/10.2307/2371086
• A. W. Tucker, Linear inequalities and convex polyhedral sets, Proc. Second Symposium in Linear Programming, Washington D.C., 1955, 569–602.
• B. Grünbaum, Convex Polytopes, 2nd ed., Springer GTM 221, 2003, §11.3. https://doi.org/10.1007/978-1-4613-0019-9
• G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995, Theorem 3.14. https://doi.org/10.1007/978-1-4613-8431-1

Motivation

This mission completes chapter 7's L-convex function theory and closes the book on it. It first finishes the theory of positively homogeneous L-convex functions — showing they coincide exactly with the classical Lovász extensions of submodular set functions, a one-to-one correspondence that recognizes forty years of submodular-optimization machinery as a special case of L-convex function theory. It then proves the L-side capstone this series has been building toward since mission 26-ch07b-lconvexfunctions: polyhedral L-convexity is characterized simultaneously by directional derivatives, subdifferentials, and weighted-minimizer polyhedra — the exact mirror of what mission 24-ch06d-mconvexfunctions proved for M-convex functions. Finally it develops quasi L-convex functions, the L-side analogue of mission 25-ch06e-mconvexfunctions's quasi M-convex functions, ending exactly where chapter 7 itself ends.

Setting

Fix a finite ground set $V$. The class $0L[\mathbb R \to \mathbb R]$ consists of polyhedral L-convex functions that are positively homogeneous; $0L[\mathbb Z \to \mathbb Z]$, its integer-valued integer-domain analogue. A positively homogeneous L-convex function $g$ induces a submodular set function $\rho_g(X) = g(\chi_X)$; conversely the Lovász extension $\hat\rho$ of a submodular set function is positively homogeneous L-convex. The base polyhedron $B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ \forall X,\ x(V) = \rho(V)\}$ of a submodular $\rho$ is always an M-convex polyhedron. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is quasi submodular (QSB) if $g(p\wedge q) \le g(p)$ or $g(p\vee q) \le g(q)$ for all $p,q$; the weaker (QSBw) requires only $\max\{g(p),g(q)\} \ge \min\{g(p\wedge q), g(p\vee q)\}$.

Formalization targets

Goal: the four characterizations of polyhedral L-convexity (Theorem 7.45)

For a polyhedral convex function $g$ with $\operatorname{dom}_{\mathbb R} g \ne \emptyset$: $g$ is L-convex if and only if every directional derivative $g'(p;\cdot)$ is $0L[\mathbb R \to \mathbb R]$, if and only if every subdifferential $\partial_{\mathbb R} g(p)$ is an M-convex polyhedron, if and only if every weighted minimizer set is an L-convex polyhedron. Not present in this chunk's own extraction table (its label opens mid-paragraph, missed by the same extractor failure already documented for mission 25-ch06e-mconvexfunctions's Theorem 6.68), found by direct reading and chosen as goal because it is the exact L-side mirror of mission 24-ch06d-mconvexfunctions's own milestone Theorem 6.63, and its proof is assembled entirely from results already in this series (Theorem 7.43, Proposition 7.34, Theorem 7.40).

Supporting structural targets

Fifteen further results build the two remaining pieces of chapter 7's theory. Propositions 7.37-7.39 and Theorem 7.40 establish the one-to-one correspondence between positively homogeneous L-convex functions and submodular set functions via the Lovász extension; Proposition 7.41 gives a minimizer-polyhedron characterization of this class, and Proposition 7.42 shows directional derivatives of L-convex functions automatically land in it. Theorem 7.43 — the L-side mirror of mission 24-ch06d-mconvexfunctions's own goal, Theorem 6.61 — proves the directional- derivative/subdifferential correspondence via the induced submodular set function's base polyhedron; Proposition 7.44 checks consistency at integer points, and Theorem 7.46 refines Theorem 7.45 to the integral case. Theorem 7.49 (also missed by the extractor) gives the quasi-submodularity implication hierarchy and its perturbation-equivalence capstone, mirroring mission 25-ch06e-mconvexfunctions's Theorem 6.68 exactly. Proposition 7.50 and Theorems 7.51-7.52 build the level-set/perturbation machinery quasi submodularity needs; Theorems 7.53-7.54 (both missed by the extractor, the latter's full statement requiring one page beyond this chunk's nominal range, at the very end of chapter 7) give the quasi L-optimality and quasi L-proximity theorems.

Significance

The 0L/submodular correspondence (Theorem 7.40) is the precise sense in which L-convex function theory generalizes submodular set function theory rather than merely resembling it: every submodular set function is literally the restriction to $\{0,1\}^V$ of a positively homogeneous L-convex function, and every algorithm for one transfers to the other through this exact dictionary. The goal, Theorem 7.45, completes the parallel structure this series has built since chapter 6: M-convexity and L-convexity are now each characterized in the same four convex-analytic vocabularies, setting up chapter 8's conjugacy theorem, which will show these two characterizations are not merely analogous but literally dual to each other under the Legendre-Fenchel transform. The quasi-submodularity results matter for the same reason as their M-side counterparts: chapter 10's algorithms for L-convex-function minimization remain correct under nonlinear rescalings that destroy L-convexity itself but preserve quasi submodularity.

None of these results are open — they are Murota's account of how far L-convex function theory extends beyond the polyhedral case (to positive homogeneity and its submodular-function incarnation) and how far its exchange-style inequality can be relaxed while preserving optimization theory (to quasi submodularity), mirroring chapter 6's identical two-part program for M-convex functions. What this mission contributes is a faithful, machine-checked formal statement of each, including four theorems (7.45, 7.49, 7.53, 7.54) the platform's own automated extractor missed entirely — one of them requiring a page beyond this chunk's own nominal range to complete, since chapter 7 ends there and this is the last mission covering it — extending the shared Lean vocabulary (ZeroLR, BasePolyhedron, QSBw) this series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to prove all six pairwise implications among its four conditions independently; the book's own proof instead chains through results already established: (a)⇒(b) is Proposition 7.42, (a)⇒(c) is Theorem 7.43, (a)⇒(d) is Proposition 7.34, (b)⇔(c) uses the 0L/M0[R] correspondence, and (d)⇒(b) is the genuinely hard direction, requiring Proposition 7.41 applied to the directional derivative itself (showing $\arg\min(g'(p;\cdot)[-x])$ is an L-convex cone by an explicit description via the admissible-potential set of the distance function underlying $\arg\min g[-x]$). The remaining combinatorial difficulty in this block is in Theorem 7.43's proof: identifying $\partial_{\mathbb R} g(p)$ with the base polyhedron $B(\rho_{g,p})$ requires the L-optimality criterion (Theorem 7.33, mission 27-ch07c-lconvexfunctions) applied pointwise, a chain of logical equivalences with no single-step shortcut, exactly mirroring how mission 24-ch06d-mconvexfunctions's Theorem 6.61 needed the M-optimality criterion.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; L-convex functions are (V→ℝ)→WithTop ℝ (polyhedral) or (V→ℤ)→WithTop ℝ (integer-domain). All sixteen numbered results found in this chunk's page range — the twelve in BRIEF.md's own table plus four the extractor missed (Theorems 7.45, 7.49, 7.53, 7.54) — are placed, with two documented, content-preserving scope decisions: Theorem 7.43 omits the dual-integral refinement clauses for L[R→R|Z]/L[Z→Z] (the same decision mission 24-ch06d-mconvexfunctions's Theorem 6.61 made), and Proposition 7.50 states the general inequalities without restating their "In particular" specializations, which add no independent content — see HARD.md. "$\inf g[-x]>-\infty$" is replaced by the equivalent (ArgMinR ...).Nonempty hypothesis throughout, matching mission 25-ch06e-mconvexfunctions's identical substitution. This mission's base vocabulary is redeclared from missions 20-ch04b-mconvexsets, 21-ch05b-lconvexsets, 23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the sixteen sorrys are welcome; the goal and Theorem 7.43 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 [152] (the polyhedral theory Theorems 7.26-7.46 are drawn from).
• P. Milgrom and C. Shannon, "Monotone comparative statics," Econometrica, 62 (1994), pp. 157-180 [129] (the origin of the quasi-submodularity condition (SSQSB)).

Motivation

Every characterization of M-convexity so far in this series — the exchange axiom, the optimality criterion, convex extensibility, the directional-derivative/subdifferential correspondence — has been an equivalence with M-convexity itself: a function either is M-convex or it is not. Section 6.14 asks a different question: what happens when the exchange axiom's defining inequality is relaxed to only the sign patterns it actually forces? The answer is a hierarchy of "quasi M-convex" conditions — weaker than M-convexity, strong enough to keep the optimality criterion and the proximity/minimizer-cut theorems intact — and, at the top of that hierarchy, a genuinely new characterization of M-convexity itself: a function is M-convex if and only if every one of its linear perturbations is quasi M-convex in the weakest sense. This mission formalizes that entire hierarchy and its capstone, plus two further characterizations of polyhedral M-convexity (via directional derivatives, subdifferentials, and weighted-minimizer polyhedra) that complete the real-variable theory chunk 24-ch06d-mconvexfunctions began.

Setting

Fix a finite ground set $V$ and $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$. Write $\Delta f(z;v,u) = f(z + \chi_v - \chi_u) - f(z)$. Relaxing the exchange axiom's inequality $\Delta f(x;v,u) + \Delta f(y;u,v) \le 0$ to the sign patterns it forces gives quasi M-convexity (QM) and semistrict quasi M-convexity (SSQM), and requiring only some pair $(u,v)$ rather than every $u$ gives their weaker variants (QMw), (SSQMw); the minimization-only variants (SSQM$\ne$), (SSQM$\ne_w$) replace "$x,y \in \operatorname{dom} f$" with "$f(x) \ne f(y)$". The set-level analogue (Q-EXC)/(Q-EXCw) relaxes the M-convex-set exchange axiom the same way. For $\alpha \in \mathbb R$, the level set $L(f,\alpha) = \{x \in \mathbb Z^V : f(x) \le \alpha\}$. A polyhedral convex function $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (real-variable) M-convex, $f \in M[\mathbb R \to \mathbb R]$, if it satisfies the real exchange axiom (M-EXC[R]) from chunk 24-ch06d-mconvexfunctions; $L_0[\mathbb R]$ denotes polyhedra realized as $D(\gamma)$ for a triangle-inequality distance function $\gamma$, and $M_0[\mathbb R]$ denotes real M-convex polyhedral cones.

Formalization targets

Goal: the quasi M-convexity hierarchy (Theorem 6.68)

For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$: (1) the implication diagram (M-EXC[Z]) $\Rightarrow$ (SSQM) $\Rightarrow$ (QM), (M-EXCw[Z]) $\Rightarrow$ (SSQMw) $\Rightarrow$ (QMw), (M-EXC[Z]) $\Leftrightarrow$ (M-EXCw[Z]), (SSQM) $\Rightarrow$ (SSQMw), (QM) $\Rightarrow$ (QMw); (2) $f$ satisfies (M-EXC[Z]) if and only if $f[p]$ satisfies (QMw) for every $p \in \mathbb R^V$. This theorem is not named in the chunk's own extraction table — the automated extractor, which requires a result's label to start a text line, misses it because it opens mid-paragraph directly after an ASCII-rendered implication diagram — but it is the capstone of the section: its own proof is "combining Theorems 6.72 and 6.74," both formalized here as milestones, and part (2) answers exactly the question a reader of this stretch would ask: what does the entire apparatus of quasi M-convexity ultimately say about M-convexity itself?

Supporting structural targets

Fourteen further results build the hierarchy and complete the real-variable theory. Proposition 6.62 checks the two halves of chunk 24-ch06d-mconvexfunctions's Theorem 6.61 agree at integer points. Theorems 6.63–6.64 add two more characterizations of polyhedral M-convexity — via positively homogeneous directional derivatives and $L_0[\mathbb R]$-valued subdifferentials, and via $M_0[\mathbb R]$/$M_0[\mathbb Z|\mathbb R]$-valued weighted-minimizer polyhedra — to the convex-extensibility characterization chunk 23-ch06c-mconvexfunctions proved. Theorem 6.67 gives two equivalent reformulations of (QMw) as pointwise inequalities; Propositions 6.69–6.70 and Theorems 6.72–6.74 build the level-set/perturbation machinery the goal needs. Theorem 6.75 is the (SSQM$\ne_w$) analogue of Theorem 6.67. Theorem 6.76 is the quasi M-optimality criterion (optimality still characterized by local non-improvement, under only the weak quasi-convexity hypotheses). Theorems 6.77–6.79 show the M-minimizer-cut and M-proximity theorems (from missions 06-mconvex-functions-i and 23-ch06c-mconvexfunctions) hold verbatim under the strictly weaker (SSQM$\ne$) hypothesis.

Significance

The hierarchy's practical payoff is immediate: Theorems 6.77–6.79 mean the algorithms of chapter 10 that rely on minimizer cuts and proximity bounds do not actually need the full exchange axiom to run correctly on nonlinearly rescaled M-convex functions (Example 6.66 shows any nondecreasing scaling $\phi \circ f$ of an M-convex $f$ is quasi M-convex, yet nonlinear scalings are common in practice and destroy M-convexity itself). The goal, Theorem 6.68, is significant independently: it says the exchange axiom — a condition that looks irreducibly combinatorial, quantifying over pairs of points and directions — is equivalent to a purely ordinal, perturbation-based condition (every linear tilt of $f$ has no strict local improvement that a level set can't witness), giving a genuinely different lens on why M-convexity is the right discrete analogue of convexity. Theorems 6.63–6.64 close out chunk 24-ch06d-mconvexfunctions's program of characterizing polyhedral M-convexity in every classical convex-analytic vocabulary at once (directional derivatives, subdifferentials, weighted minimizers), completing the bridge to Chapter 8's duality theory that chunk builds toward.

None of these results are open — they are Murota's account of how far the exchange axiom's defining inequality can be relaxed while keeping optimization theory intact. What this mission contributes is a faithful, machine-checked formal statement of each, including four theorems (6.68, 6.76, 6.77, 6.78) the platform's own automated extractor missed entirely, extending the shared Lean vocabulary (DeltaF, QMw, LevelSet) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to prove the implication diagram's six arrows and the perturbation equivalence as six independent facts; the book's own proof of part (2) instead derives it in one step from Theorems 6.72 and 6.74 — themselves nontrivial (Theorem 6.74's proof strengthens the local exchange axiom equivalence (Theorem 6.4) to hold whenever the domain merely satisfies (Q-EXCw), then runs a bipartite-matching argument on a 4-point neighborhood to verify the resulting local condition). The difficulty is genuinely upstream of the goal's own statement: everything the goal needs is already proved by the time Theorem 6.68 is reached, so the formalization work is in stating the sixteen distinct axioms and their level-set reformulations precisely enough that "combining 6.72 and 6.74" is literally how a Lean proof would proceed.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; integer-domain functions are (V→ℤ)→WithTop ℝ, real-domain ones (V→ℝ)→WithTop ℝ. All fifteen numbered results — including the four (6.68, 6.76, 6.77, 6.78) the automated extractor missed because their labels open mid-paragraph — are placed as milestone or goal, and every clause of every one is stated in full; no partial-coverage scope reduction was needed in this chunk (contrast chunks 22-ch06b-mconvexfunctions/24-ch06d-mconvexfunctions, which restated 4-of-8-part operations theorems). Two formalization choices are recorded in HARD.md/MODERATION_NOTES.md: "$\inf f[-p] > -\infty$" is replaced by the equivalent (ArgMinOn ...).Nonempty hypothesis (WithTop ℝ has no $-\infty$ element), matching mission 23-ch06c-mconvexfunctions's identical substitution; and $M_0[\mathbb R]$/$M_0[\mathbb Z|\mathbb R]$ are realized via the book's own indicator-function device rather than a freestanding cone axiom. This mission's definitions are redeclared from chunks 06-mconvex-functions-i, 22–24-ch06*-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the fifteen sorrys are welcome; the goal and Theorem 6.74 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• M. Avriel, W. E. Diewert, S. Schaible, and I. Zang, Generalized Concavity, Plenum Press, 1988 (the continuous quasi-convexity theory this chapter's discrete analogue generalizes).

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.

Motivation

A convex polytope has two standard descriptions: as the convex hull of finitely many points, and as the intersection of finitely many half-spaces. Linear programming uses both at once. The feasible region of a linear program is given by inequalities, while the simplex method and the theory of basic solutions work with its vertices. That the two descriptions define the same class of sets is the Minkowski–Weyl theorem.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv., 1935, pp. 290–306) gave an elementary, self-contained proof of this equivalence. An English translation appeared in Contributions to the Theory of Games I (Annals of Mathematics Studies 24, 1950), where it served as the polyhedral foundation for the minimax theorem and linear inequality theory in early game theory and linear programming.

Timeline:

• Minkowski (1896, 1910): convex bodies, supporting planes and polyhedra in Geometrie der Zahlen, the setting Weyl's paper takes up.
• Farkas (1902): the lemma on homogeneous linear inequalities that is Weyl's Satz 3.
• Weyl (1935): the finite-basis theorem for cones (Hauptsatz, Satz 1), the duality between a cone and its extreme supports (§3), and the two descriptions of a convex polyhedron (§4). The paper states explicit conditions under which a finite system of inequalities defines a polytope.
• Motzkin (1936), Gale, Kuhn, Tucker (1951): systematic treatments of linear inequalities built on this foundation.

Setting

Write $(a x) = a_1 x_1 + \dots + a_n x_n$ for vectors of $\mathbb{R}^n$. A point system is a finite set $S \subseteq \mathbb{R}^n$. It is non-degenerate if no $\alpha \neq 0$ has $(\alpha s) = 0$ for all $s \in S$. A vector $\alpha \neq 0$ is a support of $S$ if $(\alpha s) \ge 0$ for all $s \in S$. A support is an extreme support if equality holds at $n-1$ linearly independent points of $S$. A point $x$ is representable by $S$ if $x = \sum_{s \in S} c_s s$ with all $c_s \ge 0$.

Read as inequalities $(a \xi) \ge 0$, $a \in S$, the same $S$ defines the cone $(S)$ of solutions. An extreme solution is a nonzero $\xi \in (S)$ at which $n-1$ linearly independent inequalities of $S$ are tight. The dual system $\Sigma$ consists of the inequalities $(\alpha x) \ge 0$, one for each extreme solution $\alpha$, and $(\Sigma)$ is the cone it defines.

For polytopes, Weyl passes to the hyperplane $x_n = -1$, identified with $\mathbb{R}^m$, $m = n-1$. A convex polyhedron is $\operatorname{conv} S$ for a finite $S \subseteq \mathbb{R}^m$ whose affine span is all of $\mathbb{R}^m$. Given a finite index set $J$, normals $A_j \in \mathbb{R}^m$ and constants $b_j \in \mathbb{R}$, the inequalities $A_j \cdot x - b_j \ge 0$ cut out a region

$$H = \{x \in \mathbb{R}^m : A_j \cdot x - b_j \ge 0 \ \text{for all } j \in J\}.$$

In Weyl's notation, row $j$ is $(\alpha x) \equiv \alpha_1 x_1 + \dots + \alpha_{n-1}x_{n-1} - \alpha_n \ge 0$, with $A_j = (\alpha_1,\dots,\alpha_{n-1})$ and $b_j = \alpha_n$.

Formalization targets

Goal: §4 II (pp. 302–303)

Assume no row is identically zero ($A_j \ne 0$ or $b_j \ne 0$). Then

$$H \text{ is a convex polyhedron} \iff \Big(\forall \pi' \in \mathbb{R}^m\ \exists \nu \ge 0:\ \pi' = \sum_j \nu_j A_j\Big) \ \wedge\ \Big(\exists c:\ A_j \cdot c - b_j > 0 \ \forall j\Big).$$

In words, the normals must positively span $\mathbb{R}^m$ and $H$ must contain an inner point. The goal is the equivalence, not either half alone.

Milestones, in the order the proof of §4 II uses them

1. Satz 1 (Hauptsatz), p. 291: for a non-degenerate $S$, every $x$ with $(\alpha x) \ge 0$ for all extreme supports $\alpha$ is representable by $S$.
2. Zusatz, pp. 294–295: a non-degenerate $S$ has no extreme support iff $0 = \sum_s c_s s$ with all $c_s > 0$.
3. Satz 3, p. 296 (Farkas): if $(p\xi) \ge 0$ on all of $(S)$, then $p$ is a nonnegative combination of $S$. This milestone is the published platform theorem LinearOptimization.farkas_cone_corollary.
4. Satz 6, p. 297: for non-degenerate $S$, $p \in (\Sigma)$ iff $(p\xi) \ge 0$ for all $\xi \in (S)$.
5. §3 II, p. 298: for non-degenerate $S$, every $\pi \in (S)$ is a nonnegative combination of finitely many extreme solutions.
6. Satz 9, p. 299: if $S$ is non-degenerate and $(S)$ has an inner point, then $\Sigma$ is non-degenerate.
7. §4 I, p. 301: a convex polyhedron $\operatorname{conv} S$ has an extreme support and equals the set cut out by its extreme supports.

Significance

The result. §4 II gives both directions of the Minkowski–Weyl theorem for full-dimensional polytopes, together with a test on the data $(A, b)$: positive spanning of the normals is equivalent to boundedness, and a strictly feasible point is equivalent to full dimension. Several parts of LP theory start from this equivalence: finiteness of the vertex set of a bounded feasible region, the existence of an optimal vertex, and the passage between the primal (inequality) and dual (generator) descriptions used in polyhedral combinatorics.

Formalizing it. The theorem has been proved since 1935; the work here is formalization. Mathlib has convex hulls, extreme points, and pointed cones with their duals, but no Minkowski–Weyl theorem for polytopes or for cones. On this platform, Farkas-type lemmas (LinearOptimization.farkas_cone_corollary) and the statement that a nonempty bounded polyhedron is the hull of its extreme points (Bertsimas–Tsitsiklis Thm 2.9) are published. Neither gives the "only if" direction, the positive-spanning criterion, or full-dimensionality.

Difficulty

The "only if" direction and the reduction from a strictly feasible bounded region to cones are routine. The hard step is the finiteness statement: why a finite set of inequalities has only finitely many generators, and why these generate the whole region. Mathlib's compactness results give "a compact convex set is the closed hull of its extreme points" (Krein–Milman). That result does not show that the extreme points are finite in number, nor that there are finitely many of them in a form that can be computed from the inequalities. Weyl's route avoids topology. It goes through the Hauptsatz, proved by induction on dimension, and the duality between $S$ and $\Sigma$. Each step of that duality needs non-degeneracy, and keeping that hypothesis alive through the dualization (Satz 9) is where care is needed.

Formalization scope

• The homogeneous space is Fin n → ℝ, with dot product ⬝ᵥ. Point systems are Finsets; the zero vector is allowed in them. "Representable" is an explicit nonnegative sum over the Finset.
• Non-degeneracy is the literal condition "$(\alpha s)=0$ for all $s \in S$ implies $\alpha = 0$", not span = ⊤.
• Extreme supports and extreme solutions quantify over all vectors with the property. Positive multiples are not identified, and no representatives are chosen.
• Extreme solutions are required to be nonzero and to lie in $(S)$. This is implicit in the paper.
• §4 is stated in affine form on Fin m → ℝ, a point $x$ standing for Weyl's $(x,-1)$. Linear independence of $n-1$ homogenized points becomes affine independence of $m$ points, and non-degeneracy becomes affineSpan ℝ S = ⊤.
• A "convex polyhedron" is the hull of a finite set with full affine span. Dropping full-dimensionality would make the "only if" false, since a segment in $\mathbb{R}^2$ has no inner point.
• Added hypotheses: no zero row in the goal (Weyl's half-spaces have nonzero normal $(\alpha_1,\dots,\alpha_n)$, p. 291). Non-degeneracy of $S$ in Satz 6 and in the p. 298 representation, where it is inherited from Satz 4.
• Condition (i) of the goal is positive spanning, i.e. nonnegative coefficients. Linear spanning of $\mathbb{R}^m$ would be strictly weaker and would make the statement false.
• A trivializing formalization is ruled out: the goal is an equivalence, "convex polyhedron" is an existential over finite point sets with full affine span, and no hypothesis restricts $J$, $m$ or the data beyond the nonzero rows. For $m = 0$ the statement is true and non-vacuous.
• Useful infrastructure, reusable beyond this mission: a Minkowski–Weyl theorem for polyhedral cones in Fin n → ℝ, extreme rays of pointed polyhedral cones, and the homogenization dictionary between cones in $\mathbb{R}^{m+1}$ and polytopes in $\mathbb{R}^m$. Proofs of any milestone, and alternative routes to the goal (e.g. via Fourier–Motzkin elimination), are welcome.

Selected references

• H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici (1935), 290–306. https://doi.org/10.1007/bf01292722
• H. Weyl, The elementary theory of convex polyhedra, in: H. W. Kuhn, A. W. Tucker (eds.), Contributions to the Theory of Games I, Annals of Mathematics Studies 24, Princeton University Press, 1950.
• J. Farkas, Theorie der einfachen Ungleichungen, Journal für die reine und angewandte Mathematik 124 (1902), 1–27. https://doi.org/10.1515/crll.1902.124.1
• H. Minkowski, Geometrie der Zahlen, Teubner, Leipzig, 1896/1910.
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (Minkowski–Weyl).

Motivation

Matroids abstract the combinatorial content of linear independence: which sets of columns of a matrix are independent, which are maximal (bases), and how bases relate to each other. This abstraction, isolated independently by Whitney (1935) and van der Waerden's school, turned out to be exactly the right level of generality for a large family of greedy and augmenting-path algorithms — a base of a matroid can always be reached from another by a sequence of single-element swaps, and this exchange property is what makes local search on bases correct and efficient.

A natural question, raised in the 1980s once matroid-based combinatorial optimization was mature, is what happens when bases are not merely present or absent but carry real-valued weights that must interact well with the exchange structure. Dress and Wenzel answered this with the notion of a valuated matroid: a real-valued function on the bases of a matroid satisfying a weighted strengthening of the exchange axiom. Their motivation was explicitly algorithmic — valuated matroids are exactly the structures for which a greedy algorithm computes an optimal basis under linear objectives, and more generally under the family of "tilted" objectives obtained by adding an arbitrary linear functional. Independently, valuated matroids arise from the classical Grassmann–Plücker relation applied to matrices over a field with a valuation (hence the name), connecting them to tropical geometry.

This mission formalizes the two theorems of Murota's Discrete Convex Analysis (2003, §2.4) that make this story precise: the classical correspondence between a matroid's base family and its rank function (Theorem 2.29), and the characterization of valuations by a perturbation-robustness property (Theorem 2.32). Theorem 2.32 is also historically the entry point of the book's central theme — it is the special case, for the two-valued lattice $\{0,1\}^V$, of the general local-exchange criterion for M-convex functions that occupies chapters 6 and 7.

Setting

Let $V$ be a finite set (the ground set). A matroid on $V$ is a pair $(V, \mathcal B)$ where $\mathcal B$, the base family, is a nonempty family of subsets of $V$ satisfying the simultaneous exchange axiom (B): for every $J, J' \in \mathcal B$ and every $i \in J \setminus J'$, there exists $j \in J' \setminus J$ such that both

$$J - i + j := (J \setminus \{i\}) \cup \{j\} \in \mathcal B \quad\text{and}\quad J' + i - j := (J' \setminus \{j\}) \cup \{i\} \in \mathcal B.$$

Equivalently (Theorem 2.29 below), a matroid can be described by its rank function $\rho : 2^V \to \mathbb Z$, a set function satisfying:

• (R1) $0 \le \rho(X) \le |X|$ for every $X \subseteq V$;
• (R2) monotonicity: $X \subseteq Y \implies \rho(X) \le \rho(Y)$;
• (R3) submodularity: $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$.

A valuation of a base family $\mathcal B$ is a function $\omega : \mathcal B \to \mathbb R$ satisfying the axiom (VM): for every $J, J' \in \mathcal B$ and $i \in J \setminus J'$, there is $j \in J' \setminus J$ with $J - i + j, J' + i - j \in \mathcal B$ and

$$\omega(J) + \omega(J') \le \omega(J - i + j) + \omega(J' + i - j).$$

The pair $(V, \omega)$ is then a valuated matroid. For $p : V \to \mathbb R$, the perturbation of $\omega$ by $p$ is

$$\omega[-p](J) = \omega(J) - \sum_{j \in J} p(j).$$

Formalization targets

Goal: Theorem 2.32 (the valuated matroid characterization)

$$\omega \text{ is a valuation of } \mathcal B \iff \forall\, p : V \to \mathbb R,\ \{J \in \mathcal B : \omega[-p](J') \le \omega[-p](J)\ \forall J' \in \mathcal B\} \text{ is a nonempty family satisfying (B)}.$$

The right-hand side says: for every linear perturbation $p$, the set of $\omega[-p]$-maximal bases is again the base family of a matroid. The universal quantifier over $p$ is not optional — a version of this statement quantified over a single fixed $p$ is either vacuous or false, and does not capture what makes valuated matroids useful.

Milestone: Theorem 2.29 (the base-family / rank-function correspondence)

The maps

$$\rho(X) = \max\{|X \cap J| : J \in \mathcal B\}, \qquad \mathcal B = \{J \subseteq V : \rho(J) = |J| = \rho(V)\}$$

are mutually inverse bijections between nonempty families satisfying (B) and set functions satisfying (R1)-(R3). This is weaker groundwork than the goal, stated first because it fixes the exact axiomatic vocabulary — (B) and (R) — that Theorem 2.32 is built on.

Significance

The result itself. Theorem 2.32 is the reason valuated matroids are the right object for weighted combinatorial optimization on matroids: it says a function on bases behaves correctly under every linear re-weighting of the ground set exactly when it satisfies the local exchange inequality (VM). This is what guarantees, for instance, that a greedy algorithm which is correct for the unweighted matroid extends correctly to families of tilted objectives, and it is the germ of the general local-optimality criterion for M-convex functions (chapters 6–7), which underlies most of the algorithmic content of the rest of the book. Theorem 2.29 is the classical result — due jointly to the development of matroid theory from the 1930s onward — that the base-exchange and rank-submodularity axiomatizations of a matroid carry the same information; it is the finite, unweighted precursor of Theorem 2.32.

Formalizing it. Neither theorem has a machine-checked proof on the platform prior to this mission (see Formalization scope for the prior-art check). Theorem 2.29's own proof is elementary but has two independent halves (each map preserves its target axiom class, and the two maps compose to the identity in both directions) that must all be established; Theorem 2.32's proof, as given in the source, defers entirely to a later, more general chapter-6 theorem, so a solver working only from this mission must either reconstruct a direct combinatorial argument for this special case or await chunk 06 (DiscreteConvex.MConvexFunctions, a separate mission) and specialize its main theorem.

Difficulty

The obvious approach to Theorem 2.32 — fix an optimal basis $J$ for $\omega[-p]$ and try to show the exchange condition on maximizers directly from (VM) — proves one direction (VM implies the maximizer property) in a few lines, since perturbing does not change which exchange moves are available. The converse is the substantial direction: from "the maximizer set is always a matroid, for every $p$," one must recover the single global inequality (VM) that must hold for all pairs $J, J' \in \mathcal B$, not just optimal ones. The standard argument constructs, for a given non-optimal pair, a perturbation $p$ under which that specific pair becomes simultaneously optimal, and this construction is exactly the step the book skips by citing chapter 6's general theorem. A formalization attempting to bypass this by only checking the maximizer property for a finite or generic sample of perturbations would trivialize the statement to something false or vacuous — a pitfall the goal's explicit ∀ p is designed to prevent.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $2^V$ is represented as Finset (Finset V), and $V \to \mathbb R$ as a plain function type. The rank function is $\mathbb Z$-valued (matching the book's own convention for matroid rank, as opposed to the $\mathbb R$-valued conventions used from chapter 6 onward for general M-convex functions); RankOfFamily is implemented with Finset.sup over $\mathbb N$ rather than a partial max', so that it is a total function — its junk value at the empty family is never invoked, since every hypothesis in this mission supplies nonemptiness explicitly, matching the book's own phrasing.

A trivializing formalization of the goal is one that quantifies over a single fixed $p$, or allows $\mathcal B$ to be empty; both are explicitly excluded by keeping $\mathcal B.\text{Nonempty}$ a hypothesis and $p$ universally quantified inside the theorem statement itself.

Checked against Mathlib (commit 0df444a360eaa60ab8c11dca51a86af692955474): Mathlib's Matroid structure is axiomatized via the single-element (asymmetric) exchange property, classically but not definitionally equivalent to Murota's simultaneous axiom (B) used throughout this book, and Mathlib provides no constructor recovering a base family or a Matroid from a bare rank function satisfying (R1)-(R3). Theorem 2.29 is therefore genuine, reusable infrastructure, not a restatement of existing Mathlib API. No reference item was found on the platform for either theorem (GET /theorems?q=matroid, q=valuated matroid return only unrelated tropical-geometry and k-server results). Contributions to a shared DiscreteConvex.Combinatorial definitions layer (the exchange and rank axioms) are welcome from later chunks of this series that build on matroid or base-polyhedron structure.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• H. Whitney, "On the abstract properties of linear dependence," American Journal of Mathematics, 57(3), 1935, pp. 509–533.
• A. W. M. Dress, W. Wenzel, "Valuated matroids," Advances in Mathematics, 93(2), 1992, pp. 214–250.
• R. A. Brualdi, "Comments on bases in dependence structures," Bulletin of the Australian Mathematical Society, 1(2), 1969, pp. 161–167.