Discrete Geometry

Motivation

How many times can $n$ points and $t$ lines in the plane meet? The question is the prototype of incidence geometry, and the answer controls a long list of problems in discrete and computational geometry: the number of lines rich in points, the number of distinct distances or unit distances among $n$ points, the complexity of arrangements, and sum–product estimates in additive combinatorics. Erdős asked for the order of magnitude when $t = n$ and conjectured that the answer is $n^{4/3}$; Erdős and Purdy asked for the matching bound on the number of lines containing at least $k$ of the points.

Szemerédi and Trotter settled both questions in Extremal Problems in Discrete Geometry (Combinatorica 3 (1983) 381–392, doi:10.1007/BF02579194). Their principal theorem bounds the number of point–line incidences by $c_1 n^{2/3} t^{2/3}$ over the whole range $\sqrt n \le t \le \binom n2$, and the same paper derives from it the Erdős–Purdy bound on $k$-rich lines, a version of Dirac's conjecture (proved independently by Beck, Combinatorica 3 (1983)), and a bound on the number of sequences of line densities.

Timeline.

• Erdős conjectures $O(n^{4/3})$ incidences for $n$ points and $n$ lines, and shows by a grid construction that this order would be sharp.
• 1983: Szemerédi and Trotter prove the bound $c_1 n^{2/3} t^{2/3}$ for $\sqrt n \le t \le \binom n2$, with $c_1 = 10^{60}$, by a minimal-counterexample argument and a covering lemma for squares from their earlier paper.
• 1990: Clarkson, Edelsbrunner, Guibas, Sharir and Welzl give a second proof by cuttings, with a far smaller constant (Discrete Comput. Geom. 5 (1990) 99–160).
• 1997: Székely derives the bound in a few lines from the crossing lemma (Combin. Probab. Comput. 6 (1997) 353–358).

Setting

Work in the Euclidean plane $\mathbb R^2$, written Plane in the Lean development. A line is an affine subspace $l \subseteq \mathbb R^2$ whose direction space has dimension one (IsLine l). Let $\mathcal P$ be a finite set of $n$ points and $\mathcal L$ a finite family of $t$ distinct lines. The number of incidences is

$$I(\mathcal P, \mathcal L) = \#\{(p, l) \in \mathcal P \times \mathcal L : p \in l\},$$

written incidences P L. The degree $d_i$ of a point $p_i$ is the number of lines of $\mathcal L$ through it (degree L p), and the density $y_j$ of a line $l_j$ is the number of points of $\mathcal P$ on it (density P l); so $I = \sum_i d_i = \sum_j y_j$.

For the covering lemma, coordinate axes are fixed and a square is a closed axis-parallel square $Q(a,b,s) = [a, a+s] \times [b, b+s]$ with side $s > 0$ (closedSquare (a, b, s)); its interior is the open square $(a, a+s) \times (b, b+s)$ (openSquare). A square contains the points of $\mathcal P$ in the closed square, and a family of squares covers the points lying in at least one of them.

Formalization targets

Goal: Theorem 1 (p. 381, restated and proved on p. 383)

There is an absolute constant $c_1$ such that for every finite point set $\mathcal P$ with $|\mathcal P| = n$ and every finite family $\mathcal L$ of $t$ distinct lines,

$$\sqrt n \le t \le \binom n2 \quad\Longrightarrow\quad I(\mathcal P, \mathcal L) \le c_1\, n^{2/3}\, t^{2/3}.$$

The goal leaves $c_1$ unspecified. The paper's proof gives $c_1 = 10^{60}$, and later proofs give much smaller values; any improvement of the constant still proves this statement.

Milestones, in the order the proof uses them

1. Section 3, display on p. 383. Two distinct lines meet in at most one point, so the number of good intersections is at most the number of pairs of lines:

$$\sum_{i} \binom{d_i}{2} \le \binom t2, \qquad \frac{I^2}{2n} - \frac I2 \le \frac{t^2}{2}.$$

2. Section 3, inequality (1), p. 384. $0.6\,x + (1-x)^{2/3} \le 1$ for $0 < x \le 1/2$.
3. Section 3, inequality (5), p. 385. $x^{2/3} + (1-x)/100 + 2^{-1/3}(1-x)^{2/3} \le 1$ for $0 < x \le 0.1$, and the reverse strict inequality holds somewhere in $(0.1, 0.2)$.
4. Section 3, display on p. 387. With $M = 10^{10}$, $2^{i/3}(1 - 2/M)^{4i/3} \ge 200/((0.1)^{1/3} 2^{2/3})$ for every integer $i \ge 30$.
5. Section 2, Lemma (covering lemma), p. 382. For integers $1 \le r_1 \le n$ and $r_2 \ge 256 r_1$, every set of $n$ points is covered, to at least $n/16$ of its points, by a family of squares with pairwise disjoint interiors, each containing between $r_1$ and $r_2$ of the points.

Significance

The result. The bound $n^{2/3} t^{2/3}$ is sharp up to the constant throughout the range $\sqrt n \le t \le \binom n2$, as integer-grid configurations show. Outside that range the trivial bounds $n + t^2$ and $t + n^2$ take over. Theorem 1 is the source of the $O(n^2/k^3)$ bound on $k$-rich lines (the paper's Theorem 2), of Beck's theorem (Theorem 3), and, through them, of the unit-distance bound $O(n^{4/3})$, of the Elekes sum–product estimate and of many algorithmic bounds on arrangements. It is the first nontrivial case of the polynomial-partitioning incidence theory developed since 2010.

Formalizing it. The theorem has been proved, and reproved in several ways, for four decades. To the best of the mission's knowledge Mathlib has no statement of it, of the crossing lemma, or of any point–line incidence bound in the Euclidean plane. This mission produces a checked statement of the theorem with lines as genuine one-dimensional affine subspaces and an absolute constant. It also produces checked statements of the auxiliary facts the 1983 proof uses. A complete proof may follow the original argument, the cutting argument or Székely's crossing-lemma argument; any of them closes the goal.

Difficulty

Counting pairs of lines through common points (milestone 1) gives only $I \lesssim n^{1/2} t + n$, and its dual gives $I \lesssim t^{1/2} n + t$. These Cauchy–Schwarz bounds use only the fact that two lines meet at most once, a property shared by lines in finite projective planes, where the incidence count genuinely reaches order $n^{3/2}$. Any proof of the $n^{2/3} t^{2/3}$ bound must therefore use a property of the real plane that the finite geometries lack: order, continuity, or the planarity of drawings. Szemerédi and Trotter use it through a covering lemma for axis-parallel squares, whose proof is only cited in the paper ([7]). The remaining difficulty is keeping the constants of a multi-stage minimal-counterexample argument under control.

Formalization scope

The plane is EuclideanSpace ℝ (Fin 2). A line is an AffineSubspace ℝ Plane whose direction has Module.finrank equal to $1$. Every statement requires IsLine of each member of $\mathcal L$, so neither the whole plane nor a single point counts as a line. The points form a Finset Plane and the lines a Finset (AffineSubspace ℝ Plane), which makes the $t$ lines distinct. Incidences, degrees and densities are Finset.filter cardinalities under classical decidability. Powers $n^{2/3}$, $t^{2/3}$ are Real.rpow of the counts cast to $\mathbb R$, and $\binom n2$ is Nat.choose.

In the goal, the constant $c_1$ is quantified before the points and the lines. The form "for every configuration there is a $c_1$" is trivially true (take $c_1 = I + 1$) and is not this theorem. Both ends of the range $\sqrt n \le t \le \binom n2$ are kept exactly: without the lower end, a single line through $n$ collinear points has $n$ incidences, more than $c_1 n^{2/3}$ for large $n$.

The goal follows the wording of p. 381 ("at most"). The restatement on p. 383 says "less than", which fails at $n = t = 0$ and is equivalent for $n \ge 1$ after doubling $c_1$. The covering lemma is stated with the added non-degeneracy hypotheses $1 \le r_1 \le n$. As printed it fails when $0 < n < r_1$ (no square can hold $r_1$ points), and when $r_1 = r_2 = 0$ with $n > 0$.

A full development needs a real-plane incidence toolkit: a crossing lemma or a cutting lemma, or the covering lemma with its quadtree proof. That toolkit is reusable for $k$-rich lines, Beck's theorem, unit distances and sum–product bounds, and contributions of such infrastructure as separate theorems are welcome. The three numerical milestones are self-contained real-analysis exercises.

Selected references

• E. Szemerédi, W. T. Trotter, Jr., Extremal problems in discrete geometry, Combinatorica 3 (1983) 381–392. https://doi.org/10.1007/BF02579194
• E. Szemerédi, W. T. Trotter, Jr., A combinatorial distinction between the Euclidean and projective planes, European J. Combin. 4 (1983) 385–394. https://doi.org/10.1016/S0195-6698(83)80036-5
• J. Beck, On the lattice property of the plane and some problems of Dirac, Motzkin and Erdős in combinatorial geometry, Combinatorica 3 (1983) 281–297. https://doi.org/10.1007/BF02579184
• K. L. Clarkson, H. Edelsbrunner, L. J. Guibas, M. Sharir, E. Welzl, Combinatorial complexity bounds for arrangements of curves and spheres, Discrete Comput. Geom. 5 (1990) 99–160. https://doi.org/10.1007/BF02187783
• L. A. Székely, Crossing numbers and hard Erdős problems in discrete geometry, Combin. Probab. Comput. 6 (1997) 353–358. https://doi.org/10.1017/S0963548397002976

Motivation

Every physical or engineering model built from linear relations mixes two kinds of numbers. Some coefficients are exact — the $\pm 1$ entries recording Kirchhoff's current and voltage laws in an electrical network, or the incidence structure of a mechanical linkage — because they come from a topological or combinatorial fact, not a measurement. Others are physical parameters: resistances, masses, spring constants, reaction rates. These are known only approximately, and different parameters are, for modeling purposes, independent of one another. Classical linear algebra treats every entry of a coefficient matrix alike, so it cannot express this distinction, and a numerical computation on a matrix with noisy parameter entries can accidentally hit a non-generic coincidence — a determinant that would vanish only for a measure-zero set of parameter values, but that plain Gaussian elimination has no way to certify is not actually structurally forced to vanish. Murota and collaborators (see the bibliographical notes to chapter 12; the underlying theory is developed at length in Murota's Matrices and Matroids for Systems Analysis, 2000) formalized this distinction through mixed matrices, and showed that their key structural questions — is the matrix nonsingular, and what is its rank — reduce to a combinatorial optimization problem solvable by the discrete convex analysis this book develops. This mission formalizes that reduction and its capstone consequence, a generalization of the classical König–Egerváry theorem.

Setting

Fix two fields $K \subseteq F$: typically $K = \mathbb{Q}$ and $F$ a field large enough to hold every number in the problem. A family $t_1, \dots, t_m \in F$ is algebraically independent over $K$ if no nonzero polynomial with coefficients in $K$ vanishes at $(t_1, \dots, t_m)$ — informally, the $t_i$ behave as free, unconstrained parameters relative to $K$. Fix finite row and column index sets $R$ and $C$. A matrix $A = (A_{ij})_{i \in R, j \in C}$ over $F$ is a mixed matrix with respect to $(K, F)$ if it decomposes as

$$A = Q + T$$

where $Q = (Q_{ij})$ has every entry in $K$, and $T = (T_{ij})$ has entries in $F$ whose nonzero values, taken together as one family, are algebraically independent over $K$. $Q$ models the exact, structural part of the system; $T$ models the independent physical parameters. For $I \subseteq R$ and $J \subseteq C$, write $A[I,J]$ for the submatrix with rows $I$ and columns $J$. The rank of $A$ is its rank over $F$ — equivalently, the size of the largest nonvanishing-determinant square submatrix. Write $\rho(I,J) = \operatorname{rank} Q[I,J]$, $\tau(I,J) = \operatorname{rank} T[I,J]$, and $\gamma(I,J)$ for the number of rows of $I$ that contain a nonzero entry of $T$ in some column of $J$. A mixed polynomial matrix $A(s) = Q(s) + T(s)$ is the same decomposition applied entrywise to matrices whose entries are polynomials in an indeterminate $s$ (used to model the Laplace- or $z$-transform variable of a linear time-invariant system): $Q(s)$ has every coefficient of every entry in $K$, and the coefficients of $T(s)$'s entries, taken together, are algebraically independent over $K$.

Formalization targets

$$\textbf{Theorem 12.9 (goal).}\quad \text{For a mixed matrix } A=Q+T,\ \exists\, I \subseteq R,\ J \subseteq C:\quad |I|+|J|-\operatorname{rank} Q[I,J] = |R|+|C|-\operatorname{rank} A \ \ \text{and}\ \ \operatorname{rank} T[I,J] = 0.$$

This is the König–Egerváry theorem for mixed matrices: a combinatorial certificate of $A$'s rank deficiency, generalizing the classical theorem relating the maximum matching size of a bipartite graph (equivalently, the rank of a 0-1 matrix) to a minimum vertex cover. It is reached via three supporting results, each a genuine theorem in its own right: Proposition 12.6 (nonsingularity of $A$ reduces to nonsingularity of a $Q$-part and a $T$-part on complementary index splits), Theorem 12.7 (the resulting rank max-formula), and Theorem 12.8 (the three dual min-formulas Theorem 12.9 is extracted from). Theorem 12.13 extends the max-formula to the degree of the determinant of a mixed polynomial matrix.

Significance

The result itself. Theorem 12.9 gives a certificate, not just a number: a pair $(I,J)$ that simultaneously proves the exact numeric rank contribution of $Q$ and exhibits a submatrix of $T$ that vanishes identically. Because $\rho$ (via Gaussian elimination on $Q$) and $\gamma$, $\tau$ (via maximum bipartite matching on $T$'s nonzero pattern) are each individually cheap to evaluate, and the min-max structure of Theorem 12.8 is exactly the kind of problem Edmonds's matroid intersection theorem (a special case of this book's Theorem 4.18) and this book's discrete convexity machinery solve efficiently, the whole rank computation for a mixed matrix — and hence the generic solvability test for a physical system modeled by one — is polynomial-time, despite Theorem 12.7's formula naively ranging over exponentially many index-set pairs.

Formalizing it. All five results in this mission are proved in the source text (this is textbook, not open, mathematics). What formalization adds is a machine-checked confirmation that the genericity hypothesis — "the nonzero entries of $T$ are algebraically independent" — is precisely what the printed proofs use, expressed through Mathlib's own AlgebraicIndependent rather than an informal paraphrase such as "generic" or "random" values, which would be either meaningless or a different (probabilistic) condition.

Difficulty

The naive approach to testing whether $A = Q+T$ is nonsingular is to expand $\det A$ directly and check whether the resulting expression, as a polynomial in $T$'s free parameters, is the zero polynomial. This is exactly what genericity is supposed to let you avoid: Proposition 12.6's proof observes that the Laplace-type expansion $\det A = \sum_{|I|=|J|} \pm \det Q[I,J] \cdot \det T[R\setminus I, C\setminus J]$ has no cancellation between distinct terms, precisely because the nonzero entries of $T$ are algebraically independent — a coincidental cancellation would be a nontrivial polynomial relation among free parameters, which cannot happen. This turns a determinant computation with symbolic entries into a purely combinatorial search over row/column splits, each of whose two pieces is checked in the "easy" arithmetic appropriate to it (numeric determinant for $Q$, a nonzero-pattern-only matching argument for $T$). Missing this point — e.g. by treating $T$'s entries as merely "distinct" or "typically nonzero" rather than algebraically independent — reintroduces exactly the cancellation risk the theorem is built to rule out.

Formalization scope

Row and column index sets $R$, $C$ are general finite types (Fintype, with DecidableEq where needed for Finset operations), not fixed to $\mathrm{Fin}\ n$. No constant appears in any statement in this mission — every quantity (ranks, cardinalities, $\gamma$) is instance-dependent, so rule 7's explicit-constant obligation does not apply here. "Nonsingular" for a (possibly rectangular, cross-type-indexed) submatrix $M[I,J]$ is formalized as I.card = J.card together with rank M[I,J] = I.card (full rank) rather than via Matrix.det, because Mathlib's determinant requires both index sets to be the same Lean type, which I : Finset R and J : Finset C are not in general even when equinumerous; this coincides with ordinary nonsingularity whenever the ambient matrix is genuinely square. The degree of the determinant of a submatrix in Theorem 12.13 is computed the same way, via an arbitrary reindexing bijection between the row- and column-index subtypes — a choice that changes the determinant by at most a sign and hence never changes its degree. A formalization that replaced the genericity hypothesis on $T$ with mere distinctness of its nonzero entries would admit spurious cancellations in the determinant expansion and would not prove Proposition 12.6 or any of its consequences; AlgebraicIndependent K is the precise, non-trivializing condition the book's proofs use. This chapter is self-contained: no definitions from any other mission in this series are imported. Reusable beyond this mission: MatrixSubRank, IsNonsingularSub, and SubDegDet apply to any pair of matrices over any field, not only to mixed-matrix decompositions.

Selected references

• Murota, K. Discrete Convex Analysis. SIAM, 2003. DOI: 10.1137/1.9780898718508. (Chapter 12.)
• Murota, K. Matrices and Matroids for Systems Analysis. Springer, 2000.
• Murota, K. "Systems Analysis by Graphs and Matroids: Structural Solvability and Controllability." Springer, 1987.
• König, D. "Gráfok és mátrixok" (Graphs and matrices). Matematikai és Fizikai Lapok 38, 1931, 116–119.
• Egerváry, J. "Matrixok kombinatorius tulajdonságairól" (On combinatorial properties of matrices). Matematikai és Fizikai Lapok 38, 1931, 16–28.

Motivation

This mission continues chapter 10's algorithmic account across its remaining two sections: finishing the Iwata-Fleischer-Fujishige fixing algorithm for submodular minimization (§10.2.3's tail), the steepest descent algorithm for L-convex function minimization (§10.3), and — the capstone of chapter 10's account of the M-convex submodular flow problem (§10.4) — conjugate scaling, the operation that finally makes the primal-dual algorithm run in polynomial time. As in mission 34-ch10b-algorithms, most of this block's numbered results are asymptotic complexity bounds; this mission places the results that are ordinary mathematical propositions.

Setting

The IFF fixing algorithm (mission 34-ch10b-algorithms) builds an acyclic graph D=(U,F) and partition Z,H,Γ certifying the maximal minimizer of a submodular ρ once η≤0 (Eq. (10.26)); this mission places the case-independent inequality its own legitimacy rests on, and restates its correctness conclusion. The steepest descent algorithm for an L-convex function g repeatedly minimizes the submodular set function ρ_p(X)=g(p+χ_X)-g(p) and moves to p+χ_X for its minimal minimizer X (the tie-breaking rule (10.33)); this mission places the resulting monotonicity fact and a domain-size bound for the L$^\natural$-convex adaptation. Conjugate scaling replaces a dual-integral M-convex function's conjugate g with g_α(p)=g(αp)/α, defining f⟨α⟩ via the resulting sup-formula (Eq. (10.77)) — a scaling operation compatible with M-convexity where the naive ⌈f(·)/α⌉ is not.

Formalization targets

Goal: Conjugate scaling preserves M-convexity (Proposition 10.41)

For a dual-integral polyhedral M-convex function f (represented as the mixed real-primal/ integer-dual conjugate of an L$^\natural$-convex g), the conjugate scaling f⟨α⟩ is again dual-integral M-convex, witnessed by g_α itself being L$^\natural$-convex, provided f⟨α⟩>-∞. Chosen as goal: this is the fact the whole conjugate scaling algorithm — chapter 10's final and most refined algorithm for the M-convex submodular flow problem — depends on, and the book's own text singles it out as the "compatible scaling operation" that makes M-convex cost scaling work where a naive approach provably does not.

Supporting structural targets

Proposition 10.26 (the case-independent inequality underlying the IFF fixing algorithm's own legitimacy) and Proposition 10.28 (that algorithm's correctness conclusion) close out mission 34-ch10b-algorithms's coverage of §10.2.3. Proposition 10.30 gives the steepest descent algorithm's monotonicity property under its tie-breaking rule; Proposition 10.32 (found by direct reading) bounds the L$^\natural$-convex adaptation's domain-size parameter in terms of the original function's.

Significance

Conjugate scaling is chapter 10's demonstration that M-convexity, while a combinatorial rather than a numeric-magnitude notion, still admits a genuine scaling technique compatible with its own structure — completing the book's account of the M-convex submodular flow problem with an algorithm whose polynomial running time depends on exactly this compatibility. Propositions 10.26/10.28 complete the correctness/legitimacy argument for the strongly polynomial submodular- minimization algorithm mission 34-ch10b-algorithms began placing, and Propositions 10.30/10.32 are the analogous structural facts for L-convex function minimization, chapter 10's third major algorithmic thread.

None of these results are open — they are Murota's own account of submodular-function- minimization (§10.2 continued), L-convex minimization (§10.3), and conjugate scaling (§10.4.5). What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Proposition 10.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

As in mission 34-ch10b-algorithms, several numbered results in this block are excluded as hard for being pure algorithmic-complexity bounds (Propositions 10.25, 10.27, 10.31); see HARD.md. A further three (Propositions 10.37-10.39, on the primal-dual algorithm's maximum submodular flow subproblem) are excluded for a distinct reason: the source text's own OCR extraction demonstrably cannot distinguish the two visually different capacity-bound symbols (c* overlined vs. underlined) central to their shared defining formula, confirmed directly against the raw extracted bytes, making faithful reconstruction of that formula impossible from the available text; see HARD.md.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq. All apparatus needed for Propositions 10.26/10.28 (Submodular, GammaSet, RhoTilde, ReachSet, Eta, IsMaximalMinimizer) is redeclared fresh from mission 34-ch10b-algorithms, genericized over an arbitrary ground type where the original was V-specific, since this draft cannot import that sibling. Proposition 10.26 is placed as the case-independent core inequality its own proof establishes, rather than by replicating the three-case verification against Proposition 10.24's own internal proof objects (Cases (i)-(iii)); see HARD.md. Proposition 10.30 omits its own trailing iteration-count corollary (a pure complexity bound); see HARD.md. Six numbered results (Propositions 10.25, 10.27, 10.31, 10.37, 10.38, 10.39) are hard. Contributions completing any of the five sorrys are welcome; the goal carries the most independent proof content (via the conjugacy theorem and Theorem 7.10(2), both established elsewhere in this series).

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• S. Iwata, "A faster scaling algorithm for minimizing submodular functions," SIAM Journal on Computing, 32 (2003), pp. 833-840 [99] (conjugate scaling's origin).
• A. Frank, "A weighted matroid intersection algorithm," Journal of Algorithms, 2 (1981), pp. 328-336 [55] (the primal-dual framework this mission's Proposition 10.28 continues, via mission 34-ch10b-algorithms's own Proposition 10.24).

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

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

Chunk 10 formalized the discrete conjugacy theorem — the Legendre-Fenchel transform's bijection between the classes of M-convex and L-convex functions — and, along the way, a function-level generalization of Edmonds's intersection theorem. Section 8.4 turns that machinery toward a different question: not "how are two convexity classes related," but "when does a discrete optimization problem have a dual that meets it with equality." The classical route to such strong-duality results in continuous convex programming — Lagrangian relaxation, an embedding of the problem in a family of perturbed problems, and a saddle-point characterization of when primal and dual values coincide — has a discrete analogue that needs no continuity, no differentiability, and no convexity in the classical sense at all: only the elementary fact that the Legendre-Fenchel transform, once discretized, is still an involution on the right class of functions. This mission formalizes that discrete Lagrangian duality framework and its central saddle-point theorem, in full generality — before the book specializes it, in the section that follows, to the specific M-convex perturbation that gives the chapter's headline strong-duality result for M-convex programs.

Setting

Let $V$ and $U$ be finite ground sets. A perturbation of an optimization problem $\min\{f(x) : x \in \mathbb Z^V\}$ is a function $F : \mathbb Z^V \times \mathbb Z^U \to \mathbb Z \cup \{+\infty\}$ such that $F(x,0) = f(x)$ for all $x$ (Eq. (8.54)) and, for each fixed $x$, $F(x,\cdot)$ is self-biconjugate: $F(x,\cdot)^{\bullet\bullet} = F(x,\cdot)$ under the discrete Legendre-Fenchel transform of chunk 10 (Eq. (8.55)). The Lagrangian function is $K(x,y) = \inf\{F(x,u) + \langle u,y\rangle : u \in \mathbb Z^U\}$ (Eq. (8.58)), valued in $\mathbb Z \cup \{\pm\infty\}$ (formalized in EReal, since both the infimum and the supremum below can be genuinely unbounded). The dual objective is $g(y) = \inf\{K(x,y) : x \in \mathbb Z^V\}$ (Eq. (8.60)). Writing $\inf(P) = \inf_x f(x)$, $\sup(D) = \sup_y g(y)$, $\operatorname{opt}(P) = \{x : f(x) = \inf(P)\}$, $\operatorname{opt}(D) = \{y : g(y) = \sup(D)\}$, the primal problem $P$ is to minimize $f$ over $\mathbb Z^V$ and the dual problem $D$ is to maximize $g$ over $\mathbb Z^U$.

Formalization targets

Goal: Theorem 8.54 (the saddle-point theorem)

Assuming $F$ is self-biconjugate (Eq. (8.55)): both $\inf(P)$ and $\sup(D)$ are finite and $\min(P) = \max(D)$ if and only if there exist $\bar x \in \mathbb Z^V$, $\bar y \in \mathbb Z^U$ with $K(\bar x,\bar y)$ finite and $K(x,\bar y) \le K(\bar x,\bar y) \le K(\bar x,y)$ for all $x,y$ — a saddle point of the Lagrangian kernel. When this holds, $\bar x \in \operatorname{opt}(P)$ and $\bar y \in \operatorname{opt}(D)$.

Milestones: Theorem 8.52, Proposition 8.51(1)-(2)

Theorem 8.52 (weak duality): $\inf(P) \ge \sup(D)$ always, with no biconjugacy hypothesis on $F$ at all — the baseline the saddle-point theorem sharpens to equality. Proposition 8.51(1)-(2): under self-biconjugacy, the perturbation $F$ (and hence the primal objective $f$) is itself recoverable from the Lagrangian kernel $K$ by a supremum, $F(x,u) = \sup_y\{K(x,y) - \langle u,y\rangle\}$ and $f(x) = \sup_y K(x,y)$ — the algebraic identity the saddle-point theorem's proof turns on directly.

Significance

The result itself. The saddle-point theorem is the general-purpose engine behind every strong-duality result the book proves for specific classes of discrete optimization problems: the book's own next section specializes it (via a particular choice of $F$ built from an M-convex regularizer $r$) to obtain strong duality for M-convex programs, but the theorem itself needs no M-convexity, no submodularity, and no exchange axiom — only the elementary self-biconjugacy of a perturbation under the discrete Legendre-Fenchel transform. It is, in that sense, the most general and most reusable strong-duality statement in the book: any future mission proving strong duality for a specific class of discrete programs (M-convex, M2-convex, network flow, or otherwise) by exhibiting a self-biconjugate perturbation can cite this theorem directly rather than reproving the saddle-point argument from scratch.

Formalizing it. No matching item exists on the platform for a discrete Lagrangian saddle- point theorem, discrete weak duality, or this perturbation-based duality framework. (A prior-art search turned up an unrelated continuous Lagrangian saddle-point theorem for convex cones, Luenberger's Chapter 8 §8.4, formalized as VectorSpaceOpt.lagrangian_saddle_sufficient_pointed — a genuinely different setting: no discreteness, no biconjugacy hypothesis, and a one-directional sufficiency statement rather than this mission's iff. Not reused.) This mission gives the first formal statement of discrete Lagrangian duality, and directly reuses chunk 10's ConvexConjugate apparatus (self-biconjugacy is stated using chunk 10's own conjugate-of-conjugate composition), demonstrating exactly the kind of shared-substrate payoff the discrete conjugacy theorem was built to provide.

Difficulty

The saddle-point theorem's "only if" direction is not a routine unwinding of definitions: given $\min(P) = \max(D)$ at finite common value, one must construct the saddle point $(\bar x,\bar y)$ — the book's proof takes $\bar x \in \operatorname{opt}(P)$, $\bar y \in \operatorname{opt}(D)$ (which exist because the infimum/supremum are attained at a finite optimum) and verifies the sandwiching inequality using Proposition 8.51(2)'s identity $f(x) = \sup_y K(x,y)$ together with weak duality, rather than by any direct algebraic manipulation of $K$ alone. Skipping straight to a "trivial" biconditional that never invokes Proposition 8.51 would misrepresent the actual proof structure the book relies on for exactly this direction.

Formalization scope

$V, U$ are Fintype ground types; LagrangianKernel, DualObjective, InfP, SupD are EReal-valued to keep both the defining infima/suprema total (a complete lattice) without an artificial finiteness side-condition; OptP, OptD compare PrimalValue/DualObjective against InfP/SupD after casting through chunk 10's ToEReal, mirroring that chunk's own round-trip convention. "Finite" throughout is formalized as ≠ ⊤ ∧ ≠ ⊥ in EReal. The perturbation $F$ itself is left fully abstract (an arbitrary function satisfying the self-biconjugacy hypothesis where needed) — this mission does not draft the specific M-convex perturbation $F_r$ (Eq. (8.61)) that the book's next subsection (§8.4.3) uses to specialize this framework to M-convex programs, nor Theorem 8.59 (the resulting M-convex strong-duality theorem) itself, which needs that specific perturbation plus its own regularity conditions (REG)/(OBJ) and a chain of M-convex-specific propositions (8.55–8.58) beyond what the general framework built here provides. A trivializing formalization would state the saddle-point theorem's sandwiching inequality with a weaker order (e.g., only one of the two directions) or would omit the "$\bar x \in \operatorname{opt}(P), \bar y \in \operatorname{opt}(D)$" consequence clause; neither is done — both inequalities and the full consequence clause are included exactly as the book states them.

Selected references

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

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

L-convex functions were defined purely combinatorially, on the integer lattice. Chapter 6's M-convex theory showed that combinatorial definition always extends to a genuine convex function on real space (missions 23-ch06c-mconvexfunctions/24-ch06d-mconvexfunctions); this mission carries out the identical program for the L side. It first shows L$^\natural$-convexity is exactly integral convexity plus ordinary submodularity — a clean synonym that also explains why submodular set functions are a natural special case — then builds the entire polyhedral (real-variable) theory of L-convex functions: the axioms (SBF[R])/(TRF[R]), two practical local criteria for verifying submodularity without checking every pair of points, the fact that the classical Lovász extension of a submodular set function is itself a polyhedral L-convex function, the six-operation closure toolkit, and — this mission's goal — the L-optimality criterion in its full polyhedral generality, characterizing global optimality by finitely many directional derivatives.

Setting

Fix a finite ground set $V$. A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain is polyhedral L-convex, $g \in L[\mathbb R \to \mathbb R]$, if it satisfies (SBF[R]): $g(p)+g(q) \ge g(p\vee q)+g(p\wedge q)$, and (TRF[R]): $\exists r \in \mathbb R$, $g(p+\alpha\mathbf 1) = g(p)+\alpha r$ for all $p \in \mathbb R^V$, $\alpha \in \mathbb R$; it is polyhedral L$^\natural$-convex if its lift to one extra real coordinate is polyhedral L-convex. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is integrally convex if its convex closure agrees, at every real point, with the closure taken using only that point's integral neighborhood. The Lovász extension $\hat\rho$ of a submodular set function $\rho$ is the piecewise-linear interpolation built from the sorted distinct components of $p \in \mathbb R^V$. The directional derivative $g'(p;d)$ is $\inf_{t>0}(g(p+td)-g(p))/t$.

Formalization targets

Goal: the polyhedral L-optimality criterion (Theorem 7.33)

For a polyhedral L-convex function $g$ and $p \in \operatorname{dom}_{\mathbb R} g$: $g(p) \le g(q)$ for all $q$ if and only if $g'(p;\chi_Y) \ge 0$ for every $Y \subseteq V$ and $g'(p;\mathbf 1)=0$; for polyhedral L$^\natural$-convex $g$, the criterion simplifies to $g'(p;\pm\chi_Y) \ge 0$ for every $Y$. This is the direct L-side mirror of mission 24-ch06d-mconvexfunctions's M-optimality criterion (Theorem 6.52) and the polyhedral generalization of mission 08-lconvex-functions-i's integer-domain L-optimality criterion (Theorem 7.14): checking global optimality against exponentially many points reduces to $|V|+1$ (or $2|V|$) directional-derivative inequalities.

Supporting structural targets

Twelve further results build the polyhedral theory from the ground up. Theorems 7.20-7.21 identify L$^\natural$-convexity with the conjunction of ordinary submodularity and integral convexity — a genuinely different, function-analytic characterization from the exchange-axiom- style definitions used so far. Propositions 7.23-7.24 give two practical sufficient conditions for verifying (SBF[R]) locally, at a single scale, rather than globally. Proposition 7.25 shows the Lovász extension of any submodular set function is automatically polyhedral L-convex — not in this chunk's own extraction table (its label is preceded by an unlabeled restatement of the same fact, which evidently confused the extractor), found and placed by direct reading. Theorem 7.26 shows an L-convex function's convex extension, when polyhedral, inherits polyhedral L-convexity, continuing mission 26-ch07b-lconvexfunctions's Theorem 7.19. Theorems 7.28-7.32 restate the discrete theory's core equivalences (translation submodularity, the L/L$^\natural$ correspondence, the six basic operations, restrictions) in the polyhedral setting, and Proposition 7.34 shows minimizer sets of linearly-perturbed polyhedral L-convex functions are themselves L-convex polyhedra — flagged by the book itself as a partial result whose full converse characterization (Theorem 7.45) lies beyond this chunk's range.

Significance

Theorems 7.20-7.21's synonym is structurally important: it means every algorithm and theorem already known for submodular-function minimization over $\{0,1\}^V$-type domains applies, after a midpoint-convexity check, to the vastly larger class of integer-lattice L$^\natural$-convex functions, with no new proof technique required. Proposition 7.25 is the bridge that lets the combinatorial Lovász extension — the workhorse of submodular optimization for forty years — be recognized as a special case of the polyhedral L-convex function theory this mission builds, explaining why algorithms for one transfer so readily to the other. The goal, Theorem 7.33, is the precise tool chapter 10's continuous-relaxation algorithms for L-convex-function minimization actually verify against: a scaling algorithm's claimed optimum is confirmed correct exactly by checking the criterion's finitely many directional-derivative inequalities.

None of these results are open — they are Murota's account of how the integer-lattice theory of L-convexity survives, result by result, the passage to polyhedral convex functions on $\mathbb R^V$, mirroring chapter 6's identical program for M-convexity. What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Proposition 7.25) the platform's own automated extractor missed, extending the shared Lean vocabulary (SBFR, TRFR, LovaszExtension, DirDeriv) this series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to verify $g(p) \le g(q)$ directly against every $q \in \mathbb R^V$; the book's actual proof instead reduces this to the finite family of directional derivatives via Theorem 7.20's integral-convexity fact (an L$^\natural$-convex function's local behavior determines its global behavior) applied to the polyhedral setting through Theorem 3.21's general optimality criterion for integrally convex functions — a two-layer reduction (polyhedral $\to$ integral-convexity $\to$ finite local check) with no direct one-step argument. The genuine combinatorial content in this block is in Proposition 7.25's proof: showing the Lovász extension is submodular requires the finite-valued case (a direct calculation split on whether the two perturbed coordinates land in the same or different threshold sets) and then a limiting argument over a sequence of finite-valued truncations $\rho_k \to \rho$ for the general, possibly-infinite case — a genuine two-step argument, not a single inequality chase.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; polyhedral L-(natural-)convex functions are (V→ℝ)→WithTop ℝ. All thirteen numbered results found in this chunk's page range are placed, with one documented scope reduction: Proposition 7.24 states only part (1) (the unconditional-on-magnitude sufficient condition), not part (2)'s sharper, sorted-index-restricted version, which needs the same SortedValues apparatus a second time for no other result's benefit — see HARD.md. "$g_U > -\infty$" and its variants are replaced by the equivalent (DomR ...).Nonempty hypothesis throughout, matching mission 24-ch06d-mconvexfunctions's identical substitution. "Domain is closed"/"domain is an interval" (Propositions 7.23-7.24) are stated via Mathlib's IsClosed and Set.OrdConnected respectively, the latter being the precise order-theoretic notion of "interval" in a pointwise-ordered space. This mission's base vocabulary is redeclared from missions 08-lconvex-functions-i, 20-ch04b-mconvexsets (for the Lovász extension machinery), 21-ch05b-lconvexsets, 23-ch06c-mconvexfunctions/ 24-ch06d-mconvexfunctions, and 26-ch07b-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 7.25 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 [152] (the polyhedral L-convex function theory this mission's real-variable results are drawn from).

Motivation

Chapter 5 characterized L-convex sets — sublattice-closed, translation-periodic subsets of $\mathbb Z^V$ — and showed they interact cleanly with integral convexity. Chapter 7 asks the functional analogue: which functions on the integer lattice deserve to be called convex in the "L" sense, and how do they relate back to L-convex sets? This mission (continuing mission 08-lconvex-functions-i, which built the axioms (SBF[Z])/(TRF[Z])/(SBF$^\natural$[Z]) and proved the L-optimality and L-proximity theorems) answers the second question at its sharpest: an L-convex function is exactly a function whose every weighted-minimizer set is an L-convex polyhedron — the discrete analogue of the fact that a convex function is determined by the convex geometry of its sublevel sets. Along the way it settles the chapter's basic toolkit: operations that preserve L-convexity, the local nature of submodularity, the correspondence with ordinary submodular set functions, and the first two structural facts about the convex extension every L-convex function admits.

Setting

Fix a finite ground set $V$. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain is L-convex, $g \in L[\mathbb Z \to \mathbb R]$, if it satisfies submodularity (SBF[Z]): $g(p)+g(q) \ge g(p\vee q) + g(p\wedge q)$, and translation invariance (TRF[Z]): $\exists r \in \mathbb R$, $g(p+\mathbf 1) = g(p) + r$ for all $p$. It is L$^\natural$-convex if its lift to one extra coordinate (Eq. (7.2)) is L-convex. A set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ is submodular if $\rho(X)+\rho(Y) \ge \rho(X\cup Y) + \rho(X\cap Y)$; it corresponds to an L$^\natural$-convex function supported on $\{0,1\}^V$ via $g(\chi_X) = \rho(X)$ (Eq. (7.5)). The convex closure $\bar g$ of $g$ is its extension to $\mathbb R^V$ by finite convex combinations.

Formalization targets

Goal: L-convexity via minimizer polyhedra (Theorem 7.17)

For $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with bounded nonempty effective domain: $g$ is L-convex if and only if $\arg\min g[-x]$ is an L-convex set for every $x \in \mathbb R^V$; the L$^\natural$ analogue holds with L$^\natural$-convex sets. This is the direct mirror of mission 23-ch06c-mconvexfunctions's own goal (Theorem 6.43, characterizing M-convex functions via M-convex weighted-minimizer polyhedra) — the book's text calls it exactly "how the concept of L-convex functions can be defined from that of L-convex sets."

Supporting structural targets

Eleven further results build the chapter's basic vocabulary. Theorem 7.2 strengthens translation submodularity to allow negative shifts; Theorem 7.3 places L-convexity inside L$^\natural$- convexity; Proposition 7.4 identifies submodular set functions with a subclass of L$^\natural$-convex functions via the indicator embedding, and Theorem 7.15 derives the classical submodular-minimizer local-optimality criterion as its corollary; Proposition 7.5 shows submodularity is a local property, needing only unit-distance pairs; Proposition 7.8 transfers L-(natural-)convexity from functions to their effective domains; Proposition 7.9 and Theorem 7.10–7.11 give the chapter's basic examples (univariate and pairwise-difference functions) and its six-operation closure toolkit (scaling, affine reparametrization, linear perturbation, projection, infimal convolution with a separable function, and sums), both for L-convex and L$^\natural$- convex functions, the latter also admitting interval and coordinate restrictions; Proposition 7.16 shows minimizer sets of L-convex functions are themselves L-convex, the special case ($x=0$) the goal generalizes to every linear perturbation; Theorem 7.19 begins the convex-extension program this chapter's next chunk completes, establishing that the convex closure agrees with $g$ on $\mathbb Z^V$ and inherits its translation constant.

Significance

The goal is significant for the same structural reason as its M-side counterpart: it says L-convexity is not merely a combinatorial condition on lattice differences but is equivalent to a purely polyhedral-geometric one, closing the loop between chapters 5 and 7 the way Theorem 6.43 closes the loop between chapters 4 and 6. Theorem 7.15's corollary status is itself instructive: the well-known fact that a submodular set function's global minimizer needs only local verification against comparable sets — the theoretical basis of every submodular-minimization algorithm in chapter 10 — falls out of the L-optimality criterion (mission 08-lconvex-functions-i's Theorem 7.14) applied to the indicator embedding, rather than needing an independent proof. Theorem 7.10–7.11's six operations are the toolkit every later construction in this chapter and chapter 9's network transformations builds new L-convex functions from old.

None of these results are open — they are Murota's account of the basic function-level theory of L-convexity, mirroring chapter 6's M-convex function theory chunk-by-chunk. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (SBF, TRF, LNaturalConvex, LConvexSet) that missions 08-lconvex-functions-i and 21-ch05b-lconvexsets began; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to verify L-convexity's submodularity inequality directly against the definition of an L-convex set applied to each minimizer family; the book's actual proof instead routes through Theorem 7.10 (3)'s closure of L-convexity under linear perturbation and Proposition 7.16's minimizer-is-L-convex-set fact for the forward direction, and defers the converse entirely to a later note (Note 7.47, outside this chunk and mission 08's combined range) proved via the integral-convexity machinery of section 7.7 onward. The genuine combinatorial difficulty in this block is upstream, in Theorem 7.10 (5)'s infimal-convolution operation: proving L-convexity of the perturbed function requires a four-term submodularity inequality assembled from the separable function's own convexity and $g$'s submodularity applied at the optimal $q_1,q_2$ simultaneously — a genuine two-hypothesis combination with no single-inequality shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; L-(natural-)convex functions are (V→ℤ)→WithTop ℝ. All twelve numbered results found in this chunk's page range are placed, with one documented scope reduction: Theorem 7.19 states only parts (3)-(4) (that the convex closure agrees with $g$ on $\mathbb Z^V$ and inherits its translation constant), not the explicit Lovász-extension-formula construction of parts (1)-(2) and (5), which needs a sorted-distinct- component apparatus no other result in this chunk requires — see HARD.md. "$g_U > -\infty$" and its variants are replaced by the equivalent (DomZ ...).Nonempty hypothesis throughout, matching mission 24-ch06d-mconvexfunctions's identical substitution (WithTop ℝ has no $-\infty$ element). This mission's base vocabulary (SBF, TRF, LNaturalConvex, etc.) is redeclared verbatim from mission 08-lconvex-functions-i rather than imported, since sibling drafts in this series cannot yet reference one another; LConvexSet is likewise redeclared from mission 21-ch05b-lconvexsets. Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 7.10 carry 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 original account of L-convex functions this chapter's basic theory is drawn from).

Motivation

Milgrom and Shannon's theory of quasi-supermodularity, developed for monotone comparative statics in economics, showed that many of the consequences of lattice submodularity survive under a much weaker, purely ordinal relaxation of the defining inequality. Chapter 7's final section imports this idea into discrete convex analysis: does L-convexity's optimality and proximity theory survive when the additive submodularity inequality is relaxed to an ordinal condition on the sign pattern of the two relevant differences, rather than their sum? This mission formalizes the chapter's answer for the strongest of the relevant relaxations, (SSQSB) (semistrict quasi submodularity): yes, and the class is large enough to include every strictly increasing rescaling of an L-convex function — exactly mirroring chunk 07's result for the M-convex side, and completing the "quasi" theory on both halves of the exchange-axiom framework before chapter 8 unifies them under conjugacy.

Setting

Let $V$ be a finite ground set and $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$. Building on chunk 08's submodularity axiom (SBF[Z]), this section introduces four ordinal relaxations. $g$ is quasi submodular, satisfying (QSB), if for every $p, q \in \mathbb Z^V$, $g(p \wedge q) \le g(p)$ or $g(p \vee q) \le g(q)$. $g$ is semistrictly quasi submodular, satisfying (SSQSB), if additionally $g(p \vee q) \ge g(q) \implies g(p \wedge q) \le g(p)$ and symmetrically. The weak variants (QSBw) and (SSQSBw) restrict attention to points of the effective domain and compare $\max(g(p), g(q))$ against $\min(g(p \wedge q), g(p \vee q))$ directly, with (SSQSBw) additionally allowing the four-way tie $g(p) = g(q) = g(p\wedge q) = g(p \vee q)$. The linear perturbation of $g$ by $x : V \to \mathbb R$ is $g[x](p) = g(p) + \langle p, x \rangle$.

Formalization targets

Goal: Theorem 7.54 (the quasi L-proximity theorem)

Let $g$ satisfy (SSQSB) and $g(p) = g(p + \mathbf 1)$ for all $p$, $n = |V|$, $\alpha$ a positive integer. If $p_\alpha \in \operatorname{dom} g$ satisfies $g(p_\alpha) \le g(p_\alpha + \alpha \chi_Y)$ for all $Y \subseteq V$, then $\arg\min g \ne \emptyset$ and there is $p^* \in \arg\min g$ with the componentwise bound $p_\alpha \le p^* \le p_\alpha + (n-1)(\alpha-1) \mathbf 1$ — verbatim the same conclusion, and the same exact bound, as chunk 08's Theorem 7.18(1), now established for the strictly larger class satisfying (SSQSB) rather than (SBF[Z]).

Milestones: Theorems 7.49, 7.53

Theorem 7.49: the full nesting chain (SBF[Z]) $\Rightarrow$ (SSQSB) $\Rightarrow$ (QSB), (SSQSB) $\Rightarrow$ (SSQSBw) $\Rightarrow$ (QSBw), together with the collapse theorem that (SBF[Z]) holds if and only if every linear perturbation of $g$ satisfies (QSBw) — precisely quantifying how weak (QSBw) is pointwise and how the classes reunite under universal perturbation. Theorem 7.53 (the quasi L-optimality criterion): the direct analogue of chunk 08's Theorem 7.14, showing that global (or, for the weaker (QSBw) case, unique-up-to-translation) optimality still reduces to a purely local check against the $2^n - 2$ nontrivial sign-pattern neighbors $p + \chi_X$.

Significance

The result itself. As with the M-convex case (chunk 07), the proximity theorem is what algorithms actually need: an L-convex-flavored objective transformed by any strictly increasing scalar rescaling (a common device — expressing a network-flow cost in a different currency, or applying a monotone risk adjustment) retains a scaling algorithm's correctness guarantee with exactly the same distance bound, even though the rescaled function is generally no longer L-convex itself.

Formalizing it. No matching item exists on the platform for quasi submodularity or quasi L-convexity in any form. Together with chunk 07 (the M-side quasi-convexity theory), this mission completes the "quasi" relaxation on both halves of the exchange-axiom framework the book develops, immediately before chapter 8 unifies M-convexity and L-convexity under a single conjugacy relationship.

Difficulty

As with chunk 07's quasi M-proximity theorem, the temptation is to imitate chunk 08's L-proximity proof line by line. The overall architecture does survive — translate so $p_\alpha = 0$, find a lattice-minimal sufficiently-good point, and bound the gap using submodularity — but chunk 08's proof uses (SBF[Z])'s additive inequality directly to compare four function values at once, while this proof must instead route every such comparison through (SSQSB)'s two one-directional implications (Proposition 7.50's quasi-version of the same two-sided inequality), which only ever license moving in one direction at a time depending on which side of a comparison is tight. The book's proof handles this by working with the specific implications (7.43)–(7.44) in place of the L♮-approach property used in chunk 08's proof — an ordinal substitute for the same additive step, at the cost of a case analysis chunk 08's proof did not need.

Formalization scope

This mission builds directly on chunk 08's published items (SBF, DomZ, ArgMin, IndicatorVec), per the platform's textbook convention that a later chapter section of the same book imports an earlier one's definitions; its own namespace DiscreteConvex.LConvexFunctions.Quasi nests under chunk 08's DiscreteConvex.LConvexFunctions accordingly. Note the sign convention of the linear perturbation here, $g[x](p) = g(p) + \langle p,x\rangle$, is the opposite of the M-side's $f[p](x) = f(x) - \langle p,x\rangle$ (chunks 06–07) — verified against the book's own formula rather than assumed by analogy.

A trivializing formalization of the goal would silently strengthen (SSQSB) back to plain (SBF[Z]) (making this mission redundant with chunk 08's Theorem 7.18) or loosen the exact bound $(n-1)(\alpha-1)$; neither is done. Only (QSB), (SSQSB), (QSBw), (SSQSBw) are drafted, matching exactly what the chosen three items need; the polyhedral L-convex-function bridge (§7.8–7.9, Theorems 7.40–7.46) and the level-set characterizations (Theorems 7.51–7.52) are left for a follow-on mission. Contributions building the 0L ↔ S correspondence (Theorem 7.40, a bridge back to chunk 04's submodular-set-function vocabulary) or the scaled quasi L-minimizer-cut analogue are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• P. Milgrom, C. Shannon, "Monotone comparative statics," Econometrica, 62(1), 1994, pp. 157–180.

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

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

Shortest-path distances and network potentials are among the oldest objects in combinatorial optimization: a directed graph with arc lengths, its shortest-path distances, and the "feasible potentials" (vertex labels consistent with those lengths) underlie duality in min-cost flow, scheduling, and difference-constraint systems. Murota's Discrete Convex Analysis (SIAM, 2003) isolates the abstract structure behind these objects — distance functions satisfying the triangle inequality, and their associated sets of admissible potentials — and shows it is governed by exactly the same discrete-convexity machinery as submodular set functions: a one-to-one correspondence with a second family of well-behaved integer point sets, the L-convex sets. Where an M-convex set (chapter 4) is defined by an exchange axiom generalizing matroid base exchange, an L-convex set is defined by closure under coordinatewise lattice operations (∨, ∧) and translation by the all-ones vector — a genuinely different axiom system that nonetheless produces a parallel structural theory: hole-freeness, a polyhedral description via an induced distance function, and integral convexity.

Companion mission 05-lconvex-sets (Discrete Convex Analysis IV) covers this chapter's other half: the hole-free property (Theorem 5.2), the one-to-one correspondence between L-convex sets and integer-valued triangle-inequality distance functions (Theorem 5.5), the intersection properties (Theorem 5.7), and the chapter's discrete separation theorem (Theorem 5.9, 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 the chapter leaves for its second half: the fundamental facts connecting a distance function to its admissible potentials (Proposition 5.1), the two-way polyhedral correspondence's supporting propositions (5.3-5.4), Minkowski-sum convexity (Theorem 5.8), and — this mission's goal — the explicit description of an L-convex set's convex hull that establishes its integral convexity (Theorem 5.10).

Setting

Fix a finite ground set $V$. A distance function is a map $\gamma : V \times V \to \mathbb R \cup \{+\infty\}$ with $\gamma(v,v) = 0$; it may take negative finite values and need not be symmetric. It defines a directed graph $G_\gamma = (V, A_\gamma)$ with $A_\gamma = \{(u,v) : \gamma(u,v) < +\infty\}$, arc $(u,v)$ having length $\gamma(u,v)$. Write $\bar\gamma(u,v)$ for the shortest-path length from $u$ to $v$ in $G_\gamma$ ($+\infty$ if none exists); $\gamma$ is well defined ($\bar\gamma$ finite-valued wherever a path exists) exactly when $G_\gamma$ has no negative cycle. The triangle inequality $\gamma(v_1,v_2) + \gamma(v_2,v_3) \ge \gamma(v_1,v_3)$ defines the class $T[\mathbb R]$ (or $T[\mathbb Z]$ when integer-valued). A vector $p \in \mathbb R^V$ is an admissible potential of $\gamma$ if $p(v) - p(u) \le \gamma(u,v)$ for all $u \ne v$; write $D(\gamma)$ for the set of all such potentials.

A nonempty set $D \subseteq \mathbb Z^V$ is L-convex if it satisfies (SBS[Z]): $p, q \in D \implies p \vee q,\ p \wedge q \in D$ (coordinatewise max/min), and (TRS[Z]): $p \in D \implies p \pm \mathbf 1 \in D$. A set $S \subseteq \mathbb Z^V$ is integrally convex if every point of its convex hull $\overline S$ lies in the convex hull of $S$ restricted to that point's integral neighborhood $N(p) = \{y \in \mathbb Z^V : \lfloor p \rfloor \le y \le \lceil p \rceil\text{ coordinatewise}\}$ — a strong, local form of "no holes" saying every real point of the hull is explained by nearby integer points alone.

Formalization targets

Goal: integral convexity of L-convex sets

For an L-convex set $D \subseteq \mathbb Z^V$, writing $a = p - \lfloor p \rfloor$ for the fractional part of $p \in \mathbb R^V$, $\alpha_1 > \cdots > \alpha_m$ for the distinct nonzero values of $a$, and $U_i(p) = \{v : a(v) \ge \alpha_i\}$ (with $U_0 = \emptyset$):

$$\overline D = \{p \in \mathbb R^V : \lfloor p \rfloor + \chi_{U_i(p)} \in D\ \ (i = 0, 1, \ldots, m)\}, \qquad \text{hence } D \text{ is integrally convex}.$$

This is the weakest stable form available: it exhibits an explicit, finite set of at most $|V|+1$ integer witnesses for every point of the hull, which is what "integrally convex" asserts abstractly, rather than a numerical bound that a sharper construction could later shrink.

Supporting structural targets

Four further results build the correspondence this goal uses: the basic duality between a distance function's admissible potentials, its shortest-path closure, and negative-cycle freedom (Prop. 5.1); the induced-distance-function construction recovering a triangle-inequality distance function from any integer point set, and the convex hull of an L-convex set as its associated polyhedron (Prop. 5.3); the converse construction recovering an L-convex set from an integer-valued distance function (Prop. 5.4); and convexity in Minkowski sum (Thm. 5.8).

Significance

Theorem 5.10 is what makes "L-convex" a genuinely convex-analytic notion rather than a combinatorial curiosity: it shows the convex hull of an L-convex set is not merely a polyhedron (already known from the chapter's polyhedral-description results) but one with the strongest local integrality property discrete convex analysis considers, integral convexity — every real point's hull membership is certified by a small, explicitly constructed set of nearby lattice points, uniformly across the whole set. This is the L-convex counterpart of the corresponding M-convex fact (chapter 4's Theorem 4.24) and is used later in the book wherever L-convex functions (chapter 7) need their epigraphs' local structure. Proposition 5.1 is the combinatorial engine underneath: it is exactly the LP-duality statement between shortest paths and feasible potentials that appears, in various guises, throughout network flow theory, made precise here as the base case the L-convex correspondence rests on.

None of these results are open — Murota presents them as, in his own words, "fundamental facts well known in network flow theory" (Proposition 5.1) systematized into the discrete convex analysis framework. What this mission contributes is a faithful, machine-checked formal statement of each, in the shared Lean vocabulary (LConvexSet, AdmissiblePotentials, ShortestDist) the rest of the Discrete Convex Analysis series can build on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The shortest-path closure $\bar\gamma$ is not a bookkeeping convenience but genuinely graph-theoretic content: proving Proposition 5.1 requires constructing an admissible potential from a shortest-path labeling and, conversely, deriving the negative-cycle-freeness of $G_\gamma$ from the mere existence of one admissible potential — a min-cost-flow-style LP duality argument, not a direct combinatorial check. Theorem 5.10's difficulty sits in a different place: the naive approach to "$D$ is integrally convex" would attempt an inductive argument peeling off one coordinate at a time, but the actual proof constructs a single, uniform family of $m+1$ witness points from the sorted fractional values of $p$ — a Carathéodory-style representation (Eq. (5.11)) that must simultaneously stay inside the integral neighborhood $N(p)$ and land in $D$ itself via the triangle inequality of $D$'s induced distance function, a construction with no one-coordinate-at-a-time shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; L-convex sets are Set (V → ℤ); distance functions are V → V → WithTop ℝ; admissible-potential sets are Set (V → ℝ). The shortest-path closure is formalized directly from finite walks (Fin (k+1) → V) rather than via a graph-library shortest-path predicate, matching the book's own construction. The Eq. (5.11) witnesses are built exactly as the book describes them — sorted distinct nonzero fractional values and their level sets — mirroring the Lovász-extension construction of the companion mission 20-ch04b-mconvexsets. No numeric constants are hard-coded anywhere in this mission (rule 7 is vacuous). The goal's explicit witness set (at most $|V|+1$ points) is not a trivializing special case: it holds for every L-convex set and every point of its hull, with no extra hypothesis narrowing the class. This mission's definitions (LConvexSet, AdmissiblePotentials, DistanceFunction, IsIntegrallyConvex) are redeclared from chunk 05-lconvex-sets (and, for IsIntegrallyConvex/IntegralNeighborhood, from chapter 3's own definitions) 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 five sorrys are welcome; Proposition 5.1's LP-duality argument and the goal's Carathéodory-style construction are the two with the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• A. J. Hoffman, "On abstract dual linear programs," Naval Research Logistics Quarterly, 10 (1963), pp. 369-373 (feasible-potential duality in network flow theory).