The OR Formalization Drive

Motivation

Matroid intersection is one of the founding results of combinatorial optimization: given two matroids on a common ground set, the largest common independent set can be found in polynomial time, and its size equals the minimum of a natural upper bound ranging over all subsets — a min-max theorem in the spirit of König's theorem and Menger's theorem, but for a strictly richer combinatorial structure. Jack Edmonds proved this in 1970, and Jack Edmonds and Rick Giles's subsequent generalization to submodular flows, together with André Frank's discrete separation theorem for submodular and supermodular set functions (1982), placed matroid intersection inside a single unifying framework: submodular function duality. This framework explains, in one stroke, matroid intersection, the base-exchange structure of matroids, and a family of other combinatorial min-max theorems that had previously seemed unrelated.

Murota's Discrete Convex Analysis develops this framework as the theory of M-convex sets: sets of integer vectors satisfying a lattice-exchange axiom that turns out to be exactly equivalent to being the integer points of a base polyhedron of an integer-valued submodular set function. This mission formalizes the chapter's central results: the equivalence of four variant forms of the exchange axiom (Theorem 4.3), the M-convex set / submodular function correspondence (Theorem 4.15), Frank's discrete separation theorem (Theorem 4.17), and Edmonds's intersection theorem itself (Theorem 4.18) — the deepest duality result in the theory of submodular functions and the historical origin of the M-convexity concept that the rest of the book generalizes to real-valued functions.

Setting

Let $V$ be a finite ground set. A set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ with $\rho(\emptyset) = 0$ and $\rho(V) < +\infty$ is submodular (the class $S[\mathbb R]$) if

$$\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y) \qquad (X, Y \subseteq V).$$

Its base polyhedron and submodular polyhedron are

$$B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X \subseteq V),\ x(V) = \rho(V)\}, \qquad P(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X \subseteq V)\},$$

where $x(X) = \sum_{v \in X} x(v)$; a supermodular function $\mu$ is one with $-\mu$ submodular. A nonempty set $B \subseteq \mathbb Z^V$ is an M-convex set if it satisfies the exchange axiom (B-EXC[Z]): for $x, y \in B$ and $u$ in the positive support of $x-y$, there is $v$ in the negative support of $x-y$ with both $x - \chi_u + \chi_v \in B$ and $y + \chi_u - \chi_v \in B$, where $\chi_u$ is the characteristic vector of $u$. A polyhedron $P \subseteq \mathbb R^V$ is integral if $P = \operatorname{conv}(P \cap \mathbb Z^V)$.

Formalization targets

Goal: Theorem 4.18 (Edmonds's intersection theorem)

For submodular set functions $\rho_1, \rho_2 \in S[\mathbb R]$,

$$\max\{x(V) : x \in P(\rho_1) \cap P(\rho_2)\} = \min\{\rho_1(X) + \rho_2(V \setminus X) : X \subseteq V\},$$

with both sides attained. If $\rho_1, \rho_2$ are integer valued, $P(\rho_1) \cap P(\rho_2)$ is an integral polyhedron and the maximum is attained at an integer point. Dropping the integrality clause and stating only the real max-min equality would leave ordinary LP duality with no discrete content at all; this mission keeps it in the goal at every strength the book proves it.

Milestones: Theorems 4.3, 4.15, 4.17

Theorem 4.3: the exchange axiom (B-EXC[Z]) is equivalent to three variants that impose the exchange condition asymmetrically or only for distinct vectors — groundwork establishing that M-convexity does not depend on which variant is taken as primitive. Theorem 4.15: $B$ is M-convex if and only if $B = B(\rho) \cap \mathbb Z^V$ for some integer-valued submodular $\rho$ — M-convex sets and integer-valued submodular set functions are two descriptions of the same combinatorial object. Theorem 4.17 (Frank): if a submodular $\rho$ dominates a supermodular $\mu$ pointwise, a single vector $x^*$ separates them ($\rho \ge x^* \ge \mu$ pointwise on every subset), integrally when $\rho, \mu$ are integer valued — derived, in the book, as a direct corollary of the goal theorem.

Significance

The result itself. Edmonds's intersection theorem is the min-max theorem underlying polynomial-time matroid intersection (a matroid's rank function is submodular, so the classical matroid intersection theorem is the special case $\rho_1, \rho_2$ both matroid rank functions), and its generality — arbitrary submodular set functions, not just matroid ranks — is what lets Frank's discrete separation theorem, and through it a wide range of combinatorial duality results in network flows, scheduling, and matroid theory, be derived as corollaries rather than proved from scratch each time. The integrality clause specifically is the fact that makes these duality theorems combinatorial: it guarantees that optimal fractional solutions to the underlying linear program can always be taken integral, without which the connection to discrete optimization would be lost.

Formalizing it. No matching item exists on the platform (searches for "submodular set function", "base polyhedron", "matroid intersection" return no relevant hits; Mathlib's Combinatorics/Matroid/ develops matroid rank functions, a special case, but not general submodular set functions or their polyhedra). This mission gives the first formal statement of the theorem at its natural generality, together with the M-convex-set viewpoint that motivates the rest of the book, and Frank's separation theorem as an explicit worked corollary.

Difficulty

The real-valued half of Theorem 4.18 is ordinary LP duality applied to a cleverly chosen primal program (maximize $\langle p, x\rangle$ over $P(\rho_1) \cap P(\rho_2)$) and its dual — routine once the right LP is written down. The integrality half is where the combinatorics enters: an optimal dual solution can always be chosen supported on a chain in each $\rho_i$'s effective domain (an extremal argument maximizing a strictly convex potential over the optimal dual face), and the incidence matrix of a chain of subsets is totally unimodular — this is the fact, external to ordinary LP theory, that forces an integral optimal solution to exist whenever the data ($\rho_1, \rho_2$) are integral. A proof that stops at real-valued LP duality, however carefully done, misses this step entirely and cannot produce the integrality clause; total unimodularity of a chain's incidence matrix is the one piece of combinatorics doing all the discrete work in an otherwise classical convex-duality argument.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; subsets are Finset V, vectors are V → ℝ/V → ℤ. Submodular functions take values in WithTop ℝ (exactly $\mathbb R \cup \{+\infty\}$); supermodular functions in WithBot ℝ; comparisons across the two use an explicit embedding into EReal. The max/min in the goal are stated via IsGreatest/IsLeast sharing a common EReal witness, so that "both sides attained, at the same value" — not merely "sup equals inf" — is what the Lean statement asserts, which is essential since the integrality clause's whole content is about which point attains the maximum.

A trivializing formalization of the goal would drop the integrality clause (leaving unqualified LP duality) or replace IsGreatest/IsLeast with a bare supremum/infimum equality (losing the "is attained" content the second half of the theorem needs); both are avoided. Theorem 4.15 is stated as the existential "iff" (some integer submodular $\rho$ realizes $B$) rather than reifying the book's own named bijection $\Phi, \Psi$ explicitly — a deliberate, documented scope reduction of that one milestone (see MODERATION_NOTES.md), not of the goal. Contributions building the explicit $\Phi$ map, the Lovász extension (needed for Theorem 4.16, not drafted here), or M-convex-set infrastructure reusable by chunks 06–07 (M-convex functions, which build on this chapter's vocabulary) are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• J. Edmonds, "Submodular functions, matroids, and certain polyhedra," in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, pp. 69–87.
• A. Frank, "An algorithm for submodular functions on graphs," Annals of Discrete Mathematics, 16, 1982, pp. 97–120.

Motivation

A decision maker who does not know the true parameters of the system they are controlling — the success probability of a slot machine, the drift of an asset, the failure rate of a machine — faces a genuinely different problem from one who knows them: every action taken has two effects, an immediate payoff and a change in what is known. Formalizing this "explore versus exploit" tension precisely is the subject of Bayesian sequential decision theory, whose best-known instance is the multi-armed bandit problem (Robbins, 1952; Gittins and Jones, 1974). Bäuerle and Rieder's treatment (Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5) gives the finite-horizon Bayesian theory its cleanest general form: rather than analyzing each bandit variant from scratch, it builds one reduction — from a Markov Decision Model with an unknown parameter to an ordinary, fully observed Markov Decision Model on an enlarged "information state" — and one structural theorem that turns primitive monotonicity hypotheses on the original ingredients into monotonicity of the optimal policy in the information state. Two classical finite-horizon bandit results (Theorems 5.5.1, 5.5.2) then follow as applications, not separate proofs.

Setting

A Bayesian Model is a Markov Decision Model whose unobservable component is a single, never-changing, unknown parameter $\theta$, drawn once from a prior distribution $Q_0$ on a parameter space $\Theta$. Concretely: an observable state space $E_X$, an action space $A$, a disturbance space $Z$ with reference measure $\nu$, a feasible set $D \subseteq E_X \times A$, a deterministic transition $T^X : E_X \times A \times Z \to E_X$, a disturbance density $q_Z(x,\theta,a,z)$, a reward $r(x,\theta,a)$, a terminal reward $g(x,\theta)$, and a discount $\beta \in (0,1]$.

Because $\theta$ is never observed directly, the decision maker's state of knowledge at stage $n$ is the posterior $\mu_n(\cdot \mid \tilde h_n)$, the conditional law of $\theta$ given the full observable history $\tilde h_n = (x_0,a_0,z_1,\dots,x_n)$. Bayes' rule updates this posterior one disturbance at a time; unrolling the update gives $\mu_n$ an explicit closed form as a product of likelihoods against the prior (Lemma 5.4.1), and the process $\mu_n(C\mid \cdot)$, for any fixed event $C$, is a martingale (Lemma 5.4.2) — it is, after all, a sequence of conditional expectations of the same random variable $\mathbf 1_{\theta \in C}$ against a refining amount of information.

Often the whole posterior is not needed to act optimally: a sufficient statistic $t_n$ compresses $\tilde h_n$ into a value in some space $I$ from which $\mu_n$ can still be recovered, and it is sequential if $t_{n+1}$ updates from only $(x_n, t_n, a_n, z_{n+1})$. Given a sequential sufficient statistic, the information-based Markov Decision Model replaces the never-observed $\theta$ by the always-computable $t_n$ as the second state coordinate, giving an ordinary Markov Decision Model on $E_X \times I$ whose reward, terminal reward, and transition law are the original ones averaged against the current posterior $\hat\mu(\cdot\mid i)$.

Formalization targets

$$\textbf{Theorem 5.4.10.} \quad \begin{aligned} &\text{Given: } D(\cdot) \text{ increasing; } q_Z(\cdot\mid\theta,a) \le_{lr} q_Z(\cdot\mid\theta',a) \text{ for } \theta \le \theta'\text{; } (x,z)\mapsto T^X(x,a,z),\\ &(\theta,x)\mapsto r(\theta,x,a),\ (\theta,x)\mapsto g(\theta,x) \text{ increasing; every increasing } v \in IB_b^+ \text{ has a maximizer in } \Delta.\\ &\text{Then: } IM := \{v \in IB_b^+ \mid v \text{ increasing}\} \text{ and } \Delta \text{ satisfy the Structure Assumption.} \end{aligned}$$

This is the weakest, most reusable form of the result: it names exactly the primitive hypotheses on the original model's ingredients under which the reduced model's Bellman equation holds and its value function and an optimal policy are monotone in the information state — without fixing which bandit or estimation problem those ingredients come from. Theorems 5.5.1 and 5.5.2 are downstream applications kept as milestones, not additional goals: proving the general theorem subsumes verifying its hypotheses in each concrete case.

Significance

Every one of the classical finite-horizon two-armed-bandit results — "switch to the arm with higher posterior mean once the advantage function is nonnegative," "never abandon a winning arm," "once you commit to the known arm, never leave it" — is, in this book's organization, a one-page corollary of Theorem 5.4.10 plus a routine (if occasionally fiddly) check of its five hypotheses on a two- or four-dimensional concrete state space. The theorem is what makes the qualitative behavior of an optimal bandit policy provable in general, rather than re-derived by induction for each new bandit variant.

Formalizing it also isolates, in one place, exactly which comparison of distributions (likelihood-ratio order, not the weaker stochastic order) makes the reduction go through, and exactly which practically checkable joint-density condition (MTP2) implies it (Lemma 5.4.9) — a genuinely reusable piece of probability theory beyond Markov decision theory.

Difficulty

The obvious first idea — "the information state's order is defined via the likelihood ratio order on posteriors, so just check the transition kernel is stochastically monotone and invoke the general increasing-model theorem of Chapter 2" — hides the actual difficulty: the state space of the reduced model is $E_X \times I$, and $I$ is itself a space of posterior distributions, so "the transition kernel is monotone" is a statement about how the whole posterior moves when a new observation arrives, not a fact about $E_X$ alone. The crux is showing that the sequential-sufficient-statistic update $\hat\Phi$ is jointly increasing in the current information state and the new disturbance — and this is exactly where Lemma 5.4.9's MTP2 characterization does the real work: MTP2 of the disturbance density in $(z,\theta)$ is what turns "a good disturbance is more likely under a good $\theta$" into "an increasing information state produces an increasing posterior update," without which the hypotheses on $D$, $T^X$, $r$, $g$ alone would not propagate to the enlarged state space at all.

Formalization scope

The Bayesian Model, its posterior, and the information-based model are formalized as they are introduced in the book: BayesModel bundles the primitive data (disturbance density, prior, reward, discount); Posterior bundles the filter $(\mu_n)$ as data satisfying its defining one-step Bayes update, rather than constructed from a canonical probability space, matching how MDPFinance.POMDP.FilterData (chunk 05a) treats the general Bayes operator; the Structure Assumption, Bellman operators, and bounding-function machinery of Chapter 2 are restated specialized to the stationary form the information-based model needs. "$\Theta, Z \subseteq \mathbb R$" and "$q_Z$ independent of $x$" (the "Monotonicity Results" subsection's own standing simplifications) are carried as explicit hypotheses of Lemma 5.4.9 and the goal, not silently dropped. A formalization that merely assumed the reduced model's disturbance kernel monotone, rather than deriving it via Lemma 5.4.9 from the checkable hypothesis on $q_Z$, would trivialize the theorem; this one keeps hypothesis (ii) exactly as the book states it. The two bandit applications (Theorems 5.5.1, 5.5.2) are formalized as self-contained concrete finite (countable-state, finite-action) Markov Decision Models, since the book itself reduces them to explicit recursions before stating the results — no general measure-theoretic machinery is needed there. Reusable beyond this mission: the likelihood-ratio order and MTP2 definitions (LikelihoodRatioOrder, IsMTP2), applicable to any Bayesian comparison result.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• H. Robbins, "Some aspects of the sequential design of experiments," Bulletin of the American Mathematical Society, 58(5), 1952, 527-535.
• J. C. Gittins and D. M. Jones, "A dynamic allocation index for the sequential design of experiments," in Progress in Statistics, 1974.
• A. Müller and D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002 (the book's own reference for the likelihood-ratio order and MTP2 functions, Appendices A.3, B.3).

Motivation

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

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

Setting

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

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

Formalization targets

Goal: discrete separation for M-convex sets

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

Machine scheduling asks how to assign jobs to machines over time. In many applications a job also needs additional scarce resources while it runs: a tool, a skilled operator, a memory bank, a channel. Adding such resources can turn a problem with a polynomial algorithm into an NP-hard one. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification $\alpha\,|\,\beta\,|\,\gamma$ of scheduling problems (Graham, Lawler, Lenstra and Rinnooy Kan 1979) with a resource field $res\lambda\sigma\rho$. They then drew the complete borderline between easy and hard problems for unit-time jobs, identical or uniform machines and the makespan criterion. Their Fig. 2 marks each problem type as polynomially solvable or NP-hard.

This mission formalizes the two hardness results of that classification that come from graph partition problems (Theorems 2 and 3, p. 15). Two identical machines are easy under any resource constraints (Theorem 1, after Garey and Johnson 1975). Theorems 2 and 3 show that a third identical machine, or two machines of different speeds, already makes the problem strongly NP-hard, once the number of unit resources is part of the input.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$. Each machine processes at most one job at a time, and each job runs on one machine without interruption. Machine $M_i$ has a speed $q_i>0$, and every job has unit execution requirement $p_j=1$, so it takes time $1/q_i$ on $M_i$. Identical machines ($P$) are the case $q_i=1$; uniform machines ($Q$) allow arbitrary speeds.

There are $l$ resources $R_1,\dots,R_l$. Resource $R_h$ has a positive integer size $s_h$, the amount available at any time. Job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. A schedule assigns each job a machine $\mu(j)$ and a start time $S_j\ge 0$. Its completion time is $C_j=S_j+1/q_{\mu(j)}$, and it is being executed at every time $t$ with $S_j\le t<C_j$. A schedule is feasible when:

• jobs on the same machine do not overlap in time;
• at every time $t$, the set $S_t$ of jobs being executed satisfies

$$\sum_{j\in S_t} r_{hj}\le s_h\qquad(h=1,\dots,l).$$

The makespan is $C_{\max}=\max_j C_j$.

The resource type $res{\cdot}11$ means three things: the number $l$ of resources is part of the input, every size is $s_h=1$, and every requirement satisfies $r_{hj}\le1$. A unit resource is therefore a conflict: two jobs that both need it can never run at the same time. The problems here have no precedence constraints. $Pm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ and $Qm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ ask for a feasible schedule of minimum makespan. Their decision versions ask, for a threshold $y$, whether a feasible schedule with $C_{\max}\le y$ exists.

The source problems are two graph problems on a graph $G=(V,E)$ with $|V|=3t$:

• PARTITION INTO TRIANGLES: can $V$ be partitioned into $t$ triples of pairwise adjacent vertices?
• PARTITION INTO PATHS OF LENGTH 2: can $V$ be partitioned into $t$ triples, each with at most one nonadjacent pair, that is, each spanning a path of length 2?

Both are NP-complete (Garey and Johnson 1979, problems GT11 and GT13).

The construction of p. 15 introduces one job per vertex and one unit resource $R_{\{j,k\}}$ per nonadjacent pair $\{j,k\}$, required by $J_j$ and $J_k$ only.

Formalization targets

Goal: Theorem 3

$$Q2\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}\ \text{is NP-hard in the strong sense.}$$

Formally: if the language of PARTITION INTO PATHS OF LENGTH 2 is NP-hard, then the language of unary codes of yes-instances of the decision version of $Q2\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard. The two speeds are arbitrary positive integers.

Milestones

1. The construction's key property (p. 15). In the constructed instance, two distinct jobs can be executed simultaneously if and only if their vertices are adjacent.
2. The triangle equivalence (proof of Theorem 2). $G$ has a partition into triangles if and only if the constructed instance on three identical machines has a feasible schedule with $C_{\max}\le t$.
3. Theorem 2. $P3\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard in the strong sense, given the NP-hardness of PARTITION INTO TRIANGLES.
4. The paths equivalence (proof of Theorem 3). $G$ has a partition into paths of length 2 if and only if the constructed instance on two uniform machines with speeds $q_1=2$, $q_2=1$ has a feasible schedule with $C_{\max}\le t$.

Significance

The results. Theorems 2 and 3 are two of the minimal NP-hard problems in the paper's classification. Together with Theorem 1 they place the borderline exactly: with unit resources whose number is part of the input, two identical machines are polynomial, while three identical machines, or two machines of different speeds, are strongly NP-hard. Strong NP-hardness rules out pseudo-polynomial algorithms unless P = NP, and it carries over to every more general resource type and machine environment in Fig. 1 and Fig. 2. Section 4.1 of the paper also derives hardness for $\sum C_j$ and $L_{\max}$ from these instances.

Formalizing it. The results are classical and proved on paper, but the paper's proofs are one sentence each ("Clearly", "It is easily seen"). No machine-checked proof exists, and the platform has no model of resource-constrained scheduling with real-valued time. This mission produces that model. It also produces a precise statement of strong NP-hardness on top of Cook's Turing-machine definitions, and the first formal NP-hardness reductions from graph partition problems to scheduling.

Difficulty

The scheduling half of each equivalence depends on the real-time model. On two uniform machines of speeds 2 and 1, jobs take time $\tfrac12$ and $1$, so jobs on the fast machine start at half-integers or anywhere else. The resource constraint must hold at every real time, not at a finite set of checkpoints. An argument that treats time as integer slots applies to the triangle case but does not transfer to the paths case.

The complexity half needs polynomial-time computability of the construction on Cook's one-tape Turing machines, on encoded strings that include malformed inputs. It also needs closure of polynomial-time reductions under composition, which the imported complexity layer states but does not prove.

Formalization scope

• Time and schedules. Start times are nonnegative reals, execution intervals are half-open $[S_j,C_j)$, and the resource constraints are imposed at every real time. Schedules are nonpreemptive.
• Indices. Jobs, machines and resources are 0-based (Fin n, Fin m, Fin l), so $q_1,q_2$ are q 0, q 1.
• Decision versions. "NP-hard" refers to the decision version with a threshold $y$. Thresholds are natural numbers and the $Q2$ speeds are positive integers. This restricted problem is a subproblem of the one with rational data, so its hardness is the stronger statement.
• Encodings and strong NP-hardness. Instances are strings over a two-letter alphabet with every number in unary. Graphs are $t$ in unary followed by the $3t\times 3t$ adjacency matrix, so $|V|=3t$ is part of the instance. Languages contain only codes of yes-instances. Strong NP-hardness is NP-hardness of the unary code language. With unary numbers, $\mathrm{Max}(I)\le\mathrm{Length}(I)$, so this is equivalent to Garey and Johnson's definition. The complexity layer is the published module CookPvsNP_defs.
• Cited hypothesis. Each hardness theorem takes as its only hypothesis the NP-hardness of its source problem, which the paper cites from Garey and Johnson rather than proves. The hypothesis is a true statement about a nonempty, non-universal language. The statements are not weakened to a reduction between languages, and they assume nothing about P versus NP.
• Source problems. The paper's phrase "three vertices, at most two of which are nonadjacent" is read as "at most one nonadjacent pair", which is Garey and Johnson's GT13. Reading it as "at most two nonadjacent pairs" would admit triples with a single edge and change the problem. PARTITION INTO PATHS OF LENGTH 2 reuses the published definition CubicP3Partition.P3Factor, a spanning non-induced $P_3$-factor.
• Construction. Resources are indexed by the nonadjacent pairs $j<k$ in lexicographic order, one per unordered pair and none for a pair $\{j,j\}$. A diagonal resource would make every job infeasible.
• Not trivial. A model that checks resources only at integer times, or only at start times, would make the paths equivalence false. A hypothesis on the target problem would make the goal circular. The definitions rule out both.

Welcome contributions: proofs of the two equivalences, polynomial-time computability of the construction on Cook's machines, and a general composition lemma for polynomial-time reductions. The composition lemma is reusable for every hardness mission built on CookPvsNP_defs.

Selected references

• J. Błażewicz, J. K. Lenstra, A. H. G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
• M. R. Garey, D. S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, 1979, ISBN 0-7167-1045-5.
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

The classical separating hyperplane theorem says that any two disjoint convex sets in $\mathbb R^n$ can be separated by a hyperplane with an arbitrary real normal vector. When the sets in question are not arbitrary convex sets but the integer points of specially structured discrete sets, one can sometimes ask for much more: not merely that a separator exists, but that it can be chosen from a small, structured, dimension-independent family regardless of the size or shape of the sets being separated. Results of this kind — "discrete separation theorems" — are a recurring and often surprising theme in combinatorial optimization, playing the role that the ordinary separation theorem plays in continuous convex analysis, but with genuinely combinatorial content beyond it.

L-convex sets, introduced by Murota as part of the discrete convex analysis framework, are one of the two dual families of well-behaved discrete convex sets studied in the book (the other being M-convex sets, chunk 04 of this series). They are defined by a lattice-closure axiom together with translation invariance, and they correspond one-to-one to integer-valued distance functions satisfying the triangle inequality — objects long familiar from network flow theory and shortest-path duality, even though the L-convexity terminology is not traditionally used there. This mission formalizes the chapter's central results, culminating in Theorem 5.9: two disjoint L-convex sets can always be separated by a vector with entries in $\{-1, 0, 1\}$, no matter how large or complicated the sets are.

Setting

Let $V$ be a finite ground set. A nonempty set $D \subseteq \mathbb Z^V$ is an L-convex set if it satisfies the sublattice axiom (SBS[Z]) — $p, q \in D \implies p \vee q,\ p \wedge q \in D$, where $\vee, \wedge$ are componentwise maximum and minimum — and the translation axiom (TRS[Z]) — $p \in D \implies p \pm \mathbf 1 \in D$, where $\mathbf 1$ is the all-ones vector. A distance function $\gamma : V \times V \to \mathbb R \cup \{+\infty\}$ satisfies $\gamma(v,v) = 0$ for every $v$; it satisfies the triangle inequality if $\gamma(v_1,v_2) + \gamma(v_2,v_3) \ge \gamma(v_1,v_3)$ for all $v_1, v_2, v_3$. The admissible-potential polyhedron of $\gamma$ is

$$D(\gamma) = \{p \in \mathbb R^V : p(v) - p(u) \le \gamma(u,v)\ (\forall u \ne v)\}.$$

The convex hull of a discrete set $D \subseteq \mathbb Z^V$ is written $\bar D \subseteq \mathbb R^V$.

Formalization targets

Goal: Theorem 5.9 (discrete separation for L-convex sets)

If $D_1, D_2 \subseteq \mathbb Z^V$ are disjoint L-convex sets, there exists $x^* \in \{-1,0,1\}^V$ such that

$$\inf\{\langle p, x^*\rangle : p \in D_1\} - \sup\{\langle p, x^*\rangle : p \in D_2\} \ge 1.$$

Dropping the $\{-1,0,1\}^V$ restriction and allowing an arbitrary real separator would recover the classical separation theorem for convex sets, which holds regardless of L-convexity and carries no discrete-convexity content; the three-valued restriction is the weakest correct strengthening and is kept in full.

Milestones: Theorems 5.2, 5.5, 5.7

Theorem 5.2: an L-convex set is hole free ($D = \bar D \cap \mathbb Z^V$) — its integer points are exactly the integer points of its own convex hull. Theorem 5.5: $D$ is L-convex if and only if $D = D(\gamma) \cap \mathbb Z^V$ for some integer-valued distance function $\gamma$ satisfying the triangle inequality — L-convex sets and such distance functions are two descriptions of the same object, the discrete analogue of chunk 04's M-convex-set / submodular- function correspondence. Theorem 5.7 (parts (1), (4)): L-convex sets are closed under intersection in the strongest sense — the convex hulls intersect exactly where the sets do, and a nonempty intersection of L-convex sets is again L-convex.

Significance

The result itself. Theorem 5.9 packs two claims into one, as the book itself points out: the separator is forced into $\{-1,0,1\}^V$ (explicit in the statement), and disjoint L-convex sets satisfy "convexity in intersection" — their convex hulls are already disjoint whenever the sets themselves are (implicit, and necessary for the stated inequality to be possible at all). The $\{-1,0,1\}$ structure connects directly to combinatorial duality in network flows: L-convex polyhedra are, without the name, a familiar object there, and a $\{-1,0,1\}$-separator corresponds to a signed cut or a negative-cost cycle in an associated graph. Theorem 5.5's correspondence is the L-convex mirror of chunk 04's M-convex/submodular correspondence, and the book explicitly flags that the two will be unified into a single conjugacy relationship in a later chapter (Note 5.6) — this mission's formalization of the L-side is a prerequisite for that later unification.

Formalizing it. No matching item exists on the platform (searches for "L-convex", "distance function", and "negative cycle" return only unrelated results — number-theoretic distance estimates, polytope graph metrics, shortest-path graph structures — none matching the combinatorial L-convexity/discrete-separation content here). This mission gives the first formal statement of L-convex sets and their central separation theorem. Notably, Theorem 5.9's own statement — unlike the analogous M-convex Theorem 4.18 — needs none of the distance-function machinery that its proof uses; only the L-convexity axiom itself appears in the goal, making its formal statement comparatively lean even though the underlying mathematics is just as deep.

Difficulty

The natural first attempt at Theorem 5.9 is to try to construct $x^*$ directly from the structure of $D_1, D_2$ — for instance, from a normal vector to a real separating hyperplane, rounded coordinatewise. This does not work: rounding an arbitrary real separator gives no control over its entries, and there is no reason a rounded vector should still separate. The book's actual proof instead represents $D_1, D_2$ via distance functions $\gamma_1, \gamma_2$ (Theorem 5.5), combines them into $\gamma_{12} = \min(\gamma_1, \gamma_2)$, and extracts the separator from a shortest negative cycle in the associated graph: the vertices of the cycle alternate between the two sets' "tight" arcs, and the alternating $\pm 1$ pattern around the cycle is exactly the $\{-1,0,1\}$ vector $x^*$ — with the cycle's negativity translating directly into the required gap of at least $1$. Locating the right combinatorial object (a shortest negative cycle, not an arbitrary one) is what pins the separator down to a vector supported on a single alternating cycle rather than an arbitrary $\{-1,0,1\}$ pattern, and is the step a naive rounding or linear-algebra argument has no analogue of.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $D \subseteq \mathbb Z^V$ is a Set (V → ℤ). Distance functions take values in WithTop ℝ; the goal's infimum and supremum are taken in EReal (a complete lattice), since L-convex sets are always infinite (translation invariance along the all-ones direction), so an ℝ-valued supremum/infimum would silently return a junk value on an unbounded set. The conclusion is stated as $\sup_{D_2}\langle p,x^*\rangle + 1 \le \inf_{D_1}\langle p,x^*\rangle$, an addition-based reformulation of the book's subtraction inequality that avoids EReal's ⊤ - ⊤ ambiguity while remaining equivalent whenever both sides are finite.

A trivializing formalization of the goal would drop the $\{-1,0,1\}^V$ constraint on $x^*$ (recovering the classical, L-convexity-independent separation theorem) or fix a single coordinate pattern rather than asserting existence over the full three-valued family; neither is done here. Theorem 5.5 is stated existentially rather than via the book's named bijection $\Phi, \Psi$ (a documented scope reduction, parallel to chunk 04's treatment of Theorem 4.15), and Theorem 5.7 is drafted with only its two representation-independent clauses (parts (1) and (4); see MODERATION_NOTES.md). Contributions building the distance-function/admissible- potential apparatus needed for Theorem 5.7's remaining clauses, or the L-convex/integrally-convex bridge (Theorem 5.10, needing chunk 03's vocabulary), are welcome.

Selected references

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

Motivation

Every portfolio-choice model treated so far in this series assumes the investor knows the exact law governing the market's returns. Real investors do not: the drift of a stock, the regime a market is in, or the probability of an up-move in a simplified binomial model is itself uncertain and must be learned from the very prices being observed. Bäuerle and Rieder's Chapter 6 (Markov Decision Processes with Applications to Finance, Springer, 2011) is the book's synthesis of two threads developed separately earlier: Chapter 5's reduction of a partially observable decision problem to an ordinary one on an enlarged "belief" state space, and Chapter 4's classical solutions of terminal-wealth utility maximization and dynamic mean-variance portfolio choice. Combining them answers a natural question with no simple a priori answer: how does not knowing which market you are in change the qualitatively optimal way to invest, and can the closed-form solutions of the fully-observed theory be recovered, term for term, once the unknown factor is replaced by a belief about it?

Setting

The market has an unobservable factor Y (state space E_Y) driving the vector of relative risks Z ∈ ℝ^d of d risky assets: given Y_n = y, the next return Z_{n+1} has a density q_R(y,\cdot), and Y itself evolves via its own transition density q_Y(y,\cdot), jointly — crucially, this joint law depends only on y, never on wealth or the action taken. An investor observes only the stock prices (equivalently, the return history), never Y itself. Bayes' rule turns this into a filtering problem: the investor's belief ρ_n \in \mathbb P(E_Y) about the current factor is updated one return at a time by an operator Φ(ρ,z) that depends only on the current belief and the newly observed return — a genuine simplification of Chapter 5's general Bayes operator, forced by the market's own structure. The pair (x_n,ρ_n) — observable wealth and current belief — is then an ordinary, fully observed state for an ordinary Markov Decision Model, and every value function and optimal policy of this chapter lives on that enlarged state space.

Formalization targets

The goal, Theorem 6.2.3, solves the dynamic mean-variance problem (MV): minimize the variance of terminal wealth X_N subject to a target expectation \mathbb E[X_N] \ge \mu, under partial observation. It is reached by a Lagrangian embedding into an auxiliary quadratic-loss problem QP(b), solved explicitly in Theorem 6.2.2, whose value function factors as ((xS^0_N/S^0_n)-b)^2 d_n(\rho) for a belief-only sequence (d_n) satisfying the backward recursion (6.7); Lemma 6.2.1 shows this sequence always lies strictly between 0 and 1, which is exactly what makes the final variance formula and Lagrange multiplier well-posed. The remaining milestones develop the parallel terminal-wealth theory of §6.1: the general structure theorem (Theorem 6.1.1), its power- and logarithmic-utility closed forms (Theorems 6.1.2, 6.1.7), and — for the specific binomial market with an unknown up-probability — a likelihood-ratio monotonicity result for the filter update (Lemma 6.1.4) and a comparison between the partially and completely observed optimal investment fractions (Theorem 6.1.5).

Significance

The chapter's organizing insight is that partial observation does not require a new theory: once the belief is added as a state coordinate, every general result already proved for fully observed Markov Decision Models — the Bellman equation, the existence of optimal Markov policies, the Lagrangian embedding technique for mean-variance problems — applies unchanged. What is genuinely new, and genuinely non-trivial, is checking that the reduced model inherits the structural hypotheses (monotonicity, boundedness, positive-definiteness of covariance matrices) those general theorems require, expressed now as conditions on the belief-indexed quantities Φ(ρ,z), d_n(\rho), \ell_n(\rho), C_n(\rho) rather than on the original, unobserved factor. Theorem 6.1.5's comparison result is a genuinely new phenomenon with no fully-observed analogue at all: it quantifies, in the two opposite directions dictated by the sign of the risk-aversion parameter γ, how residual uncertainty about the market itself changes the qualitatively optimal amount to invest — the discrete-time analogue of a continuous-time result in the literature this book cites (Sass and Haussmann 2004).

Difficulty

The recurring difficulty across every result in this mission is that the reduced model's state space E_X \times \mathbb P(E_Y) includes a space of probability measures as one coordinate, and every quantity that must be shown well-defined, monotone, or bounded is a functional on that space, not a function on a concrete Euclidean set. Formalizing the mean-variance recursion (6.7) in particular is a three-way mutual computation — a scalar d_n(\rho), a vector \ell_n(\rho), and a matrix C_n(\rho), each an integral against the same belief-dependent predictive law of the next return, each feeding the next stage's version of all three — where Lemma 6.2.1's strict-inequality bound is not a bookkeeping detail but exactly the fact that keeps C_n(\rho) invertible and the whole construction from breaking down. Theorem 6.2.3 itself is the hardest single step: verifying that the specific constant b^* the Lagrangian method selects makes the mean constraint bind at exact equality, and that the resulting variance is the true constrained minimum (not merely a feasible value), is exactly the non-trivial content a superficial restatement of Theorem 6.2.2 at an unspecified b would silently discard.

Formalization scope

Every value function of this chapter — the terminal-wealth maximization of §6.1, the quadratic loss QP(b) and the mean-variance problem (MV) of §6.2 — is built from one shared history-dependent value-function scaffold, parametrized by its terminal payoff (the utility U, a quadratic loss, or the raw first/second moment), its rate sequence (constant in §6.1, non-stationary in §6.2), and its feasible-action correspondence, rather than four separately re-derived constructions. Optimal fractions in the binomial sub-model (Lemma 6.1.4, Theorem 6.1.5) are characterized as any maximizer of the relevant one-step concave problem rather than through the closed-form solution the book's own proof derives via machinery from a different, unavailable chunk (Lemma 4.2.9) — the comparison and monotonicity results proved here are facts about any such maximizer, not about that specific formula. A formalization that assumed the reduced model's filter update or covariance structure directly, rather than deriving it from the market's own return and factor densities via the Bayes operator Φ, would trivialize every result in this mission; none of the items here take that shortcut.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• R. Sass and U. G. Haussmann, "Optimizing trading strategies with respect to drawdown in the hidden Markov model," Statistics & Decisions, 2004.
• N. Bäuerle and U. Rieder, "Portfolio optimization with unobservable Markov-modulated drift process," Journal of Applied Probability, 2007.
• V. Runggaldier, W. Trivellato, and T. Vargiolu, "A Bayesian adaptive control approach to parameter estimation and optimal portfolio selection," in Mathematical Finance, Trends in Mathematics, Birkhäuser, 2002 (the binomial-market source this chapter's §6.1 example specializes).

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

Every mission in this series so far has treated a finite-horizon decision problem: an investor or planner with a fixed, known number of periods left. Many of the most important applications — perpetual investment, an infinitely-repeated inventory or maintenance problem, a firm that never stops operating — have no natural end date at all. Chapter 7 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) builds the theory needed to make sense of "the value of a decision problem that never ends," and does so on a general Borel state space rather than a finite one. This mission covers the chapter's first three sections: the general infinite-horizon setup, the semicontinuous existence theory that makes it usable, and the sharper contraction-based theory that is the chapter's, and arguably the whole book's, theoretical center.

Setting

An infinite-horizon Markov Decision Model reuses the same data $(E,A,D,Q,r,\beta)$ as the finite-horizon models of earlier chapters, but drops the terminal reward and applies a single (possibly randomized) decision rule at every one of infinitely many stages. Its performance criterion, $J_\infty(x) := \sup_\pi \mathbb E^\pi_x\big[\sum_{k=0}^\infty \beta^kr(X_k,f_k(X_k)) \big]$, is only meaningful once an integrability condition (Assumption (A)) and a convergence condition (Assumption (C)) rule out the sum diverging or the finite-horizon approximations failing to settle down. Both conditions follow automatically once the model has an upper bounding function $b$ — a function controlling both the size of the reward and how fast the transition kernel can grow $b$ itself — with $\beta\alpha_b < 1$, the manageable special case that covers both the classical bounded-reward discounted case and the case of a non-positive reward.

Formalization targets

The goal, Theorem 7.3.5 (Structure Theorem), is the chapter's capstone: under a genuine bounding function (a two-sided reward bound making the space $IB_b$ of finite-weighted-norm functions a Banach space) with $\beta\alpha_b < 1$, and one abstract structural hypothesis — a closed class $IM \subset IB_b$ containing $0$, mapped into itself by the Bellman operator $T$, on which a maximizing action always exists — Banach's fixed point theorem delivers existence, uniqueness, an explicit geometric convergence rate for value iteration, and existence of an optimal stationary policy, all at once. The milestones build up to it in three stages: the general infinite-horizon machinery (Lemmas 7.1.4-7.1.5, Theorems 7.1.6-7.1.8 — reward iteration, a verification theorem, and a structure theorem under an abstract structure assumption that is not yet tied to any checkable property of the model); the semicontinuous existence theory that gives primitive, checkable conditions implying that abstract assumption (Theorem 7.2.1 and its two corollaries, including a genuine policy iteration conclusion); and the contracting theory proper (Lemma 7.3.3's contraction estimate, Theorem 7.3.4's sharpened verification theorem, and Theorem 7.3.6's continuous specialization of the goal).

Significance

The goal is the direct, general-Borel-space generalization of what finite-state dynamic programming theorems already on the platform (BertsekasDP.discounted_main_theorem, BertsekasDP.ssp_main_theorem) establish only for a finite state and action space, where Banach's theorem is applied directly on $\mathbb R^n$: this mission's content is that the same conclusions — including the same explicit geometric convergence rate for value iteration — hold on an arbitrary Borel state space, the moment one abstract, structural condition is checked. That condition is not vacuous or automatic: Example 7.2.4 (cited but not itself formalized, being an unnumbered worked counterexample rather than a numbered result) shows that without compactness of the feasible-action correspondence, the naive Structure Assumption of Chapter 2 is not enough and value iteration can converge to the wrong limit ($J \ne J_\infty$). Theorems 7.1.8's Structure Assumption (SA) is built precisely to rule this out, and Theorem 7.2.1's semicontinuity/ compactness conditions are the practical, checkable sufficient conditions for it.

Difficulty

The central formalization challenge is representing $J_\infty^\pi$, the genuine infinite-horizon expected discounted reward, without constructing a canonical infinite-horizon path measure from the model's transition kernel — a substantial undertaking the book itself sidesteps by proving (via an appendix result, Theorem B.1.1, not itself reproved here) that $J_\infty^\pi$ equals the limit of the finite-horizon truncations $J_n^\pi$. This mission takes that limit characterization as its own definition, via Filter.limsup for the same total, junk-safe reasons this book's series has used throughout (no canonical path measure anywhere in chunks 02a, 05a, 05b, 06). A second, genuinely new difficulty is Ls, the "upper limit of a sequence of sets" that drives every policy-iteration conclusion: it is a statement about accumulation points of a sequence of points, one drawn from each set in the sequence, not the more familiar set-theoretic limsup of a sequence of sets — getting this distinction right is the entire content of what "policy iteration" asserts.

Formalization scope

Every operator, bounding-function class, and value function of §7.1-7.3 is restated (not imported) in this chunk's own namespace from the finite-horizon originals of chunks 02a/02b, adapted to drop the time index and bake the discount into the one-stage operator directly, per this chapter's own presentation. The contracting theory's genuinely real-valued Banach-space objects ($T_f'$, $T'$, $IB_b$, the weighted norm $\|\cdot\|_b$) are kept separate from the general theory's EReal-valued objects ($T_f$, $T$, $IM(E)$), matching the book's own distinction between a value function that is a priori only known to avoid $+\infty$ and one known to be genuinely finite everywhere. Part (d) of the goal — the explicit geometric convergence rate — is stated in full, not weakened to bare qualitative convergence, since a formalization that dropped it would lose exactly the fact (used again by this book's own Theorem 7.5.12, a different chunk) that makes value iteration a genuine numerical method with a computable error bound rather than merely an existence argument.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. II, 4th ed., Athena Scientific, 2012 (the finite-state discounted/SSP theorems this goal generalizes).
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (analytic measurability of $J_\infty$, $J$; cited by the book for this chapter's foundational measure-theoretic facts).
• K. Hinderer, Foundations of Non-stationary Dynamic Programming with Discrete Time Parameter, Lecture Notes in Operations Research and Mathematical Systems 33, Springer, 1970 (Theorem 18.4, cited for the fact that history-dependent policies do not improve on Markov ones).

Motivation

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

Companion mission 05-lconvex-sets (Discrete Convex Analysis IV) covers this chapter's other half: the hole-free property (Theorem 5.2), the one-to-one correspondence between L-convex sets and integer-valued triangle-inequality distance functions (Theorem 5.5), the intersection properties (Theorem 5.7), and the chapter's discrete separation theorem (Theorem 5.9, its goal). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results the chapter leaves for its second half: the fundamental facts connecting a distance function to its admissible potentials (Proposition 5.1), the two-way polyhedral correspondence's supporting propositions (5.3-5.4), Minkowski-sum convexity (Theorem 5.8), and — this mission's goal — the explicit description of an L-convex set's convex hull that establishes its integral convexity (Theorem 5.10).

Setting

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

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

Formalization targets

Goal: integral convexity of L-convex sets

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

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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