Discrete Geometry

Motivation

Finite group equations arise when an integer program is expressed relative to an integer basis: the residue of a candidate solution in a finite Abelian group records whether it satisfies the original integrality requirement. Gomory's group polyhedron collects the nonnegative integer solutions with one prescribed residue. Its faces give valid linear inequalities for the group relaxation, so a description of those faces is useful to anyone studying integer programming cuts or the geometry of integer hulls. Gomory's 1969 paper develops the group equation and its polyhedra in this setting and then gives a finite system for the faces of the largest, or master, polyhedron. Gomory 1969, pp. 457–458, 474, 480–483.

The main question is how to recognize a facet inequality without ranging over every nonnegative integer solution of the group equation. The paper's Theorem 7 characterizes facets through a system with one row for each integer solution, an infinite collection in general. Theorem 18 replaces that family by rows determined by pairs of group elements and a rank condition at the candidate coefficient vector. Gomory 1969, pp. 469–470, 481–483.

Setting

Let $\mathcal G$ be a finite Abelian group with zero $0$, and let $\mathcal G^+=\mathcal G\setminus\{0\}$. For a subset $\mathcal N\subseteq\mathcal G^+$ and a right-hand side $g_0\in\mathcal G$, a group-equation solution is a nonnegative integer vector $t\in\mathbb N^{\mathcal N}$ satisfying

$$\sum_{g\in\mathcal N}t(g)g=g_0.$$

The set of solutions is $T(\mathcal G,\mathcal N,g_0)$, and the group polyhedron $P(\mathcal G,\mathcal N,g_0)$ is their convex hull in the real coordinate space $\mathbb R^{\mathcal N}$. The master polyhedron $P(\mathcal G,g_0)$ uses $\mathcal N=\mathcal G^+$. This mission concerns $g_0\ne0$; Gomory specifies a separate convention at $g_0=0$, excluding the zero solution from that master polyhedron. Gomory 1969, pp. 457–458, 474–475.

Gomory calls $\pi\cdot x\ge\pi_0$ a face when $\pi\ne0$, all points of $P$ satisfy the inequality, and its tight points generate the entire hyperplane $\pi\cdot x=\pi_0$ by affine combinations. Thus "face" means a facet of full hyperplane dimension here. The equivalent integer-point criterion uses the tight members of $T$, which is the representation adopted in Lean. A basic feasible solution of a linear system satisfies every equation and inequality and has tight rows whose coefficient vectors span the full variable space. Gomory 1969, pp. 468–469.

Formalization targets

The path to the goal starts with the sign of the face coefficients, the infinite-system characterization, and the shortest-path interpretation. An integer vector $t$ represents a path whose total group displacement is $\sum_g t(g)g$ and whose length is $\pi\cdot t$. The shortest-path statements lead to subadditivity and complementary equalities for face coefficients. For $P(\mathcal G,g_0)$, Theorem 17 collects the row conditions needed for the final system. Gomory 1969, pp. 469–473, 480–481.

The target is Theorem 18. Fix $g_0\ne0$ and $\pi_0>0$. With $\pi(0)=0$, system (13) is

$$\begin{aligned} \pi(g_0)&=\pi_0,\\ \pi(g)+\pi(g_0-g)&=\pi_0 &&(g\in\mathcal G^+,\ g\ne g_0),\\ \pi(g)+\pi(h)&\ge\pi(g+h) &&(g,h\in\mathcal G^+),\\ \pi(g)&\ge0 &&(g\in\mathcal G^+). \end{aligned}$$

The goal asserts the full equivalence

$$\pi\cdot x\ge\pi_0\text{ is a face of }P(\mathcal G,g_0) \quad\Longleftrightarrow\quad \pi\text{ is a basic feasible solution of (13).}$$

The equation rows, ordered pair rows, and nonnegativity rows all count toward basicness; $\pi_0$ is held fixed. Gomory 1969, pp. 481–483, Theorem 18.

Significance

Theorem 18 turns a geometric property defined against infinitely many integer vectors into a finite test in $|\mathcal G|-1$ coefficient variables. A solver can check its displayed equations and inequalities and then check whether the tight row vectors have full rank. That gives a concrete route to enumerating the facet coefficient vectors of $P(\mathcal G,g_0)$ for a fixed finite group, the use Gomory reports immediately after the proof. Gomory 1969, p. 483.

The result was proved in the paper; the work here is to formalize that known theorem and the numbered results it uses. The group-solution model, the integer-point facet criterion, and the generic tight-row definition of basic feasibility can also support other group-polyhedron arguments. The local prior-art search found related formalizations of facets and polyhedra, but none with the same integer-point-generated hyperplane and finite-group conventions, so these definitions are stated for this paper's objects.

Difficulty

Validity of the rows of (13) for a face does not by itself establish Theorem 18. Basicness requires the tight rows to span all $|\mathcal G|-1$ coefficient directions, and the converse must turn that rank information into enough tight integer solutions to generate a hyperplane. A supporting inequality that is tight at only a smaller face would pass a mere feasibility check while failing Gomory's face definition. The shortest-path results connect the group equations to the coefficient restrictions, but do not erase the rank requirement. Gomory 1969, pp. 468–470, 472–473, 481–483.

Formalization scope

Lean uses a finite Abelian group and a Finset $\mathcal N$ of nonzero elements. Its real vectors have coordinates indexed by $\mathcal N$ itself, with no unconstrained zero coordinate. The group equation is a finite sum of natural-number multiples in $\mathcal G$; $P$ is the real convex hull of the cast integer solutions. A face requires a nonzero normal, validity on every integer solution, and equality between the affine span of tight integer points and the entire hyperplane. This excludes the trivial reading that merely asks for one tight point. It also makes an empty solution set incapable of supplying a face. Theorem 7 assumes $\mathcal N$ nonempty ($n'\ge1$), as the paper does implicitly: with no coordinates every vector would be trivially basic.

Paths are represented by their nonnegative integer arc-multiplicity vectors. The same vector can describe several arc orders, but the length and group displacement used here depend only on multiplicity. Shortestness is stated by comparison with every competing vector of the same displacement; no infimum with an empty-set default is used. The complement and subadditivity rows of (13) use $\pi(0)=0$, and the subadditivity rows include ordered pairs with equal entries. Basic feasible solutions use the span of tight coefficient rows, including equation rows, in the full real space of $|\mathcal G|-1$ variables.

The mission includes the paper's Theorems 6, 7, 10, 17, Lemmas 1–2, and both numbered corollaries on p. 473 as milestones. Contributions that establish the affine-span and rank equivalences, or reusable finite-group shortest-path and polyhedral lemmas, directly advance the target. Theorems for $g_0=0$ and for other sections of the paper are outside this mission's stated domain.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. DOI: 10.1016/0024-3795(69)90017-2.

Motivation

The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph, its 1-skeleton. Whether this number is bounded by a polynomial in the dimension $d$ and the number of facets $n$ is a long-standing open question in polyhedral combinatorics; edge walks are the moves of vertex-following methods such as the simplex method, so the question bounds what any such method can achieve in the worst case. For fixed dimension, Larman proved in 1970 that the diameter grows at most linearly in $n$, with a constant exponential in $d$ (Larman 1970).

Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry of polyhedra such upper bounds actually use. They isolate a single combinatorial path property shared by the graphs of non-degenerate polyhedra and announce that the known upper bounds, Larman's among them, "continue to hold in the base abstraction" defined by that property (Dagstuhl abstract, p. 3). The next sentence of the abstract reads: "While the first bound is merely an adaption of the proof in [13], our proof of the second bound is much simpler than the one which was proved for polyhedra in [16]."

The held source is the five-page Dagstuhl extended abstract dated June 15, 2010, which states the results and proves none of them. The full proofs appear in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted theorem of the paper, not an open conjecture; the formal proof remains to be supplied.

Setting

Let $[n]=\{1,\ldots,n\}$ and write $\binom{[n]}{d}$ for the family of its $d$-element subsets. A graph $G=(V,E)$ in the base abstraction has a nonempty vertex set $V\subseteq\binom{[n]}{d}$: every vertex is a $d$-element set of labels, and distinct vertices carry distinct sets. The edges are arbitrary subject to condition i): for each $u,v\in V$ there exists a path connecting $u$ and $v$ whose intermediate vertices all contain $u\cap v$. Condition i) makes $G$ connected. The class of all such graphs is $\mathcal B_{d,n}$; $d$ is called the dimension and $n$ the number of facets of the abstraction, and $D(d,n)$ denotes the largest diameter of a graph in $\mathcal B_{d,n}$ (p. 2).

The distance $\operatorname{dist}_G(u,v)$ is the least number of edges of a path from $u$ to $v$. The motivating example is the graph of a non-degenerate polyhedron (each vertex on exactly $d$ facets), each vertex labelled by its $d$ facets: two vertices are joined by a path inside the minimal face containing both, and every vertex of that path lies on the facets the two endpoints share (pp. 2–3). The class $\mathcal B_{d,n}$ is not restricted to such graphs.

Formalization targets

Larman's bound in the base abstraction

The abstract prints the bound as $\Delta_u(d,n)\le 2^{d-1}\cdot n$ and states that it continues to hold in the base abstraction. The target is the pointwise form of $D(d,n)\le 2^{d-1}\, n$:

$$\forall d\ge 1,\ \forall n,\ \forall G\in\mathcal B_{d,n},\ \forall u,v\in V(G):\qquad \operatorname{dist}_G(u,v)\le 2^{d-1}\, n .$$

In Lean this is the existence, for every pair $u,v$, of a walk from $u$ to $v$ with at most $2^{d-1}n$ edges. The statement quantifies over every graph satisfying the paper's definition, not over polyhedron graphs or a chosen family.

Significance

For fixed $d$ the bound is linear in $n$, and it holds for a class defined only by finite sets and one path condition. Together with the almost-quadratic lower bound $D(n/4,n)=\Omega(n^2/\log n)$ announced in the same paper, it shows what this one property of polyhedra can and cannot deliver: linear growth in $n$ for fixed dimension, but not a linear bound uniform in $d$ and $n$. Since the graph of every non-degenerate polyhedron lies in $\mathcal B_{d,n}$ (a separate mission of this series), the result also recovers a Larman-type bound for polyhedra, with constant $2^{d-1}$.

Prove2Me already has proved polytope versions: Hirsch.larman_bound (the sharper constant $n\,2^{d-3}$ for nonempty bounded $H$-polytopes), Hirsch.larman_high_dimension, Hirsch.larman_layer_recursion, and Hirsch.tight_row_interval, the polytope form of the interval property that condition i) abstracts. They concern a different object, the vertex-edge graph of an $H$-polytope, and are credited as prior work; none states the bound for every graph of $\mathcal B_{d,n}$. The platform definition Hirsch_clf (connected layer families) is a related abstraction in layered form and is not the graph class used here.

Difficulty

The class contains graphs with no geometric realization, so a proof cannot use convexity, faces as polyhedra, or linear-algebraic facts about vertices; only labels, intersections and walks are available. Condition i) guarantees a path preserving the common labels of two endpoints, but says nothing directly about the length of that path. Mere connectivity on $d$-subsets of $[n]$ gives only the trivial bound $|V|-1\le\binom{n}{d}-1$, which is far from linear in $n$. A linear bound in $n$ has to be extracted from condition i) alone, uniformly over all graphs of the class. The abstract describes its proof only as much simpler than Larman's for polyhedra and states no intermediate lemma, so the mission carries no milestones.

Formalization scope

• $[n]$ is represented by Fin n, labels $0,\ldots,n-1$; only the number of labels matters.
• A vertex set is V : Finset (Finset (Fin n)) and the graph is G : SimpleGraph V; vertices are therefore distinct label sets, as in the paper. InB d n V G requires V.Nonempty, every vertex of cardinality $d$, and CondI V G.
• CondI asks for a walk all of whose vertices contain $u\cap v$. This is the source's path condition: a walk contains a path on a subset of its vertices, and the endpoints contain $u\cap v$ automatically.
• "Continue to hold in the base abstraction" is read as the bound for every graph of $\mathcal B_{d,n}$ and every pair of its vertices. No numeric $D(d,n)$ is defined, so no supremum with a default value enters; a bounded walk witnesses the distance bound.
• $d\ge 1$ is an explicit hypothesis: $d$ is the dimension, and it makes $d-1$ ordinary subtraction in $\mathbb N$. At $d=0$ the class consists only of the one-vertex graph on $\emptyset$, so nothing is lost. For $n<d$ the class is empty.
• The constant is $2^{d-1}$, the paper's constant for the abstraction; the polytope constant $2^{d-3}$ of Hirsch.larman_bound is not claimed here.

Trivializing formalizations are ruled out: labels are the vertices themselves (not an arbitrary labelling that could repeat), and condition i) is required for all pairs, not for one chosen path or only adjacent vertices. A proof only for polyhedron graphs, for graphs with extra structure, or with a larger constant leaves the goal open. Useful contributions include general lemmas about CondI and walk-length bookkeeping for SimpleGraph on a finite vertex type; these are reusable by the other missions of this series.

Selected references

• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Dagstuhl Seminar Proceedings 10211 (Flexible Network Design), 2010. https://drops.dagstuhl.de/opus/volltexte/2010/2724
• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Mathematics of Operations Research 35(4), 786–794, 2010. https://doi.org/10.1287/moor.1100.0470
• D. G. Larman, Paths on polytopes, Proceedings of the London Mathematical Society (3) 20, 161–178, 1970. https://doi.org/10.1112/plms/s3-20.1.161

Motivation

The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph. Bounding that number from the dimension and the number of facets is a central question in polyhedral combinatorics because edge walks are the discrete moves available to many vertex-based optimization methods. The Kalai–Kleitman bound gives a quasi-polynomial upper bound in these parameters. Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry is needed to retain such a bound. They isolate one path property of polyhedron graphs and show that the upper bound persists for every graph satisfying it, including graphs that need not arise from a polyhedron (Dagstuhl abstract, pp. 1–3).

This mission concerns that extension of the Kalai–Kleitman bound. The held source is the five-page Dagstuhl extended abstract dated June 15, 2010. It states the result without its proof. The full proofs appeared in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted result of the paper, not an open conjecture; the formal proof remains to be supplied.

Setting

Let $[n]=\{1,\ldots,n\}$, and let $\binom{[n]}{d}$ be the family of its $d$-element subsets. A graph $G=(V,E)$ in the paper's base abstraction has a nonempty vertex set $V\subseteq\binom{[n]}{d}$. Thus each graph vertex is labelled by a distinct $d$-element subset. The edges can be chosen freely subject to condition i): for every pair $u,v\in V$, there is a path from $u$ to $v whose intermediate vertices all contain$u\cap v$. The condition implies that the graph is connected. The paper denotes the class of these graphs by$\mathcal B_{d,n}$and calls$d$the dimension and$n$ the number of facets of the abstraction (definition and footnote, p. 2).

The distance between two vertices is the minimum number of edges in a path between them. A graph's diameter is the largest of these distances, and $D(d,n)$ is the largest diameter among graphs in $\mathcal B_{d,n}$. Condition i) is motivated by non-degenerate polyhedra: if a vertex lies on exactly $d$ facets, its tight facets provide a $d$-element label, and two vertices can be connected inside the smallest face containing them. Every vertex on that path retains the facets common to the endpoints (pp. 2–3). This motivation does not restrict $G$ to a realizable polyhedron graph.

Formalization targets

Kalai–Kleitman bound in the base abstraction

For positive dimension, the target is the pointwise form of the paper's assertion that the upper bound continues to hold in the base abstraction:

$$\forall d\geq 1,\ \forall n,\ \forall G\in\mathcal B_{d,n},\ \forall u,v\in V(G),\quad \operatorname{dist}_G(u,v)\leq n^{1+\log_2 d}.$$

Equivalently, every pair has a connecting path with at most $n^{1+\log_2 d}$ edges. Consequently $D(d,n)\leq n^{1+\log_2 d}$. The statement covers every graph with the paper's labels and condition i), rather than a selected realization or a graph with extra geometric properties. The source prints the inequality for $\Delta_u(d,n)$, its polyhedron-diameter notation, and says in the same sentence that it continues to hold for the base abstraction (p. 3).

Significance

The bound shows that a common-facet path property is enough to prevent arbitrarily large diameter once $d$ and $n$ are fixed. It extends an upper bound first attached to graphs of polyhedra to a class specified entirely by finite sets and graph paths. This locates a concrete portion of the polyhedral diameter theory within combinatorics. The same paper gives an almost-quadratic lower bound for the abstraction, so the path property alone does not imply a linear bound in $n$ (p. 3).

A machine-checked proof would connect a precise finite graph model with the real-exponent inequality, without relying on a polyhedron representation. Prove2Me already has a proved theorem called Hirsch.kalai_kleitman_bound for a bounded $H$-polytope, with a different exponent $\log_2 d+2$, and a proved Hirsch.kalai_kleitman_recursion for that polytope model. It also has Hirsch.clf_endpoint_peeling for connected layer families. Those results concern different objects or bounds and are useful prior work, but none is a formalization of the present claim for all $G\in\mathcal B_{d,n}$.

Difficulty

The class permits edges and vertex families with no geometric realization, so a proof cannot use metric or convexity properties of a particular polyhedron. Condition i) guarantees one path preserving the common labels of two endpoints; it does not directly bound that path's length. Connectivity by itself would be too weak: a connected graph on the allowed labels can have a long shortest path unless its labels and the path condition constrain it. The formal task is to obtain the claimed uniform length bound from that condition across all finite families of $d$-sets. The Dagstuhl abstract calls the argument an adaptation of Kalai and Kleitman's proof but states no intermediate lemmas, so this proposal does not assign any in-source milestones (p. 3).

Formalization scope

Lean represents $[n]$ by Fin n, with labels $0,\ldots,n-1$ instead of $1,\ldots,n$; only the number of labels matters. A vertex set is a Finset of Finset (Fin n), and a SimpleGraph has exactly those sets as vertices. This representation enforces distinct labels. InB d n V G requires $V$ to be nonempty, every label to have cardinality $d$, and CondI for every ordered pair. The walk in CondI is equivalent to the source's path: repeated vertices can be erased, and the endpoints themselves contain $u\cap v$. Nonemptiness and condition i) together give the source's connectedness. A path through all graph vertices without the common-intersection condition would be a weaker and inadmissible model.

The theorem takes $d\geq1$, so the logarithm has its ordinary positive-dimension interpretation. The source does not print a logarithm base; the statement reads it as base two, following the cited Kalai–Kleitman convention. This interpretation is explicit in the theorem's prose and is an open source-reading question. The exponent is real: the path length is cast from a natural number to $\mathbb R$ for comparison with $(n:\mathbb R)^{1+\log_2 d}$. No floor is applied to the exponent. The theorem asserts a bounded walk for each pair; that avoids defining $D(d,n)$ through a supremum with an artificial value for an empty class. At $n=0$ with $d\geq1$, InB has no instance, as there are no $d$-element labels; at $d=1$, the bound is $n$, consistent with a connected graph on at most $n$ labels.

The development needs reusable finite-set reasoning about common intersections, graph walks and their lengths, and real-logarithm bounds. Contributions establishing those facts for the paper's CondI model are within scope. A proof only for polyhedron graphs, for graphs with extra edge restrictions, or for a single chosen graph would leave the goal open.

Selected references

• F. Eisenbrand, N. Hähnle, A. Razborov and T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Dagstuhl Seminar Proceedings 10211, 2010. Extended abstract.
• F. Eisenbrand, N. Hähnle, A. Razborov and T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Mathematics of Operations Research 35, 786–794, 2010. DOI.

Motivation

The smallest enclosing ball problem asks, for finitely many points $p_1,\dots,p_n\in\mathbb{R}^d$, for a ball of the smallest radius that contains all of them. It appears in clustering, in collision detection and bounding-volume hierarchies, in facility location (placing one service point so that the farthest client is as close as possible), and in the analysis of geometric algorithms. Sylvester posed the planar version in 1857; Megiddo (1983) gave a linear-time algorithm in fixed dimension, and Welzl (1991) a simple randomized one.

This mission formalizes Section 8.7 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer, 2007), which uses the problem to introduce convex programming. Unlike the geometric problems of the book's Chapter 2, the smallest ball cannot be written as a linear program. The section shows instead that it is a convex quadratic program, derives the Karush–Kuhn–Tucker (KKT) conditions for convex programs in equational form from the duality theorem of linear programming, and uses them to prove that the smallest enclosing ball exists and is unique. It is the book's bridge from linear to convex optimization.

Setting

A function $f:\mathbb{R}^n\to\mathbb{R}$ is convex if $f((1-t)x+ty)\le(1-t)f(x)+tf(y)$ for all $x,y\in\mathbb{R}^n$ and $t\in[0,1]$. A convex program in equational form is

$$\text{minimize } f(x)\quad\text{subject to } Ax=b,\ x\ge 0,$$

with $A$ a real $m\times n$ matrix with columns $a_1,\dots,a_n$, $b\in\mathbb{R}^m$ and $f$ convex. A vector $x$ is feasible if $Ax=b$ and $x\ge 0$ componentwise, and optimal if it is feasible and $f(x)\le f(x')$ for every feasible $x'$. For differentiable $f$, $\nabla f(x)$ is the row vector of partial derivatives, so $\nabla f(x^*)(x-x^*)$ is a scalar.

For points $p_1,\dots,p_n\in\mathbb{R}^d$, write $P=\{p_1,\dots,p_n\}$ and let $Q$ be the $d\times n$ matrix whose $j$th column is $p_j$. The program studied is

$$\text{(8.15)}\qquad \text{minimize } f(x)=x^TQ^TQx-\sum_{j=1}^n x_j\,p_j^Tp_j\quad\text{subject to } \sum_{j=1}^n x_j=1,\ x\ge 0 .$$

A ball is a closed Euclidean ball $B(c,r)=\{z\in\mathbb{R}^d:\|z-c\|\le r\}$. The ball $B(c,r)$ is the unique smallest enclosing ball of a set $S$ if $r\ge 0$, $S\subseteq B(c,r)$, every ball containing $S$ has radius at least $r$, and every ball containing $S$ of radius at most $r$ has center $c$.

Formalization targets

Goal: Theorem 8.7.4

For $n\ge 1$ points $p_1,\dots,p_n\in\mathbb{R}^d$, the objective $f$ of (8.15) is convex, and

1. (8.15) has an optimal solution $x^*$;
2. there is a point $p^*$ with $p^*=Qx^*$ for every optimal $x^*$, and for every optimal $x^*$

$$-f(x^*)\ge 0\quad\text{and}\quad B\big(p^*,\sqrt{-f(x^*)}\big)\ \text{is the unique smallest enclosing ball of } P .$$

Milestones

• Fact 8.7.1. For $C\subseteq\mathbb{R}^n$ convex, $f$ differentiable and convex, and $x^*\in C$: $x^*$ minimizes $f$ over $C$ iff $\nabla f(x^*)(x-x^*)\ge 0$ for all $x\in C$.
• Proposition 8.7.2 (KKT conditions). For $f$ convex with continuous partial derivatives and $x^*$ feasible: $x^*$ is optimal iff there is $\tilde y\in\mathbb{R}^m$ with

$$\nabla f(x^*)_j+\tilde y^Ta_j\ \begin{cases}=0&\text{if } x^*_j>0,\\ \ge 0&\text{otherwise,}\end{cases}\qquad j=1,\dots,n.$$

• Lemma 8.7.3. If $s_1,\dots,s_k$ lie on the boundary of the ball $B$ with center $s^*$, then $B$ is the unique smallest enclosing ball of $\{s_1,\dots,s_k\}$ iff for every $u\in\mathbb{R}^d$ some $j$ has $u^T(s_j-s^*)\le 0$.

Significance

The result. Theorem 8.7.4 gives existence and uniqueness of the smallest enclosing ball together with an explicit certificate: the center is a convex combination $Qx^*$ of the input points, the squared radius is the negated optimum value, and the points $p_j$ with $x^*_j>0$ lie on the boundary. It reduces the geometric problem to a convex quadratic program, for which interior-point and simplex-type solvers exist, and it is the basis of the combinatorial characterization "the center lies in the convex hull of the boundary points" used by Welzl-type algorithms. Proposition 8.7.2 is the KKT theorem for equational-form convex programs; it holds without any constraint qualification because the constraints are linear.

Formalizing it. All results here are classical and proved in the book; none is open. The mission produces machine-checked statements and, when solved, proofs of: the first-order optimality criterion for convex functions on convex sets in $\mathbb{R}^n$; the equational-form KKT theorem derived from LP duality; the boundary characterization of unique smallest enclosing balls; and existence and uniqueness of the smallest enclosing ball in every dimension. Mathlib has first-order necessary conditions at local minima and general convexity theory, but no KKT theorem for linearly constrained convex programs in this form and no smallest-enclosing-ball theory.

Difficulty

Existence of an optimum and convexity of $f$ are routine. For the KKT conditions, the necessary direction needs multipliers, which do not come from calculus alone: the obvious Lagrange-multiplier argument handles only equality constraints and says nothing about the sign pattern forced by $x\ge 0$. For the goal, a solver must connect three layers — the gradient of a quadratic form in matrix notation, the multiplier conditions, and the Euclidean geometry of distances to $p^*$ — and uniqueness of the ball does not follow from uniqueness of the optimizer $x^*$, which in general is not unique (repeated or cospherical points). The statement quantifies over all optimal $x^*$ and asserts that they all yield the same center.

Formalization scope

• Vectors of $\mathbb{R}^n$ are Fin n → ℝ, so the book's indices $1,\dots,n$ become $0,\dots,n-1$. Points of $\mathbb{R}^d$ are EuclideanSpace ℝ (Fin d), so $\|\cdot\|$ and $p^Tq$ are Euclidean. The matrix $Q$ is Matrix (Fin d) (Fin n) ℝ.
• Optimality is stated against every feasible point; no infimum or supremum is taken. $\nabla f(x^*)(x-x^*)$ is the Fréchet derivative applied to $x-x^*$, and $\nabla f(x^*)_j$ its value on the $j$th unit vector. "Continuous partial derivatives" is ContDiff ℝ 1 f. Convexity is ConvexOn ℝ Set.univ f.
• Balls are closed. The squared radius $-f(x^*)$ is expressed by asserting $-f(x^*)\ge 0$ and taking the radius $\sqrt{-f(x^*)}$. "Unique ball of smallest radius" is written out as minimality of the radius among all enclosing closed balls plus equality of centers for every enclosing ball of radius at most the optimum; merely stating that the ball encloses $P$ would not be the theorem.
• The goal assumes $n\ge 1$ (for $n=0$ the feasible set is empty). In Fact 8.7.1 the minimizer $x^*$ is assumed to lie in $C$, as "minimizes $f$ over $C$" presupposes. In Lemma 8.7.3 the radius is nonnegative and each $s_j$ is at distance exactly $r$ from $s^*$.
• Needed infrastructure: gradients of quadratic forms on Fin n → ℝ, LP duality for the pair (maximize $c^Tx$, $Ax=b$, $x\ge0$) / (minimize $b^Ty$, $A^Ty\ge c$), compactness of the standard simplex, and elementary Euclidean geometry. The first-order criterion and the KKT theorem are reusable beyond this mission; proofs through any route are welcome.

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.7, pp. 184–191. https://doi.org/10.1007/978-3-540-30717-4
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441
• N. Megiddo, Linear-time algorithms for linear programming in $\mathbb{R}^3$ and related problems, SIAM J. Comput. 12(4), 1983. https://doi.org/10.1137/0212052
• E. Welzl, Smallest enclosing disks (balls and ellipsoids), in New Results and New Trends in Computer Science, LNCS 555, Springer, 1991. https://doi.org/10.1007/BFb0038202
• J. J. Sylvester, A question in the geometry of situation, Quarterly Journal of Pure and Applied Mathematics 1, 1857.

Motivation

A basic question of combinatorial geometry asks when a family of sets can be pierced (or stabbed) by few points. For intervals on the real line the answer is classical: if every two of finitely many closed intervals intersect, one point meets all of them, namely the rightmost left endpoint. This is the one-dimensional case of Helly's theorem. The situation changes as soon as the sets are allowed to have holes. Unions of two intervals can intersect pairwise without any point being common to three of them, so no single point suffices, and it is not obvious that any bound depending only on the number of holes exists.

This mission formalizes the answer given in Section 8.6 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer, 2007): pairwise intersecting unions of $d$ intervals can always be pierced by $2d^2$ points. The section uses the result to illustrate a general method of combinatorics, in which a linear programming relaxation of a covering problem is bounded through LP duality and then rounded. The same scheme, a bound on the fractional transversal number followed by a rounding step, appears across discrete geometry and combinatorial optimization.

Timeline.

• 1970: Gyárfás and Lehel prove that a bound depending only on $d$ exists; their bound is exponential in $d$ (A Helly-type problem in trees, in Combinatorial Theory and its Applications, North-Holland).
• 1992: Alon and Kleitman solve the Hadwiger–Debrunner $(p,q)$-problem with a method combining fractional transversals and LP duality (Adv. Math. 96).
• 1997: Kaiser proves the bound $d^2$ using algebraic topology (Discrete Comput. Geom. 18).
• 1998: Alon gives the short LP-duality proof of the bound $2d^2$ formalized here (Discrete Comput. Geom. 19).
• 2001: Matoušek shows that the transversal number cannot in general be below a constant multiple of $d^2/\log d$ (Discrete Comput. Geom. 26).

Setting

Fix an integer $d \ge 1$. A $d$-interval is a union of $d$ closed intervals on the real line,

$$J = [a_1,b_1] \cup \dots \cup [a_d,b_d], \qquad a_k \le b_k .$$

The numbers $a_k$ and $b_k$ are the endpoints of $J$. A finite family $\mathcal J$ of $d$-intervals is pairwise intersecting if $J_1 \cap J_2 \ne \emptyset$ for all $J_1, J_2 \in \mathcal J$. A set $X$ of real numbers is a transversal of $\mathcal J$ if every $J \in \mathcal J$ contains a point of $X$.

More generally, for a finite set $V$ and a system $\mathcal F$ of subsets of $V$: a transversal is a set $X \subseteq V$ meeting every member; the transversal number $\tau(\mathcal F)$ is the smallest size of a transversal; a matching is a subsystem of pairwise disjoint members, and the matching number $\nu(\mathcal F)$ is the largest size of a matching. The fractional transversal number $\tau^*(\mathcal F)$ is the optimal value of the linear program

$$\min \sum_{v\in V} x_v \quad \text{s.t.} \quad \sum_{v \in F} x_v \ge 1 \ (F \in \mathcal F),\ x \ge 0,$$

and the fractional matching number $\nu^*(\mathcal F)$ is the optimal value of

$$\max \sum_{F\in\mathcal F} y_F \quad \text{s.t.} \quad \sum_{F :\, v \in F} y_F \le 1 \ (v \in V),\ y \ge 0 .$$

Formalization targets

Goal: Theorem 8.6.1

$$\mathcal J \text{ finite, pairwise intersecting family of } d\text{-intervals} \;\Longrightarrow\; \exists X \subset \mathbb R,\ |X| \le 2d^2,\ X \cap J \ne \emptyset \ \ \forall J \in \mathcal J .$$

This is the book's theorem with its constant $2d^2$.

Milestones

1. Lemma 8.6.2. If $J_1,\dots,J_n$ ($n \ge 1$, repetitions allowed) are $d$-intervals with $J_i \cap J_j \ne \emptyset$ for all $i,j$, then some endpoint of some $J_i$ lies in at least $n/2d$ of the $J_j$.
2. §8.6, p. 182. For every finite set system with nonempty members,

$$\nu(\mathcal F) \le \nu^*(\mathcal F) = \tau^*(\mathcal F) \le \tau(\mathcal F).$$

3. Lemma 8.6.3. If $\mathcal J$ is a finite pairwise intersecting family of $d$-intervals and $P$ its set of endpoints, there are weights $x_p \ge 0$, $p \in P$, with $\sum_{p \in J \cap P} x_p \ge 1$ for every $J \in \mathcal J$ and $\sum_{p\in P} x_p \le 2d$.

Significance

The result. Theorem 8.6.1 shows that the piercing number of pairwise intersecting $d$-intervals is bounded by a function of $d$ alone, and that this function is polynomial. The section also states, without proof, the extension $\tau(\mathcal J) \le 2d^2\,\nu(\mathcal J)$ for arbitrary finite families of $d$-intervals. Upper bounds of this kind feed into piercing and hitting-set questions for families with bounded "complexity", and the chain $\nu \le \nu^* = \tau^* \le \tau$ is the standard frame in which such bounds are proved.

Formalizing it. The theorem, both lemmas and the duality chain are proved in the literature and in the book. None of them is on the platform. The work consists of formalizing the book's proof: a double-counting argument, LP duality for the pair of fractional programs together with the rationality of an optimal basic solution, and a rounding step. The general-set-system milestone is reusable for any transversal problem, independent of $d$-intervals.

Difficulty

The obvious generalization of the one-dimensional argument fails: for $d \ge 2$ no point need be common to all members, so there is no single extremal endpoint to choose, and a greedy piercing procedure has no control over how many points it uses. The difficulty is to obtain a bound that does not depend on the size of the family. In the book's route the counting statement of Lemma 8.6.2 holds only for equal weights, while the fractional programs produce arbitrary real weights, and the passage between the two, as well as the passage from a fractional transversal of small total weight to an actual finite set of points, are the steps that need care.

Formalization scope

A $d$-interval is stored as data: two functions left, right : Fin d → ℝ with left k ≤ right k, together with the set toSet $= \bigcup_k [a_k,b_k]$. Components are indexed $0,\dots,d-1$. Endpoints are those of the given components, so they depend on the representation, as in the book's proofs. Families are Finsets of such data; Lemma 8.6.2 uses a Fin n-indexed sequence, since the proof of Lemma 8.6.3 applies it to a sequence with repetitions. The hypotheses $d \ge 1$ (the book's definition) and, in Lemma 8.6.2, $n \ge 1$ are explicit. The quantity $n/2d$ is real division. Transversal sizes are cardinalities of a Finset ℝ bounded by $2d^2$.

For set systems, $V$ is a finite type and $\mathcal F$ a Finset (Finset V) with nonempty members; without this assumption no transversal exists and both fractional programs degenerate. The numbers $\tau^*$ and $\nu^*$ are expressed through optimal feasible solutions, not as infima or suprema, so no junk value of an empty or unbounded set is involved. $\tau$ is an sInf over $\mathbb N$ that is attained under the nonemptiness assumption, and $\nu$ is a maximum over the finite family of matchings.

A trivializing formalization is ruled out: the pairwise-intersection hypothesis is satisfiable by nonempty families, the transversal is required to meet the actual sets $J$, not a representation artifact, and the bound $2d^2$ and $2d$ are the book's constants, not weakened ones.

Needed infrastructure: finite sums over Finset ℝ, LP duality for a finite primal–dual pair in inequality form (or a direct proof of the chain), rationality of an optimal vertex, and a left-to-right sweep over a sorted finite set of reals. Contributions of a general LP duality statement for set-system relaxations are welcome and reusable.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.6. https://doi.org/10.1007/978-3-540-30717-4
• N. Alon, Piercing d-intervals, Discrete Comput. Geom. 19 (1998) 333–334.
• N. Alon, D. Kleitman, Piercing convex sets and the Hadwiger–Debrunner (p, q)-problem, Adv. Math. 96 (1992) 103–112.
• T. Kaiser, Transversals of d-intervals, Discrete Comput. Geom. 18 (1997) 195–203.
• J. Matoušek, Lower bounds on the transversal numbers of d-intervals, Discrete Comput. Geom. 26 (2001) 283–287.
• A. Gyárfás, J. Lehel, A Helly-type problem in trees, in Combinatorial Theory and its Applications (P. Erdős, A. Rényi, V. T. Sós, eds.), North-Holland, 1970, 571–584.

Motivation

The Thomson problem asks for the configuration of $N$ electrons, constrained to the surface of the unit sphere and repelling each other according to Coulomb's law, that minimises the total electrostatic potential energy. J. J. Thomson posed it in 1904 in connection with his "plum pudding" atomic model. The same energy-minimisation question reappears in the arrangement of protein subunits in spherical virus shells, in colloidosomes, in fullerene patterns and in multi-electron bubbles, and it is a special case ($s=1$) of the Riesz $s$-energy problem on the sphere; the logarithmic variant is Smale's 7th problem.

Despite its elementary statement, the minimum is rigorously known only for a handful of values of $N$.

Timeline of exact solutions (as reported in the source).

• $N=1,2$: trivial; for $N=2$ the optimum is an antipodal pair with $U=1/2$.
• $N=3$: equilateral triangle on a great circle — L. Föppl (1912).
• $N=4$: regular tetrahedron (listed in the source without a citation).
• $N=6$: regular octahedron — V. A. Yudin (1992).
• $N=12$: regular icosahedron — N. N. Andreev (1996).
• $N=5$: triangular bipyramid — R. Schwartz (2013), computer-assisted.
• $N=7$: pentagonal bipyramid — long observed numerically; in September 2026 an exact, Lean-kernel-checked proof was claimed (H. Tran, Vals AI).
• $N=8$ and $N=20$: numerically, the optimum is not the cube, resp. the dodecahedron.

Setting

A configuration of $N$ points is a map $x:\{0,\dots,N-1\}\to\mathbb R^3$. It is admissible if every point lies on the unit sphere, $\|x_i\|=1$, and the points are pairwise distinct. In units with $e=1$ and $k_e=1$ its Coulomb energy is

$$U(x)=\sum_{0\le i<j\le N-1}\frac{1}{\|x_i-x_j\|}.$$

An admissible $x$ is an energy minimiser (solves the Thomson problem for $N$) if $U(x)\le U(y)$ for every admissible $N$-point configuration $y$.

Explicit candidate configurations are fixed in the definitions file: the antipodal pair ($N=2$), an equatorial equilateral triangle ($N=3$), the regular tetrahedron ($N=4$), the triangular bipyramid ($N=5$), the regular octahedron ($N=6$), the pentagonal bipyramid ($N=7$: the two poles plus a regular pentagon $(\cos\tfrac{2\pi k}5,\sin\tfrac{2\pi k}5,0)$ on the equator) and the regular icosahedron ($N=12$).

Formalization targets

Goal: $N=7$

$$\text{the pentagonal bipyramid is an energy minimiser for } N=7 .$$

This asserts admissibility of the seven points and the inequality $U(P_7)\le U(y)$ against every admissible seven-point configuration $y$. It fixes no numerical value of the minimum and does not assert uniqueness.

Milestones: the other known exact solutions

$$N=1:\ U\equiv 0;\qquad N=2:\ \text{antipodal pair optimal},\ U=\tfrac12;$$ $$N=3,4,5,6,12:\ \text{triangle, tetrahedron, triangular bipyramid, octahedron, icosahedron are energy minimisers.}$$

Significance

The result. Among the values of $N$ listed in the source, $N=7$ is the smallest one whose optimum was, until the 2026 claim, supported only by numerical computation; the cases $N\le 6$ and $N=12$ were settled earlier. Settling $N=7$ extends the short list of rigorously known Thomson minimisers.

Formalizing it. The $N=7$ result reported in the source is recent and described there as a claimed Lean-kernel-checked proof; a formalization on this platform against a public, reviewed statement would corroborate it independently. For the milestones, the source attributes the $N=3,5,6,12$ cases to published proofs (Föppl 1912, Schwartz 2013, Yudin 1992, Andreev 1996); the source does not describe machine-checked proofs of these, and each is a self-contained formalization target.

Difficulty

The energy is a non-convex function on the configuration space $(S^2)^N$ with many critical points, so numerical minimisation — which is how most entries of the source's table of smallest known energies were obtained — does not certify global optimality. The $N=5$ case, the most recent classical entry before $N=7$, was resolved only with a computer-assisted proof (Schwartz 2013).

Formalization scope

Points live in EuclideanSpace ℝ (Fin 3); configurations are functions Fin N → EuclideanSpace ℝ (Fin 3). Admissibility requires unit norm and injectivity (distinct points), matching the source's "$N$ distinct points". The energy sums $1/\mathrm{dist}(x_i,x_j)$ over $i<j$; Lean's $1/0=0$ convention is harmless because coincident points are excluded by admissibility. The candidate configurations are fixed in one particular orientation; since the energy is invariant under orthogonal maps and relabelling, this is no loss of generality. The statement "$x$ is an energy minimiser" includes admissibility of $x$ itself, so the goal cannot be satisfied by a degenerate candidate.

Reusable infrastructure welcome: energy invariance under isometries and permutations, existence of minimisers by compactness, linear-programming (Delsarte–Yudin) bounds on the sphere, and interval-arithmetic tooling for certified numerical bounds.

Selected references

• Wikipedia, Thomson problem (source of this mission). https://en.wikipedia.org/wiki/Thomson_problem
• J. J. Thomson, On the Structure of the Atom…, Philosophical Magazine 7 (1904), 237–265.
• L. Föppl, Stabile Anordnungen von Elektronen im Atom, J. Reine Angew. Math. 141 (1912), 251–301. https://doi.org/10.1515/crll.1912.141.251
• V. A. Yudin, The minimum of potential energy of a system of point charges, Discrete Math. Appl. 3 (1993), 75–81. https://doi.org/10.1515/dma.1993.3.1.75
• N. N. Andreev, An extremal property of the icosahedron, East J. Approx. 2 (1996), 459–462.
• R. Schwartz, The five-electron case of Thomson's problem, Experimental Mathematics 22 (2013), 157–186. https://arxiv.org/abs/1001.3702
• S. Smale, Mathematical Problems for the Next Century, Math. Intelligencer 20 (1998), 7–15. https://doi.org/10.1007/bf03025291
• Vals AI, A Lean Proof of the Thomson Problem for Seven Electrons (2026). https://www.vals.ai/blogs/thomson-n7-lean-proof

Motivation

This mission continues chapter 11's account of the M♮-concave/M♮-convex exchange-economy model begun in mission 14-economic-equilibrium, placing seven of that chunk's own results that were previously left out-of-cone: the two gross-substitutes-style characterizations of M♮-concavity (§11.3), the transfer theorem that lifts an equilibrium of the continuous relaxation to one for indivisible commodities (§11.4), and the explicit polyhedral description of the equilibrium price set together with its feasibility criterion (§11.5).

Setting

Mission 14-economic-equilibrium built the exchange-economy vocabulary this mission redeclares in full (UDom, ArgMaxBot/ArgMinTop, PriceShift/PriceShiftConvex, DemandSet/SupplySet, IsEquilibrium, MNaturalConcave, IsMNaturalConvexSet, the concave/convex closures ConcaveClosureR/ConvexClosureR and their continuous analogues ContDemandSet/ContSupplySet/ IsContEquilibrium) and placed the qualitative structural theorems (Theorems 11.1-11.3, 11.4, 11.16-11.18, 11.23-11.24). This mission adds the gross-substitutes axioms (−M♮-GS[Z], the price-monotonicity property NegGS, and −M♮-SWGS[Z], its one-price-at-a-time refinement NegSWGS), the M♮-convex-set transfer machinery connecting a continuous equilibrium to a discrete one, and the equilibrium price polyhedron built from the three bound families ℓ(j), u(j), u(i,j) (Eqs. (11.40)-(11.42)) that make Theorem 11.16's qualitative L♮-convex-polyhedron fact concrete and linear-programming-checkable.

Formalization targets

Goal: The equilibrium price set is the explicit L♮-convex polyhedron (11.43) (Theorem 11.21)

For a fixed allocation (x,y), the set P* of all equilibrium price vectors is an L♮-convex polyhedron and equals the polyhedron cut out by max{0,ℓ(j)} ≤ p(j) ≤ u(j) and p(j)-p(i) ≤ u(i,j). Chosen as goal: it is the sharpest structural result of chapter 11's computation section, upgrading Theorem 11.16's qualitative fact to a concrete description, and is what Theorem 11.22 (also placed) builds on directly.

Supporting structural targets

Theorem 11.5 and Theorem 11.6 characterize M♮-concavity via the gross-substitutes and stepwise gross-substitutes properties, completing chapter 11's suite of M♮-concavity characterizations begun with Theorem 11.4 (mission 14). Theorem 11.15 is the general transfer theorem (continuous equilibrium ⟹ discrete equilibrium) that mission 14's own Theorem 11.14 invokes as a special case. Theorem 11.22 gives the feasibility criterion for the existence of an equilibrium price vector, the mission's second theorem built on the equilibrium price polyhedron.

Significance

Together with mission 14-economic-equilibrium, this mission completes the book's account of how M♮-concavity/convexity — a purely combinatorial exchange condition — reproduces, and sharpens, the classical gross-substitutes theory of competitive equilibrium for economies with indivisible goods: existence transfers from the continuous relaxation, and the equilibrium price set itself has a description exact enough to reduce to a linear feasibility question. None of these results are open — they are Murota's own account (attributed in the book's own notes to Danilov-Koshevoy- Lang and Murota-Tamura for the gross-substitutes theorems, and to Murota-Tamura for the equilibrium price polyhedron); this mission contributes a faithful, machine-checked formal statement of each (see Formalization scope).

Difficulty

Two of this chunk's seven BRIEF.md results are not drafted this pass, for a disclosed time- budget reason rather than any faithfulness failure: Proposition 11.19 and Theorem 11.20 require the H,L-indexed bipartite MSFP2 flow-network vocabulary (separate vertex sets V+_e, V+_l, V-_h, an M-convex/M-concave-combining flow objective) that neither this mission nor mission 14 builds, and building it in proportion to placing exactly these two results was judged disproportionate to the remaining time in this pass; see HARD.md and STATUS.md. This is explicitly not a hard exclusion — both results are well-posed and provable from the book's own complete proofs — and is recorded as an honest scope limitation for a future pass. Theorem 11.22's own trailing algorithmic remark (that equilibrium prices can be found via a shortest-path computation, yielding a polynomial-time equilibrium-checking algorithm) is a computational/ complexity claim outside this series' propositional-formalization methodology and is omitted; the mathematical "iff feasibility" content is placed in full. See HARD.md.

Formalization scope

Ground set K is a Fintype with DecidableEq; consumer/producer index sets H, L are Fintypes (Nonempty where the price-bound formulas (11.40)-(11.42) need a nonempty sup'/inf' range). All base vocabulary is redeclared fresh from mission 14-economic-equilibrium's own definitions, since this draft cannot import that sibling mission. The gross-substitutes axioms are formalized directly from their defining inequalities (Eqs. preceding (11.19) and following, and p.331); the equilibrium price polyhedron's bound families ℓ(j)/u(j)/u(i,j) are formalized literally from Eqs. (11.40)-(11.42), extracting each WithBot ℝ/WithTop ℝ operand to ℝ before subtracting (since WithBot ℝ carries no subtraction instance). Two results (Proposition 11.19, Theorem 11.20) are not drafted this pass for the disclosed time-budget reason above; one result (Theorem 11.22's trailing algorithmic remark) is scoped out as computational content. Contributions completing any of the five sorrys, or building the MSFP2 vocabulary to place Proposition 11.19/Theorem 11.20 in a follow-up mission, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• V. Danilov, G. Koshevoy, K. Murota, "Discrete convexity and equilibria in economies with indivisible goods and money," Mathematical Social Sciences, 41 (2001), pp. 251-273 [33] (origin of the gross-substitutes characterization, Theorem 11.6).
• K. Murota, A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [160] (origin of the equilibrium price polyhedron, Theorems 11.20-11.22).

Motivation

Chapter 10 turns from structure theory to algorithms: efficient methods for minimizing M-convex functions (via domain reduction) and submodular set functions (via Schrijver's and the Iwata-Fleischer-Fujishige scaling algorithms). Most of chapter 10's numbered results are asymptotic running-time bounds for specific procedural algorithms — a genuinely different kind of claim from the rest of this book (see Formalization scope). This mission places the results of this block that ARE ordinary mathematical propositions: correctness certificates, min-max theorems, and structural facts the algorithms rely on and produce.

Setting

For an M-convex set B ⊆ Z^V, the central part B° (the vectors of B lying away from its boundary, defined via per-coordinate bounds ℓ°_B, u°_B) is what the domain reduction algorithm searches from. For a submodular set function ρ : 2^V → R, the base polyhedron B(ρ) and its extreme bases (one per linear ordering of V, via Eq. (10.12)) let any base be written as a convex combination of finitely many extreme bases (Eq. (10.13)); a candidate minimizer W is certified via the linear orderings representing an optimal base. The Iwata-Fleischer-Fujishige (IFF) scaling algorithm relaxes this problem with a flow-augmentation parameter δ, maintaining a δ-feasible flow φ and vector z = x + ∂φ; near the end of a scaling phase, no augmenting path and no "active triple" together certify near-optimality.

Formalization targets

Goal: Near-optimality from the absence of augmenting paths (Proposition 10.20)

If S ⊆ W ⊆ V∖T, no arc of the auxiliary network leaves W, and no active triple exists, then z⁻(V) ≥ ρ(W)-nδ and x⁻(V) ≥ ρ(W)-n²δ; moreover W exactly minimizes ρ once δ is small enough relative to the smallest positive gap between two values of ρ. Chosen as goal: the book calls this "a key property of the scaling algorithm" and "a relaxation version of the min-max relation in Proposition 10.8", its own proof is the most substantial argument among this chunk's placed results, and Proposition 10.23 is a direct corollary of it.

Supporting structural targets

Proposition 10.8 is the min-max relation underlying the whole of section 10.2 (an Edmonds- intersection-theorem consequence, found by direct reading — the extractor's table missed it). Proposition 10.9 gives the three-part sufficient condition for optimality, in terms of the linear orderings representing an optimal base, that both Schrijver's algorithm and the IFF algorithm use as their termination criterion (also found by direct reading). Propositions 10.5-10.6 establish that the domain reduction algorithm's central part B° is always nonempty, via an explicit vector-extension step (Proposition 10.5 likewise missing from the extractor's table). Proposition 10.23 fixes individual coordinates once a scaling phase ends, and Proposition 10.24 gives the termination certificate for the IFF fixing algorithm's own separate graph-contraction procedure.

Significance

Chapter 10 is where this book cashes out its structure theory as algorithms with provable running times, and this mission places every result of that chapter's first two sections that is a mathematical proposition rather than a runtime bound: two min-max/optimality-certificate theorems (10.8-10.9) that are the combinatorial core making the following two strongly polynomial algorithms (Schrijver's, and Iwata-Fleischer-Fujishige's) correct, one central-part nonemptiness fact (10.5-10.6) underlying the domain reduction algorithm, and the two fixing/termination certificates (10.23-10.24) that let the scaling algorithms actually output a minimizer with a proof of optimality attached, not just a numerical answer.

None of these results are open — they are Murota's own account of submodular-function- minimization algorithms (sections 10.1-10.2). What this mission contributes is a faithful, machine-checked formal statement of each, including two results (Propositions 10.5 and 10.8) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

Six numbered results in this block (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are excluded as hard: each states a Big-O asymptotic bound on the running time, function-evaluation count, or internal-procedure-call count of a specific iterative algorithm (the domain reduction algorithm, its scaling variant, Schrijver's algorithm, the IFF scaling algorithm). Faithfully stating "this algorithm runs in O(g(n)) time" requires a cost-tracked operational semantics for that specific algorithm — a well-founded recursive procedure with an oracle for evaluating the input function, threading a step/evaluation counter, instantiated over an unbounded family of ground-set sizes n and numeric parameters (K∞, M) — which is a fundamentally different kind of formalization task (computational complexity theory) from every one of the roughly 280 other numbered results in this book, none of which require modeling the cost of computing them. See HARD.md.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq. Base M-convex-set vocabulary is redeclared from prior missions. Linear orderings of V are represented as bijections V ≃ Fin (Fintype.card V) rather than as lists, matching this series' established preference for order-indexed families over sequential data structures. Proposition 10.5's witness vector is stated as an existence claim (the mathematical content of the proposition), rather than by reconstructing the specific recursive modification procedure the book uses to produce it — a choice consistent with how this series has always formalized "the algorithm produces X" claims where X is a mathematical property, by asserting X's existence rather than executing the algorithm (see, e.g., mission 33-ch09c-networkflows's cycle-cancellation theorem). Six numbered results (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are hard; see HARD.md. Contributions completing any of the seven sorrys are welcome; the goal and Proposition 10.9 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• S. Iwata, L. Fleischer, and S. Fujishige, "A combinatorial strongly polynomial algorithm for minimizing submodular functions," Journal of the ACM, 48 (2001), pp. 761-777 [102] (the IFF scaling algorithm this mission's Proposition 10.20 certifies).
• A. Schrijver, "A combinatorial algorithm minimizing submodular functions in strongly polynomial time," Journal of Combinatorial Theory, Series B, 80 (2000), pp. 346-355 [182] (Schrijver's algorithm, whose termination criterion is Proposition 10.9).

Motivation

Mission 32-ch09b-networkflows established the potential and negative-cycle optimality criteria for M-convex submodular flow problems. This mission finishes chapter 9 with the two topics that close it out: the constructive engine behind the negative-cycle criterion — cycle cancellation, which actually improves a nonoptimal flow rather than merely detecting suboptimality, resting on a delicate "unique-min condition" for bipartite matchings — and network duality, the chapter's capstone structural theorem showing that M-convexity and L-convexity are preserved (and their conjugacy is preserved) under transformation by an arbitrary network.

Setting

For a feasible integer flow ξ in the M-convex submodular flow problem MSFP2, a negative cycle in the auxiliary network (Gξ,ℓξ) witnesses suboptimality (mission 32's Theorem 9.20); cycle cancellation modifies ξ along a smallest such cycle to produce a strictly better flow ξ̄ (Eq. (9.75)). The unique-min condition for a pair (x,y) of integer vectors with ‖x-y‖∞=1 asks whether the bipartite graph G(x,y) — vertices the positive/negative supports of x-y, weights the M-convex exchange values Δf(x;v,u) — has a unique minimum-weight perfect matching; when it does, the M-convex exchange inequality of Proposition 6.25 becomes an equality. Separately, a network G=(V,A;S,T) with entrance set S and exit set T transforms a pair of functions f,g on Zˢ into induced functions f̃,g̃ on Zᵀ (Eqs. (9.81)-(9.82)), the minimum cost to meet a boundary specification at the exit given a production cost at the entrance and a transportation cost along arcs.

Formalization targets

Goal: Network duality for Z→Z functions (Theorem 9.26)

M-(resp. M$^\natural$-)convexity and integer-valuedness of f transfer to the induced f̃; L-(resp. L$^\natural$-)convexity and integer-valuedness of g transfer to g̃; and if f is M$^\natural$-convex, g is its L$^\natural$-conjugate, and each arc cost ga is the conjugate of fa, then g̃ is the conjugate of f̃. Chosen as goal: the book calls this "the harmonious relationship between network flow and M-/L-convexity", its own proof runs roughly six pages (the longest argument in this chunk), and it is the general fact from which Theorems 9.27-9.28 (analogues for other type combinations) and Notes 9.29-9.30 (the aggregation and infimal- convolution closure properties of M-convex functions, already placed in mission 22-ch06b-mconvexfunctions's own Theorem 6.13) all descend.

Supporting structural targets

Theorem 9.22 shows cycle cancellation strictly improves the objective; Propositions 9.23-9.25 are "the key ingredient" behind it: Proposition 9.23 shows the unique-min condition upgrades the M-convex exchange inequality to an equality, Proposition 9.24 gives a checkable characterization of when a bipartite weighted graph has a unique minimum-weight perfect matching, and Proposition 9.25 is the fact that makes the machine run — the specific pair (∂ξ,∂ξ̄) arising from cycle cancellation always satisfies the unique-min condition. Theorems 9.27 and 9.28 are the network duality theorem's own analogues for Z→R and R→R functions, the second restoring the conjugacy assertion (missing for Z→R) via the ordinary real Legendre-Fenchel transform.

Significance

Cycle cancellation is this book's constructive answer to the negative-cycle criterion: not just a certificate of suboptimality, but an actual improvement step, the combinatorial core of the cycle-canceling algorithm explained in section 10.4.3 (mission 35-ch10c-algorithms). Its correctness proof is one of the most intricate combinatorial arguments in the entire book — a proof by contradiction using a multiset-union identity (Eq. (9.80)) to derive a smaller negative cycle from an assumed non-uniqueness, itself resting on Proposition 9.24's Monge-like characterization of unique bipartite matchings. Network duality, meanwhile, is the theorem that explains why discrete convex analysis and network flow theory are so tightly intertwined throughout this book: it is the general mechanism (matroid induction, min-max relations, the M-convex aggregation and infimal-convolution closure properties) underlying nearly every construction chapter 2 introduced informally and chapter 6 proved piecemeal.

None of these results are open — they are Murota's own account of cycle cancellation (section 9.5.2) and network duality (section 9.6). What this mission contributes is a faithful, machine-checked formal statement of each, completing the platform's coverage of chapter 9 begun in missions 12-network-flows and 32-ch09b-networkflows; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

Theorem 9.26's own proof needs the full weight of everything chapter 9 has built (Theorem 9.16's potential criterion for integer flows, the conjugacy theorem of chapter 8), which this mission does not re-prove (proofs are sorry throughout, per this pass's scope) but whose statement still needs the induced-function machinery built faithfully: since the general framework's optimal-value-type quantities can genuinely be -∞ (the book's own blanket hypothesis f̃ > -∞ acknowledges this), InducedFTilde/InducedGTilde are EReal-valued, following the same soundness discipline established in mission 31-ch08d-conjugacyduality for Lagrangian duality's derived quantities.

Formalization scope

Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity vocabulary is redeclared from prior missions. Functions "on Zˢ" for S a proper subset of the ground set are represented as ordinary V→Z functions required to vanish outside S (SupportedOn), rather than as functions on a dependent subset type — a padding-with-zero encoding consistent with this whole series' preference for a single ambient ground-set domain. C[R→R] (univariate real polyhedral convex functions, needed only for Theorem 9.28's arc costs) is formalized as ordinary midpoint-style convexity (IsConvexUnivariateR) rather than the book's own polyhedral characterization, since polyhedrality plays no role in Theorem 9.28's conclusion beyond ensuring the induced functions are well-behaved. All seven numbered results found in this chunk's page range are placed in full, with no partial-coverage scope reduction. Contributions completing any of the seven sorrys are welcome; the goal and Proposition 9.25 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota, "Valuated matroid intersection," SIAM Journal on Discrete Mathematics, 9 (1996), pp. 545-561 [135] (the unique-max lemma Proposition 9.23 reformulates, and the proof technique behind Proposition 9.25).
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (network duality and cycle cancellation for the M-convex submodular flow problem).

Motivation

Chapter 9 is where discrete convex analysis meets classical network flow theory: the minimum cost flow problem's three hallmark properties — an optimality criterion by potentials, an optimality criterion by negative cycles, and integrality of optimal solutions — are shown to survive, in a precise and increasingly general form, first for arbitrary polyhedral convex costs (MCFP3), then for the M-convex submodular flow problem (MSFP2/MSFP3), the chapter's own combinatorial generalization of the classical problem. This mission places the potential criterion (Theorem 9.4) and its cascade of six corollaries and generalizations, the block of results this book's own text uses to carry every other result in the chapter.

Setting

A digraph G = (V,A) with tail/head maps ∂⁺,∂⁻ : A → V. A flow ξ : A → R has boundary ∂ξ(v) = Σ{ξ(a) : ∂⁺a=v} − Σ{ξ(a) : ∂⁻a=v}. A potential p : V → R has coboundary δp(a) = p(∂⁺a) − p(∂⁻a). The minimum cost flow problem MCFP3 minimizes Γ₃(ξ) = Σₐ fₐ(ξ(a)) + f(∂ξ) over flows, for polyhedral convex arc costs fₐ : R → R∪{+∞} and boundary cost f : Rⱽ → R∪{+∞}; MCFP0 is its linear-cost, fixed-supply special case. The M-convex submodular flow problem MSFP3 is MCFP3 with f additionally M-convex; MSFP2 is its linear-arc-cost special case.

Formalization targets

Goal: The potential criterion for MCFP3 (Theorem 9.4)

For a feasible flow ξ, ξ is optimal for MCFP3 iff there is a potential p with ξ(a) a minimizer of the reduced arc cost fₐ[δp(a)] for every arc and ∂ξ a minimizer of the reduced boundary cost f[−p]; and any such optimal potential characterizes optimality of every feasible flow. This is the hub result of the whole chunk: the book states Theorem 9.14 is "immediate" from it, and every other placed result either specializes it directly or builds on that specialization.

Supporting structural targets

Theorem 9.5 reformulates MCFP0's optimality as the absence of a negative cycle in an auxiliary network; Theorem 9.6 gives MCFP0's primal and dual integrality, the latter identifying the optimal-potential set as an L-convex polyhedron. Theorem 9.14 specializes the goal to MSFP3; Theorem 9.15 upgrades this to a full polyhedral and integrality structure theorem for MSFP3's optimal-flow-boundary and optimal-potential sets (M2-convex and L-convex polyhedra respectively); Theorem 9.16 is the integer-flow analogue, with the boundary set now literally M2-convex and the integer-optimal-potential set literally L-convex. Theorems 9.18 and 9.20 give the negative-cycle reformulation for MSFP2, real and integer flows respectively, generalizing Theorem 9.5 by admitting a third class of auxiliary arcs governed by the M-convex boundary cost's directional derivative (or its discrete difference, in the integer case).

Significance

This is the chapter's demonstration that M-convexity is not merely an abstract combinatorial axiom but the exact structural hypothesis under which classical network-flow duality survives intact: every one of the four "nice properties" the book opens the chapter with (potentials, negative cycles, integrality, efficient algorithms) is preserved verbatim in the M-convex generalization, and this mission's eight results are the proof of that claim for the first three. The chunk's own internal dependency structure — one foundational theorem (9.4) from which every other placed result descends by specialization or direct generalization — is itself characteristic of how this book organizes its combinatorial machinery around a single convex- analytic core.

None of these results are open — they are Murota's own account of network flow duality under M-convexity (sections 9.1, 9.4, and 9.5). What this mission contributes is a faithful, machine-checked formal statement of each, extending the platform's coverage of chapter 9 begun in mission 12-network-flows (which covered §9.1.1-9.1.2 and §9.3, the feasibility and max-flow min-cut results, deliberately leaving this block for later apparatus); no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The eight results span real- and integer-flow versions of two nested problem hierarchies (MCFP0 ⊂ MCFP3, MSFP2 ⊂ MSFP3) and two distinct optimality certificates (potentials, negative cycles), which this mission handles by building one shared apparatus — FeasibleFlowMCFP3, Gamma3, OptimalFlowMCFP3, IsOptimalPotential — that MCFP0 and MSFP3 both instantiate (MCFP0 literally as the linear-cost/singleton-boundary special case of Eq. (9.11)), and one shared generic cycle/negative-cycle apparatus (IsCycle, CycleLength, HasNegativeCycle) instantiated three times with different auxiliary-arc types (A⊕A for MCFP0, A⊕A⊕(V×V) for MSFP2's extra Cξ arcs governed by the boundary cost's directional derivative). "Primal integral" and "dual integral" polyhedral convex functions (the book's own C[Z|R→R]/C[R→R|Z] notation, used in Theorem 9.15) needed a modeling decision, since the book's own definition of these classes lies outside this chunk's page range; see Formalization scope.

Formalization scope

Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity vocabulary is redeclared from prior missions in this series. "Primal integral" (C[Z|R→R], M[Z|R→R]) is formalized as integer effective domain (IsDomainIntegerArc/IsDomainIntegerR); "dual integral" (C[R→R|Z], M[R→R|Z]) is formalized as the existence of an integer subgradient at every domain point (IsDualIntegralArc/IsDualIntegralR) — a standard equivalent characterization for polyhedral convex functions, and a deliberate modeling choice recorded in MODERATION_NOTES.md rather than a literal transcription of the book's own (out-of-range) definition of these two notation classes. All eight numbered results found in this chunk's page range are placed in full, with no partial-coverage scope reduction. Contributions completing any of the eight sorrys are welcome; the goal and Theorem 9.15 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• R. T. Rockafellar, Network Flows and Monotropic Optimization, Wiley, 1984 [178] (the classical potential/Fenchel-duality framework this mission's Theorem 9.4 adapts).
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (the Lagrange duality and negative-cycle theory of section 9.5 this mission's Theorems 9.18 and 9.20 draw from).

Motivation

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

Setting

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

Formalization targets

Goal: Theorem 7.18 (the L-proximity theorem)

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

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

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

Milestones: Theorems 7.1, 7.7, 7.14

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

Formalization targets

Goal: the directional-derivative/subdifferential correspondence

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

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

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

Setting

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

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

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

Formalization targets

Goal: Theorem 6.37 (the M-proximity theorem)

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

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

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

Milestones: Theorems 6.2, 6.26, 6.28

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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