Discrete Convex Analysis

Motivation

In economics, a pair of goods are substitutes if raising the price of one increases demand for the other, and complements if it decreases it; formally, a utility or value function is submodular in the substitutes case and supermodular in the complements case. A natural question is which of these two regimes a given optimization problem's value function falls into, and whether the answer depends on the underlying combinatorial structure of the problem rather than being a coincidence of the particular numbers involved. Murota's Discrete Convex Analysis (SIAM, 2003) answers this question for the maximum-weight circulation problem in a directed network: the value function is submodular in some coordinates and supermodular in others, purely as a consequence of a graph-theoretic distinction — whether the arcs involved are parallel or series — and this chapter shows the distinction is explained precisely by the dual pair of discrete convexity notions (L-natural-convexity and M-natural-convexity) developed elsewhere in the book. This mission also completes the quadratic-forms thread the previous mission in this series (Discrete Convex Analysis XV) began, by formalizing its natural generalization to functions that may take the value $+\infty$.

Setting

Let $G=(V,A)$ be a directed graph with vertex set $V$ and arc set $A$; write $\partial^+a$, $\partial^-a$ for the initial and terminal vertex of arc $a$. For a flow $\xi:A\to\mathbb R$, its boundary is $\partial\xi(v)=\sum_{a:\partial^+a=v}\xi(a)-\sum_{a:\partial^-a=v}\xi(a)$, the net flow leaving $v$. Given a capacity $c:A\to\mathbb R_{\ge0}$, $\xi$ is a feasible circulation for $c$ if $0\le\xi(a)\le c(a)$ for every arc and $\partial\xi(v)=0$ for every vertex. For a weight $w:A\to\mathbb R$, $F(w,c)=\max\{\langle w,\xi\rangle : \xi\text{ feasible for }c\}$ is the maximum-weight circulation value, and $\xi$ is optimal for $w$ (with capacity $c$) if it is feasible and attains this maximum. A simple cycle is an alternating sequence of pairwise distinct vertices $v_0,\dots,v_{k-1}$ and arcs $a_1,\dots,a_k$ with $\{\partial^+a_i,\partial^-a_i\}=\{v_{i-1},v_i\}$ (indices mod $k$) and $v_0=v_k$. Two arcs are parallel if every simple cycle containing both of them orients them oppositely, and series if every such cycle orients them the same way; a set of arcs is parallel (series) if its arcs are pairwise parallel (series). A circuit is a $\{0,\pm1\}$-valued $\pi:A\to\mathbb R$ with $\partial\pi=0$ whose support forms a simple cycle. For $x\in\mathbb R^n$, $\operatorname{supp}^+(x)=\{i:x_i>0\}$, $\operatorname{supp}^-(x)=\{i:x_i<0\}$. A function $g:\mathbb R^n\to\mathbb R$ is submodular if $g(p)+g(q)\ge g(p\vee q)+g(p\wedge q)$, supermodular with the reverse inequality, and has translation submodularity (is L-natural-convex) if the stronger inequality $g(p)+g(q)\ge g((p-\alpha\mathbf1)\vee q)+g(p\wedge(q+\alpha\mathbf1))$ holds for every $\alpha\ge0$. A function $f$ has the M-natural exchange property (is M-natural-convex) if for $i\in\operatorname{supp}^+(x-y)$ there exist $j\in \operatorname{supp}^-(x-y)\cup\{0\}$ and $\alpha_0>0$ with $f(x)+f(y)\ge f(x-\alpha(\chi_i-\chi_j))+f(y+\alpha(\chi_i-\chi_j))$ for $\alpha\in[0,\alpha_0]$; a function is M-natural-concave or L-natural-concave if its negation is M-natural- or L-natural-convex.

Formalization targets

Goal (Theorem 2.23). For $P$ a parallel arc set and $S$ a series arc set,

$$F\text{ is L-natural-convex in }w_P\text{ and M-natural-concave in }c_P,$$ $$F\text{ is M-natural-convex in }w_S\text{ and L-natural-concave in }c_S,$$

where $w_P$, $c_P$ denote $F$'s dependence on the coordinates of $w$, $c$ indexed by $P$ (resp. $S$) with the remaining coordinates held fixed. This is the mission's capstone: it upgrades the plain submodularity/supermodularity split of Theorem 2.22 to the sharper pair of combinatorial convexity classes that explains it.

Supporting milestones. Proposition 2.21 (the classical fact that $F$ is convex in $w$ and concave in $c$, with no combinatorial content — the baseline against which Theorem 2.23's sharper claim is measured); Theorem 2.16 (the general, possibly-$+\infty$-valued extension of the quadratic-form conjugacy from Discrete Convex Analysis XV's Theorem 2.11, to functions restricted to a linear subspace); Theorem 2.22 (plain submodularity/supermodularity of $F$ in $w_P,c_P$ and $w_S,c_S$, the result Theorem 2.23 strengthens); and Propositions 2.24–2.28 (the graph-theoretic lemmas — sparse intersection of a circuit's support with a parallel or series arc set, merging two circuits along a series set, and three existence statements for optimality-preserving perturbations — that the book's own proof of Theorem 2.23 is built from).

Significance

Theorem 2.23 gives a structural explanation, rather than a case-by-case verification, for a phenomenon well known in network flow theory: that convexity/concavity and submodularity/supermodularity are independent properties, appearing in all four combinations depending on which side of the problem (weights or capacities) and which graph-theoretic role (parallel or series) is varied. Without it, (2.55)'s four combinations would be four separate facts with no common cause; with it, they are corollaries of two applications of a single pair of dual discrete-convexity notions, the same notions the book uses throughout to unify matroid theory, submodular optimization, and convex analysis. Formalizing this mission produces, so far as a platform search shows, the first Lean statement of a combinatorial-convexity classification result for a network optimization value function, together with the graph-theoretic vocabulary (simple cycles, parallel/series arcs, circuits) needed to state it — infrastructure with no prior formalized counterpart on the platform that a later mission on network flows or matroid union could reuse.

Difficulty

The naive approach to Theorem 2.23 tries to verify translation submodularity or the exchange property directly from the linear-programming definition of $F$ as a maximum over a polytope, treating $w_P\mapsto F(w,c)$ as an abstract convex-piecewise-linear function; this loses the graph structure entirely and gives at best the plain submodularity of Theorem 2.22, not the sharper L-natural/M-natural classification, because submodularity alone does not distinguish a combinatorially meaningful discrete convexity from an arbitrary submodular function. The book's actual route instead works with explicit optimal circulations for the two perturbed weight vectors and reconstructs a feasible pair achieving the target inequality by rerouting flow along a circuit — and the existence of a usable circuit (one that touches the perturbed arcs in a way compatible with the parallel or series structure) is exactly what Propositions 2.24–2.28 supply via the conformal decomposition of a difference of two circulations into elementary circuits. This is why those five propositions, although individually narrow existence lemmas, are included as milestones: they are the load-bearing combinatorial content the naive convex-analytic argument cannot reach.

Formalization scope

The graph is {V A : Type*} with src dst : A → V rather than a bundled structure, matching the book's own $\partial^+,\partial^-$ notation directly. $F(w,c)$ is a real sSup over feasible circulations' weights (existence of a maximizer is not asserted, since no proof is attempted this pass); IsOptimalCirc is a separate, directly-stated primitive for "$\xi$ is optimal for $w$", matching the book's own working vocabulary in the propositions that need it. A simple cycle is formalized as an injective cyclically-indexed vertex sequence together with a matching arc sequence, exactly as the book's own footnote defines it; parallel and series arcs are defined by quantifying over every such representation of every simple cycle containing the two arcs, which is checked to be independent of which of a cycle's two traversal directions or starting vertex is chosen. Viewing $F$ as a function of $w_P$ alone extends a partial vector by a fixed background vector on the complement of $P$, the same partial-application device the book uses informally. M-natural- and L-natural-concavity are recorded as the corresponding convexity property of the negated function, the standard convention. The formalization does not trivialize: parallel and series arc sets are genuine graph-theoretic hypotheses (not, e.g., specialized to $|P|=1$ or a graph with no simple cycles, which would make the parallel/series distinction vacuous), and Theorem 2.23's four conclusions are stated with the same combinatorial-convexity predicates (TranslationSubmodular, MNatExchangeR) used for the book's sharpest discrete convexity classes, not weakened to plain submodularity/supermodularity. Theorem 2.16 additionally needs Set (V → ℝ)-valued subspaces K, H (following the book's own set-builder notation for ker M and X⊥ rather than bundling them as Mathlib Submodules) and a WithTop ℝ-valued Legendre- Fenchel conjugate. Infrastructure needed beyond Mathlib: all graph, circulation, and combinatorial-convexity vocabulary is defined fresh in DiscreteConvex.CombinatorialC; a contribution proving any of the five graph-theoretic lemmas (Propositions 2.24–2.28) or the convex/concave halves of Proposition 2.21 independently would be a natural entry point.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 2.
• K. Murota, A. Shioura, "Conjugacy relationship between M-convex and L-convex functions in continuous variables," Mathematical Programming 101 (2004), 415–433.
• R. T. Rockafellar, Network Flows and Monotropic Optimization, Wiley, 1984.

Motivation

Duality is the organizing principle of convex optimization: a minimization problem's optimal value equals a maximization problem's optimal value, and this coincidence, rather than being a lucky accident, follows from a separating-hyperplane argument that applies whenever the two problems' feasible regions are shaped compatibly enough. Werner Fenchel formalized this in the 1950s for pairs of convex and concave functions related by the Legendre-Fenchel transform, and the resulting Fenchel duality theorem specializes, for linear objectives over polyhedral feasible regions, to linear programming duality — the fact, central to the entire theory of combinatorial optimization, that a linear program's optimal value can always be certified from above and below by a pair of primal and dual feasible solutions. Murota's Discrete Convex Analysis (SIAM, 2003) collects this classical machinery, together with the integrality theory that lets it produce combinatorial (integer-valued) certificates rather than merely real ones, as the technical foundation the rest of the book builds its discrete theory on top of.

Setting

For $f : \mathbb R^n \to \mathbb R \cup \{+\infty\}$, the epigraph is $\operatorname{epi} f = \{(x,Y) : Y \ge f(x)\}$, and $f$ is convex iff $\operatorname{epi} f$ is a convex set; $f$ is proper if additionally its effective domain $\operatorname{dom} f = \{x : f(x) < +\infty\}$ is nonempty, and closed if $\operatorname{epi} f$ is topologically closed. A function $h : \mathbb R^n \to \mathbb R \cup \{-\infty\}$ is concave, proper, closed analogously via its hypograph. The convex conjugate is $f^\bullet(p) = \sup_x\{\langle p,x\rangle - f(x)\}$, and the concave conjugate $h^\circ(p) = \inf_x\{\langle p,x\rangle - h(x)\}$. The relative interior $\operatorname{ri} S$ of a set $S$ is the interior of $S$ relative to its affine hull. A function is polyhedral if its epigraph (or hypograph) is a finite intersection of half-spaces. Given an $m \times n$ matrix $A$, $b \in \mathbb R^m$, $c \in \mathbb R^n$, the primal and dual linear programs are $\min\{c^\top x : Ax=b,\ x\ge0\}$ and $\max\{b^\top y : A^\top y \le c\}$, with feasible regions $P$, $D$. A matrix is totally unimodular if every square submatrix has determinant $0$, $1$, or $-1$. A discrete set $S \subseteq \mathbb Z^n$ is hole free if $S = \bar S \cap \mathbb Z^n$, where $\bar S$ is the convex hull of $S$'s real embedding; the discrete Minkowski sum is $S_1+S_2 = \{x_1+x_2 : x_1\in S_1, x_2\in S_2\}$.

Formalization targets

Goal (Theorem 3.6, Fenchel duality). For proper convex $f$ and proper concave $h$ satisfying at least one of four alternative conditions — a relative-interior condition on $\operatorname{dom} f \cap \operatorname{dom} h$, a polyhedrality condition on the same, or the analogous pair of conditions on $\operatorname{dom} f^\bullet \cap \operatorname{dom} h^\circ$ together with closedness of $f$, $h$ —

$$\inf_x\{f(x)-h(x)\} = \sup_p\{h^\circ(p)-f^\bullet(p)\},$$

with the extremum on the appropriate side attained whenever the common value is finite. This is the mission's capstone: the four alternative hypotheses make it the most broadly applicable statement of the four convex-duality results in this mission, each of the other three being either a special case in substance (Theorem 3.5, separation, which 3.6 is proved from) or a literal specialization to linear data (Theorem 3.10, LP duality).

Supporting milestones. Theorem 3.2 (biconjugation: $f^\bullet$ is always closed proper convex, and $g^{\bullet\bullet}=g$ for closed proper convex $g$); Theorem 3.5 (the separation theorem for convex/concave functions, under two of Theorem 3.6's four hypotheses); Theorem 3.9 (the Farkas lemma, equality form); Theorem 3.10 (LP duality: weak duality, strong duality with attainment, and complementary slackness); Theorem 3.13 (total unimodularity of the constraint matrix guarantees an integral optimal solution whenever an optimal solution exists); Proposition 3.14 (an explicit potential function certifying a minimum-weight bipartite perfect matching, via the totally unimodular incidence-matrix LP); and Proposition 3.16 (for a translation-invariant family of hole-free discrete sets, the property that discrete disjointness implies closure disjointness is equivalent to the discrete Minkowski sum matching the integer points of the closures' Minkowski sum).

Significance

Fenchel duality is the single result from which the separation theorem, LP duality, and (via the totally-unimodular incidence matrix of a bipartite graph) the combinatorial duality underlying weighted bipartite matching all descend, in one unbroken chain of specialization; formalizing this chain in one mission exhibits that structure directly, rather than treating each result as an independent fact. Proposition 3.16 plays a different role: it is the chapter's warning that naive discrete analogues of convexity (hole-freeness) do not automatically inherit convexity's good closure properties under Minkowski sums, which is exactly the gap the book's later M-convexity and L-convexity machinery is built to close — this mission's Proposition 3.16 is therefore the motivating negative result for the rest of the book's positive theory, not a loose end. So far as a platform search shows, no existing formalization matches this chunk's specific combination of extended-valued (possibly $\pm\infty$) functions, the four-alternative Fenchel duality hypothesis, or the bipartite-matching-via-total-unimodularity argument; the one related platform result (VectorSpaceOpt.fenchel_duality, from Luenberger) is for real-valued functions on general normed spaces under a single relative-interior-and-solidness hypothesis, a different generality from the extended-valued, four-hypothesis statement here.

Difficulty

The naive approach to Theorem 3.6 tries to prove the duality gap is zero directly from the definitions of the two conjugates, which only gives the easy inequality $\inf \ge \sup$ (a one-line computation, shown in the book's own proof in three lines); the substantive content is the reverse inequality, and it genuinely fails without a constraint-qualification hypothesis like (a1)-(b2) — Example 3.8 in the book exhibits a convex/concave pair with $\inf = 0 \ne -1 = \sup$ when none of the four conditions hold. The book's actual route reduces Theorem 3.6 to the separation theorem (Theorem 3.5) applied to $f$ shifted down by the (assumed finite) infimum, which produces the separating affine function directly; this is why Theorem 3.5, although logically a special case in spirit, earns its own milestone rather than being subsumed silently.

Formalization scope

All convex and concave functions are represented uniformly as (V → ℝ) → EReal-valued (Fintype V), rather than mixing WithTop ℝ for convex and WithBot ℝ for concave functions, so that Theorem 3.2's biconjugate — whose properness is a conclusion, not an assumption — has a well-defined codomain without extra casts. Convexity is defined via the epigraph being a convex subset of the ordinary real vector space $(V\to\mathbb R)\times\mathbb R$ (Mathlib's Convex ℝ), following the book's own equivalent characterization, rather than unfolding the direct inequality definition, which would require a extended-arithmetic scalar-multiplication convention (0\cdot(+\infty)=0) that Mathlib does not provide for EReal. The relative interior is defined directly from the book's own metric-ball-intersected-with-affine-hull description, since Mathlib has no relative-interior primitive at the pinned revision. Polyhedra are finite intersections of explicit half-spaces. A bipartite perfect matching is represented as a bijection between the two vertex sides restricted to the edge set — a faithful, not narrower, representation since every perfect matching between equal-size parts arises this way. The formalization does not trivialize: Theorem 3.6's four hypotheses are carried in full (not reduced to the easiest single case), and no result is stated only for finite-valued (never $\pm\infty$) functions, which would discard the entire point of the extended-value convex-analysis framework this chapter sets up for the rest of the book. Infrastructure needed beyond Mathlib's Convex, Matrix, and EReal API: all epigraph/hypograph, conjugate, relative-interior, and polyhedral apparatus is defined fresh in DiscreteConvex.IntegralConvexityB; a contribution proving any of the seven milestones independently, or supplying Mathlib-quality relative-interior lemmas, would be a natural entry point.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 3.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

Motivation

Submodular set functions are the combinatorial stand-in for convexity: a function $\rho : 2^V \to \mathbb R$ on the subsets of a finite ground set $V$ is submodular if $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$, and this single diminishing-returns inequality drives an enormous range of combinatorial optimization — matroid rank functions, graph cut capacities, entropy, coverage functions, and the max-flow min-cut theorem all arise as special or dual cases (Edmonds 1970; Lovász 1983; Fujishige 2005). M-convex sets are the "vector" incarnation of the same idea: subsets $B$ of $\mathbb Z^V$ satisfying an exchange axiom that generalizes the basis-exchange property of matroids to sets of integer points lying on a common hyperplane. Murota's Discrete Convex Analysis (SIAM, 2003) develops both sides of this correspondence and proves they coincide exactly: M-convex sets are precisely the integer points of the base polyhedra of integer-valued submodular functions. This mission covers the second half of that development — the structural theory (integrality, holes, Minkowski sums) that turns the correspondence into a working calculus, and its capstone, a discrete separation theorem for two disjoint M-convex sets whose separating hyperplane is forced to have $\{0,1\}$- or $\{0,-1\}$-valued coefficients.

Companion mission 04-mconvex-sets (Discrete Convex Analysis III) covers the same chapter's foundational results: the equivalence of the exchange-axiom variants, the one-to-one correspondence between M-convex sets and integer submodular functions (Theorem 4.15), Edmonds's intersection theorem (Theorem 4.18), and Frank's discrete separation theorem for submodular/ supermodular pairs (Theorem 4.17). This mission builds on that vocabulary (redeclared here, since draft missions in the same series cannot yet import one another) and proves the results the chapter leaves for its second half.

Setting

Fix a finite ground set $V$. A vector $x \in \mathbb Z^V$ assigns an integer $x(v)$ to each $v \in V$; write $x(X) = \sum_{v \in X} x(v)$ for $X \subseteq V$. For $x, y \in \mathbb Z^V$, the positive support $\operatorname{supp}^+(x-y) = \{v : x(v) > y(v)\}$ and negative support $\operatorname{supp}^-(x-y) = \{v : x(v) < y(v)\}$ record where $x$ exceeds, and falls short of, $y$. A nonempty set $B \subseteq \mathbb Z^V$ is M-convex if it satisfies the exchange axiom (B-EXC[Z]): for all $x, y \in B$ and $u \in \operatorname{supp}^+(x-y)$, some $v \in \operatorname{supp}^-(x-y)$ has 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 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]$, or $S[\mathbb Z]$ when integer-valued) if $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$ for all $X, Y$. Its base polyhedron is $B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X),\ x(V) = \rho(V)\}$. The Lovász extension $\hat\rho : \mathbb R^V \to \mathbb R \cup \{\pm\infty\}$ linearly interpolates $\rho$ off $\{0,1\}^V$: sorting the distinct values of $p \in \mathbb R^V$ as $\hat p_1 > \cdots > \hat p_m$ and setting $U_i = \{v : p(v) \ge \hat p_i\}$, it is $\hat\rho(p) = \sum_{i=1}^{m-1}(\hat p_i - \hat p_{i+1})\rho(U_i) + \hat p_m \rho(U_m)$.

Formalization targets

Goal: discrete separation for M-convex sets

$$B_1 \cap B_2 = \emptyset \implies \exists\, p^* \in \{0,1\}^V \cup \{0,-1\}^V,\quad \inf_{x \in B_1}\langle p^*, x\rangle - \sup_{x \in B_2}\langle p^*, x\rangle \ge 1,$$

for M-convex sets $B_1, B_2 \subseteq \mathbb Z^V$ (Theorem 4.21). This is the weakest stable form of the result — it asserts only the existence of a combinatorially special separator, not any bound tied to $|V|$ or a particular construction, so it is not invalidated by a sharper algorithm for finding $p^*$.

Supporting structural targets

Eleven further results build the calculus this goal rests on: the hyperplane property of M-convex sets (Prop. 4.1), an equivalent one-sided exchange axiom (Prop. 4.2), nonemptiness and the support-function identity for $B(\rho)$ (Props. 4.4-4.5), integrality of $B(\rho)$ for integer-valued $\rho$ (Prop. 4.6), the hole-free property identifying an M-convex set with the integer points of its own convex hull (Thm. 4.12), the two-way polyhedral description of M-convex sets via induced submodular functions (Props. 4.13-4.14), the equivalence of submodularity with convexity of the Lovász extension (Thm. 4.16, due to Lovász), integrality of the intersection of M-convex sets (Thm. 4.22), and Minkowski-sum identities for base polyhedra and M-convex sets (Thm. 4.23).

Significance

The discrete separation theorem is what makes M-convexity discrete rather than merely a polyhedral fact: ordinary separation of two disjoint convex sets by a hyperplane is classical, but here the separator is forced into $\{0,1\}^V \cup \{0,-1\}^V$ — a purely combinatorial object — with no loss of strength. This is the mechanism behind integrality results across combinatorial optimization (e.g., that the intersection of two integral base polyhedra is integral, Theorem 4.22, used pervasively in matroid intersection and submodular flow algorithms). The structural results (holes, Minkowski sums, the Lovász-extension convexity equivalence) are the working toolkit every later use of M-convexity in the book — proximity theorems for M-convex functions (chunks 06+), the discrete conjugacy theorem, submodular flows — draws on without restating.

None of these results are open: Murota attributes the exchange-axiom theory to the matroid and submodular-function literature it systematizes, citing Edmonds, Frank, and Lovász by name for the specific theorems. What this mission produces is a machine-checked formal statement of each result exactly as the book states it, in a shared Lean vocabulary (ExchangeAxiomB, BasePolyhedron, LovaszExtension) that the rest of the Discrete Convex Analysis series builds on; no result here has a prior formalization on the platform (see Formalization scope).

Difficulty

The separation theorem is not proved by convex separation directly — the whole point is that the naive proof (apply the ordinary hyperplane separation theorem to the convex hulls of $B_1, B_2$, then argue the separator can be taken $\{0,1\}$-valued) does not go through, because convex separation alone gives no control over the separator's coefficients. The book instead derives it from Edmonds's intersection theorem (Theorem 4.18, chunk 04-mconvex-sets) applied to a submodular/supermodular pair built from $B_1, B_2$'s associated set functions (Theorem 4.15), routed through Frank's discrete separation theorem (Theorem 4.17) — a genuine two-step reduction, not a direct argument. A second, independent difficulty sits in the supporting results: the hole-free property (Theorem 4.12) requires an explicit induction reducing an arbitrary convex combination representing an integer point to a single element of $B$, a combinatorial exchange argument with no shortcut through general polyhedral theory.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; M-convex sets are Set (V → ℤ); submodular/supermodular functions are Finset V → WithTop ℝ / WithBot ℝ; base polyhedra are Set (V → ℝ). The Lovász extension is formalized directly from the book's own sorted-values construction (SortedValues, LevelSet, Eq. (4.4)-(4.6)), not via an equivalent closed form. Since WithTop ℝ carries no Module ℝ structure, convexity for Theorem 4.16 is stated via a bespoke nonnegative-scalar action (ScalarWithTop) rather than Mathlib's ConvexOn — this changes no mathematical content, only its packaging (see MODERATION_NOTES.md). No numeric constants are hard-coded anywhere in this mission (rule 7 is vacuous). The goal's hypothesis (ExchangeAxiomB plus Nonempty on each $B_i$) is exactly the book's own definition of M-convexity — no weaker substitute (e.g. requiring a specific $\rho$ witness in the hypothesis rather than deriving one, or dropping the $\{0,1\}/\{0,-1\}$ constraint on $p^*$ in favor of a generic separator) would be faithful, and both trivializations are ruled out by construction. This mission's definitions (ExchangeAxiomB, BasePolyhedron, SubmodularSetFunction, LovaszExtension) are redeclared from chunk 04-mconvex-sets rather than imported, since sibling drafts in this series cannot yet reference one another; a later, published version of this book's namespace should consolidate them. Contributions completing any of the twelve sorrys are welcome; the hole-free property (Theorem 4.12) and the goal are the two with the most independent proof content.

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, 1970, pp. 69-87.
• A. Frank, "An algorithm for submodular functions on graphs," Annals of Discrete Mathematics, 16 (1982), pp. 97-120.
• L. Lovász, "Submodular functions and convexity," in Mathematical Programming: The State of the Art, Springer, 1983, pp. 235-257.

Motivation

Convexity is normally defined additively — a function's value at a mixture is bounded by the mixture of its values — but many of the properties that make convexity useful in optimization (a local minimum is global, level sets are well-behaved) survive under a much weaker, purely ordinal notion: quasi-convexity, which compares function values rather than adding them. A nondecreasing rescaling of a convex function is generally not convex, but it is always quasi-convex — so a theory built only on ordinal comparisons automatically covers every such rescaling for free, at the cost of a more delicate proof architecture (since the algebraic cancellations available to additive convexity are no longer available).

Chapter 6's second half asks exactly how far this idea extends in the discrete setting: does the M-convexity exchange axiom have an ordinal, quasi-convex relaxation that still supports the same strong minimization theory — an optimality criterion, a minimizer-cut lemma, and, most significantly, a proximity theorem with the same explicit distance bound? This mission formalizes the chapter's answer: yes, and the relevant relaxed class, functions satisfying condition (SSQM$_{\ne}$), is large enough to include every strictly increasing rescaling of an M-convex function, a class the M-convex theory of chunk 06 alone says nothing about.

Setting

Let $V$ be a finite ground set and $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain. Building on chunk 06's M-convex exchange axiom (M-EXC[Z]), this chapter introduces several ordinal relaxations. $f$ is weakly quasi M-convex, satisfying (QMw), if for every pair of distinct points $x, y \in \operatorname{dom} f$ there exist $u$ in the positive support and $v$ in the negative support of $x - y$ with $f(x - \chi_u + \chi_v) \le f(x)$ or $f(y + \chi_u - \chi_v) \le f(y)$ — an "or" where (M-EXC[Z]) demands an additive inequality. Two further conditions restrict attention to points of different function value and sharpen the conclusion to a three-way trichotomy (strictly better on one side, or exactly tied on both): (SSQM$_{\ne}$) quantifies universally over $u$ (as in (M-EXC[Z])), while (SSQM$_{\ne,w}$) quantifies existentially over both $u$ and $v$ (as in (QMw)). The linear perturbation of $f$ by $p : V \to \mathbb R$ is $f[p](x) = f(x) - \langle p, x \rangle$.

Formalization targets

Goal: Theorem 6.78 (the quasi M-proximity theorem)

Let $f$ satisfy (SSQM$_{\ne}$), $n = |V|$, $\alpha$ a positive integer. If $x_\alpha \in \operatorname{dom} f$ satisfies $f(x_\alpha) \le f(x_\alpha + \alpha(\chi_v - \chi_u))$ for all $u, v \in V$, then $\arg\min f \ne \emptyset$ and there is $x^* \in \arg\min f$ with $\|x_\alpha - x^*\|_\infty \le (n-1)(\alpha - 1)$ — verbatim the same conclusion, and the same exact bound, as chunk 06's Theorem 6.37(1), now established for the strictly larger class satisfying (SSQM$_{\ne}$) rather than the M-convex exchange axiom itself.

Milestones: Theorems 6.68(2), 6.76, 6.77

Theorem 6.68(2): $f$ satisfies (M-EXC[Z]) if and only if every linear perturbation $f[p]$ satisfies (QMw) — quantifying exactly how much weaker (QMw) is pointwise, and how the gap closes once quantified over every perturbation. Theorem 6.76 (the quasi M-optimality criterion): the direct analogue of chunk 06's Theorem 6.26 for the quasi-convexity classes — a purely pairwise local check still characterizes global (or, in the (QMw) case, strict unique) optimality. Theorem 6.77 (the quasi M-minimizer cut): chunk 06's Theorem 6.28 continues to hold verbatim when its M-convexity hypothesis is replaced by (SSQM$_{\ne}$) — the structural fact the proximity theorem's proof is built from survives the relaxation intact.

Significance

The result itself. The proximity theorem is the result algorithms actually use: a scaling algorithm for minimizing quasi-convex functions of this kind inherits exactly the same correctness guarantee, with exactly the same distance bound, as the M-convex case — this is a genuine broadening of chapter 10's algorithmic reach, not a restatement dressed in weaker hypotheses. Every strictly increasing scalar transformation of an M-convex objective (a common modeling device — re-expressing a cost in utility units, or applying a monotone risk measure) now falls under a proximity theorem, whereas prior to this chapter's relaxation such a transformation would generally destroy M-convexity itself and leave optimization theory silent on the transformed problem.

Formalizing it. No matching item exists on the platform for quasi M-convexity in any of its forms. Formalizing Theorem 6.78 requires first pinning down (SSQM$_{\ne}$) exactly (there are six closely related axiom variants in this section of the book, only three of which — (QMw), (SSQM$_{\ne}$), (SSQM$_{\ne,w}$) — are needed for this mission's chosen results), and this mission also captures, via Theorem 6.68(2), the precise sense in which these relaxed conditions are strictly weaker than plain M-convexity while remaining tightly connected to it.

Difficulty

The natural first instinct, given how close the quasi-convexity axioms look to (M-EXC[Z]), is to try to prove Theorem 6.78 by directly imitating chunk 06's proof of Theorem 6.37 line by line. This mostly works — the proof structure (fix a target coordinate, build a chain of strictly decreasing values via repeated exchange steps, bound the chain's length using the scaled hypothesis) survives verbatim — but every step that chunk 06's proof took by adding two instances of the exchange inequality together must be replaced by an ordinal argument, since (SSQM$_{\ne}$) only ever asserts a disjunction of value comparisons, never an additive inequality relating four function values simultaneously the way (M-EXC[Z])'s $f(x)+f(y) \ge f(x-\chi_u+\chi_v)+f(y+\chi_u-\chi_v)$ does. The book's proof handles this by working with strict inequalities and the trichotomy structure of (SSQM$_{\ne}$) directly rather than algebraic cancellation — the same overall architecture, but every arithmetic step rebuilt as a case analysis on which disjunct of (SSQM$_{\ne}$) fires.

Formalization scope

This mission builds directly on chunk 06's published items (CharVec, SuppPos, SuppNeg, DomZ, MExchangeAxiom, ArgMin), per the platform's textbook convention that a later chapter of the same book imports an earlier one's definitions rather than redrafting them; its own namespace DiscreteConvex.MConvexFunctions.Quasi nests under chunk 06's DiscreteConvex.MConvexFunctions accordingly. Δf(z;v,u) (Eq. (6.2)) is never reified as a separate object; every occurrence is unfolded directly into an f-value comparison, avoiding WithTop ℝ subtraction throughout, consistent with chunk 06's own convention.

A trivializing formalization of the goal would silently strengthen (SSQM$_{\ne}$) back to plain M-convexity (making this mission redundant with chunk 06's Theorem 6.37) or loosen the exact bound $(n-1)(\alpha-1)$ to an unspecified function of $n, \alpha$; neither is done. Six axiom variants appear in this section of the book ((QM), (SSQM), (QMw), (SSQM$_w$), (SSQM$_{\ne}$), (SSQM$_{\ne,w}$)); only the three actually needed by this mission's four items are drafted, and Theorem 6.68's first part (an implication chain among the other three) is left out — see MODERATION_NOTES.md. Contributions building the polyhedral M-convex-function bridge (§6.11–6.12, Theorems 6.59–6.64), the level-set characterizations (Theorems 6.72, 6.74), or the scaled quasi M-minimizer cut (Theorem 6.79, the direct generalization of Theorem 6.77 drafted here) are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• M. Avriel, W. E. Diewert, S. Schaible, I. Zang, Generalized Concavity, Plenum Press, 1988.

Motivation

Convexity on the integer lattice cannot be defined by the classical secant-line inequality alone: a function can be midpoint-convex along every line and still admit no useful global optimality theory, because integer points off a chosen line are invisible to it. M-convex functions, introduced by Murota, resolve this by replacing the secant condition with an exchange axiom directly generalizing the basis-exchange property of matroids and the convex-hull structure of network flows: a function on the integer lattice is M-convex if, whenever two points can be improved by moving one coordinate up and a compensating coordinate down, at least one such move weakly improves the sum of the two function values. This single axiom turns out to be equivalent to several strikingly different-looking properties — invariance under a wide family of domain operations, supermodularity in the M♮ (translation-invariant) case, and, most importantly, a local-to-global optimality principle: a point is a global minimizer of an M-convex function if and only if no single coordinate exchange improves it. This mission develops the algebraic core of that theory — the exchange axiom's basic consequences, its equivalent local and dynamic reformulations, and the operations that preserve it — building toward the theorem that recasts M-convexity itself as an algorithmically meaningful local-search guarantee.

Companion mission 06-mconvex-functions-i (Discrete Convex Analysis V) covers this chapter's own primary line of development: the equivalence of M-convexity and M♮-convexity with their respective exchange axioms (Theorem 6.2), the M-optimality criterion (Theorem 6.26), a minimizer-cut lemma (Theorem 6.28), and the M-proximity theorem (Theorem 6.37, its goal). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results that chapter leaves for a second pass: the domain structure of M- and M♮-convex functions, worked examples (quadratic forms, quasi-separable functions), the operations that preserve M-convexity, supermodularity of the M♮-convex case, the descent-direction property, and — this mission's goal — the equivalence of the exchange axiom with a dynamic sequential-improvement property.

Setting

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

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

Writing $\tilde f(x_0, x) = f(x)$ when $x_0 = -x(V)$ and $+\infty$ otherwise (a lift to one extra coordinate), $f$ is M$^\natural$-convex if $\tilde f$ is M-convex; M♮-convexity is a genuine generalization of M-convexity (every M-convex function is M♮-convex, but not conversely) and coincides with it exactly when $\operatorname{dom} f$ lies on a single hyperplane. The linear-weighted function $f[p](x) = f(x) - \langle p, x \rangle$ (for $p \in \mathbb R^V$) is the standard device for testing local optimality under an arbitrary reweighting.

Formalization targets

Goal: the exchange axiom as sequential improvement

$$f \text{ is M-convex} \iff \forall p \in \mathbb R^V,\ \forall x, y \in \operatorname{dom} f,\ f[p](x) > f[p](y) \implies f[p](x) > \min_{u \in \operatorname{supp}^+(x-y)}\ \min_{v \in \operatorname{supp}^-(x-y)} f[p](x - \chi_u + \chi_v),$$

with the analogous statement for M♮-convexity (Theorem 6.24). This is the weakest stable form: it makes no reference to a specific algorithm, only to the existence of an improving single exchange whenever the current point is suboptimal under any linear reweighting — a property a faster algorithm could exploit without invalidating the characterization itself.

Supporting structural targets

Eleven further results build the vocabulary and toolkit this goal draws on: the domain structure of M-convex and M♮-convex functions (Propositions 6.1, 6.7), the equivalence of the exchange axiom with a local, bounded-distance version (Theorem 6.4), worked examples establishing M-convexity for quadratic forms, univariate, conservation-law, and quasi-separable functions (Propositions 6.8-6.9), the domain and range operations preserving M-convexity (Theorem 6.13, Proposition 6.14), supermodularity of the M♮-convex case (Theorem 6.19), the descent-direction property (Proposition 6.23) that Theorem 6.24 generalizes, and a discrete subgradient inequality (Proposition 6.25).

Significance

Theorem 6.24 is the bridge between the static exchange axiom (a property of function values at pairs of points) and the dynamic behavior of local-search algorithms: it says a greedy single-coordinate-exchange step, applied to any linearly reweighted version of an M-convex function, always finds a strict improvement when one exists. This is exactly the guarantee that makes steepest-descent-type algorithms for M-convex function minimization correct, and it is the theorem chapter 10's algorithmic analysis (Schrijver-type methods) relies on implicitly whenever it argues that local exchange steps make global progress. The descent-direction property (Proposition 6.23) is the special case $p=0$, isolating the core combinatorial fact before the reweighting machinery is added. The operations catalog (Theorem 6.13) is the practical toolkit that lets later chapters build complex M-convex functions (network flow costs, matroid rank functions composed with linear maps) from simple pieces without re-verifying the exchange axiom from scratch each time.

None of these results are open — they are Murota's own systematic development of the exchange- axiom theory, with worked examples drawn from classical quadratic and separable function theory. What this mission contributes is a faithful, machine-checked formal statement of each, sharing the Lean vocabulary (MExchangeAxiom, MNaturalConvex, LinearWeight) the rest of the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The forward direction of Theorem 6.24 (M-convex $\implies$ sequential improvement) follows in one step from Proposition 6.23 applied to $f[p]$, itself M-convex by Theorem 6.13(3) — routine once those two pieces are in hand. The converse is the substantial direction: it must derive the full static exchange axiom from a property that only ever exhibits some improving exchange at some linear weighting, for every pair of suboptimal points — the proof constructs an explicit adversarial weighting $p$ designed so that failure of the local exchange step at that specific $p$ forces the domain itself to be M-convex (via Theorem 4.3) and then forces the local exchange axiom (M-EXCloc[Z]) via a bipartite-matching argument on the coordinates that differ, finally invoking Theorem 6.4 to lift locality to the full exchange axiom. No shortcut bypasses this two-stage reduction (domain structure, then local exchange) — attempting to verify (M-EXC[Z]) directly from (M-SI[Z]) without first pinning down that $\operatorname{dom} f$ is M-convex fails because the exchange axiom's own statement presupposes a well-structured domain.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; functions are (V → ℤ) → WithTop ℝ. SuppPos/SuppNeg are Finset V (not Set V), matching how the (M-SI[Z])/(M♮-SI[Z]) axioms and the descent-direction property use Finset.inf, whose value on an empty index set is ⊤ — exactly the book's own stated convention for an empty minimum. No Module ℝ or ConvexOn machinery is used for WithTop ℝ-valued arithmetic; scalar actions by positive reals (PosScalarMul, Theorem 6.13(1)) and by naturals (FCheck's flow coefficients, Proposition 6.25) are built directly from the native order and AddMonoid structure. No numeric constants are hard-coded anywhere in this mission (rule 7 is vacuous); Proposition 6.8's quadratic-form conditions are stated with the book's own literal coefficients ($0$, and the min/≥ structure of Eq. (6.25)-(6.28)), not a special case. Theorem 6.13's parts (7) (aggregation) and (8) (integer infimal convolution) are not restated here since the book itself proves them only later via Chapter 9's network-transformation machinery — see the Difficulty note and MODERATION_NOTES.md; this is not a trivializing omission, since the six operations that are included already exercise every domain- and range-transformation technique this mission's goal needs. This mission's definitions (MExchangeAxiom, MNaturalConvex, CharVec, DomZ, SuppPos, SuppNeg, CharVecOpt) are redeclared from chunk 06-mconvex-functions-i rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal's converse direction and Theorem 6.13's operations are the two with the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 (the exchange axiom and its equivalent local/dynamic reformulations).

Motivation

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

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

Setting

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

Formalization targets

Goal: convex extensibility characterizes M-convexity

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

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

The Legendre-Fenchel transform is the single most structurally important operation in convex analysis: for a proper closed convex function $f$, its conjugate $f^\bullet(p) = \sup_x \{\langle p,x\rangle - f(x)\}$ is again proper closed convex, and the transform is an involution — $f^{\bullet\bullet} = f$. This one fact underlies duality theory across optimization: every strong-duality theorem is, at bottom, a statement about conjugate pairs. Chapters 6 and 7 of this book developed M-convex and L-convex functions as if they were two separate theories, each with its own exchange axiom, optimality criterion, and proximity theorem. Chapter 8 reveals they were never separate: the Legendre-Fenchel transform, suitably discretized, is a bijection between the two classes. This mission formalizes that discrete conjugacy theorem together with its classical real-valued precursor and a genuine function-level generalization of Edmonds's intersection theorem, completing the picture that chunks 06 through 09 built the two halves of.

Setting

Let $V$ be a finite ground set. For $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$, the Legendre-Fenchel transform is $f^\bullet(p) = \sup\{\langle p,x\rangle - f(x) : x \in \mathbb R^V\}$; $f$ is submodular if $f(x)+f(y) \ge f(x\vee y)+f(x\wedge y)$ and supermodular under the reverse inequality. For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$, the discrete Legendre-Fenchel transform restricts the same supremum formula to $p \in \mathbb Z^V$: $f^\bullet(p) = \sup\{\langle p,x\rangle - f(x) : x \in \mathbb Z^V\}$ for $p \in \mathbb Z^V$ — a genuinely different object from the real-valued transform, since the supremum is now over integer $x$ only, and the codomain is checked back against the discrete M-/L-convexity axioms of chunks 06–09. The integer biconjugate $f^{\bullet\bullet}$ is the transform applied twice. $f$ is integer valued if every finite value it takes is an integer (the classes $M[\mathbb Z\to\mathbb Z]$, $L[\mathbb Z\to\mathbb Z]$ of the goal theorem are exactly the M-/L-convex functions with this property).

Formalization targets

Goal: Theorem 8.12 (the discrete conjugacy theorem)

(1) The classes $M[\mathbb Z\to\mathbb Z]$ and $L[\mathbb Z\to\mathbb Z]$ are in one-to-one correspondence under the discrete Legendre-Fenchel transform: for $f \in M[\mathbb Z\to\mathbb Z]$ and $g \in L[\mathbb Z\to\mathbb Z]$, $f^\bullet \in L[\mathbb Z\to\mathbb Z]$, $g^\bullet \in M[\mathbb Z\to\mathbb Z]$, $f^{\bullet\bullet}=f$, and $g^{\bullet\bullet}=g$. (2) The same correspondence holds between $M^\natural[\mathbb Z\to\mathbb Z]$ and $L^\natural[\mathbb Z\to\mathbb Z]$.

Milestones: Theorem 8.1, Proposition 8.11, Theorem 8.17

Theorem 8.1: the conjugate of a real-valued submodular function is always supermodular — the classical warm-up, and evidence that submodularity/supermodularity is not symmetric under conjugation on its own (the converse fails). Proposition 8.11: the integer biconjugate recovers $f$ at any point with a nonempty integer subdifferential — the fact that makes discrete biconjugation meaningful at all. Theorem 8.17 (the M-convex intersection theorem): a point jointly minimizes a sum of two M$^\natural$-convex functions if and only if a single linear functional separately certifies it as a minimizer of each perturbed function — the function-level generalization of chunk 04's Edmonds's intersection theorem for M-convex sets.

Significance

The result itself. The discrete conjugacy theorem is, in the book's own words, "the unifying result of the entire book": every theorem proved separately for M-convex functions (chunks 06–07) has an exact mirror for L-convex functions (chunks 08–09) precisely because the Legendre-Fenchel transform carries one class to the other. Theorem 8.17's function-level Edmonds generalization shows the payoff directly — the classical matroid-intersection-style min-max duality of chunk 04 was never really about sets; it is a special case (indicator functions) of a duality that holds for the whole class of M-convex functions.

Formalizing it. No matching item exists on the platform for conjugate functions, discrete conjugacy, or this generality of intersection theorem. This mission gives the first formal statement of the discrete conjugacy theorem, distinguishing it carefully from its real-valued (polyhedral) precursor, Theorem 8.4 — a genuinely different, harder theorem this mission does not draft (see Formalization scope), since the integer bijection needs the M-/L-proximity theorems of chunks 06–09 to control integrality under convex extension, while the real-valued case does not.

Difficulty

The obvious approach — try to prove the discrete conjugacy theorem directly by mimicking the real-valued proof (Theorem 8.4) with ℤ in place of ℝ everywhere — fails, because the real-valued proof's key step (Proposition 8.3, an infimal-convolution argument comparing arg min sets of perturbed polyhedral functions) has no immediate discrete analogue: a discrete arg min need not vary continuously with the perturbation the way a polyhedral one does. The book's actual strategy instead routes through the convex extension of the discrete function (chunk 06/08's bridge to chapter 3's integral convexity), applies the already-proved real-valued conjugacy theorem to the extension, and then must separately argue that the resulting conjugate, restricted back to integer points, is again integer-valued and satisfies the discrete exchange axiom — an argument that needs different treatment depending on whether the original function's domain is bounded or unbounded (an exhaustion argument via restriction to a growing integer interval, invoking chunk 06's proximity theorem to control convergence). Skipping this discreteness argument and treating the real-valued theorem as if it settled the integer case would silently discard exactly the chapter's own point.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq. ConvexConjugate (the discrete transform) has domain and codomain both (V → ℤ) → WithTop ℝ, obtained by taking the defining supremum in EReal (a complete lattice, so it is always total) and projecting back via a new FromEReal map — this is what lets the biconjugate f•• typecheck as an equality of functions of the same type as f. ConvexConjugateR (the real-valued transform, used only by the milestone Theorem 8.1) is a separate object with no shared code, per the explicit warning against conflating the two transforms; the two never appear in the same item.

A trivializing formalization of the goal would draft only the real-valued case (Theorem 8.4) as if it were the discrete theorem, or would silently allow WithTop ℝ's subtraction-avoidance convention to change which values are compared; neither is done. Theorem 8.4 itself (the polyhedral conjugacy theorem) is not drafted in this mission at all — it would require a fresh, otherwise-unused polyhedral M-/L-convex-function layer on Rⱽ that no other item here needs (see MODERATION_NOTES.md). The M-/L-separation theorems (8.15, 8.16) and the Fenchel-type duality theorem (8.21) are likewise left for a follow-on mission; contributions building the polyhedral bridge or the separation theorems, which depend on machinery this mission establishes, are welcome.

Selected references

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

Motivation

Chapter 8 is where discrete convex analysis explains why it needed two separate notions — M-convexity (exchangeability) and L-convexity (submodularity) — rather than one. The answer is conjugacy: under the classical Legendre-Fenchel transform, the two classes turn out to be exactly dual to each other, the discrete analogue of the fact that convex analysis's transform is self-dual within a single class of convex functions. Mission 10-conjugacy-i proved the integer-lattice version of this fact (Theorem 8.12) but explicitly deferred the polyhedral version — Theorem 8.4, the chapter's own headline "Conjugacy theorem" — noting it needed a real-variable M-/L-convex-function layer the series had not yet built. That layer now exists, built across missions 23-24-ch06*-mconvexfunctions and 26-27-ch07*-lconvexfunctions. This mission proves Theorem 8.4 and its companions: the polar-cone correspondence it induces, its nonpolyhedral generalization, the separation and Fenchel-duality theorems for M♮-/L♮-convex functions, and the basic theory of M2-convex functions (sums of M-convex functions), which the Edmonds intersection theorem's own combinatorics is built from.

Setting

Fix a finite ground set $V$. For $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$, the Legendre-Fenchel transform is $f^\bullet(p) = \sup_x [\langle p,x\rangle - f(x)]$. A polyhedral convex function $f$ is M-convex ($f \in M[\mathbb R \to \mathbb R]$) if it satisfies (M-EXC[R]); $g$ is L-convex ($g \in L[\mathbb R \to \mathbb R]$) if it satisfies (SBF[R]) and (TRF[R]). A concave function $h$ is always represented via $h_2 = -h$, an ordinary convex function, so every "$f \ge h$" hypothesis is restated as "$f + h_2 \ge 0$" — an equivalent formulation avoiding any need to represent $-\infty$ in the codomain. A polyhedral cone's polar is $C^\circ = \{y : \langle y,x\rangle \le 0\ \forall x \in C\}$. A function is M2-convex if it is the sum of two M-convex functions.

Formalization targets

Goal: the conjugacy theorem (Theorem 8.4)

The classes of polyhedral M-convex functions and polyhedral L-convex functions are in one-to-one correspondence under the Legendre-Fenchel transform: $f \in M \Rightarrow f^\bullet \in L$, $g \in L \Rightarrow g^\bullet \in M$, and the transform is an involution ($f^{\bullet\bullet}=f$, $g^{\bullet\bullet}=g$) on each class, with the identical statement for the M$^\natural$/L$^\natural$ variants. This is the theorem mission 10-conjugacy-i deferred, citing exactly the missing infrastructure this series has since built.

Supporting structural targets

Twelve further results build the surrounding theory. Proposition 8.2 gives the easy two-variable case of the general submodularity-preservation fact (Theorem 8.1, already a milestone of mission 10-conjugacy-i); Proposition 8.3 is the technical minimizer-difference lemma the goal's harder direction is built from. Theorem 8.5 derives the M-convex/L-convex cone polarity from the goal, and Theorem 8.6 extends the correspondence beyond the polyhedral case to general closed proper convex functions. Proposition 8.14 and Theorems 8.15-8.16 build the separation theory for M♮-/L♮-convex and concave function pairs, with integral witnesses when the functions are integer valued; Theorem 8.21 (parts 1-2) derives the Fenchel-type strong-duality equality these separation theorems make possible. Propositions 8.29-8.30 and Theorem 8.31 (plus Theorem 8.32, found by direct reading immediately after 8.31) build the basic theory of M2-convex functions: their domains and minimizer sets are M2-convex, they are integrally convex, and their global optimality reduces to a finite local check.

Significance

The goal is the theorem that retroactively explains this entire series' two-track structure: missions 20-25 (M-convex sets and functions) and 08/21/26-28 (L-convex sets and functions) are not two independent theories that happen to share techniques — they are conjugate images of each other, so every theorem proved on one side has a dual counterpart automatically available on the other via Theorem 8.4. This is made concrete immediately: Theorem 8.5's cone polarity and the diagram the book draws connecting $M_0[\mathbb R]$, $0L[\mathbb R\to\mathbb R]$, and submodular set functions $S[\mathbb R]$ (already correspondences this series proved independently, in missions 24-ch06d-mconvexfunctions and 28-ch07d-lconvexfunctions) are shown to be facets of one single conjugacy fact rather than three separate coincidences. The separation and Fenchel duality theorems (8.15, 8.16, 8.21) are the discrete analogues of the two theorems every convex optimization course opens with, and the book is explicit that they are not corollaries of the classical versions plus convex extensibility — they carry genuinely combinatorial content, specializing to Frank's discrete separation theorem and Edmonds's intersection theorem as examples the book itself gives.

None of these results are open — they are Murota's account of the duality at the heart of discrete convex analysis, the reason the theory needed two dual notions rather than one. What this mission contributes is a faithful, machine-checked formal statement of each, completing a theorem mission 10-conjugacy-i explicitly left for a future session once the necessary polyhedral apparatus existed, and including one result (Theorem 8.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal's harder direction (L⇒M) would try to verify the exchange inequality for $g^\bullet$ directly from the definition of the transform; the book's actual proof instead identifies the exchange inequality with a statement about weighted minimizers of $g$ itself via Proposition 8.3 (the minimizer-difference bound), converting a claim about the conjugate function into a claim about $g$'s own combinatorial structure — a genuine change of perspective, not a direct calculation. Proposition 8.3's own proof is the hardest single argument in this block: it derives the minimizer-difference bound by a contradiction argument that constructs an explicit pair of "worse" minimizers via a join/meet perturbation and derives a strict inequality from Theorem 7.29's translation inequality — a multi-step combinatorial argument with no direct shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; convex functions are WithTop ℝ valued throughout (never EReal, except for the Legendre-Fenchel transform itself, whose defining supremum/infimum can genuinely be infinite). All thirteen numbered results found in this chunk's page range — the twelve in BRIEF.md's own table plus Theorem 8.32 — are placed, with one documented scope reduction: Theorem 8.21 states only its real-attainment parts (1)-(2), not the integer-attainment refinement of parts (3)-(4), which needs a separate argument no other result in this chunk requires — see HARD.md. Concave functions $h$ are always represented via $h_2 = -h$ and every inequality $f \ge h$ restated as $f + h_2 \ge 0$, avoiding WithTop ℝ negation entirely. This chunk's own BRIEF.md inherited the chapters-4-7 page-offset boilerplate (printed = PDF $-$ 19); chapter 8 uses offset 18, confirmed against the PDF's own footers — every citation here uses the corrected offset. This mission's base vocabulary is redeclared from missions 10-conjugacy-i, 20-ch04b-mconvexsets, 21-ch05b-lconvexsets, 23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the thirteen sorrys are welcome; the goal and Proposition 8.3 carry the most independent proof content.

Selected references

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

Motivation

Mission 29-ch08b-conjugacyduality opened chapter 8's account of M2-convex functions — sums of M-convex functions — proving their domains and minimizers are M2-convex and that they are integrally convex. This mission completes that program and builds its exact mirror for L2-convex functions (integer infimal convolutions of L-convex functions), the class that appears on the opposite side of Edmonds's intersection theorem's min-max relation from M2-convexity. It proves optimality and proximity theorems for both classes, shows their subdifferentials add (a discrete analogue of the classical subdifferential sum rule), derives how the Legendre-Fenchel transform interacts with the sum/infimal-convolution operation, and — the technically hardest result in the whole cluster — establishes that L♮₂-convex functions are integrally convex, by a genuinely different and more intricate argument than the M2-side analogue required.

Setting

Fix a finite ground set $V$. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is L2-convex if $g = g_1 \square g_2$, the integer infimal convolution $g_1\square g_2(p) = \inf\{g_1(p_1)+g_2(p_2) : p_1+p_2=p\}$, of two L-convex functions $g_1, g_2$; L$^\natural_2$-convex if the summands are L$^\natural$-convex. An M2-convex function is a sum $f_1+f_2$ of two M-convex functions (mission 29-ch08b-conjugacyduality). The integer subdifferential $\partial_{\mathbb Z} f(x)$ and real subdifferential $\partial_{\mathbb R} f(x)$ generalize the subgradient set to integer- and real-valued perturbation directions respectively.

Formalization targets

Goal: L$^\natural_2$-convex functions are integrally convex (Theorem 8.42)

Every L$^\natural_2$-convex function is integrally convex, and in particular every L$^\natural_2$-convex set is integrally convex. The book's own proof is the most intricate argument in this cluster: given $p$ in the Minkowski sum $D_1+D_2$ of two L-convex sets, it constructs an explicit representation of $p$ as a convex combination of finitely many integer points of $D_1+D_2$, all lying in $p$'s own integral neighborhood, via the sorted fractional-part values of a chosen decomposition $p=p_1+p_2$ — a genuinely different technique from the M2-side analogue (Theorem 8.31), whose proof is a two-line consequence of convex extensibility.

Supporting structural targets

Eleven further results build the M2-/L2-convex theory in parallel. Theorems 8.33-8.34 give the M2-optimality criterion (a nonnegative-sum condition over cyclic exchange families) and its scaling-based proximity theorem; Theorem 8.35 shows subdifferentials of a sum of M$^\natural$- convex functions add, and that subdifferentials of M2-/M$^\natural_2$-convex functions are L2-/L$^\natural_2$-convex; Theorem 8.36 computes the conjugate of a sum as the infimal convolution of conjugates, with biconjugacy recovering the original sum. Propositions 8.39-8.41 transfer L-(natural-)convexity from summands to the domain and minimizer set of an L2-convex function, and give the precise attainment condition under which a linearly-perturbed infimal convolution's minimizer set splits additively. Theorems 8.43-8.44 give the L2-optimality and L2-proximity theorems, the exact L-side mirrors of Theorems 8.33-8.34; Theorem 8.45 mirrors Theorem 8.35 for subdifferentials of an infimal convolution; and Theorem 8.46 (found by direct reading, immediately following 8.45 and explicitly named by the book as 8.36's counterpart) shows biconjugacy for L$^\natural$-convex infimal convolutions.

Significance

The M2-/L2-convex function classes are where discrete convex analysis's abstract machinery meets concrete combinatorial optimization: Edmonds's matroid intersection theorem and its generalizations are literally statements about M2-convex minimization, with the L2-convex side supplying the dual bound. Theorem 8.35's subdifferential additivity is the discrete analogue of the classical Moreau-Rockafellar sum rule, and its proof (via the M-convex intersection theorem, already a milestone of mission 10-conjugacy-i) shows the sum rule holding without the constraint-qualification technicalities the continuous theory needs — a case where the discrete theory is cleaner than its continuous ancestor. Theorem 8.42's harder, dedicated proof technique is itself informative: it demonstrates that L2-convexity's combinatorial structure is not a routine transcription of the M2-convex case, foreshadowing the book's broader theme that M- and L-convexity, while conjugate, are not interchangeable in how their proofs actually work.

None of these results are open — they are Murota's account of the sum/infimal-convolution closure properties of M-convex and L-convex functions, continuing chapter 8's duality program into its most combinatorially concrete corner. What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Theorem 8.46) the platform's own automated extractor missed, extending the shared Lean vocabulary (InfConv, L2Convex, M2ConvexSet) mission 29-ch08b-conjugacyduality began; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to adapt the M2-side integral-convexity proof (a direct appeal to convex extensibility) verbatim; the book's own proof shows this does not work, requiring instead a from-scratch construction: decompose $p=p_1+p_2$, take fractional parts $a_1 = p_1-\lfloor p_1\rfloor$ and $a_2=\lceil p_2\rceil-p_2$, sort their combined distinct values, build threshold sets exactly as in the Lovász-extension construction, and verify each resulting integer point $q_i = \lfloor p_1\rfloor+\chi_{U_{1i}}+\lceil p_2\rceil-\chi_{U_{2i}}$ both lies in $D_1+D_2$ (via L-convex-set closure properties, Theorem 5.10) and in $p$'s integral neighborhood (a case split on whether $p(v)$ is itself an integer) — a genuinely multi-stage combinatorial argument with no single-inequality shortcut, unlike almost every other result in this mission.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; M2-/L2-convex functions are (V→ℤ)→WithTop ℝ. All twelve numbered results found in this chunk's page range are placed, with no partial-coverage scope reduction needed — every clause of every result, including all three parts of Theorems 8.35 and 8.45 and the full cyclic-exchange condition of Theorems 8.33-8.34, is stated in full. One numbered result nominally in this chunk's page range, Theorem 8.32, is not re-placed here: it was already found and placed as a milestone in mission 29-ch08b-conjugacyduality, whose own page range overlaps this chunk's by one page (PDF245) — see HARD.md. "g1□g2 > −∞" hypotheses are omitted rather than translated, since WithTop ℝ has no −∞ element to violate. This mission's base vocabulary is redeclared verbatim from mission 29-ch08b-conjugacyduality rather than imported, since sibling drafts in this series cannot yet reference one another; ConvexConjugate is redeclared from mission 10-conjugacy-i. Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 8.35 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, "Extreme points of a generalized polymatroid," Discrete Applied Mathematics, 152 (2005), pp. 268-278 [153] (the L2-convex integral-convexity proof this mission's goal is drawn from).
• K. Murota and A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [162] (the M2-proximity theorem, Theorem 8.34).

Motivation

Missions 29-ch08b-conjugacyduality and 30-ch08c-conjugacyduality built the M2-/L2-convex function classes and proved their conjugacy correspondence is nearly complete. This mission finishes that correspondence (Theorems 8.48-8.49) and then turns to chapter 8's capstone application: a Lagrangian duality theory for integer programs, built entirely from the M-/L-convexity machinery developed across the whole book. It develops the general perturbation-based duality framework (mirroring Rockafellar's conjugate duality for nonlinear programming), specializes it to M-convex programs via the perturbation $F_r$, and proves the strong duality theorem this specialization exists to deliver — together with its mirror construction recovering the primal problem from the dual.

Setting

An M-convex program consists of a set $B\subseteq\mathbb Z^V$ satisfying (REG) — $B$ is an M-convex set — and an objective $c:\mathbb Z^V\to\mathbb Z\cup\{+\infty\}$ satisfying (OBJ) — $c$ is an M-convex function. The general duality framework embeds any $f(x)=c(x)+\delta_B(x)$ in a family of perturbed problems via $F:\mathbb Z^V\times\mathbb Z^V\to\mathbb Z\cup\{+\infty\}$ with $F(x,0)=f(x)$, yielding an optimal-value function $\varphi$, a Lagrangian $K$, and a dual objective $g$. For M-convex programs the perturbation $F_r(x,u)=c(x)+\delta_B(x+u)+r(u)$, for an M-convex regularizer $r$ with $r(0)=0$, makes this framework concrete; the case $r\equiv 0$ is written with subscript $0$.

Formalization targets

Goal: Strong duality for M-convex programs (Theorem 8.59)

For a feasible, bounded-below M-convex program, $\min(P)=\varphi_r(0)=\varphi_r^{\bullet\bullet}(0) =\max(D_r)$, and $\operatorname{opt}(D_r)=-\partial_{\mathbb Z}\varphi_r(0)$. This is the theorem mission 11-conjugacy-ii-lagrange's own STATUS.md explicitly deferred, noting it needs the specific M-convex perturbation $F_r$ (Eq. (8.61)) and Propositions 8.55-8.56/Theorems 8.57-8.58 as prerequisites — all built as milestones of this mission.

Supporting structural targets

Theorem 8.48 completes the M2-/L2-convex conjugacy correspondence; Theorem 8.49 characterizes separable convex functions as exactly the M$^\natural_2$-and-L$^\natural_2$-convex functions. Theorem 8.53 (reduced to parts (1),(2),(4)) gives the general perturbation-independent duality identities: the dual objective is $g=-\varphi^{\bullet}(-\cdot)$, weak duality's biconjugate form $\sup(D)=\varphi^{\bullet\bullet}(0)$, and the equivalence of strong duality with biconjugate exactness. Proposition 8.55 shows the M-convex perturbation $F_r$ legitimately instantiates the general framework; Proposition 8.56 (reduced to part (1)) gives the closed form for the unregularized Lagrangian kernel $K_0$ via the conjugate of $B$'s indicator function; Theorems 8.57 and 8.58 establish the resulting convexity/concavity of the kernel, the dual objective, and the optimal-value function in each of their arguments. Propositions 8.62-8.63 and Theorems 8.64-8.65 build and analyze the mirror construction — the dual perturbation $G_r$, its optimal-value function $\gamma_r$, and the dual-of-dual reconstruction — showing that for bounded $B$ the process exactly recovers the primal problem and its own strong duality theorem.

Significance

This is chapter 8's payoff: a full nonlinear-integer-programming duality theory, built without any convexity assumption beyond M-/L-convexity, mirroring Rockafellar's classical conjugate duality approach line for line while replacing every continuous convexity argument with a discrete M-/L-convexity one. Theorem 8.59's proof is a two-line consequence of the machinery this mission assembles (Theorems 8.35, 8.53, 8.58), which is itself the point: the discrete theory's hard combinatorial work (Theorems 8.35, 8.36, 8.42 from prior missions) is what makes the strong duality theorem here nearly free, exactly as convex analysis makes classical Lagrangian duality nearly free once Fenchel duality is established. The bidirectional construction of Theorems 8.62-8.65 is the discrete analogue of the classical fact that Lagrangian duality is symmetric between primal and dual convex programs.

None of these results are open — they are Murota's own account of M2-/L2-conjugacy and Lagrangian duality (section 8.3.3 and section 8.4), continuing chapter 8's duality program to its conclusion. What this mission contributes is a faithful, machine-checked formal statement of each, completing the platform's coverage of chapter 8's duality theorems begun in missions 10-conjugacy-i and 11-conjugacy-ii-lagrange; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The EReal-valued ($\mathbb Z\cup\{\pm\infty\}$) typing is essential and new to this mission: unlike every prior mission in this series, the general framework's derived quantities ($\varphi$, $K$, $g$, and their mirror-construction analogues $G_r$, $\gamma_r$, $\tilde K_r$, $\tilde f$) are defined as infima/suprema over families that are not a priori bounded, so they can genuinely equal $-\infty$ or $+\infty$ — a value WithTop ℝ cannot represent and whose sInf instance would silently substitute a junk value (0) rather than correctly returning $-\infty$. The book's own repeated "$X$ is convex (resp. concave), or $X\equiv+\infty$, or $X\equiv-\infty$" disjunctive escape clauses (Theorems 8.57, 8.58, Propositions 8.63) are captured with two small generic combinators, IsEmbedOf/IsNegOf, rather than restating the embedding by hand at each of the roughly dozen occurrences.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; the base M-/L-/M2-/L2-convexity vocabulary is redeclared verbatim from missions 29-ch08b-conjugacyduality and 30-ch08c-conjugacyduality, since sibling drafts in this series cannot yet reference one another. Two results carry a documented partial-coverage scope reduction (see HARD.md): Theorem 8.53 is placed with only parts (1),(2),(4), the purely algebraic identities holding unconditionally for any perturbation $F$, omitting parts (3),(5),(6), which characterize $\operatorname{opt}(D)$ under the book's own biconjugacy hypothesis (8.55) — a hypothesis this mission's M-convex-specific Theorem 8.59 later establishes directly rather than invoking Theorem 8.53's general form; and Proposition 8.56 is placed with only part (1), the $K_0$ closed form, omitting part (2), the $K_r$ closed form via the infimal convolution $\delta_{-B}\square r[y]$, not independently needed elsewhere in this chunk. One numbered result nominally in this chunk's page range, Theorem 8.46, is not re-placed here: it was already found and placed as a milestone in mission 30-ch08c-conjugacyduality, whose own page range overlaps this chunk's by one page (PDF251/printed 233) — see HARD.md. Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 8.57 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• R. T. Rockafellar, "Conjugate duality and optimization," CBMS-NSF Regional Conference Series in Applied Mathematics, SIAM, 1974 [177] (the classical conjugate-duality framework this mission's section 8.4 adapts to the discrete M-/L-convex setting).
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (the original source of M2-/L2-convexity, Theorems 8.35, 8.36, 8.45, 8.46, 8.48, and the Lagrange duality theory of section 8.4).

Motivation

Chapters 6 through 8 built M-convex and L-convex functions and their conjugacy theory as abstract combinatorial objects on the integer lattice. Chapter 9 grounds that theory in a setting every reader already knows: network flows. The chapter's throughline is that the classical minimum cost flow problem — flows bounded by simple arc capacities, with a single linear cost — is a shadow of a much richer submodular flow problem, in which the constraint on a flow's boundary is not "equal a fixed supply vector" but "lie in the base polyhedron of an arbitrary submodular set function." This mission formalizes the feasibility theory for both problems and its capstone: a max-flow min-cut theorem for submodular flows that specializes to the classical max-flow min-cut theorem exactly when the submodular function degenerates to a plain capacity function.

Setting

Let $G = (V, A)$ be a finite directed graph, with $\mathrm{tail}, \mathrm{head} : A \to V$ giving each arc's start and end vertex. The boundary of a flow $\xi : A \to \mathbb R$ is $\partial\xi(v) = \sum_{a : \mathrm{tail}(a) = v} \xi(a) - \sum_{a : \mathrm{head}(a) = v} \xi(a)$. For $X \subseteq V$, $\Delta^+X$ and $\Delta^-X$ are the arcs leaving and entering $X$. Given an upper capacity $\bar c : A \to \mathbb R \cup \{+\infty\}$ and lower capacity $\underline c : A \to \mathbb R \cup \{-\infty\}$, the cut capacity function is $\kappa(X) = \bar c(\Delta^+X) - \underline c(\Delta^-X)$. A submodular set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ with $\rho(\emptyset) = \rho(V) = 0$ plays the same structural role as $\kappa$ but is arbitrary problem data rather than a derived quantity.

Formalization targets

Goal: Theorem 9.13 (max-flow min-cut for submodular flows)

For a feasible maximum submodular flow problem on a specified arc $a_0$: $\sup\{\xi(a_0) : \xi \text{ feasible}\} = \min\big(\bar c(a_0), \min_X\{\bar c(\Delta^-X) - \underline c(\Delta^+X \setminus \{a_0\}) + \rho(X) : a_0 \in \Delta^+X\}\big)$, a common value in $\mathbb R \cup \{+\infty\}$; if the data is integer valued and the value is finite, an integer-valued maximum flow exists.

Milestones: Proposition 9.2, Theorem 9.3, Theorem 9.10

Proposition 9.2: the cut capacity function $\kappa$ is always submodular — the fact that lets the classical minimum cost flow problem's feasibility be phrased in exactly the same base- polyhedron language as the general submodular flow problem. Theorem 9.3: a flow meeting the capacity constraint with boundary $x$ exists if and only if $x(X) \le \kappa(X)$ for all $X$ and $x(V) = 0$ — the classical case, and the direct predecessor of the goal's feasibility side. Theorem 9.10: the submodular flow problem is feasible if and only if $\bar c(\Delta^-X) - \underline c(\Delta^+X) + \rho(X) \ge 0$ for all $X$ — obtained from Theorem 9.3 via Edmonds's intersection theorem in the book's own proof, and the feasibility half of the goal's own maximum-flow variant.

Significance

The result itself. Theorem 9.13 is a genuine generalization of the max-flow min-cut theorem — one of the most-cited results in combinatorial optimization — to a submodularly constrained setting where the classical single-source-single-sink cut structure is replaced by an arbitrary vertex subset $X$ scored by a submodular function $\rho$ rather than merely counted. It specializes to the classical theorem when $\rho$ is the indicator of a fixed boundary value and the graph carries a single source/sink; the book's own derivation (dividing the target arc $a_0$ and reducing to Theorem 9.10's feasibility criterion) is exactly the kind of "one shared mechanism explains two theorems" result this whole book is organized around.

Formalizing it. A prior-art search (GET /theorems?q=max-flow min-cut) found two existing platform items for the classical theorem — LinearOptimization.max_flow_min_cut (Bertsimas & Tsitsiklis, single source/sink, plain capacities) and menger_directed_max_flow (Ford-Fulkerson, integer capacities) — both at a genuinely different, simpler generality (no lower capacity bounds, no submodular vertex-cut function, a fixed source/sink rather than an arbitrary marked arc). A further search (q=network flow) found a distinct mission formalizing Bertsimas & Tsitsiklis's uncapacitated network flow LP theory (basic feasible solutions, tree solutions, basis-matrix integrality) — a different technique (linear-algebraic, not cut-based) for a different problem (no capacities at all). Neither family is reused; this mission gives the first formal statement of submodular-flow feasibility and its max-flow min-cut theorem at the book's own generality.

Difficulty

The obvious shortcut — state only the value equality of Theorem 9.13 and drop the integrality clause — would misrepresent the theorem's own content: the equality of the extremal values follows from ordinary LP duality on the polyhedron $B(\kappa) \cap B(\rho)$ (arguably already within reach of chunk 04's Edmonds's intersection theorem machinery, as the book's own proof of the feasibility predecessor Theorem 9.10 uses exactly that), whereas the integer-flow existence half is the theorem's genuine combinatorial content, unique to the integer lattice. This chunk keeps both halves in every drafted theorem (Theorem 9.3, 9.10, and the goal) rather than only the polyhedral half.

A second, more structural difficulty governed this chunk's scope: BRIEF.md recommended Theorem 9.4 (the potential-optimality criterion) and its M-convex-cost specialization Theorem 9.14 as milestones, but both need a polyhedral convexity hypothesis on real-valued (or M-convex) functions over $\mathbb R^V$ that this series has never built — the identical scope boundary chunk 10 hit with Theorem 8.4. Rather than silently drop the polyhedral-convexity hypothesis (which would make the drafted statement unsound, since the theorem's hard direction genuinely needs it), this chunk selects only results — Proposition 9.2, Theorem 9.3, Theorem 9.10, Theorem 9.13 — that need no convexity apparatus of any kind, only the submodularity of $\kappa$/$\rho$ and elementary capacity-constraint feasibility.

Formalization scope

$V$ and $A$ are Fintypes with DecidableEq V (and DecidableEq A where a Finset.erase is needed); tail, head : A → V are plain functions, not a bundled graph structure. Every capacity- and cut-related quantity is WithTop ℝ-valued (ℝ ∪ {+∞}) throughout, with no EReal: a per-term check (documented in MODERATION_NOTES.md) confirms every subtraction this chunk needs is really an addition of two terms each individually in $\mathbb R \cup \{+\infty\}$, via a small new cast NegLowerToUpper : WithBot ℝ → WithTop ℝ. The base polyhedron $B(\rho)$ is stated by its defining inequalities rather than via a named polyhedral object (chunk 04's BasePolyhedron is ℤ^V-domain and does not fit chapter 9's real-vector- space setting). Not drafted: Theorem 9.4/9.14 (needs the real-domain polyhedral-convexity layer above), Theorem 9.6 (needs a real-domain polyhedral L-convexity notion for its dual-integrality half), Theorem 9.5/9.18/9.20/9.22 (negative-cycle criteria, an alternative non-potential certificate family, checked against platform prior art and found adjacent only), Propositions 9.23–9.25 (supporting technical facts), and Theorems 9.26–9.28 (the separate network- transformation technique of §9.6). A trivializing formalization would state Theorem 9.13's value equality with the integrality clause dropped, or would silently allow $\bar c$/$\underline c$ to range over all of EReal (permitting a nonsensical $\underline c(a) = +\infty$ upper- capacity-like lower bound); neither is done — both the integrality clause and the WithTop ℝ/WithBot ℝ type-level domain restriction are kept exactly as the book states them.

Selected references

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