Convex Optimization

Motivation

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

Setting

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

Formalization targets

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Setting

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

Formalization targets

Goal: The potential criterion for MCFP3 (Theorem 9.4)

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Setting

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

Formalization targets

Goal: Theorem 7.18 (the L-proximity theorem)

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

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

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

Milestones: Theorems 7.1, 7.7, 7.14

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

Formalization targets

Goal: the directional-derivative/subdifferential correspondence

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

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

The relaxation method for a system of linear inequalities, introduced by Agmon and by Motzkin and Schoenberg in back-to-back papers of the Canadian Journal of Mathematics (1954), solves $\sum_j a_{ij}x_j + b_i \ge 0$ by repeatedly moving a point towards, or across, the most violated half-space. It is the ancestor of the perceptron algorithm, of Kaczmarz-type projection methods, and of the method of alternating projections, all of which are still used in feasibility problems, tomography and machine learning.

Motzkin and Schoenberg's paper ends (Part IV, §§9–10) by asking whether the behaviour of the reflexion process — the relaxation step with factor $\lambda = 2$ — survives when the finite family of half-spaces is replaced by an infinite one. They answer this for one natural infinite family: all supporting half-spaces of a closed bounded convex set. This mission formalizes that answer, Theorem 3 of the paper.

Timeline of the thread this mission belongs to:

• 1922 — Fejér observes that a sequence approaching every point of a set monotonically has useful convergence properties (Fejér, Math. Annalen 85, 1922).
• 1954 — Agmon proves convergence of the relaxation method for $0 < \lambda < 2$ (Agmon, Canad. J. Math. 6, 1954, pp. 382–392); Motzkin and Schoenberg prove finite termination of the reflexion method ($\lambda = 2$) for full-dimensional solution polytopes (Theorem 1), the oscillation behaviour in lower dimension (Theorem 2), and the convex-body version (Theorem 3) (Motzkin–Schoenberg 1954).

Setting

Let $E_n$ be $n$-dimensional Euclidean space and let $A \subseteq E_n$ be a nonempty, closed, bounded, convex set. Its dimension $r$ is the dimension of its affine span $L_r$, the smallest flat containing $A$.

For $p \notin A$ let $q$ be the point of $A$ nearest to $p$; it exists and is unique. The image of $p$ with respect to $A$ is

$$p_1 = F(p) = p + 2(q - p), \qquad (3.1)$$

the reflexion of $p$ through $q$. The reflexion process starts at $p_0 \notin A$ and sets $p_{\nu+1} = F(p_\nu)$ as long as $p_\nu \notin A$ (3.2). Either the process terminates with some $p_N \in A$, or it produces an infinite sequence of points outside $A$.

The family $F$ of supporting half-spaces of $A$ consists of the closed half-spaces $H \supseteq A$ whose bounding hyperplane touches $A$. The paper observes that the half-space $H_0$ through $q$ normal to $pq$ is the member of $F$ farthest from $p$, so (3.1) is exactly the reflexion step of the relaxation method applied to the infinite family $F$.

A sequence $\{q_\nu\}$ of points outside $A$ is Fejér-monotone with respect to $A$ if $q_\nu \ne q_{\nu+1}$ and $|q_{\nu+1} - a| \le |q_\nu - a|$ for all $a \in A$. Two points $u, v$ are symmetric with respect to a flat $L$ if their midpoint lies in $L$ and $u - v$ is orthogonal to $L$.

Formalization targets

Goal: Theorem 3 (p. 402)

For every nonempty closed bounded convex $A \subseteq E_n$ with affine span $L_r$, every $p_0 \notin A$ and every run $\{p_\nu\}$ of the reflexion process:

$$\textbf{Case 1: } r = n \implies \exists N,\ p_N \in A.$$ $$\textbf{Case 2: } r < n \implies \begin{cases} p_0 \in L_r \implies \exists N,\ p_N \in A,\\[2pt] p_0 \notin L_r \implies p_\nu \notin A\ \forall \nu, \text{ and } \exists \nu_0, u \ne v \text{ symmetric w.r.t. } L_r:\ \{p_\nu, p_{\nu+1}\} = \{u, v\}\ \forall \nu > \nu_0. \end{cases}$$

No number of steps is fixed: termination is finite but not uniformly bounded.

Milestones (attack order)

1. §9 — the half-space $H_0$ belongs to $F$, maximizes $\operatorname{dist}(p, H)$ over $F$, and every farthest member of $F$ yields the step (3.1).
2. §10 — an infinite run of the reflexion process is Fejér-monotone with respect to $A$.
3. Lemma 1, Case 1 — a sequence Fejér-monotone with respect to a set of dimension $n$ converges to a point.
4. §10 — the limit of an infinite run lies in $A$ and on its boundary.
5. Theorem 3, Case 1 — if $r = n$ the process always terminates.
6. §10 — orthogonal projection on a flat $L \supseteq A$ commutes with the image map, and each step keeps the distance to $L$ while switching sides.

Significance

The result. Theorem 3 shows that the dichotomy proved in the paper for finitely many half-spaces — finite termination when the target is full-dimensional, eventual oscillation otherwise — holds for the infinite family of all supporting half-spaces of a convex body. Case 1 says that reflecting through the nearest point, a method that uses no information about $A$ beyond metric projection, reaches a full-dimensional convex body in finitely many steps from any start. Case 2 says that for a lower-dimensional body the process detects this: the iterates settle into a two-cycle whose midpoint is a point of $A$, so a solution can be read off.

Formalizing it. The theorem is proved in the paper (1954), with a short proof of Case 1 that relies on geometric intuition about normal cones near a boundary point. To our knowledge no machine-checked proof exists. A complete development produces a verified finite-termination theorem for a projection method on general convex bodies, together with reusable facts about Fejér-monotone sequences and metric projections that recur throughout the analysis of projection algorithms.

Difficulty

The obvious argument for Case 1 is: the run is Fejér-monotone, hence converges (Lemma 1), and its limit $a$ lies on the boundary of $A$; then derive a contradiction. For a polytope (Theorem 1) the contradiction comes from finiteness: eventually every reflexion is in one of finitely many hyperplanes through $a$, which keeps the iterates on a sphere around $a$. For a convex body there are infinitely many supporting hyperplanes near $a$, and the iterates are reflected in a different one at every step; no finiteness argument is available. What replaces finiteness is an argument about how the supporting hyperplanes of $A$ at boundary points near $a$ are oriented, and the paper gives it only as an informal geometric sketch. Making this step rigorous is the main work of the mission.

Numerical experiments show that termination can take tens of thousands of steps near sharp corners of a polygon, so no bound on the number of steps in terms of the distance of $p_0$ to $A$ alone can be expected.

Formalization scope

• Space. $E_n$ is EuclideanSpace ℝ (Fin n). $A$ is a Set with four explicit hypotheses: A.Nonempty, IsClosed A, Convex ℝ A, Bornology.IsBounded A. Nonemptiness is implicit in the paper ("of dimension $r$", "the point of $A$ nearest to $p$").
• The image as a relation. IsImage A p p₁ holds when $p_1 = p + 2(q - p)$ for a nearest point $q$ of $A$; the nearest point is not chosen by a function. For closed convex nonempty $A$ this relation is a function on $E_n$. A run is any sequence with IsImage A (p ν) (p (ν+1)) whenever p ν ∉ A; values after entering $A$ are unconstrained. Every statement quantifies over every run from every $p_0 \notin A$; a formalization that only asserts the existence of some terminating run is ruled out.
• Dimension. $L_r$ is affineSpan ℝ A; $r = n$ is affineSpan ℝ A = ⊤, $r < n$ is affineSpan ℝ A ≠ ⊤. No separate natural number $r$ is introduced.
• Symmetry. IsSymmetricWrt L u v: midpoint ℝ u v ∈ L and u - v orthogonal to L.direction. For $r < n - 1$ this is a point reflection through the foot of the perpendicular, not a reflection in a hyperplane. The goal also requires $u \ne v$ and strict alternation $p_\nu \leftrightarrow p_{\nu+1}$ for $\nu > \nu_0$ (strict inequality, as printed).
• Boundary is frontier A; distances to sets are Metric.infDist.
• Generalizations recorded. Lemma 1, Case 1 is stated for an arbitrary set $A \subseteq E_n$ with full affine span (the paper states it for the polytope of (1.4) and applies it in §10 to a convex body). The projection milestone is stated for any flat $L \supseteq A$, not only after the paper's reduction to $r = n - 1$. The §9 milestone expresses "the reflexion process with respect to $F$ amounts to (3.1)" as: every farthest member of $F$, with any nearest point on it, gives the same step.
• Duplication. Case 1 appears both as a milestone and inside the goal, because the paper's proof of Case 2 cites Case 1. Solvers will need to transfer Case 1 from $E_n$ to the flat $L_r$ (an isometric copy of $E_r$).
• Infrastructure. Mathlib's metric projection onto complete convex sets (exists_norm_eq_iInf_of_complete_convex, norm_eq_iInf_iff_real_inner_le_zero) and EuclideanGeometry.orthogonalProjection cover the basic geometry. Normal cones of convex sets and their upper semicontinuity are not in Mathlib; a contribution there is reusable well beyond this mission. Proofs of any milestone, and alternative proofs of Case 1, are welcome.

Selected references

• T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 393–404. https://doi.org/10.4153/CJM-1954-038-x
• S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 382–392 (the companion paper in the same issue).
• L. Fejér, Über die Lage der Nullstellen von Polynomen, die aus Minimumforderungen gewisser Art entspringen, Mathematische Annalen 85 (1922), 41–48.

Motivation

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

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

Setting

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

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

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

Formalization targets

Goal: Theorem 6.37 (the M-proximity theorem)

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

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

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

Milestones: Theorems 6.2, 6.26, 6.28

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

Training a statistical model by empirical risk minimization means minimizing an average of $N$ losses over a parameter vector $w\in\mathbb R^n$, where both $N$ and $n$ can be in the millions. Stochastic gradient descent (SGD) is the standard method: each step uses the gradient of a small random batch of losses. It is cheap per step but sensitive to the scaling of the problem. Quasi-Newton methods such as L-BFGS correct the scaling in deterministic optimization, but naive stochastic versions are unstable, because differences of noisy gradients are poor curvature estimates.

Byrd, Hansen, Nocedal and Singer (SIAM J. Optim. 26(2), 2016) proposed the stochastic quasi-Newton (SQN) method. It decouples the two estimates: gradients come from small batches at every step, while curvature pairs are formed only every $L$ steps, from averaged iterates and subsampled Hessian–vector products. The paper's analysis (Section 3) shows that the method keeps the $O(1/k)$ expected suboptimality rate of SGD on strongly convex problems. The same eigenvalue bound was obtained independently by Mokhtari and Ribeiro (JMLR 16, 2015). Bottou, Curtis and Nocedal later gave a general treatment of such preconditioned stochastic methods (SIAM Review 60(2), 2018).

Setting

Let $f_1,\dots,f_N:\mathbb R^n\to\mathbb R$ be twice continuously differentiable losses and

$$F(w)=\frac1N\sum_{i=1}^N f_i(w).$$

For a sample $\mathcal S\subseteq\{1,\dots,N\}$ of size $b$, the minibatch gradient is $\nabla F_{\mathcal S}(w)=\frac1b\sum_{i\in\mathcal S}\nabla f_i(w)$. For a sample $\mathcal S_H$ of size $b_H$, the subsampled Hessian is $\nabla^2F_{\mathcal S_H}(w)=\frac1{b_H}\sum_{i\in\mathcal S_H}\nabla^2 f_i(w)$.

Assumption 1 requires constants $0<\lambda,\Lambda$ with $\lambda I\prec\nabla^2F_{\mathcal S_H}(w)\prec\Lambda I$ for every $w$ and every Hessian sample. It also requires a bound $\gamma^2$ on the second moment of the stochastic gradient. $w^*$ denotes the minimizer of $F$.

Algorithm 2 turns correction pairs $(s_j,y_j)$ into a matrix $H_t$. With $\tilde m=\min\{t,M\}$, it starts from $\frac{s_t^Ty_t}{y_t^Ty_t}I$ and applies the BFGS update

$$H\leftarrow(I-\rho_js_jy_j^T)H(I-\rho_jy_js_j^T)+\rho_js_js_j^T,\qquad\rho_j=\frac1{y_j^Ts_j},$$

for $j=t-\tilde m+1,\dots,t$.

Algorithm 1 (SQN) runs for $k=1,2,\dots$. It draws a gradient sample $\mathcal S_k$ and steps

$$w^{k+1}=w^k-\alpha^kH\nabla F_{\mathcal S_k}(w^k),$$

where $H=I$ for $k\le2L$ and $H=H_t$, $t=\lfloor(k-1)/L\rfloor-1$, afterwards. Every $L$ iterations it forms the block average $\bar w_t$ of the last $L$ iterates and a new pair

$$s_t=\bar w_t-\bar w_{t-1},\qquad y_t=\nabla^2F_{\mathcal S_{H,t}}(\bar w_t)\,s_t .$$

Samples are drawn independently and uniformly among the subsets of their size. The step length is $\alpha^k=\beta/k$.

Formalization targets

Goal: Corollary 3.3, with a corrected constant

There are $0<\mu_1\le\mu_2$, depending only on the problem data, such that every matrix Algorithm 1 applies satisfies $\mu_1I\prec H\prec\mu_2I$. Moreover, for every $\beta>1/(2\mu_1\lambda)$,

$$E[F(w^k)-F(w^*)]\le\frac{Q_c(\beta)}k\qquad(k\ge1),$$ $$Q_c(\beta)=\max\Big\{\frac{\Lambda\mu_2^2\beta^2\gamma^2}{2(2\mu_1\lambda\beta-1)},\ \Lambda\mu_2^2\beta^2\gamma^2,\ F(w^1)-F(w^*)\Big\}.$$

The constants $\mu_1,\mu_2$ are not fixed numerically. The goal asserts a rate of order $1/k$ with an explicit constant in terms of them.

Milestones

• (3.8)–(3.10): the curvature bounds $\lambda\|s\|^2\le y^Ts\le\Lambda\|s\|^2$ and $\lambda\le\|y\|^2/y^Ts\le\Lambda$ for Hessian-product pairs.
• (3.11) and (3.12): the trace bound and Powell's determinant formula for the direct L-BFGS matrices.
• Lemma 3.1: $\mu_1I\prec H_t\prec\mu_2I$ uniformly along every run.
• (3.18): expected descent for the general Newton-like iteration $w^{k+1}=w^k-\alpha^kH_k\nabla f(w^k,\xi^k)$.
• (3.19): $2\lambda[F(w)-F(w^*)]\le\|\nabla F(w)\|^2$.
• (3.22): the recursion $\phi_{k+1}\le(1-2\alpha^k\mu_1\lambda)\phi_k+\frac\Lambda2(\alpha^k\mu_2)^2\gamma^2$.
• Theorem 3.2: the $Q_c(\beta)/k$ rate for the Newton-like iteration.

Significance

The corollary says that curvature information costs nothing in rate. With uniformly bounded preconditioners and the $\beta/k$ schedule, the SQN method converges in expectation at the same order as SGD, which is the order known to be optimal for this class of problems. Lemma 3.1 is the reusable part: it holds for any L-BFGS matrix built from pairs whose curvature is controlled by a bounded Hessian. Theorem 3.2 applies to every stochastic method whose preconditioner is fixed before the sample is drawn and has uniformly bounded spectrum.

The formalization adds three things. First, it states the result correctly. As printed, Theorem 3.2 is false and Assumption 1(3) cannot be satisfied (see Formalization scope), and the mission states and labels the repaired versions. Second, it gives a machine-checked statement of the SQN algorithm itself, which is not currently formalized anywhere. Third, it provides L-BFGS and preconditioned-SGD infrastructure that later missions on stochastic second-order methods can reuse. To our knowledge none of these results has a machine-checked proof.

Difficulty

The natural first idea is to feed the iterates of Algorithm 1 to a standard SGD rate theorem. This fails for two reasons. The preconditioner $H_t$ depends on the past iterates and on independent Hessian samples, so the analysis needs a filtration in which $H_t$ is known before the gradient sample is drawn. Also, the rate proof itself is an induction that breaks in the first iterations, which is exactly where the printed argument goes wrong.

On the linear-algebra side, the difficulty is a lower bound on the smallest eigenvalue of $H_t$ that is uniform over all runs and all $t$. The curvature bounds on each individual pair do not give it directly, because the BFGS updates compound across the memory window. The expectation side needs conditional expectations of vector-valued functions and a descent inequality under a Hessian bound, neither of which Mathlib packages for this setting.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin n), matrices are Matrix (Fin n) (Fin n) ℝ acting through Matrix.toEuclideanLin, and $A\prec B$ is (B - A).PosDef. Hessians are fderiv ℝ (gradient f) w. Indices $k,t$ start at $1$ as in the paper. In the corollary, $E$ is an exact finite average over sample histories, and "almost surely" means "on every history". Theorem 3.2 uses a general probability space with a filtration. $H_k$ and $w^k$ are $\mathcal F_k$-measurable, the sample $\xi^k$ is $\mathcal F_{k+1}$-measurable, and unbiasedness is a conditional expectation. Integrability of $F(w^k)$ is part of each conclusion, so a junk-zero integral cannot satisfy it.

Two corrections to the paper, each labelled in the item titles and notes:

• Iterate-wise $\gamma$. Assumption 1(3) says $E_\xi\|\nabla f(w,\xi)\|^2\le\gamma^2$ for all $w$. Together with unbiasedness and $\lambda$-strong convexity on $\mathbb R^n$, this forces $\lambda\|w-w^*\|\le\|\nabla F(w)\|\le\gamma$ for every $w$, which is impossible. The mission imposes the bound at the iterates, conditionally on the past, which is how the proof uses it.
• Constant $Q_c(\beta)$. The induction after (3.22) multiplies by $1-2\beta\mu_1\lambda/k$, which is negative for $k<2\beta\mu_1\lambda$. Counterexample: $n=1$, $f_{1,2}(w)=(w\mp1)^2/2$, $H_k=I$, $w^1=0$, $\beta=2$, $\gamma^2=5$. Then $F(w^2)-F(w^*)=2>Q(2)/2=5/3$, and the example survives perturbing the constants so that every strict inequality holds. The middle entry of $Q_c$ repairs it, and $Q_c=Q$ whenever $2\mu_1\lambda\beta\le3/2$.

Smaller conventions:

• The pairs must satisfy $s_t\neq0$, since Algorithm 2 is undefined otherwise.
• Hessian samples have size $b_H\ge1$; the empty sample makes (2.3) a $0/0$.
• The corollary's undefined $\mu_2$ is Lemma 3.1's constant, enlarged together with $\mu_1$ to cover the initial $H=I$ steps.
• The block average of Algorithm 1 is used, not Eq. (2.1).

Trivializing encodings are ruled out: $H_t$ is Algorithm 2 applied to Algorithm 1's own pairs, not an arbitrary bounded matrix, and the second-moment bound is not imposed for all $w$.

Needed infrastructure, all welcome as contributions: the symmetry and spectral bounds of Hessians of $C^2$ functions, trace and determinant identities for BFGS updates, the descent lemma from a Hessian upper bound, conditional-expectation manipulations for adapted iterations, and the reduction of Algorithm 1 with uniform finite sampling to the abstract iteration.

Selected references

• R. H. Byrd, S. L. Hansen, J. Nocedal, Y. Singer, A Stochastic Quasi-Newton Method for Large-Scale Optimization, SIAM J. Optim. 26(2):1008–1031, 2016. https://doi.org/10.1137/140954362
• A. Mokhtari, A. Ribeiro, Global Convergence of Online Limited Memory BFGS, J. Mach. Learn. Res. 16:3151–3181, 2015. https://jmlr.org/papers/v16/mokhtari15a.html
• L. Bottou, F. E. Curtis, J. Nocedal, Optimization Methods for Large-Scale Machine Learning, SIAM Review 60(2):223–311, 2018. https://doi.org/10.1137/16M1080173
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust Stochastic Approximation Approach to Stochastic Programming, SIAM J. Optim. 19(4):1574–1609, 2009. https://doi.org/10.1137/070704277
• M. J. D. Powell, Some global convergence properties of a variable metric algorithm for minimization without exact line searches, in Nonlinear Programming, SIAM-AMS Proc. IX, 1976, pp. 53–72.

Motivation

Many first-order methods in optimization are fixed-point iterations $x^{k+1}=f(x^k)$ of a nonexpansive map $f:\mathbb R^n\to\mathbb R^n$: proximal gradient descent, projected gradient descent, alternating projections, ISTA and Douglas–Rachford splitting (with the conic solver SCS as an instance) all have this form (Zhang, O'Donoghue, Boyd 2020, §4.2). The averaged (Krasnosel'skiĭ–Mann) iteration $x^{k+1}=(1-\alpha)x^k+\alpha f(x^k)$ converges to a fixed point whenever one exists, but it is often slow in its terminal phase. Anderson acceleration (AA) combines the last few iterates through a quasi-Newton update of an approximate Jacobian; it is used for electronic-structure computations and, in the stabilized form studied here, in the solver SCS 2.1. Its type-I variant (AA-I) is often faster in practice than the more studied type-II variant, but it can be numerically unstable, and no global convergence guarantee existed for it on nonsmooth problems.

Timeline (as recounted in the paper's related-work section):

• 1965. Anderson introduces the method for nonlinear integral equations (J. ACM 12).
• 1978. Gay and Schnabel prove local Q-superlinear convergence of a full-memory AA-I-type method (Broyden with projected updates), assuming $f$ continuously differentiable near the solution.
• 2009. Fang and Saad connect AA with multisecant Broyden methods and distinguish the two types (Numer. Linear Algebra Appl. 16).
• 2011. Walker and Ni show the essential equivalence of full-memory AA with GMRES for affine $f$ (SIAM J. Numer. Anal. 49); Rohwedder and Schneider prove local Q-linear convergence of limited-memory AA-II for differentiable $f$.
• 2015. Toth and Kelley give local linear convergence of AA-II for contractive $f$ (SIAM J. Numer. Anal. 53).
• 2020. Zhang, O'Donoghue and Boyd introduce a stabilized AA-I method (Powell-type regularization, restart checking, safeguarding) and prove global convergence for every nonexpansive map with a fixed point, without differentiability (SIAM J. Optim. 30(4), 3170–3197; longer version arXiv:1808.03971).

Setting

Let $f:\mathbb R^n\to\mathbb R^n$ satisfy $\|f(x)-f(y)\|_2\le\|x-y\|_2$ for all $x,y$ (the Euclidean norm), and assume the solution set $X=\{x^\star\mid x^\star=f(x^\star)\}$ is nonempty. The residual is $g(x)=x-f(x)$, $g_k=g(x^k)$, and the averaged operator is $f_\alpha(x)=(1-\alpha)x+\alpha f(x)$.

Powell's weight. For $\bar\theta\in(0,1)$, $\phi_{\bar\theta}(\eta)=1$ if $|\eta|\ge\bar\theta$ and $\phi_{\bar\theta}(\eta)=(1-\operatorname{sign}(\eta)\bar\theta)/(1-\eta)$ otherwise, with $\operatorname{sign}(0)=1$.

Window matrices. For vectors $s_0,\dots,s_{m_k-1}$ and $y_0,\dots,y_{m_k-1}$, let $\hat s_i$ be their unnormalized Gram–Schmidt orthogonalization (3.2), $B^0=I$, and

$$B^{i+1}=B^i+\frac{(\tilde y_i-B^is_i)\hat s_i^T}{\hat s_i^Ts_i},\qquad \tilde y_i=\theta^iy_i+(1-\theta^i)B^is_i,\qquad \theta^i=\phi_{\bar\theta}\Bigl(\frac{\hat s_i^T(B^i)^{-1}y_i}{\|\hat s_i\|_2^2}\Bigr).$$

The matrix norm $\|\cdot\|_2$ is the induced $\ell_2$ operator norm.

Algorithm 3.1 (AA-I-S-m). With parameters $\bar\theta,\tau,\alpha\in(0,1)$, $D,\epsilon>0$ and max-memory $m\ge1$: start from $H_0=I$, $m_0=0$, $n_{AA}=0$, $\bar U=\|g_0\|_2$ and $x^1=\tilde x^1=f_\alpha(x^0)$. At iteration $k\ge1$, set $s_{k-1}=\tilde x^k-x^{k-1}$ and $y_{k-1}=g(\tilde x^k)-g(x^{k-1})$, orthogonalize $s_{k-1}$ against the current window, and restart the window (memory back to $1$, $H_{k-1}$ replaced by $I$) if the memory would exceed $m$ or $\|\hat s_{k-1}\|_2<\tau\|s_{k-1}\|_2$. Then apply one Powell-regularized rank-one update to obtain $H_k$ and the trial point $\tilde x^{k+1}=x^k-H_kg_k$. The trial point is accepted if $\|g_k\|_2\le D\bar U(n_{AA}+1)^{-(1+\epsilon)}$ (and $n_{AA}$ increases); otherwise $x^{k+1}=f_\alpha(x^k)$.

Formalization targets

Goal: Theorem 4.1

$$\text{for every run of Algorithm 3.1:}\qquad \lim_{k\to\infty}x^k=x^\star\quad\text{for some } x^\star=f(x^\star).$$

The only hypotheses are nonexpansiveness of $f$, $X\ne\emptyset$ and the parameter ranges. The limit is not specified: it depends on $x^0$ and the parameters.

Milestones

1. Lemma 3.2. Well-defined updates give $|\det B^{m_k}|\ge\bar\theta^{m_k}>0$.
2. Lemma 3.3. If $\|y_i\|_2\le2\|s_i\|_2$, $\|\hat s_i\|_2\ge\tau\|s_i\|_2$ and $m_k\le m$, then $\|B^{m_k}\|_2\le3((1+\bar\theta+\tau)/\tau)^m-2$.
3. Corollary 3.4. $\|H_k\|_2\le(3((1+\bar\theta+\tau)/\tau)^m-2)^{n-1}/\bar\theta^m$ (3.8).
4. Corollary 3.5. Along the algorithm, unless a solution is hit, (3.8) holds and $\mathrm{cond}(H_k)\le(3((1+\bar\theta+\tau)/\tau)^m-2)^n/\bar\theta^m$.
5. Eq. (4.3). $\|x^k-y\|_2\le\|x^0-y\|_2+CD\bar U\sum_{i\ge0}(i+1)^{-(1+\epsilon)}$ for every $y\in X$.
6. Eq. (4.6). $\lim_k\|g_k\|_2=0$.
7. Eq. (4.7). $\|x^{k+1}-y\|_2^2\le\|x^k-y\|_2^2+\epsilon_k$ with $\epsilon_k\ge0$ summable.
8. §4.1, Step 2. $\|x^k-y\|_2$ converges for every $y\in X$.

Significance

The theorem places a quasi-Newton acceleration scheme under the same hypotheses as the plain averaged iteration: nonexpansiveness and existence of a fixed point. It therefore applies at once to the nonexpansive examples of §4.2 of the paper (proximal gradient, projected gradient, alternating projections, ISTA, Douglas–Rachford splitting and SCS), with no smoothness, strong convexity or local assumption. The matrix bounds of Lemma 3.3 and Corollaries 3.4–3.5 are also of independent use: they give explicit, iteration-independent control of the approximate inverse Jacobians of a limited-memory type-I method, an assumption that other globalization frameworks (for example SuperMann) have to impose.

The result is proved in the paper; to our knowledge none of it is machine-checked. Mathlib has neither the Krasnosel'skiĭ–Mann iteration, nor Fejér monotonicity, nor any Anderson-type method. A formalization provides these pieces, checks the index bookkeeping of the restart and safeguard steps, and makes explicit the one place where the printed algorithm and the analysis disagree (line 9 at a window start; see below).

Difficulty

The accelerated step $\tilde x^{k+1}=x^k-H_kg_k$ need not decrease the distance to the solution set, so the Fejér argument for averaged iterations does not apply to it directly. The naive fix, bounding $\|H_kg_k\|_2$, requires a bound on $\|H_k\|_2$ that holds uniformly along the run; without the Powell regularization $B_k$ can be singular, and without the restart rule $\|B_k\|_2$ can grow without bound as the window becomes nearly linearly dependent. The determinant and norm bounds of Lemmas 3.2–3.3 have to be established for arbitrary windows and then connected to the run of the algorithm, where the window, its orthogonalization and the matrices are defined by an intertwined recursion with resets. The safeguard then turns the uniform bound into a summable perturbation of a Fejér-monotone sequence, and the final step needs an Opial-type argument to pass from convergence of distances to convergence of the iterates.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so all vector norms are Euclidean; matrices are continuous linear maps with the operator norm; $u\hat s^T$ is rankOne ℝ u ŝ; $\det$ is LinearMap.det; inverses are Ring.inverse (zero on singular maps, excluded by Lemma 3.2). The orthogonalization (3.2) is InnerProductSpace.gramSchmidt. Nonexpansive is LipschitzWith 1 f. The algorithm is the predicate IsAAISRun, a deterministic recursion: every run is determined by $f$, the parameters and $x^0$, and a sorry-free check that runs exist (for $f=\mathrm{id}$) was built locally. The reset of $H_{k-1}$ in line 8 is local to its iteration. $\mathrm{sign}(0)=1$ is encoded explicitly. Constants are the paper's explicit expressions; no milestone replaces them with an existential constant.

Line 9. The paper prints $\tilde y_{k-1}=\theta_{k-1}y_{k-1}-(1-\theta_{k-1})g_{k-1}$, derived from (3.3) through $B_{k-1}s_{k-1}=-g_{k-1}$, which fails when the window starts afresh ($m_k=1$). The mission uses (3.3) there: $\tilde y_{k-1}=\theta_{k-1}y_{k-1}+(1-\theta_{k-1})s_{k-1}$ when $m_k=1$, and the printed formula when $m_k\ge2$.

Milestones of §4.1 and Corollary 3.5 carry the hypothesis $f(x^k)\ne x^k$ for all $k$, as the paper does ("we temporarily assume for simplicity that a solution to (1.1) is not found in finite steps"); the goal does not. A goal proved from an unsatisfiable run predicate, or one that assumes a bound on $\|H_k\|_2$, contractivity of $f$, or that the accelerated step is never taken, is not this theorem. Division by zero in Lean can only occur once a fixed point has been reached, after which all later iterates coincide.

Useful reusable infrastructure includes the Krasnosel'skiĭ–Mann inequality $\|f_\alpha(x)-y\|_2^2\le\|x-y\|_2^2-\alpha(1-\alpha)\|g(x)\|_2^2$, quasi-Fejér monotone sequences and their convergence, and determinant and norm identities for rank-one updates (the matrix determinant lemma and Sherman–Morrison). Proofs of the window lemmas, of the run invariants (the window matrices coincide with the algorithm's $H_k^{-1}$) and of the convergence steps are all welcome.

Selected references

• J. Zhang, B. O'Donoghue, S. Boyd, Globally Convergent Type-I Anderson Acceleration for Nonsmooth Fixed-Point Iterations, SIAM J. Optim. 30(4), 3170–3197, 2020. https://doi.org/10.1137/18M1232772
• J. Zhang, B. O'Donoghue, S. Boyd, longer version, 2018. https://arxiv.org/abs/1808.03971
• D. M. Gay, R. B. Schnabel, Solving systems of nonlinear equations by Broyden's method with projected updates, in Nonlinear Programming 3, Academic Press, 245–281, 1978 (reference [20] of the paper). https://doi.org/10.1137/18M1232772
• D. G. Anderson, Iterative procedures for nonlinear integral equations, J. ACM 12(4), 547–560, 1965. https://doi.org/10.1145/321296.321305
• H. Fang, Y. Saad, Two classes of multisecant methods for nonlinear acceleration, Numer. Linear Algebra Appl. 16(3), 197–221, 2009. https://doi.org/10.1002/nla.617
• H. F. Walker, P. Ni, Anderson acceleration for fixed-point iterations, SIAM J. Numer. Anal. 49(4), 1715–1735, 2011. https://doi.org/10.1137/10078356X
• A. Toth, C. T. Kelley, Convergence analysis for Anderson acceleration, SIAM J. Numer. Anal. 53(2), 805–819, 2015. https://doi.org/10.1137/130919398
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7

Motivation

For a convex function on $\mathbb R^n$, a point is a global minimizer as soon as it is a local minimizer — this is one of the earliest and most consequential facts of convex analysis, and it underlies why local-search and gradient methods can certify global optimality in convex programs. The discrete analogue is not automatic: a function on the integer lattice $\mathbb Z^n$ can be "locally optimal" with respect to any fixed finite neighborhood system and still fail to be a global minimizer, unless the function's discrete structure is compatible with that neighborhood in the right way. Identifying exactly which classes of lattice functions admit a local-to-global optimality principle, and with respect to which neighborhood, is one of the organizing questions of discrete convex analysis.

Integrally convex functions, introduced by Favati and Tardella (1990) and developed systematically by Murota, are the most general class of $\mathbb Z^n$-valued functions for which such a principle holds. They are defined purely in terms of the classical convex closure of a real relaxation, which lets one import theorems from ordinary convex analysis, but the resulting notion of local optimality — checking only the $3^n - 1$ neighbors obtained by independently nudging each coordinate by $-1$, $0$, or $+1$ (excluding the trivial no-change case) — is a genuinely discrete, dimension-independent statement about functions whose domain can be arbitrarily large. Almost every discrete convex function class studied later in the book, including M-convex and L-convex functions, is a special case of integral convexity, and this mission's goal theorem is the direct ancestor of the optimality criteria (Theorems 6.26 and 7.14) that drive the algorithms in the rest of the book.

Setting

Let $f : \mathbb Z^n \to \mathbb R \cup \{+\infty\}$ be a function with nonempty effective domain $\operatorname{dom}_{\mathbb Z} f = \{x \in \mathbb Z^n : f(x) \ne +\infty\}$. The convex closure of $f$ is

$$\bar f(x) = \sup_{p \in \mathbb R^n,\, \alpha \in \mathbb R} \{\langle p,x\rangle + \alpha : \langle p,y\rangle + \alpha \le f(y)\ \forall y \in \mathbb Z^n\} \qquad (x \in \mathbb R^n),$$

the pointwise supremum of every affine function minorizing $f$ on all of $\mathbb Z^n$. If $\bar f$ agrees with $f$ on integer points, $f$ is convex extensible. 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,\ 1 \le i \le n\},$$

and the local convex extension $\tilde f$ relaxes $\bar f$'s definition by requiring the affine minorant condition only on $N(x)$ rather than on all of $\mathbb Z^n$. Always $\tilde f \ge \bar f$ pointwise, and the two agree on $\mathbb Z^n$. A function $f$ is integrally convex if $\tilde f = \bar f$ everywhere on $\mathbb R^n$ — equivalently, if $\tilde f$ is a convex function on all of $\mathbb R^n$ (it is automatically convex on every unit cube $[z, z+1]^n$ with $z \in \mathbb Z^n$, but need not be convex globally without this extra condition).

A discrete set $S \subseteq \mathbb Z^n$ is hole free if $S$ equals the set of integer points in its own real convex hull, and $\arg\min f[-p]$ denotes the minimizer set, over $\mathbb Z^n$, of the linearly perturbed function $f[-p](x) = f(x) - \langle p,x\rangle$.

Formalization targets

Goal: Theorem 3.21 (local optimality characterizes global optimality)

For integrally convex $f$ and $x \in \operatorname{dom}_{\mathbb Z} f$:

$$f(x) \le f(y)\ (\forall y \in \mathbb Z^n) \iff f(x) \le f(x + \chi_Y - \chi_Z)\ (\forall\, Y, Z \subseteq \{1,\dots,n\}),$$

where $\chi_Y \in \{0,1\}^n$ is the indicator vector of $Y$. The right-hand side is a check over at most $3^n - 1$ points (each coordinate independently unchanged, incremented, or decremented), regardless of how large $\operatorname{dom}_{\mathbb Z} f$ is; this uniform, dimension-only bound is the entire content of the theorem, and is the weakest correct formulation — restricting to a single $(Y,Z)$ or letting the right-hand side range over all of $\mathbb Z^n$ would trivialize or falsify the equivalence.

Milestones: Propositions 3.18 and 3.19

Proposition 3.18: $f$ convex extensible $\implies$ $\arg\min f[-p]$ hole free for every $p$ (and conversely, when $\operatorname{dom}_{\mathbb Z} f$ is bounded). Proposition 3.19: $f$ is integrally convex if and only if every restriction $f_{[a,b]}$ to a finite integer interval is integrally convex — integral convexity is detectable by looking at bounded pieces of $f$ one at a time.

Significance

The result itself. Theorem 3.21 is what makes integrally convex functions tractable: without it, verifying global optimality on an infinite or exponentially large integer domain would require checking every point. The theorem reduces this to a check whose size depends only on the dimension $n$, not on the size of the domain, and it does so for the widest class of lattice functions for which such a reduction is possible — the class is defined precisely so that this property holds and no wider natural class enjoys it. Every specialized local-optimality theorem later in the book (for M-convex, M$^\natural$-convex, L-convex, and L$^\natural$-convex functions) restricts this same neighborhood-checking principle to a class where the local check can be made even smaller (a single-element exchange rather than a full sign pattern) precisely because those classes are integrally convex plus more.

Formalizing it. No matching item exists on the platform: a direct search for "integrally convex" returns no results, and the theorem's own proof leans on results (Theorem 1.1's local-to-global principle for ordinary convex functions on $\mathbb R^n$, and an LP-duality-based alternate formula for $\tilde f$) that are either classical convex analysis or belong to a different chapter of this same book. The remaining work is therefore to give a complete, correct account of the definitional chain — convex closure, local convex extension, integral convexity — in a form a solver can build a proof from directly, and to state the finite local-check equivalence itself exactly at the strength the book proves it, not a plausible-looking weakening of it.

Difficulty

The natural first attempt is to try to prove the "$\Leftarrow$" direction of Theorem 3.21 by a direct induction on the $\ell^1$-distance to a global minimizer, moving one coordinate at a time. This fails in general lattice functions (a function that is only "coordinatewise convex" can have strict local minima that are not global), and the theorem's actual proof instead routes through the real relaxation: it shows the neighborhood-check hypothesis forces $x$ to be a local minimizer of the local convex extension $\tilde f$ restricted to the unit ball around $x$, then invokes ordinary convex analysis (local minimality implies global minimality for a convex function on $\mathbb R^n$) to conclude $x$ globally minimizes $\bar f$, and finally uses integral convexity ($\tilde f = \bar f$) to transfer this back to $f$ on $\mathbb Z^n$. The identification of $f$'s local behavior with $\tilde f$'s convexity on a single unit cube — rather than any coordinatewise or separable argument — is the step that makes the class of integrally convex functions exactly the right one for this theorem, and is where a naive combinatorial argument breaks down.

Formalization scope

The ground set is $\mathbb Z^n$, represented as Fin n → ℤ; $f$'s codomain is WithTop ℝ (exactly $\mathbb R \cup \{+\infty\}$), while the convex closure $\bar f$ and local convex extension $\tilde f$ take values in EReal (exactly $\mathbb R \cup \{\pm\infty\}$, a complete lattice, so their defining suprema are total functions with no side conditions). A trivializing formalization of the goal would quantify the right-hand side over a single fixed $(Y,Z)$ pair, or over all of $\mathbb Z^n$ instead of the sign-pattern neighbors; both are excluded by keeping $Y, Z$ universally quantified Finset (Fin n) ranging over the full $3^n$ sign-pattern space (minus the trivial case, which the equivalence still holds through vacuously).

Checked against the platform (GET /theorems?q=integrally convex, 0 hits) and against Mathlib's Analysis/Convex/ for the classical facts this chapter's proof would eventually need (ordinary convex-function local-to-global optimality, LP duality): these are broadly available in Mathlib's convex-analysis library in some form, but none of them is imported here, since none appears in the statement of any item this mission drafts — they belong to a proof this pass does not attempt. Contributions to a shared DiscreteConvex.IntegralConvexity definitions layer are welcome from chunks 06–09, which specialize integral convexity to M-convex and L-convex functions and will need the same convex-closure/local-extension vocabulary.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• P. Favati, F. Tardella, "Convexity in nonlinear integer programming," Ricerca Operativa, 53, 1990, pp. 3–44.