Discrete Geometry

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).

Motivation

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

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

Setting

Fix a finite ground set $V$. A vector $x \in \mathbb Z^V$ assigns an integer $x(v)$ to each $v \in V$; write $x(X) = \sum_{v \in X} x(v)$ for $X \subseteq V$. For $x, y \in \mathbb Z^V$, the positive support $\operatorname{supp}^+(x-y) = \{v : x(v) > y(v)\}$ and negative support $\operatorname{supp}^-(x-y) = \{v : x(v) < y(v)\}$ record where $x$ exceeds, and falls short of, $y$. A nonempty set $B \subseteq \mathbb Z^V$ is M-convex if it satisfies the exchange axiom (B-EXC[Z]): for all $x, y \in B$ and $u \in \operatorname{supp}^+(x-y)$, some $v \in \operatorname{supp}^-(x-y)$ has both $x - \chi_u + \chi_v \in B$ and $y + \chi_u - \chi_v \in B$, where $\chi_u$ is the characteristic vector of $u$.

A set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ with $\rho(\emptyset) = 0$ and $\rho(V) < +\infty$ is submodular (the class $S[\mathbb R]$, or $S[\mathbb Z]$ when integer-valued) if $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$ for all $X, Y$. Its base polyhedron is $B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X),\ x(V) = \rho(V)\}$. The Lovász extension $\hat\rho : \mathbb R^V \to \mathbb R \cup \{\pm\infty\}$ linearly interpolates $\rho$ off $\{0,1\}^V$: sorting the distinct values of $p \in \mathbb R^V$ as $\hat p_1 > \cdots > \hat p_m$ and setting $U_i = \{v : p(v) \ge \hat p_i\}$, it is $\hat\rho(p) = \sum_{i=1}^{m-1}(\hat p_i - \hat p_{i+1})\rho(U_i) + \hat p_m \rho(U_m)$.

Formalization targets

Goal: discrete separation for M-convex sets

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• J. Edmonds, "Submodular functions, matroids, and certain polyhedra," in Combinatorial Structures and Their Applications, 1970, pp. 69-87.
• A. Frank, "An algorithm for submodular functions on graphs," Annals of Discrete Mathematics, 16 (1982), pp. 97-120.
• L. Lovász, "Submodular functions and convexity," in Mathematical Programming: The State of the Art, Springer, 1983, pp. 235-257.

Motivation

A classical convex function's global minimality is equivalent to its local minimality — the single fact that makes convex optimization tractable, since checking a small neighborhood suffices to certify a global guarantee. The discrete analogue is not automatic: a function on the integer lattice can fail to have any well-behaved "local" notion at all, and even when a discrete convexity-like property is imposed, the naive candidate (a function's values agreeing with its own convex-hull interpolation) does not by itself guarantee that local optimality implies global optimality. Murota's Discrete Convex Analysis (SIAM, 2003) isolates exactly the extra condition — integral convexity — that restores this guarantee, and shows it is general enough to contain every other discrete convexity notion the book studies (M-convex, L-convex, and their variants), making it the common ancestor of the book's entire hierarchy of classes. This mission completes the chapter's account of integral convexity: how it behaves under sums, restrictions, and linear perturbations, how it transfers between a function and its domain or minimizer sets, and a companion fact about hole-freeness under intersection and Minkowski sums that motivates why integral convexity, not mere hole-freeness, is the right notion to use.

Setting

For $f : \mathbb Z^n \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain $\operatorname{dom}_{\mathbb Z} f$, the convex closure is $\bar f(x) = \sup_{p,\alpha} \{\langle p,x\rangle + \alpha : \langle p,y\rangle+\alpha \le f(y)\ \forall y \in \mathbb Z^n\}$. The integral neighborhood of $x \in \mathbb R^n$ is $N(x) = \{y \in \mathbb Z^n : \lfloor x_i \rfloor \le y_i \le \lceil x_i \rceil\}$, and the local convex extension $\tilde f$ replaces "for all $y \in \mathbb Z^n$" in $\bar f$'s definition with "for all $y \in N(x)$". A function is integrally convex if $\tilde f = \bar f$ everywhere on $\mathbb R^n$. A set $S \subseteq \mathbb Z^n$ is integrally convex if its indicator function is; it is hole free if $S = \bar S \cap \mathbb Z^n$, where $\bar S$ is the real convex hull of $S$. The discrete Minkowski sum is $S_1+S_2 = \{x_1+x_2 : x_1 \in S_1, x_2 \in S_2\}$. A function is separable convex if $f(x) = \sum_i f_i(x(i))$ for univariate functions $f_i$ satisfying the discrete convexity inequality $f_i(t-1)+f_i(t+1) \ge 2f_i(t)$. For $p \in \mathbb R^n$, $f[-p] (x) = f(x) - \langle p,x \rangle$ and $\arg\min f[-p]$ is its minimizer set.

Formalization targets

Goal (Theorem 3.29). For $f$ with nonempty bounded effective domain,

$$f \text{ is integrally convex} \iff \arg\min f[-p] \text{ is an integrally convex set for every } p \in \mathbb R^n.$$

This leaves the characterization at the level of the two named properties (integral convexity of the function versus of every minimizer set), the strongest statement of this kind that holds without extra hypotheses beyond boundedness of the domain.

Supporting milestones. Proposition 3.17 (four basic containment/equality relations between hole-free sets' intersections, Minkowski sums, and their real closures); Proposition 3.22 (for a periodic integrally convex function, global optimality reduces to a one-sided local check); Proposition 3.24 (an integrally convex function plus a separable convex function is integrally convex); Proposition 3.25 (separable convex functions are integrally convex, and integral convexity survives linear perturbation); Proposition 3.26 (an integrally convex set is hole free); Proposition 3.28 (the effective domain and every minimizer set of an integrally convex function are integrally convex sets — the forward direction of the goal); and Proposition 3.30 (for integer-valued integrally convex functions, a finite infimum is always attained).

Significance

Theorem 3.29 turns a statement about a function on all of $\mathbb R^n$ (integral convexity, a condition on $\tilde f$ and $\bar f$ that is a priori about uncountably many points) into a statement about a countable family of discrete sets (the minimizer sets $\arg\min f[-p]$), giving a genuinely different and often more tractable way to certify or refute integral convexity. Propositions 3.24–3.25 are the closure properties that make integral convexity useful in practice: without them, verifying integral convexity of a function built from simpler pieces (a sum with a separable cost, a linearly reweighted objective) would require re-deriving the property from scratch each time. Proposition 3.17, by contrast, is a cautionary result: Note 3.27 and Example 3.15 (the two hole-free sets whose Minkowski sum has a hole) show that hole-freeness alone does not inherit good behavior under set operations, which is exactly the gap integral convexity's stronger, locally-checkable condition is built to close — this mission's Proposition 3.17 documents the "obvious"/general-purpose relations that hold regardless, so that the reader can see precisely which inclusion is automatic and which requires more.

Difficulty

The naive approach to Theorem 3.29's converse direction (integral convexity of every minimizer set implies integral convexity of $f$) tries to check $\tilde f(x) = \bar f(x)$ directly at an arbitrary $x \in \operatorname{dom} f$; this is circular, since $\tilde f$ and $\bar f$ are themselves defined via suprema over affine minorants, not via minimizer sets. The book's actual proof instead sets up a primal-dual pair of linear programs whose optimal solutions witness $\bar f(x)$ and $\tilde f(x)$ respectively, uses LP duality's complementary slackness to show the dual optimal solution can be chosen supported inside $N(x)$, and only then concludes $\tilde f(x) = \bar f(x)$ — routing the entire argument through the integral convexity of the specific minimizer set $S = \arg\min f[-p^*]$ at the optimal dual price $p^*$. This is why Theorem 3.29's proof needs LP duality (Theorem 3.10, formalized in the previous mission in this series) as an ingredient, not just the closure-property machinery of Propositions 3.24–3.28.

Formalization scope

All apparatus (ConvexClosure, IntegralNeighborhood, LocalConvexExtension, IntegrallyConvex, ArgMinPerturbed, HoleFree, IntegrallyConvexSet, SeparableConvex, MinkowskiSumZ) is redeclared fresh in DiscreteConvex.IntegralConvexityC, mirroring chunk 03-integral-convexity's already-established constructions (Fin n-indexed, WithTop ℝ-valued functions, EReal-valued convex closures via sSup), since a draft mission cannot import another draft's definitions. IntegrallyConvexSet is defined via the book's own primary definition (indicator function integrally convex) rather than either of its two stated equivalent reformulations, since no result in this mission needs those forms as a named predicate. An integer-valued function (Proposition 3.30) is represented as Zⁿ → WithTop ℤ and cast to WithTop ℝ via a small casting map wherever the real-valued apparatus is needed — a faithful embedding. Boundedness of a discrete set is containment in a finite integer interval. The formalization does not trivialize: Theorem 3.29's hypothesis is exactly "nonempty bounded effective domain", not further restricted to, say, a fixed small dimension or a finite ground set with a fixed cardinality bound, and every milestone is stated at the same generality as Propositions 3.24–3.28 and 3.30 give it (arbitrary $n$, arbitrary integrally convex function). Infrastructure needed beyond Mathlib: all definitions are fresh; a contribution completing any milestone, or the LP-duality-based proof of Theorem 3.29's converse direction, would be a natural entry point, alongside chunk 03's Theorem 3.21 as background.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 3.
• K. Murota, A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research 24 (1999), 95–105 (Lemma 6.13, cited for Proposition 3.30).

Motivation

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

Setting

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

Formalization targets

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

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

Many polytopes that arise in combinatorial optimization, such as the matching, cut, stable set and travelling salesman polytopes, have exponentially many facets, yet some of them can be written as the linear projection of a polyhedron with far fewer facets. The smallest number of facets of such a lift decides whether the polytope admits a compact linear-programming formulation. Yannakakis (Expressing combinatorial optimization problems by linear programs, J. Comput. System Sci. 43 (1991)) showed that this number equals the nonnegative rank of the polytope's slack matrix, turning a question about formulations into a question about matrix factorizations. Gouveia, Parrilo and Thomas (arXiv:1111.3164v2) extended this correspondence from polytopes and nonnegative orthants to arbitrary convex bodies and closed convex cones.

Exact nonnegative rank is NP-hard to compute (Vavasis, SIAM J. Optim. 20 (2009)), so lower bounds matter. The oldest ones are combinatorial: they see only which entries of the slack matrix are zero. Goemans (Smallest compact formulation for the permutahedron, Math. Program. 153 (2015)) observed that a polytope with $n_C$ faces needs a lift with at least $\log_2 n_C$ facets. Section 4.2 of Gouveia–Parrilo–Thomas recasts these support-based bounds through the face lattice and derives, alongside Goemans' bound, a sharper antichain bound. This mission formalizes that chain of results.

Setting

Write $\mathbb{R}^n$ for Euclidean space with inner product $\langle\cdot,\cdot\rangle$. A polytope $C \subseteq \mathbb{R}^n$ is the convex hull of finitely many points; as throughout the paper, the origin is assumed to lie in its interior. The polar of $C$ is

$$C^\circ = \{\, y \in \mathbb{R}^n : \langle x, y\rangle \le 1 \text{ for all } x \in C \,\}.$$

Let $\operatorname{ext}(C)$ be the set of extreme points of $C$ (its vertices). The slack operator $S_C$ is the function $S_C(x, y) = 1 - \langle x, y\rangle$ on $\operatorname{ext}(C) \times \operatorname{ext}(C^\circ)$. The extreme points of $C^\circ$ correspond to the facets of $C$, the facet of $y$ being $\{x \in C : \langle x, y\rangle = 1\}$, so $S_C$ is the canonical vertex–facet slack matrix of $C$ and is nonnegative.

An $\mathbb{R}^k_+$-factorization of $S_C$ consists of maps $A : \operatorname{ext}(C) \to \mathbb{R}^k_+$ and $B : \operatorname{ext}(C^\circ) \to \mathbb{R}^k_+$ with $S_C(x, y) = \langle A(x), B(y)\rangle$. The nonnegative rank $\operatorname{rank}_+(C)$ is the least such $k$, and $+\infty$ if there is none.

The support $\operatorname{supp}(S_C)$ is the $0/1$ matrix with a one where $S_C(x,y) \ne 0$. A Boolean factorization of it of intermediate dimension $k$ assigns subsets $A(x), B(y) \subseteq [k] = \{1,\dots,k\}$ with $S_C(x,y) \ne 0 \iff A(x) \cap B(y) \ne \emptyset$; the least such $k$ is the Boolean rank.

A face of $C$ is the empty set or a set of maximizers in $C$ of a linear functional; $C$ itself is a face. The face lattice $L(C)$ is the set of faces ordered by inclusion, and the Boolean lattice $2^{[k]}$ is the set of subsets of $[k]$ ordered by inclusion. An embedding $\varphi : L(C) \to 2^{[k]}$ satisfies $H \subseteq F \iff \varphi(H) \subseteq \varphi(F)$.

Formalization targets

Goal: Corollary 4.13 (p. 16)

For a polytope $C$:

$$\text{(1)}\quad \operatorname{rank}_+(C) \ \ge\ \min\Big\{ k : p \le \tbinom{k}{\lfloor k/2 \rfloor} \Big\}$$

for every antichain of $p$ faces of $C$ (no face contained in another), and

$$\text{(2)}\quad \operatorname{rank}_+(C) \ \ge\ \log_2 n_C ,$$

where $n_C$ is the number of faces of $C$, including $\emptyset$ and $C$.

Milestones

1. §4.2, p. 15. For a nonnegative matrix $M$, $\operatorname{rank}_B(M) \le \operatorname{rank}_+(M)$: a nonnegative factorization of intermediate dimension $k$ yields a Boolean factorization of $\operatorname{supp}(M)$ of the same dimension.
2. Theorem 4.11, p. 15. $\operatorname{supp}(S_C)$ has a Boolean factorization of intermediate dimension $k$ if and only if $L(C)$ embeds into $2^{[k]}$.
3. Corollary 4.12, p. 15. $\operatorname{rank}_+(C) \ge \min\{k : L(C) \text{ embeds into } 2^{[k]}\}$.

Significance

Both bounds depend only on the combinatorial type of the polytope. For a square they give $\operatorname{rank}_+ \ge \log_2 10 \approx 3.32$ and $\operatorname{rank}_+ \ge 4$; for a three-dimensional cube $\log_2 28 \approx 4.81$ and $6$ (p. 16). For the regular $n$-gon, whose slack matrices all have rank $3$, the face-count bound gives $\operatorname{rank}_+ \ge \log_2 n$, which is of the optimal order (Example 4.14). Theorem 4.11 is the statement that the Boolean rank of a slack matrix, also known as its rectangle covering number, is an invariant of the face lattice; the rectangle-covering version is phrased as Theorem 2.9 of Fiorini, Kaibel, Pashkovich and Theis (Combinatorial bounds on nonnegative rank and extended formulations, arXiv:1111.0444), as cited by the paper.

The results are proved in the paper. The formalization provides machine-checked definitions of the polar, the slack operator of a polytope, its nonnegative and Boolean ranks and its face lattice, reusable for later work on extension complexity (for instance, rectangle-covering lower bounds for specific polytopes). No formal proof of these statements is known to exist in Lean or on this platform.

Difficulty

Milestone 1 and the passage from Corollary 4.12 to Corollary 4.13 are short: Sperner's theorem is available in Mathlib as IsAntichain.sperner, and an embedding of $L(C)$ into $2^{[k]}$ is injective. The weight lies in Theorem 4.11, which needs facts about polytopes that Mathlib does not state in this form: every vertex is an exposed point, each extreme point of the polar cuts out a face, every face of a polytope is the convex hull of the vertices it contains, and every proper face is the intersection of the facets containing it, with those facets indexed by $\operatorname{ext}(C^\circ)$. The last fact is where the origin-in-the-interior assumption and the polar enter, and it fails for faces described by an arbitrary list of inequalities that is not the facet description. A second, smaller difficulty is finiteness: the face-count bound needs the set of faces of a polytope to be finite.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with the Euclidean inner product. The polar is the one-sided polar above, not Mathlib's absolute polar. A polytope is the convex hull of a Finset with the origin in its interior; $n = 0$ is allowed ($C = \{0\}$), and all targets hold there. Faces are Mathlib's exposed faces (IsExposed ℝ C F), which include $\emptyset$ and $C$, as the paper's counts do; for a polytope these are all faces. The factorization maps are total functions on $\mathbb{R}^n$ constrained only on extreme points. The nonnegative rank is valued in ℕ∞, the infimum of the empty family being $+\infty$; part (2) of the goal is stated for every finite value of the rank. Part (1) is stated for every antichain of faces, equivalent to the paper's "largest antichain". "Smallest $k$" is sInf of a set of naturals that is nonempty in each case (the set of $k$ with $p \le \binom{k}{\lfloor k/2\rfloor}$, and the set of $k$ admitting an embedding of the finite lattice $L(C)$).

The paper says "lattice embedding". Its proof of Theorem 4.11 constructs, and uses, only a map that preserves and reflects inclusion, and $\varphi(F) = \bigcup_{v \in F} A(v)$ need not preserve joins or meets; the formalization reads "lattice embedding" as an order embedding (Face C ↪o Finset (Fin k)) throughout.

Trivializing formalizations are ruled out: the rank is not a natural-number infimum (which would be $0$ when no factorization exists); faces are not arbitrary subsets of $C$; and an embedding is order-reflecting, not merely monotone (every poset maps monotonically into $2^{[0]}$).

Welcome contributions: a proof of milestone 1; a library of polytope facts (vertices are exposed points, faces are convex hulls of their vertices, finiteness of the face lattice, facets from the polar), which is reusable well beyond this mission; then Theorem 4.11 and the corollaries.

Selected references

• J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Math. Oper. Res. 38(2):248–264, 2013; arXiv:1111.3164v2. https://arxiv.org/abs/1111.3164
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, J. Comput. System Sci. 43(3):441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
• M. X. Goemans, Smallest compact formulation for the permutahedron, Math. Program. 153:5–11, 2015. https://doi.org/10.1007/s10107-014-0757-1
• S. Fiorini, V. Kaibel, K. Pashkovich, D. O. Theis, Combinatorial bounds on nonnegative rank and extended formulations, Discrete Math. 313(1):67–83, 2013; arXiv:1111.0444. https://arxiv.org/abs/1111.0444
• S. A. Vavasis, On the complexity of nonnegative matrix factorization, SIAM J. Optim. 20(3):1364–1377, 2009. https://doi.org/10.1137/070709967

Motivation

A conic quadratic program minimizes a linear objective subject to constraints of the form $\|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell$. Interior-point methods solve such programs in polynomial time, but around 2000 the available solvers handled far smaller instances than linear programming codes did. Ben-Tal and Nemirovski (Math. Oper. Res. 26(2), 2001) asked whether a conic quadratic program can be replaced by a linear program of comparable size, and answered it by approximating each second-order cone by a projection of a polyhedral cone. Their Theorem 1.1 builds such an approximation with accuracy $\varepsilon$ using $O(k\ln(2/\varepsilon))$ variables and inequalities. The present mission is their Proposition 3.1: this size is optimal in order, because every polyhedral $\varepsilon$-approximation needs $\Omega(k\ln(1/\varepsilon))$ inequalities.

The question of how many linear inequalities are needed to represent or approximate a convex set as a projection (its extension complexity) has since become a subject of its own, and the lower bound of Proposition 3.1 is one of its early explicit instances for a non-polyhedral cone.

Setting

For $y\in\mathbb R^k$ write $\|y\|_2=\sqrt{y_1^2+\dots+y_k^2}$. The Lorentz cone is

$$L^k=\{(y,t)\in\mathbb R^k\times\mathbb R\mid t\ge\|y\|_2\}.$$

Let $\varepsilon>0$. A polyhedral $\varepsilon$-approximation of $L^k$ is a linear map $\Pi:\mathbb R^k\times\mathbb R\times\mathbb R^p\to\mathbb R^q$ such that

1. if $(y,t)\in L^k$, then $\Pi(y,t,u)\ge0$ for some $u\in\mathbb R^p$;
2. if $\Pi(y,t,u)\ge0$ for some $u$, then $\|y\|_2\le(1+\varepsilon)t$.

Here $\ge0$ is componentwise, $p$ is the number of auxiliary variables and $q$ the number of homogeneous linear inequalities. Equivalently, the polyhedral cone $K=\{(y,t,u)\mid\Pi(y,t,u)\ge0\}$ projects onto a cone $\widehat L^k$ of the $(y,t)$-space with $L^k\subseteq\widehat L^k\subseteq\{(y,t)\mid\|y\|_2\le(1+\varepsilon)t\}$. The slice of $\widehat L^k$ at height one is $G=\{y\mid(y,1)\in\widehat L^k\}$, and $B=\{y\mid\|y\|_2\le1\}$ denotes the closed unit ball.

Formalization targets

Goal: Proposition 3.1, Eq. (13)

$$\exists\,c>0\ \ \forall k\ge2,\ \forall\varepsilon\in(0,\tfrac12],\ \forall p,q,\ \forall\Pi\ \text{polyhedral }\varepsilon\text{-approximation of }L^k:\qquad q\ \ge\ c\,k\ln\tfrac1\varepsilon .$$

The constant is absolute, as in the paper, and no value is fixed; the goal asserts only the order of growth.

Milestones (claims of the proof, in order)

1. Reduction. For $\varepsilon>0$ one may replace $\Pi$ by an approximation with the same $q$, at most $p$ auxiliary variables and the same projection, whose cone $K$ contains no line.
2. Extreme rays. A line-free cone $\{z\mid Az\ge0\}$ defined by $q$ inequalities is the conic hull of at most $2^q$ extreme rays.
3. Sandwich. $B\subseteq G\subseteq(1+\varepsilon)B$.
4. Vertices. If $K$ has no line, $G$ is the convex hull of $N\le2^q$ points.
5. Covering. If $\operatorname{conv}\{y_1,\dots,y_N\}\supseteq B$ and all $\|y_i\|_2\le1+\varepsilon$, the closed balls of radius $\sqrt{2\varepsilon(1+\varepsilon)}$ about the $y_i$ cover the sphere $\{\|y\|_2=1+\varepsilon\}$.
6. Counting. For $k\ge2$ and $\varepsilon\le\tfrac12$ such a covering needs $N\ge\exp\{c\,k\ln(1/\varepsilon)\}$ balls.

Significance

The result. Proposition 3.1 shows that the construction of Theorem 1.1 is optimal up to an absolute factor in the number of inequalities: approximating a conic quadratic constraint in dimension $k$ to relative accuracy $\varepsilon$ by linear inequalities costs $\Theta(k\ln(1/\varepsilon))$ inequalities, no more and no less. It separates what lifting (auxiliary variables) buys, a logarithmic dependence on $1/\varepsilon$, from what it cannot buy, a sub-linear dependence on $k$ or on $\ln(1/\varepsilon)$. Without auxiliary variables a polytope approximating the ball needs $\varepsilon^{-\Omega(k)}$ facets; the proposition says the logarithm of that count is the true cost even when lifting is allowed.

Formalizing it. The result is proved in the paper, in about fifteen lines that appeal to "elementary geometry" and to an unstated covering estimate. No machine-checked proof is known to exist. The mission produces a checked proof of the lower bound together with reusable facts: the finiteness bound on extreme rays of a pointed polyhedral cone and a lower bound on the number of balls needed to cover a Euclidean sphere, which Mathlib does not contain in this form. A companion mission of this series formalizes the matching upper bound (Theorem 1.1).

Difficulty

The obvious argument counts vertices of $G$: at most $2^q$ of them, and a polytope between $B$ and $(1+\varepsilon)B$ needs many vertices. The difficulty is in making "many" quantitative with the right exponent. A direct volume comparison of $G$ with $B$ gives nothing, since $G$ may have the volume of $(1+\varepsilon)B$. The argument needs the transfer from "the convex hull of the points contains $B$" to "the points are $\sqrt{2\varepsilon(1+\varepsilon)}$-dense on the outer sphere", and then a lower bound on the size of a covering of a sphere by balls whose centres need not lie on the sphere, uniform down to $k=2$ and up to $\varepsilon=\tfrac12$, where $\ln(1/\varepsilon)$ is only $\ln2$ and the radius $\sqrt{2\varepsilon(1+\varepsilon)}$ is comparable to the sphere's radius. A second, easily overlooked step is the passage to a line-free cone: $K$ itself may contain lines in the $u$-directions, in which case it has no extreme rays at all.

Formalization scope

Vectors of $\mathbb R^k$ are Fin k → ℝ, and the Euclidean norm is written out as eucNorm y = √(∑ i, y i ^ 2); the norm Mathlib puts on Fin k → ℝ is the sup norm, under which $L^k$ is polyhedral and the goal is false. A polyhedral approximation is an $\mathbb R$-linear map (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ), and $p$, $q$ are the dimensions of its types; with arbitrary (nonlinear) maps, $\Pi(y,t)=t-\|y\|_2$ would give $q=1$, so linearity is what makes the statement non-trivial. "Extreme ray" means a ray $\{sr\mid s\ge0\}$, $r\ne0$, that is an extreme subset (Mathlib IsExtreme) of the cone, counted once per ray.

Corrections of the printed statement. Proposition 3.1 is printed for every positive integer $k$. It is false for $k=1$: $L^1=\{|y|\le t\}$ is polyhedral, and $\Pi(y,t)=(t-y,t+y)$ is a polyhedral $\varepsilon$-approximation with $q=2$ for every $\varepsilon$, so $q\ge c\ln(1/\varepsilon)$ fails for small $\varepsilon$. The goal and the counting milestone are therefore stated for $k\ge2$, which is the case the proof covers. The phrase "polyhedral $\alpha$ approximation" in the proof is read as $\varepsilon$. The paper's $O(1)$ constants are existential and quantified before every variable they are uniform over; no numerical value is asserted.

A complete development needs the Minkowski–Weyl representation of pointed polyhedral cones by extreme rays, basic convex-hull and separation arguments in Euclidean space, and a lower bound for covering numbers of spheres (for instance by a cap-measure or volume argument). The extreme-ray and covering lemmas are independent of the Lorentz cone and are welcome as stand-alone contributions.

Selected references

• A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
• A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM, 2001. https://doi.org/10.1137/1.9780898718829