Discrete Convex Analysis

Motivation

This mission completes chapter 7's L-convex function theory and closes the book on it. It first finishes the theory of positively homogeneous L-convex functions — showing they coincide exactly with the classical Lovász extensions of submodular set functions, a one-to-one correspondence that recognizes forty years of submodular-optimization machinery as a special case of L-convex function theory. It then proves the L-side capstone this series has been building toward since mission 26-ch07b-lconvexfunctions: polyhedral L-convexity is characterized simultaneously by directional derivatives, subdifferentials, and weighted-minimizer polyhedra — the exact mirror of what mission 24-ch06d-mconvexfunctions proved for M-convex functions. Finally it develops quasi L-convex functions, the L-side analogue of mission 25-ch06e-mconvexfunctions's quasi M-convex functions, ending exactly where chapter 7 itself ends.

Setting

Fix a finite ground set $V$. The class $0L[\mathbb R \to \mathbb R]$ consists of polyhedral L-convex functions that are positively homogeneous; $0L[\mathbb Z \to \mathbb Z]$, its integer-valued integer-domain analogue. A positively homogeneous L-convex function $g$ induces a submodular set function $\rho_g(X) = g(\chi_X)$; conversely the Lovász extension $\hat\rho$ of a submodular set function is positively homogeneous L-convex. The base polyhedron $B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ \forall X,\ x(V) = \rho(V)\}$ of a submodular $\rho$ is always an M-convex polyhedron. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is quasi submodular (QSB) if $g(p\wedge q) \le g(p)$ or $g(p\vee q) \le g(q)$ for all $p,q$; the weaker (QSBw) requires only $\max\{g(p),g(q)\} \ge \min\{g(p\wedge q), g(p\vee q)\}$.

Formalization targets

Goal: the four characterizations of polyhedral L-convexity (Theorem 7.45)

For a polyhedral convex function $g$ with $\operatorname{dom}_{\mathbb R} g \ne \emptyset$: $g$ is L-convex if and only if every directional derivative $g'(p;\cdot)$ is $0L[\mathbb R \to \mathbb R]$, if and only if every subdifferential $\partial_{\mathbb R} g(p)$ is an M-convex polyhedron, if and only if every weighted minimizer set is an L-convex polyhedron. Not present in this chunk's own extraction table (its label opens mid-paragraph, missed by the same extractor failure already documented for mission 25-ch06e-mconvexfunctions's Theorem 6.68), found by direct reading and chosen as goal because it is the exact L-side mirror of mission 24-ch06d-mconvexfunctions's own milestone Theorem 6.63, and its proof is assembled entirely from results already in this series (Theorem 7.43, Proposition 7.34, Theorem 7.40).

Supporting structural targets

Fifteen further results build the two remaining pieces of chapter 7's theory. Propositions 7.37-7.39 and Theorem 7.40 establish the one-to-one correspondence between positively homogeneous L-convex functions and submodular set functions via the Lovász extension; Proposition 7.41 gives a minimizer-polyhedron characterization of this class, and Proposition 7.42 shows directional derivatives of L-convex functions automatically land in it. Theorem 7.43 — the L-side mirror of mission 24-ch06d-mconvexfunctions's own goal, Theorem 6.61 — proves the directional- derivative/subdifferential correspondence via the induced submodular set function's base polyhedron; Proposition 7.44 checks consistency at integer points, and Theorem 7.46 refines Theorem 7.45 to the integral case. Theorem 7.49 (also missed by the extractor) gives the quasi-submodularity implication hierarchy and its perturbation-equivalence capstone, mirroring mission 25-ch06e-mconvexfunctions's Theorem 6.68 exactly. Proposition 7.50 and Theorems 7.51-7.52 build the level-set/perturbation machinery quasi submodularity needs; Theorems 7.53-7.54 (both missed by the extractor, the latter's full statement requiring one page beyond this chunk's nominal range, at the very end of chapter 7) give the quasi L-optimality and quasi L-proximity theorems.

Significance

The 0L/submodular correspondence (Theorem 7.40) is the precise sense in which L-convex function theory generalizes submodular set function theory rather than merely resembling it: every submodular set function is literally the restriction to $\{0,1\}^V$ of a positively homogeneous L-convex function, and every algorithm for one transfers to the other through this exact dictionary. The goal, Theorem 7.45, completes the parallel structure this series has built since chapter 6: M-convexity and L-convexity are now each characterized in the same four convex-analytic vocabularies, setting up chapter 8's conjugacy theorem, which will show these two characterizations are not merely analogous but literally dual to each other under the Legendre-Fenchel transform. The quasi-submodularity results matter for the same reason as their M-side counterparts: chapter 10's algorithms for L-convex-function minimization remain correct under nonlinear rescalings that destroy L-convexity itself but preserve quasi submodularity.

None of these results are open — they are Murota's account of how far L-convex function theory extends beyond the polyhedral case (to positive homogeneity and its submodular-function incarnation) and how far its exchange-style inequality can be relaxed while preserving optimization theory (to quasi submodularity), mirroring chapter 6's identical two-part program for M-convex functions. What this mission contributes is a faithful, machine-checked formal statement of each, including four theorems (7.45, 7.49, 7.53, 7.54) the platform's own automated extractor missed entirely — one of them requiring a page beyond this chunk's own nominal range to complete, since chapter 7 ends there and this is the last mission covering it — extending the shared Lean vocabulary (ZeroLR, BasePolyhedron, QSBw) this series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to prove all six pairwise implications among its four conditions independently; the book's own proof instead chains through results already established: (a)⇒(b) is Proposition 7.42, (a)⇒(c) is Theorem 7.43, (a)⇒(d) is Proposition 7.34, (b)⇔(c) uses the 0L/M0[R] correspondence, and (d)⇒(b) is the genuinely hard direction, requiring Proposition 7.41 applied to the directional derivative itself (showing $\arg\min(g'(p;\cdot)[-x])$ is an L-convex cone by an explicit description via the admissible-potential set of the distance function underlying $\arg\min g[-x]$). The remaining combinatorial difficulty in this block is in Theorem 7.43's proof: identifying $\partial_{\mathbb R} g(p)$ with the base polyhedron $B(\rho_{g,p})$ requires the L-optimality criterion (Theorem 7.33, mission 27-ch07c-lconvexfunctions) applied pointwise, a chain of logical equivalences with no single-step shortcut, exactly mirroring how mission 24-ch06d-mconvexfunctions's Theorem 6.61 needed the M-optimality criterion.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; L-convex functions are (V→ℝ)→WithTop ℝ (polyhedral) or (V→ℤ)→WithTop ℝ (integer-domain). All sixteen numbered results found in this chunk's page range — the twelve in BRIEF.md's own table plus four the extractor missed (Theorems 7.45, 7.49, 7.53, 7.54) — are placed, with two documented, content-preserving scope decisions: Theorem 7.43 omits the dual-integral refinement clauses for L[R→R|Z]/L[Z→Z] (the same decision mission 24-ch06d-mconvexfunctions's Theorem 6.61 made), and Proposition 7.50 states the general inequalities without restating their "In particular" specializations, which add no independent content — see HARD.md. "$\inf g[-x]>-\infty$" is replaced by the equivalent (ArgMinR ...).Nonempty hypothesis throughout, matching mission 25-ch06e-mconvexfunctions's identical substitution. This mission's base vocabulary is redeclared from missions 20-ch04b-mconvexsets, 21-ch05b-lconvexsets, 23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the sixteen sorrys are welcome; the goal and Theorem 7.43 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota and A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 [152] (the polyhedral theory Theorems 7.26-7.46 are drawn from).
• P. Milgrom and C. Shannon, "Monotone comparative statics," Econometrica, 62 (1994), pp. 157-180 [129] (the origin of the quasi-submodularity condition (SSQSB)).

Motivation

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

Setting

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

Formalization targets

Goal: Theorem 8.54 (the saddle-point theorem)

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

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

Chapters 6 through 9 characterized minimality for M-convex functions structurally (the M-optimality criterion, Theorem 6.26: a point is a global minimizer iff no local swap improves it) without saying how to find one. Chapter 10 turns that structural fact into an algorithm: the local characterization is the termination test of the simplest possible minimization procedure, steepest descent by coordinate swaps. This mission formalizes that algorithm and its two complexity bounds, plus a structural min-max identity for submodular base polyhedra that the chapter's heavier submodular-minimization algorithms build on. It is the first mission in this series whose goal names a method, not just a property of a class of functions — formalizing it faithfully means giving the algorithm itself a Lean representation that the complexity theorem then quantifies over, not just describing its output.

Setting

Let $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ be an M-convex function (MExchangeAxiom, chunk 06), $n = |V|$. The steepest descent algorithm repeatedly replaces the current point $x$ by $x - \chi_u + \chi_v$ for a pair $u \ne v$ minimizing $f(x - \chi_u + \chi_v)$, stopping when no such swap improves on $f(x)$ — at which point, by the M-optimality criterion, $x$ is a global minimizer. This mission represents a run of the algorithm as a sequence $x : \mathbb N \to \mathbb Z^V$ satisfying these step and termination relations directly, so that "the number of iterations" is a genuine property of any such run, not an informal gloss. Separately, for a submodular set function $\rho : 2^V \to \mathbb R$ (chunk 04's SubmodularSetFunction), the base polyhedron $B(\rho)$ (chunk 04's BasePolyhedron) is the polytope $\{x \in \mathbb R^V : x(X) \le \rho(X)\ \forall X,\ x(V) = \rho(V)\}$.

Formalization targets

Goal: Proposition 10.2 (iteration bound with tie-breaking)

For an M-convex function $f$ with finite $\ell^1$-diameter $K_1 = \max\{\|x-y\|_1 : x,y \in \operatorname{dom} f\}$ (Eq. (10.1)), the number of iterations in the steepest descent algorithm using the tie-breaking rule (10.2) — a fixed lexicographic rule for choosing among tied steepest pairs, based on an arbitrary but fixed ordering $\varphi$ of $V$ — is bounded by $K_1/2$.

Milestones: Proposition 10.1, Proposition 10.8

Proposition 10.1: an unconditional warm-up — if $f$ has a unique minimizer $x^*$, any run of the plain (untied) algorithm from $x^0$ terminates within $\|x^0 - x^*\|_1/2$ iterations, with no tie-breaking rule needed. Proposition 10.8: a structural min-max identity, $\max\{x^-(V) : x \in B(\rho)\} = \min\{\rho(X) : X \subseteq V\}$, for a submodular set function $\rho$ — chosen deliberately as a milestone that names no algorithm at all, in contrast to this mission's other two items.

Significance

The result itself. Proposition 10.2 is the complexity backbone of §10.1: it is what turns "steepest descent terminates" (an easy monotonicity observation) into a genuine polynomial bound, and it is the base case the chapter's more elaborate scaling and domain-reduction algorithms (not drafted here) improve on. Proposition 10.8, though algorithm-free, is the structural fact ("verifying membership in $B(\rho)$ seems to need a submodular minimization procedure — but demonstrating optimality of a cut $X$ only needs a base with $x^-(V) = \rho(X)$") that makes Schrijver's and the IFF algorithms' correctness proofs possible, and specializes chunk 04's Edmonds's intersection theorem to the two-function case $\rho_1 = \rho, \rho_2 = 0$.

Formalizing it. A prior-art search (q=steepest descent, q=submodular minimization, q=base polyhedron) found no existing platform items for any of this chapter's results. This mission gives the first formal statement of an M-convex minimization algorithm's complexity, and directly reuses chunk 06's MExchangeAxiom/ArgMin/CharVec/DomZ and chunk 04's SubmodularSetFunction/BasePolyhedron — genuine cross-chunk substrate reuse spanning two different chapters' worth of prior missions.

Difficulty

The chapter's own framing (quoted in BRIEF.md) is that every other chapter's theorems state a property of a class of functions or sets, while this chapter's theorems state properties of a named algorithm run on such an object. Formalizing "the number of iterations in the steepest descent algorithm is bounded by ..." faithfully means giving the algorithm's steps (S0-S3) and termination test a Lean representation that the bound then quantifies over — stating the bound about "the minimizer" alone, with the algorithm silently dropped, would misrepresent the theorem as a fact about minimizers rather than about a procedure that finds one. This mission represents a run of the algorithm as an abstract sequence satisfying the book's own step-transition relations (documented in full in MODERATION_NOTES.md), letting the complexity theorems quantify over any valid run rather than committing to one executable implementation.

A second difficulty is scope: the chapter's recommended primary goal, Proposition 10.18 (Schrijver's algorithm's complexity), needs a scaling procedure with several auxiliary data structures — a materially larger definitional undertaking than steepest descent's simple greedy-swap loop. Per BRIEF.md's own explicit fallback authorization, this mission takes Proposition 10.2 as its goal instead; see HARD.md and MODERATION_NOTES.md for the full reasoning.

Formalization scope

Runs of the algorithm are represented as x : ℕ → V → ℤ satisfying IsSteepestDescentRun (plain) or IsSteepestDescentRunTieBreak (with the tie-breaking rule) — a step relation plus a termination test, with an explicit iteration count N the theorems bound. The tie-breaking key $\Phi(u,v)$ (Eq. (10.2)) and its lexicographic order are formalized directly (a manual three-way comparison, not Mathlib's default componentwise Prod order). Both iteration bounds are stated as 2 * N ≤ k rather than N ≤ k / 2, avoiding natural-number division. Not drafted: the derived "hence ... in $O(F \cdot n^2 K_1)$ time" corollary of Proposition 10.2 (needs a cost-model primitive for "time" and "$F$" this mission does not otherwise use — the iteration-count bound itself, this proposition's genuine combinatorial content, is drafted in full); Schrijver's algorithm and everything in §10.2.2 onward; the steepest descent scaling algorithm, the domain reduction algorithm and its scaling variant (§10.1.2-10.1.3, structurally different algorithms); the quasi-M-convex extension mentioned immediately after Proposition 10.2. A trivializing formalization would state the iteration bound as an unconditional fact about "a" minimizer-finding procedure, or would drop the tie-breaking rule from Proposition 10.2 and thereby understate what the bound actually requires; neither is done.

Selected references

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

Motivation

Chapter 10 turns from structure theory to algorithms: efficient methods for minimizing M-convex functions (via domain reduction) and submodular set functions (via Schrijver's and the Iwata-Fleischer-Fujishige scaling algorithms). Most of chapter 10's numbered results are asymptotic running-time bounds for specific procedural algorithms — a genuinely different kind of claim from the rest of this book (see Formalization scope). This mission places the results of this block that ARE ordinary mathematical propositions: correctness certificates, min-max theorems, and structural facts the algorithms rely on and produce.

Setting

For an M-convex set B ⊆ Z^V, the central part B° (the vectors of B lying away from its boundary, defined via per-coordinate bounds ℓ°_B, u°_B) is what the domain reduction algorithm searches from. For a submodular set function ρ : 2^V → R, the base polyhedron B(ρ) and its extreme bases (one per linear ordering of V, via Eq. (10.12)) let any base be written as a convex combination of finitely many extreme bases (Eq. (10.13)); a candidate minimizer W is certified via the linear orderings representing an optimal base. The Iwata-Fleischer-Fujishige (IFF) scaling algorithm relaxes this problem with a flow-augmentation parameter δ, maintaining a δ-feasible flow φ and vector z = x + ∂φ; near the end of a scaling phase, no augmenting path and no "active triple" together certify near-optimality.

Formalization targets

Goal: Near-optimality from the absence of augmenting paths (Proposition 10.20)

If S ⊆ W ⊆ V∖T, no arc of the auxiliary network leaves W, and no active triple exists, then z⁻(V) ≥ ρ(W)-nδ and x⁻(V) ≥ ρ(W)-n²δ; moreover W exactly minimizes ρ once δ is small enough relative to the smallest positive gap between two values of ρ. Chosen as goal: the book calls this "a key property of the scaling algorithm" and "a relaxation version of the min-max relation in Proposition 10.8", its own proof is the most substantial argument among this chunk's placed results, and Proposition 10.23 is a direct corollary of it.

Supporting structural targets

Proposition 10.8 is the min-max relation underlying the whole of section 10.2 (an Edmonds- intersection-theorem consequence, found by direct reading — the extractor's table missed it). Proposition 10.9 gives the three-part sufficient condition for optimality, in terms of the linear orderings representing an optimal base, that both Schrijver's algorithm and the IFF algorithm use as their termination criterion (also found by direct reading). Propositions 10.5-10.6 establish that the domain reduction algorithm's central part B° is always nonempty, via an explicit vector-extension step (Proposition 10.5 likewise missing from the extractor's table). Proposition 10.23 fixes individual coordinates once a scaling phase ends, and Proposition 10.24 gives the termination certificate for the IFF fixing algorithm's own separate graph-contraction procedure.

Significance

Chapter 10 is where this book cashes out its structure theory as algorithms with provable running times, and this mission places every result of that chapter's first two sections that is a mathematical proposition rather than a runtime bound: two min-max/optimality-certificate theorems (10.8-10.9) that are the combinatorial core making the following two strongly polynomial algorithms (Schrijver's, and Iwata-Fleischer-Fujishige's) correct, one central-part nonemptiness fact (10.5-10.6) underlying the domain reduction algorithm, and the two fixing/termination certificates (10.23-10.24) that let the scaling algorithms actually output a minimizer with a proof of optimality attached, not just a numerical answer.

None of these results are open — they are Murota's own account of submodular-function- minimization algorithms (sections 10.1-10.2). What this mission contributes is a faithful, machine-checked formal statement of each, including two results (Propositions 10.5 and 10.8) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

Six numbered results in this block (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are excluded as hard: each states a Big-O asymptotic bound on the running time, function-evaluation count, or internal-procedure-call count of a specific iterative algorithm (the domain reduction algorithm, its scaling variant, Schrijver's algorithm, the IFF scaling algorithm). Faithfully stating "this algorithm runs in O(g(n)) time" requires a cost-tracked operational semantics for that specific algorithm — a well-founded recursive procedure with an oracle for evaluating the input function, threading a step/evaluation counter, instantiated over an unbounded family of ground-set sizes n and numeric parameters (K∞, M) — which is a fundamentally different kind of formalization task (computational complexity theory) from every one of the roughly 280 other numbered results in this book, none of which require modeling the cost of computing them. See HARD.md.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq. Base M-convex-set vocabulary is redeclared from prior missions. Linear orderings of V are represented as bijections V ≃ Fin (Fintype.card V) rather than as lists, matching this series' established preference for order-indexed families over sequential data structures. Proposition 10.5's witness vector is stated as an existence claim (the mathematical content of the proposition), rather than by reconstructing the specific recursive modification procedure the book uses to produce it — a choice consistent with how this series has always formalized "the algorithm produces X" claims where X is a mathematical property, by asserting X's existence rather than executing the algorithm (see, e.g., mission 33-ch09c-networkflows's cycle-cancellation theorem). Six numbered results (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are hard; see HARD.md. Contributions completing any of the seven sorrys are welcome; the goal and Proposition 10.9 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• S. Iwata, L. Fleischer, and S. Fujishige, "A combinatorial strongly polynomial algorithm for minimizing submodular functions," Journal of the ACM, 48 (2001), pp. 761-777 [102] (the IFF scaling algorithm this mission's Proposition 10.20 certifies).
• A. Schrijver, "A combinatorial algorithm minimizing submodular functions in strongly polynomial time," Journal of Combinatorial Theory, Series B, 80 (2000), pp. 346-355 [182] (Schrijver's algorithm, whose termination criterion is Proposition 10.9).

Motivation

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

Setting

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

Formalization targets

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

Competitive-equilibrium theory for economies of divisible commodities — where consumption and production are real vectors — has rested on a rigorous mathematical foundation since around 1960, built from convexity, compactness, and fixed-point theorems (Debreu 1959; Arrow–Hahn 1971; McKenzie 2002). A large share of real markets, however, trade goods that cannot be split: houses, cars, aircraft, job assignments, radio spectrum licenses. For such economies, no comparably general existence theory existed before the framework this mission formalizes. Kelso and Crawford (1982) and Gul and Stacchetti (1999) had identified the gross substitutes property as the right condition on preferences for equilibrium to exist in labor-market and assignment models; Danilov, Koshevoy, and Murota (1998, 2001) showed that gross substitutes, and several other conditions proposed independently in the economics literature, all coincide with a single combinatorial notion from discrete convex analysis: M-natural-concavity. This mission formalizes the resulting existence theorem for economies with indivisible goods, together with the definitional results that pin down exactly what M-natural-concavity of a utility function means and how it connects to the classical demand-set language of general equilibrium theory.

Setting

Fix a finite set $K$ of indivisible commodity types and a finite set $H$ of consumers ("she"). A consumption bundle is an integer vector $x \in \mathbb Z^K$, one coordinate per commodity. Consumer $h$'s preferences over bundles, net of a perfectly divisible numeraire ("money"), are summarized by a utility function $U_h : \mathbb Z^K \to \mathbb R \cup \{-\infty\}$, where $-\infty$ marks bundles outside her feasible range (her effective domain, $\operatorname{dom} U_h = \{x : U_h(x) \ne -\infty\}$). Given a price vector $p \in \mathbb R^K$ (one real price per commodity), consumer $h$ chooses a bundle from her demand set

$$D_h(p) = \arg\max_{x \in \mathbb Z^K} \big(U_h(x) - \langle p, x\rangle\big),$$

the bundles that maximize utility net of expenditure; the shorthand $U_h[-p](x) := U_h(x) - \langle p,x\rangle$ is used throughout. For the notion this mission is built around, write $\chi_i \in \mathbb Z^K$ for the $i$-th unit vector, and for $x, y \in \mathbb Z^K$ let $\operatorname{supp}^+(x-y) = \{k : x(k) > y(k)\}$ and $\operatorname{supp}^-(x-y) = \{k : x(k) < y(k)\}$. A function $U$ with nonempty effective domain is M-natural-concave if it satisfies the exchange axiom: for $x, y \in \operatorname{dom} U$ and $i \in \operatorname{supp}^+(x-y)$,

$$U(x) + U(y) \le \max\Big(U(x-\chi_i)+U(y+\chi_i),\ \max_{j \in \operatorname{supp}^-(x-y)} \big[U(x-\chi_i+\chi_j) + U(y+\chi_i-\chi_j)\big]\Big),$$

with the convention that a maximum over the empty set is $-\infty$. A producer $l$ from a finite set $L$ is symmetric, described by a cost function $C_l : \mathbb Z^K \to \mathbb R \cup \{+\infty\}$ that is M-natural-convex — the mirror-image exchange axiom with $\min$ in place of $\max$ and the inequality reversed — and a supply set $S_l(p) = \arg\max_y(\langle p,y \rangle - C_l(y))$. An equilibrium for a total initial endowment $x^\circ \in \mathbb Z^K$ is a tuple $((x_h \mid h \in H), (y_l \mid l \in L), p)$ with $x_h \in D_h(p)$, $y_l \in S_l(p)$, market clearing $\sum_h x_h = x^\circ + \sum_l y_l$, and $p \ge 0$.

Formalization targets

$$\textbf{Theorem 11.13 (goal).}\quad \text{If every } U_h \text{ is nondecreasing and M-natural-concave with bounded domain, an equilibrium exists for every } x^\circ \in \bigcap_h \operatorname{dom} U_h \text{ in the exchange economy } (L = \emptyset).$$

This is the weakest form of the existence claim the mission proves in full — no producers, so no interaction between two different M-natural-convexity classes is needed — and is the natural target because it isolates exactly what M-natural-concavity buys on the consumer side alone. Two companion results sharpen the picture: Theorem 11.4 pins down M-natural-concavity through an equivalent single-step ascent property, and Theorem 11.7 restates it through the combinatorial structure (M-natural-convexity) of the demand sets themselves, connecting the definition to the gross-substitutes literature. Proposition 11.12 supplies the structural fact the existence proof turns on (the aggregate excess-cost function inherits M-natural-convexity and has a nonempty subdifferential), Theorem 11.14 extends existence to the general economy with producers by transporting an equilibrium down from a continuous relaxation, and Theorem 11.16 establishes that the set of all equilibrium prices is not merely nonempty but a lattice-structured polyhedron.

Significance

The result itself. Theorem 11.13 is a genuine existence theorem for a discrete general- equilibrium model — not an approximation or a relaxation of the continuous theory, but a free-standing result about the integer lattice. Its consequence set is also constructive by consequence: Theorem 11.16's lattice structure and section 11.5's reduction to submodular-flow computation (not part of this mission) together show that finding an extreme equilibrium price is a polynomial-time problem, not merely a nonempty-existence claim. Before this line of work, economists working with indivisible goods either restricted to special two-sided matching structures or worked with sufficient conditions (such as gross substitutes) whose relationship to each other and to any unifying combinatorial property was not understood; Fujishige–Yang (2003) and Murota–Tamura independently identified the M-natural-concavity connection cited here.

Formalizing it. All of the results in this mission are proved in the source text; nothing here is open. What formalization adds is a machine-checked confirmation that the demand/supply-set and equilibrium definitions, and the exchange-axiom characterization of M-natural-concavity, compose exactly as the informal statements claim — a nontrivial check, since the definitions involve several layers of arg-max/arg-min over integer lattices and price-shifted objectives that are easy to state slightly wrong (e.g. conflating $\arg\max$ and $\arg\min$, or omitting the extended index $0$ in the single-improvement axiom).

Difficulty

The obvious approach to existence — relax the discrete problem to $\mathbb R^K$, apply a classical fixed-point argument, and round the resulting continuous equilibrium to the nearest integer point — fails outright, and the book devotes section 11.2 to a two-agent, two-good example that demonstrates this concretely: at certain initial endowments, every candidate integer allocation leaves an unclaimed unit of surplus, so no equilibrium price exists at all, even though the continuous relaxation of the same economy has one. The gap is a failure of convexity in the Minkowski sum $D_1(p) + D_2(p)$: ordinary discrete demand sets can be "hole-free" individually and still sum to a set with a hole. M-natural-concavity is precisely the condition under which Minkowski sums of demand sets stay hole-free (a consequence of the parallel discrete-convex-set theory this book develops earlier), which is what makes the round-down argument valid after all — but only under this specific hypothesis, not under plain concavity or submodularity.

Formalization scope

Commodities and prices live on a general finite type $K$ (Fintype, DecidableEq), not a fixed $\mathrm{Fin}\ n$; consumers and producers are indexed by general finite types $H$, $L$, with the pure exchange economy realized as the special case $L = \mathrm{PEmpty}$. Utility values lie in WithBot ℝ ($\mathbb R \cup \{-\infty\}$) and cost values in WithTop ℝ ($\mathbb R \cup \{+\infty\}$), matching the book's asymmetric conventions for the two families exactly; no constant appears anywhere in this mission's statements (all hypotheses and conclusions are qualitative), so there is no explicit-constant obligation to record. The one hypothesis that must never be silently dropped is "nondecreasing" in Theorem 11.13: it is a real, separate condition from M-natural-concavity (more of a good is always weakly preferred), stated as its own conjunct rather than folded into the concavity predicate. A formalization that replaced M-natural-concavity with ordinary real-valued concavity, or dropped the boundedness hypothesis on the domains, would be a different — and for indivisible goods, false — statement; section 11.2's example is a concrete witness that discreteness together with a weaker structural hypothesis than M-natural-concavity is not enough. This mission's "M-natural-convex set" (used in Theorem 11.7) and "L-natural-convex polyhedron" (used in Theorem 11.16) are each formalized via one of the book's own stated equivalent characterizations (projection of an M-convex set on an extended ground set, and the (SBS-natural[R]) lattice-translation property respectively) rather than reintroduced as new primitives. Reusable beyond this mission: the general subdifferential SubdiffR and the EReal-valued concave/convex closure constructions apply to any discrete convex/concave function, not only to the aggregate cost function of this chapter. Contributions welcome on the sorry'd proofs, and on formalizing section 11.5's computational reduction to the M-convex submodular flow problem (deferred here — see HARD.md — pending chunk 12's flow vocabulary).

Selected references

• Murota, K. Discrete Convex Analysis. SIAM, 2003. DOI: 10.1137/1.9780898718508. (Chapter 11.)
• Kelso, A. S., Crawford, V. P. "Job Matching, Coalition Formation, and Gross Substitutes." Econometrica 50(6), 1982, 1483–1504.
• Gul, F., Stacchetti, E. "Walrasian Equilibrium with Gross Substitutes." Journal of Economic Theory 87(1), 1999, 95–124.
• Danilov, V., Koshevoy, G., Murota, K. "Discrete Convexity and Equilibria in Economies with Indivisible Goods and Money." Mathematical Social Sciences 41(3), 2001, 251–273.
• Fujishige, S., Yang, Z. "A Note on Kelso and Crawford's Gross Substitutes Condition." Mathematics of Operations Research 28(3), 2003, 463–469.
• Debreu, G. Theory of Value: An Axiomatic Analysis of Economic Equilibrium. Yale University Press, 1959.

Motivation

This mission continues chapter 11's account of the M♮-concave/M♮-convex exchange-economy model begun in mission 14-economic-equilibrium, placing seven of that chunk's own results that were previously left out-of-cone: the two gross-substitutes-style characterizations of M♮-concavity (§11.3), the transfer theorem that lifts an equilibrium of the continuous relaxation to one for indivisible commodities (§11.4), and the explicit polyhedral description of the equilibrium price set together with its feasibility criterion (§11.5).

Setting

Mission 14-economic-equilibrium built the exchange-economy vocabulary this mission redeclares in full (UDom, ArgMaxBot/ArgMinTop, PriceShift/PriceShiftConvex, DemandSet/SupplySet, IsEquilibrium, MNaturalConcave, IsMNaturalConvexSet, the concave/convex closures ConcaveClosureR/ConvexClosureR and their continuous analogues ContDemandSet/ContSupplySet/ IsContEquilibrium) and placed the qualitative structural theorems (Theorems 11.1-11.3, 11.4, 11.16-11.18, 11.23-11.24). This mission adds the gross-substitutes axioms (−M♮-GS[Z], the price-monotonicity property NegGS, and −M♮-SWGS[Z], its one-price-at-a-time refinement NegSWGS), the M♮-convex-set transfer machinery connecting a continuous equilibrium to a discrete one, and the equilibrium price polyhedron built from the three bound families ℓ(j), u(j), u(i,j) (Eqs. (11.40)-(11.42)) that make Theorem 11.16's qualitative L♮-convex-polyhedron fact concrete and linear-programming-checkable.

Formalization targets

Goal: The equilibrium price set is the explicit L♮-convex polyhedron (11.43) (Theorem 11.21)

For a fixed allocation (x,y), the set P* of all equilibrium price vectors is an L♮-convex polyhedron and equals the polyhedron cut out by max{0,ℓ(j)} ≤ p(j) ≤ u(j) and p(j)-p(i) ≤ u(i,j). Chosen as goal: it is the sharpest structural result of chapter 11's computation section, upgrading Theorem 11.16's qualitative fact to a concrete description, and is what Theorem 11.22 (also placed) builds on directly.

Supporting structural targets

Theorem 11.5 and Theorem 11.6 characterize M♮-concavity via the gross-substitutes and stepwise gross-substitutes properties, completing chapter 11's suite of M♮-concavity characterizations begun with Theorem 11.4 (mission 14). Theorem 11.15 is the general transfer theorem (continuous equilibrium ⟹ discrete equilibrium) that mission 14's own Theorem 11.14 invokes as a special case. Theorem 11.22 gives the feasibility criterion for the existence of an equilibrium price vector, the mission's second theorem built on the equilibrium price polyhedron.

Significance

Together with mission 14-economic-equilibrium, this mission completes the book's account of how M♮-concavity/convexity — a purely combinatorial exchange condition — reproduces, and sharpens, the classical gross-substitutes theory of competitive equilibrium for economies with indivisible goods: existence transfers from the continuous relaxation, and the equilibrium price set itself has a description exact enough to reduce to a linear feasibility question. None of these results are open — they are Murota's own account (attributed in the book's own notes to Danilov-Koshevoy- Lang and Murota-Tamura for the gross-substitutes theorems, and to Murota-Tamura for the equilibrium price polyhedron); this mission contributes a faithful, machine-checked formal statement of each (see Formalization scope).

Difficulty

Two of this chunk's seven BRIEF.md results are not drafted this pass, for a disclosed time- budget reason rather than any faithfulness failure: Proposition 11.19 and Theorem 11.20 require the H,L-indexed bipartite MSFP2 flow-network vocabulary (separate vertex sets V+_e, V+_l, V-_h, an M-convex/M-concave-combining flow objective) that neither this mission nor mission 14 builds, and building it in proportion to placing exactly these two results was judged disproportionate to the remaining time in this pass; see HARD.md and STATUS.md. This is explicitly not a hard exclusion — both results are well-posed and provable from the book's own complete proofs — and is recorded as an honest scope limitation for a future pass. Theorem 11.22's own trailing algorithmic remark (that equilibrium prices can be found via a shortest-path computation, yielding a polynomial-time equilibrium-checking algorithm) is a computational/ complexity claim outside this series' propositional-formalization methodology and is omitted; the mathematical "iff feasibility" content is placed in full. See HARD.md.

Formalization scope

Ground set K is a Fintype with DecidableEq; consumer/producer index sets H, L are Fintypes (Nonempty where the price-bound formulas (11.40)-(11.42) need a nonempty sup'/inf' range). All base vocabulary is redeclared fresh from mission 14-economic-equilibrium's own definitions, since this draft cannot import that sibling mission. The gross-substitutes axioms are formalized directly from their defining inequalities (Eqs. preceding (11.19) and following, and p.331); the equilibrium price polyhedron's bound families ℓ(j)/u(j)/u(i,j) are formalized literally from Eqs. (11.40)-(11.42), extracting each WithBot ℝ/WithTop ℝ operand to ℝ before subtracting (since WithBot ℝ carries no subtraction instance). Two results (Proposition 11.19, Theorem 11.20) are not drafted this pass for the disclosed time-budget reason above; one result (Theorem 11.22's trailing algorithmic remark) is scoped out as computational content. Contributions completing any of the five sorrys, or building the MSFP2 vocabulary to place Proposition 11.19/Theorem 11.20 in a follow-up mission, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• V. Danilov, G. Koshevoy, K. Murota, "Discrete convexity and equilibria in economies with indivisible goods and money," Mathematical Social Sciences, 41 (2001), pp. 251-273 [33] (origin of the gross-substitutes characterization, Theorem 11.6).
• K. Murota, A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [160] (origin of the equilibrium price polyhedron, Theorems 11.20-11.22).

Motivation

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

Setting

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

$$A = Q + T$$

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

Formalization targets

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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