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.

Motivation

The classical separating hyperplane theorem says that any two disjoint convex sets in $\mathbb R^n$ can be separated by a hyperplane with an arbitrary real normal vector. When the sets in question are not arbitrary convex sets but the integer points of specially structured discrete sets, one can sometimes ask for much more: not merely that a separator exists, but that it can be chosen from a small, structured, dimension-independent family regardless of the size or shape of the sets being separated. Results of this kind — "discrete separation theorems" — are a recurring and often surprising theme in combinatorial optimization, playing the role that the ordinary separation theorem plays in continuous convex analysis, but with genuinely combinatorial content beyond it.

L-convex sets, introduced by Murota as part of the discrete convex analysis framework, are one of the two dual families of well-behaved discrete convex sets studied in the book (the other being M-convex sets, chunk 04 of this series). They are defined by a lattice-closure axiom together with translation invariance, and they correspond one-to-one to integer-valued distance functions satisfying the triangle inequality — objects long familiar from network flow theory and shortest-path duality, even though the L-convexity terminology is not traditionally used there. This mission formalizes the chapter's central results, culminating in Theorem 5.9: two disjoint L-convex sets can always be separated by a vector with entries in $\{-1, 0, 1\}$, no matter how large or complicated the sets are.

Setting

Let $V$ be a finite ground set. A nonempty set $D \subseteq \mathbb Z^V$ is an L-convex set if it satisfies the sublattice axiom (SBS[Z]) — $p, q \in D \implies p \vee q,\ p \wedge q \in D$, where $\vee, \wedge$ are componentwise maximum and minimum — and the translation axiom (TRS[Z]) — $p \in D \implies p \pm \mathbf 1 \in D$, where $\mathbf 1$ is the all-ones vector. A distance function $\gamma : V \times V \to \mathbb R \cup \{+\infty\}$ satisfies $\gamma(v,v) = 0$ for every $v$; it satisfies the triangle inequality if $\gamma(v_1,v_2) + \gamma(v_2,v_3) \ge \gamma(v_1,v_3)$ for all $v_1, v_2, v_3$. The admissible-potential polyhedron of $\gamma$ is

$$D(\gamma) = \{p \in \mathbb R^V : p(v) - p(u) \le \gamma(u,v)\ (\forall u \ne v)\}.$$

The convex hull of a discrete set $D \subseteq \mathbb Z^V$ is written $\bar D \subseteq \mathbb R^V$.

Formalization targets

Goal: Theorem 5.9 (discrete separation for L-convex sets)

If $D_1, D_2 \subseteq \mathbb Z^V$ are disjoint L-convex sets, there exists $x^* \in \{-1,0,1\}^V$ such that

$$\inf\{\langle p, x^*\rangle : p \in D_1\} - \sup\{\langle p, x^*\rangle : p \in D_2\} \ge 1.$$

Dropping the $\{-1,0,1\}^V$ restriction and allowing an arbitrary real separator would recover the classical separation theorem for convex sets, which holds regardless of L-convexity and carries no discrete-convexity content; the three-valued restriction is the weakest correct strengthening and is kept in full.

Milestones: Theorems 5.2, 5.5, 5.7

Theorem 5.2: an L-convex set is hole free ($D = \bar D \cap \mathbb Z^V$) — its integer points are exactly the integer points of its own convex hull. Theorem 5.5: $D$ is L-convex if and only if $D = D(\gamma) \cap \mathbb Z^V$ for some integer-valued distance function $\gamma$ satisfying the triangle inequality — L-convex sets and such distance functions are two descriptions of the same object, the discrete analogue of chunk 04's M-convex-set / submodular- function correspondence. Theorem 5.7 (parts (1), (4)): L-convex sets are closed under intersection in the strongest sense — the convex hulls intersect exactly where the sets do, and a nonempty intersection of L-convex sets is again L-convex.

Significance

The result itself. Theorem 5.9 packs two claims into one, as the book itself points out: the separator is forced into $\{-1,0,1\}^V$ (explicit in the statement), and disjoint L-convex sets satisfy "convexity in intersection" — their convex hulls are already disjoint whenever the sets themselves are (implicit, and necessary for the stated inequality to be possible at all). The $\{-1,0,1\}$ structure connects directly to combinatorial duality in network flows: L-convex polyhedra are, without the name, a familiar object there, and a $\{-1,0,1\}$-separator corresponds to a signed cut or a negative-cost cycle in an associated graph. Theorem 5.5's correspondence is the L-convex mirror of chunk 04's M-convex/submodular correspondence, and the book explicitly flags that the two will be unified into a single conjugacy relationship in a later chapter (Note 5.6) — this mission's formalization of the L-side is a prerequisite for that later unification.

Formalizing it. No matching item exists on the platform (searches for "L-convex", "distance function", and "negative cycle" return only unrelated results — number-theoretic distance estimates, polytope graph metrics, shortest-path graph structures — none matching the combinatorial L-convexity/discrete-separation content here). This mission gives the first formal statement of L-convex sets and their central separation theorem. Notably, Theorem 5.9's own statement — unlike the analogous M-convex Theorem 4.18 — needs none of the distance-function machinery that its proof uses; only the L-convexity axiom itself appears in the goal, making its formal statement comparatively lean even though the underlying mathematics is just as deep.

Difficulty

The natural first attempt at Theorem 5.9 is to try to construct $x^*$ directly from the structure of $D_1, D_2$ — for instance, from a normal vector to a real separating hyperplane, rounded coordinatewise. This does not work: rounding an arbitrary real separator gives no control over its entries, and there is no reason a rounded vector should still separate. The book's actual proof instead represents $D_1, D_2$ via distance functions $\gamma_1, \gamma_2$ (Theorem 5.5), combines them into $\gamma_{12} = \min(\gamma_1, \gamma_2)$, and extracts the separator from a shortest negative cycle in the associated graph: the vertices of the cycle alternate between the two sets' "tight" arcs, and the alternating $\pm 1$ pattern around the cycle is exactly the $\{-1,0,1\}$ vector $x^*$ — with the cycle's negativity translating directly into the required gap of at least $1$. Locating the right combinatorial object (a shortest negative cycle, not an arbitrary one) is what pins the separator down to a vector supported on a single alternating cycle rather than an arbitrary $\{-1,0,1\}$ pattern, and is the step a naive rounding or linear-algebra argument has no analogue of.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $D \subseteq \mathbb Z^V$ is a Set (V → ℤ). Distance functions take values in WithTop ℝ; the goal's infimum and supremum are taken in EReal (a complete lattice), since L-convex sets are always infinite (translation invariance along the all-ones direction), so an ℝ-valued supremum/infimum would silently return a junk value on an unbounded set. The conclusion is stated as $\sup_{D_2}\langle p,x^*\rangle + 1 \le \inf_{D_1}\langle p,x^*\rangle$, an addition-based reformulation of the book's subtraction inequality that avoids EReal's ⊤ - ⊤ ambiguity while remaining equivalent whenever both sides are finite.

A trivializing formalization of the goal would drop the $\{-1,0,1\}^V$ constraint on $x^*$ (recovering the classical, L-convexity-independent separation theorem) or fix a single coordinate pattern rather than asserting existence over the full three-valued family; neither is done here. Theorem 5.5 is stated existentially rather than via the book's named bijection $\Phi, \Psi$ (a documented scope reduction, parallel to chunk 04's treatment of Theorem 4.15), and Theorem 5.7 is drafted with only its two representation-independent clauses (parts (1) and (4); see MODERATION_NOTES.md). Contributions building the distance-function/admissible- potential apparatus needed for Theorem 5.7's remaining clauses, or the L-convex/integrally-convex bridge (Theorem 5.10, needing chunk 03's vocabulary), are welcome.

Selected references

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

Motivation

Matroid intersection is one of the founding results of combinatorial optimization: given two matroids on a common ground set, the largest common independent set can be found in polynomial time, and its size equals the minimum of a natural upper bound ranging over all subsets — a min-max theorem in the spirit of König's theorem and Menger's theorem, but for a strictly richer combinatorial structure. Jack Edmonds proved this in 1970, and Jack Edmonds and Rick Giles's subsequent generalization to submodular flows, together with André Frank's discrete separation theorem for submodular and supermodular set functions (1982), placed matroid intersection inside a single unifying framework: submodular function duality. This framework explains, in one stroke, matroid intersection, the base-exchange structure of matroids, and a family of other combinatorial min-max theorems that had previously seemed unrelated.

Murota's Discrete Convex Analysis develops this framework as the theory of M-convex sets: sets of integer vectors satisfying a lattice-exchange axiom that turns out to be exactly equivalent to being the integer points of a base polyhedron of an integer-valued submodular set function. This mission formalizes the chapter's central results: the equivalence of four variant forms of the exchange axiom (Theorem 4.3), the M-convex set / submodular function correspondence (Theorem 4.15), Frank's discrete separation theorem (Theorem 4.17), and Edmonds's intersection theorem itself (Theorem 4.18) — the deepest duality result in the theory of submodular functions and the historical origin of the M-convexity concept that the rest of the book generalizes to real-valued functions.

Setting

Let $V$ be a finite ground set. A set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ with $\rho(\emptyset) = 0$ and $\rho(V) < +\infty$ is submodular (the class $S[\mathbb R]$) if

$$\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y) \qquad (X, Y \subseteq V).$$

Its base polyhedron and submodular polyhedron are

$$B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X \subseteq V),\ x(V) = \rho(V)\}, \qquad P(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X \subseteq V)\},$$

where $x(X) = \sum_{v \in X} x(v)$; a supermodular function $\mu$ is one with $-\mu$ submodular. A nonempty set $B \subseteq \mathbb Z^V$ is an M-convex set if it satisfies the exchange axiom (B-EXC[Z]): for $x, y \in B$ and $u$ in the positive support of $x-y$, there is $v$ in the negative support of $x-y$ with both $x - \chi_u + \chi_v \in B$ and $y + \chi_u - \chi_v \in B$, where $\chi_u$ is the characteristic vector of $u$. A polyhedron $P \subseteq \mathbb R^V$ is integral if $P = \operatorname{conv}(P \cap \mathbb Z^V)$.

Formalization targets

Goal: Theorem 4.18 (Edmonds's intersection theorem)

For submodular set functions $\rho_1, \rho_2 \in S[\mathbb R]$,

$$\max\{x(V) : x \in P(\rho_1) \cap P(\rho_2)\} = \min\{\rho_1(X) + \rho_2(V \setminus X) : X \subseteq V\},$$

with both sides attained. If $\rho_1, \rho_2$ are integer valued, $P(\rho_1) \cap P(\rho_2)$ is an integral polyhedron and the maximum is attained at an integer point. Dropping the integrality clause and stating only the real max-min equality would leave ordinary LP duality with no discrete content at all; this mission keeps it in the goal at every strength the book proves it.

Milestones: Theorems 4.3, 4.15, 4.17

Theorem 4.3: the exchange axiom (B-EXC[Z]) is equivalent to three variants that impose the exchange condition asymmetrically or only for distinct vectors — groundwork establishing that M-convexity does not depend on which variant is taken as primitive. Theorem 4.15: $B$ is M-convex if and only if $B = B(\rho) \cap \mathbb Z^V$ for some integer-valued submodular $\rho$ — M-convex sets and integer-valued submodular set functions are two descriptions of the same combinatorial object. Theorem 4.17 (Frank): if a submodular $\rho$ dominates a supermodular $\mu$ pointwise, a single vector $x^*$ separates them ($\rho \ge x^* \ge \mu$ pointwise on every subset), integrally when $\rho, \mu$ are integer valued — derived, in the book, as a direct corollary of the goal theorem.

Significance

The result itself. Edmonds's intersection theorem is the min-max theorem underlying polynomial-time matroid intersection (a matroid's rank function is submodular, so the classical matroid intersection theorem is the special case $\rho_1, \rho_2$ both matroid rank functions), and its generality — arbitrary submodular set functions, not just matroid ranks — is what lets Frank's discrete separation theorem, and through it a wide range of combinatorial duality results in network flows, scheduling, and matroid theory, be derived as corollaries rather than proved from scratch each time. The integrality clause specifically is the fact that makes these duality theorems combinatorial: it guarantees that optimal fractional solutions to the underlying linear program can always be taken integral, without which the connection to discrete optimization would be lost.

Formalizing it. No matching item exists on the platform (searches for "submodular set function", "base polyhedron", "matroid intersection" return no relevant hits; Mathlib's Combinatorics/Matroid/ develops matroid rank functions, a special case, but not general submodular set functions or their polyhedra). This mission gives the first formal statement of the theorem at its natural generality, together with the M-convex-set viewpoint that motivates the rest of the book, and Frank's separation theorem as an explicit worked corollary.

Difficulty

The real-valued half of Theorem 4.18 is ordinary LP duality applied to a cleverly chosen primal program (maximize $\langle p, x\rangle$ over $P(\rho_1) \cap P(\rho_2)$) and its dual — routine once the right LP is written down. The integrality half is where the combinatorics enters: an optimal dual solution can always be chosen supported on a chain in each $\rho_i$'s effective domain (an extremal argument maximizing a strictly convex potential over the optimal dual face), and the incidence matrix of a chain of subsets is totally unimodular — this is the fact, external to ordinary LP theory, that forces an integral optimal solution to exist whenever the data ($\rho_1, \rho_2$) are integral. A proof that stops at real-valued LP duality, however carefully done, misses this step entirely and cannot produce the integrality clause; total unimodularity of a chain's incidence matrix is the one piece of combinatorics doing all the discrete work in an otherwise classical convex-duality argument.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; subsets are Finset V, vectors are V → ℝ/V → ℤ. Submodular functions take values in WithTop ℝ (exactly $\mathbb R \cup \{+\infty\}$); supermodular functions in WithBot ℝ; comparisons across the two use an explicit embedding into EReal. The max/min in the goal are stated via IsGreatest/IsLeast sharing a common EReal witness, so that "both sides attained, at the same value" — not merely "sup equals inf" — is what the Lean statement asserts, which is essential since the integrality clause's whole content is about which point attains the maximum.

A trivializing formalization of the goal would drop the integrality clause (leaving unqualified LP duality) or replace IsGreatest/IsLeast with a bare supremum/infimum equality (losing the "is attained" content the second half of the theorem needs); both are avoided. Theorem 4.15 is stated as the existential "iff" (some integer submodular $\rho$ realizes $B$) rather than reifying the book's own named bijection $\Phi, \Psi$ explicitly — a deliberate, documented scope reduction of that one milestone (see MODERATION_NOTES.md), not of the goal. Contributions building the explicit $\Phi$ map, the Lovász extension (needed for Theorem 4.16, not drafted here), or M-convex-set infrastructure reusable by chunks 06–07 (M-convex functions, which build on this chapter's vocabulary) are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• J. Edmonds, "Submodular functions, matroids, and certain polyhedra," in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, pp. 69–87.
• A. Frank, "An algorithm for submodular functions on graphs," Annals of Discrete Mathematics, 16, 1982, pp. 97–120.

Motivation

Quadratic minimization problems with a combinatorial sign pattern in their Hessian arise throughout applied mathematics: discretizations of elliptic boundary-value problems such as the Poisson equation, resistor-network energy functionals, and the Dirichlet forms of Markov-process potential theory all produce a symmetric matrix whose off-diagonal entries are nonpositive and whose rows are diagonally dominant (Fukushima, Oshima, and Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994). Such matrices are exactly the diagonally dominant symmetric M-matrices of classical numerical linear algebra (Berman and Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994). Murota's Discrete Convex Analysis (SIAM, 2003) identifies the combinatorial content of this sign pattern with a discrete convexity property — submodularity, and its strengthening translation submodularity — of the associated quadratic form, and shows that passing to the Legendre-Fenchel conjugate of such a quadratic form (i.e., inverting the matrix) transports this property to a dual combinatorial property, an exchange axiom, on the conjugate side. This mission formalizes that correspondence for the special, matrix-algebraic case of quadratic forms — the case in which Murota's book gives a self-contained proof using only the classical Farkas lemma, before generalizing the same conjugacy to a much broader class of functions in Chapter 8.

Setting

Let $V$ be a finite ground set (identified with $\{1,\dots,n\}$ in the book) and let $L = (\ell_{ij})_{i,j\in V}$ be a symmetric real matrix. $L$ has off-diagonal nonpositivity if $\ell_{ij}\le 0$ for all $i\ne j$, and diagonal dominance if $\sum_{j} \ell_{ij}\ge 0$ for every row $i$. The associated quadratic form is $g(p) = \tfrac12 p^\top L p$ for $p \in \mathbb R^V$. For $p,q\in\mathbb R^V$ write $p\vee q$, $p\wedge q$ for the componentwise maximum and minimum. A function $g:\mathbb R^V\to\mathbb R$ is submodular if $g(p)+g(q)\ge g(p\vee q)+g(p\wedge q)$ for all $p,q$, and has translation submodularity if the stronger inequality $g(p)+g(q)\ge g((p-\alpha\mathbf 1)\vee q)+g(p\wedge(q+\alpha\mathbf 1))$ holds for every $\alpha \ge 0$, where $\mathbf 1$ is the all-ones vector (ordinary submodularity is the case $\alpha=0$).

On the conjugate side, for $x\in\mathbb R^V$ write $\operatorname{supp}^+(x)=\{i : x_i>0\}$, $\operatorname{supp}^-(x)=\{i:x_i<0\}$, and let $\chi_i$ denote the $i$-th unit vector ($\chi_0$ denotes the zero vector). A function $f:\mathbb R^V\to\mathbb R$ has the exchange property if for all $x,y\in\mathbb R^V$ and $i\in\operatorname{supp}^+(x-y)$ there exist $j \in \operatorname{supp}^-(x-y)\cup\{0\}$ and $\alpha_0>0$ such that $f(x)+f(y)\ge f(x-\alpha(\chi_i-\chi_j))+f(y+\alpha(\chi_i-\chi_j))$ for every $\alpha\in[0,\alpha_0]$. The Legendre-Fenchel conjugate of $f$ is $f^\bullet(p) = \sup_x\{\langle p,x\rangle - f(x)\}$; two functions $g,f$ are conjugate to each other when $g=f^\bullet$ and $f=g^\bullet$. For positive-definite symmetric $M,L$, the quadratic forms $f(x)=\tfrac12x^\top Mx$ and $g(p)=\tfrac12p^\top Lp$ are conjugate to each other exactly when $M$ and $L$ are matrix inverses of one another.

Formalization targets

Goal (Theorem 2.11). For conjugate strictly convex quadratic forms $g$ and $f$ as above,

$$g \text{ has translation submodularity} \iff f \text{ has the exchange property.}$$

This is the mission's capstone: the statement leaves the correspondence at the level of the two named combinatorial properties, without hard-coding which of the two properties is verified in a given application, so it survives exactly as strongly as the underlying conjugacy fact does.

Supporting milestones, in the order the book develops them: Proposition 2.4 (off-diagonal nonpositivity plus diagonal dominance implies positive semidefiniteness); Proposition 2.6 (off-diagonal nonpositivity is equivalent to plain submodularity of $g$); Theorem 2.7 (the full sign pattern is equivalent to translation submodularity of $g$); Proposition 2.9 (conjugate quadratic forms correspond exactly to inverse matrix pairs); Theorem 2.12 (a nine-way equivalence, for a nonsingular symmetric $M$, among membership in the matrix class $\mathcal L^{-1}$, two sign-consistency inequalities on the columns of $M$ together with their strict forms, two directional-derivative reformulations of the exchange property together with their strict forms, and the exchange property itself together with its strict form); Proposition 2.13 (the Farkas lemma in equality form, together with the strict variant valid for a nonsingular coefficient matrix); and Proposition 2.14 (the class $\mathcal L^{-1}$ is closed under taking principal submatrices).

Significance

The M-natural exchange property is the function-level analogue of the base-exchange axiom for matroids, and translation submodularity is the analogue, on the "primal" side, of ordinary submodularity for set functions; Chapter 2's quadratic-form case is the historical and pedagogical entry point for the general conjugacy Chapter 8 proves for the full M-convex/ L-convex function classes. Establishing it here, in the self-contained matrix-algebraic setting, isolates exactly which properties of a quadratic form are combinatorial (tied to the coordinate axes) rather than purely convex-analytic (rotation-invariant): submodularity and the exchange property are not preserved by an orthogonal change of variables, in contrast to ordinary convexity, which Proposition 2.4 shows the same sign pattern also implies.

Formalizing this mission produces the first Lean statement, in this project's namespace, of a genuine conjugacy theorem between a primal-side and a dual-side combinatorial convexity property for a concrete function class; nothing of this kind is yet proved (or, so far as the platform's own search shows, formalized at all) elsewhere on the platform. The nine-way equivalence of Theorem 2.12 is a substantial independent contribution beyond the goal itself, since it is what makes the goal's proof possible via elementary linear algebra rather than the general convex-analytic machinery Chapter 8 needs.

Difficulty

The naive approach to Theorem 2.11 tries to derive the exchange property for $f$ directly from the defining supremum in the conjugate relation $f = g^\bullet$, differentiating under the sup; this fails because the exchange property compares $f$ along a specific combinatorial direction $\chi_i - \chi_j$ tied to two coordinates, not along an arbitrary direction, and no naive first-order argument isolates the right pair $(i,j)$ without already knowing the sign pattern of $M = L^{-1}$. The book's actual route is Theorem 2.12: it reduces the exchange property to a column-wise sign-consistency statement on $M$ itself (conditions (b)/(c)) via the identity $f'(x;d) = x^\top Md$, and closes the loop back to membership in $\mathcal L^{-1}$ using the Farkas lemma applied to the linear system $ML = I$ — a genuinely matrix-algebraic argument that does not generalize verbatim to non-quadratic M-/L-convex functions, which is exactly why Chapter 8 needs a different (convex-analytic) proof for the general case.

Formalization scope

Vectors and matrices are indexed by a general finite type V ([Fintype V] [DecidableEq V]) rather than a fixed Fin n, matching this project's convention elsewhere and letting Proposition 2.14's principal-submatrix statement reuse the class predicate at the restricted index type directly. Quadratic forms are real-valued ((V → ℝ) → ℝ, using Matrix.mulVec and dotProduct) since this chapter's functions are always finite everywhere; the Legendre-Fenchel conjugate is EReal-valued via sSup, since a supremum over an infinite domain need not be finite in general even though it is finite here. Every min(0, \dots)-based condition in Theorem 2.12 and the exchange axioms is unfolded as the logically equivalent disjunction over the finitely many terms achieving the minimum, rather than reified via Finset.inf/WithTop machinery — a faithful, checked-equivalent simplification, not a narrowing (see MODERATION_NOTES.md). "Nonsingular" is Matrix.det ≠ 0. No numeric constant needs instantiation anywhere in this mission. The formalization does not trivialize: the goal's exchange property is stated for the specific combinatorial direction $\chi_i - \chi_j$ with $i\in \operatorname{supp}^+(x-y)$, $j \in \operatorname{supp}^-(x-y)\cup\{0\}$ — not an arbitrary direction, which would reduce the exchange property to a restatement of ordinary convexity and discard the entire combinatorial content the mission is about.

Infrastructure needed: Matrix.PosDef/Matrix.PosSemidef/Matrix.IsSymm (present in Mathlib); everything else (submodularity, translation submodularity, the exchange axioms, the sign-consistency conditions) is defined fresh in DiscreteConvex.CombinatorialB. A solution to the goal will likely want Proposition 2.9, Theorem 2.12, and the Farkas lemma (Proposition 2.13) as lemmas; contributions completing any of the seven milestones independently, or supplying the Schur-complement induction behind Proposition 2.4, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 2.
• A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994.
• M. Fukushima, Y. Oshima, M. Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994.
• J. Farkas, Theorie der einfachen Ungleichungen, J. Reine Angew. Math. 124 (1902), 1–27.

Cutting planes from lattice-free convex sets

Cutting planes for mixed-integer linear programs are often derived from a few rows of an optimal simplex tableau. Keeping $q$ rows for basic integer variables $x_1,\dots,x_q$, dropping the nonnegativity of $x$ (Gomory's corner polyhedron, Gomory 1969) and then the integrality of the nonbasic variables leaves the set of $s\ge0$ with $f+\sum_j r^js_j\in\mathbb Z^q$. Balas observed in 1971 that convex sets with no integral point in their interior give valid inequalities for such sets (Balas 1971). Andersen, Louveaux, Weismantel and Wolsey (2007) for two rows, and Borozan and Cornuéjols (2009) for any number of rows, showed that for rational data the irredundant valid inequalities correspond to maximal lattice-free convex sets. Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543; Math. Oper. Res. 35(3), 2010) removed the rationality assumption. This mission formalizes that result, Theorem 3 of their paper.

Setting

Fix $q\ge0$, a point $f\in\mathbb R^q$ and a linear subspace $W\subseteq\mathbb R^q$, and assume that the affine space $f+W$ contains an integral point. Products such as $ry$ are standard inner products.

• $\mathcal W$ is the space of real functions $s=(s_r)_{r\in W}$ with finite support. The semi-infinite relaxation is

$$R_f(W)=\Big\{s\in\mathcal W \ \Big|\ f+\sum_{r\in W}rs_r\in\mathbb Z^q,\ s_r\ge0\ (r\in W)\Big\}.$$

• A linear inequality is a pair $(\psi,\alpha)$ with $\psi:W\to\mathbb R$ an arbitrary function and $\alpha\in\mathbb R$, read as $\Psi(s)=\sum_{r\in W}\psi(r)s_r\ge\alpha$. It is valid if every $s\in R_f(W)$ satisfies it.
• $V$ is the affine hull of $(f+W)\cap\mathbb Z^q$, and $\mathcal V=\{s\in\mathcal W\mid f+\sum_r rs_r\in V\}$. A linear inequality is trivial if every $s\in\mathcal V$ with $s\ge0$ satisfies it. When $W$ is irrational (not spanned by the integral points it contains, up to translation), $V$ is a proper affine subspace of $f+W$.
• $\sum\psi(r)s_r\ge\alpha$ dominates $\sum\psi'(r)s_r\ge\alpha$ if $\psi\le\psi'$ pointwise. A valid inequality is minimal if no valid inequality with the same $\alpha$ and a different $\psi'\le\psi$ exists.
• Choose $C\in\mathbb R^{\ell\times q}$ and $d\in\mathbb R^\ell$ with $V=\{x\in f+W\mid Cx=d\}$. Two valid inequalities are equivalent if $\psi(r)=\rho\psi'(r)+\lambda^TCr$ for all $r\in W$ and $\alpha=\rho\alpha'+\lambda^T(d-Cf)$, for some $\rho>0$, $\lambda\in\mathbb R^\ell$.
• A maximal lattice-free convex set in $f+W$ is a convex $B\subseteq f+W$ with no integral point in its interior relative to $f+W$, inclusionwise maximal with these properties.
• For $K\subseteq W$ closed, convex, with $0$ in its interior relative to $W$: the polar $K^*=\{y\in W\mid ry\le1\ \forall r\in K\}$, $\hat K=\{y\in K^*\mid\exists x\in K,\ xy=1\}$, and $\rho_K(r)=\sup_{y\in\hat K}ry$. For such a $B$ with $f$ in its interior, $\psi_B=\rho_{B-f}$; for a polyhedral $B=\{x\in f+W\mid a_i(x-f)\le1\}$ with tight rows this is $\psi_B(r)=\max_ia_ir$.

A function $\sigma:W\to\mathbb R$ is sublinear if $\sigma(\lambda r)=\lambda\sigma(r)$ for $\lambda\ge0$ and $\sigma(r+r')\le\sigma(r)+\sigma(r')$.

Formalization targets

Goal: Theorem 3 (p. 6)

1. Every nontrivial valid linear inequality for $R_f(W)$ is dominated by a nontrivial minimal valid linear inequality for $R_f(W)$.
2. Every nontrivial minimal valid linear inequality for $R_f(W)$ is equivalent to one of the form

$$\sum_{r\in W}\psi_B(r)s_r\ \ge\ 1$$

with $\psi_B\ge0$ on $W$ and $B$ a maximal lattice-free convex set in $f+W$ with $f$ in its interior.

The goal is stated as one conjunction. It fixes no constants and makes no rationality assumption on $f$ or $W$.

Milestones

In the order in which the proof on pp. 15–21 uses them:

• Lemma 23 (a sublinear valid inequality below any valid one)
• Lemma 26 (invariance under equivalence)
• Claims 1 and 2 in the proof of Theorem 3
• Theorem 28 (Basu–Cornuéjols–Zambelli: $\rho_K$ is the smallest sublinear function with $1$-sublevel set $K$)
• Remark 30 and Claim 4 (the inequality $\sum\rho_K(r)s_r\ge1$)
• Remark 29 ($\rho_K=\max_ia_ir$ for tight rows)
• Claim 6 (a shift by $\lambda^TC$ making $\psi$ nonnegative)
• Claim 7 ($\psi_B$ below a nonnegative sublinear $\psi''$)
• Lemma 31 (maximal lattice-free sets give minimal inequalities)

Significance

Theorem 3 says that the minimal valid inequalities of $R_f(W)$ are exactly those produced by maximal lattice-free convex sets, up to the equivalence forced by the affine hull $\mathcal V$. It also says that for irrational $W$, where valid inequalities can have negative coefficients, some equivalent form always has nonnegative coefficients. The paper derives two further results from it: a description of the closure of $\operatorname{conv}(R_f(W))$ in a suitable norm (Theorem 4), and a reduction of extreme inequalities of the infinite model to finite ones (Theorem 5). Both results remain unproved without it.

The result has a complete proof in the paper, which relies on the cited Theorem 28 from Basu, Cornuéjols, Zambelli. To our knowledge none of it is machine-checked. A formalization would provide a definitional layer for corner relaxations, lattice-free sets and valid inequalities, which is currently absent from Mathlib. It would also expose where the page is imprecise; see the scope section.

Difficulty

For rational data every valid inequality can be written with right-hand side $1$ and nonnegative coefficients, and $\psi$ is then the gauge of $B_\psi$. For irrational $W$ this fails. Since $R_f(W)\subseteq\mathcal V$, adding $\lambda^TCr$ to $\psi$ changes nothing on $R_f(W)$, so coefficients can be negative, and $B_\psi=\{x\in f+W\mid\psi(x-f)\le\alpha\}$ may have a full-dimensional recession cone. A maximal lattice-free set containing $B_\psi$ then yields a $\psi_B$ that need not lie below $\psi$ (the example on pp. 21–22 shows this). One must first pass to an equivalent inequality whose set has no full-dimensional recession cone within $V$. This step combines the structure theorem for maximal lattice-free sets in irrational subspaces (Theorem 9 of the paper) with a duality argument. A second obstacle is that $\psi$ is an arbitrary function: validity alone gives no convexity or continuity, and Lemma 23 is needed to recover them.

Formalization scope

• Ambient space. $\mathbb R^q$ is EuclideanSpace ℝ (Fin q), $W$ is a Submodule, and $\mathcal W$ is W →₀ ℝ. The printed phrase "the set $\{r\mid s_r>0\}$ has finite cardinality" is read as ordinary finite support.
• Standing hypothesis. Every statement assumes that $f+W$ contains an integral point. Without it $R_f(W)=\emptyset$ and every inequality is valid, so this hypothesis rules out the trivializing formalization. The equivalence predicate carries the hypothesis $V=\{x\in f+W\mid Cx=d\}$ together with validity of both inequalities. With $C,d$ unconstrained, equivalence would be rescaling only, and part 2 of the goal would be false for irrational $W$.
• Interiors. All interiors are relative: to $f+W$ for $B$ and $B_\psi$, to $W$ for $K$.
• $\psi_B$. It is defined as $\rho_{B-f}$, independent of any description of $B$.

The paper is imprecise in three places, and the formalization departs from the page in each:

1. Remark 29 is false without tight rows: for $K=(-\infty,1]\subseteq\mathbb R$ written with $a_1=1$, $a_2=1/2$, $\rho_K(r)=r\ne\max(r,r/2)$ for $r<0$. It is stated with the tightness the paper arranges before using it.
2. The identity $\operatorname{int}(B_\psi)=\{x\mid\psi(x-f)<\alpha\}$ on p. 17 fails at $\alpha=0$, for example for $\psi\equiv0$. Claims 1 and 2 use the strict sublevel set, and Claim 2 is false for the topological interior.
3. Claims 5 and 7 invoke Corollary 20 in $f+W$, although it is proved only for a lattice of a linear space. Corollary 20 and Claim 5 are therefore not milestones.

Two kinds of contributions are especially welcome: reusable infrastructure for polars of convex sets relative to a subspace and for sublinear functions on submodules, and a proof of Theorem 28.

Selected references

• A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543v1
• A. Basu, G. Cornuéjols, G. Zambelli, Convex sets and minimal sublinear functions, J. Convex Anal. 18(2), 2011 (reference [9]).
• V. Borozan, G. Cornuéjols, Minimal valid inequalities for integer constraints, Math. Oper. Res. 34(3), 2009. https://doi.org/10.1287/moor.1090.0400
• K. Andersen, Q. Louveaux, R. Weismantel, L. Wolsey, Inequalities from two rows of a simplex tableau, IPCO 2007. https://doi.org/10.1007/978-3-540-72792-7_1
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2, 1969. https://doi.org/10.1016/0024-3795(69)90017-2