Combinatorics

Motivation

A two-machine flow shop is the simplest multi-stage production system: every job visits machine 1 and then machine 2, each machine works on one job at a time, and the goal is to finish all jobs as early as possible. S. M. Johnson's 1954 paper (Naval Research Logistics Quarterly 1(1):61–68, doi:10.1002/nav.3800010110) answered this question, posed by R. Bellman, with an exact rule, now called Johnson's rule. It is one of the first exact results in machine scheduling. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) the problem is written $F2\,\|\,C_{\max}$. The rule is the standard polynomial case against which the NP-hardness of the three-machine flow shop (Garey, Johnson and Sethi 1976) is contrasted, and it is still used inside heuristics for larger shops.

Timeline:

• 1954. Johnson proves the two-machine rule and a three-machine special case (the latter is the second mission of this series).
• 1976. Garey, Johnson and Sethi prove that the three-machine flow shop is NP-hard in the strong sense, so the two-machine case marks the boundary of tractability.

Setting

There are $n$ items $i = 1, \dots, n$. Item $i$ needs $A_i > 0$ units of time on machine 1 and then $B_i > 0$ units on machine 2. Each time is setup time plus work time, and the times are otherwise arbitrary. A schedule assigns start times $s^1_i$ and $s^2_i$. It is feasible when all start times are nonnegative, the intervals $[s^1_i, s^1_i + A_i]$ of distinct items do not overlap on machine 1, the intervals $[s^2_i, s^2_i + B_i]$ do not overlap on machine 2, and $s^1_i + A_i \le s^2_i$ for every item. The total elapsed time $T(s) = \max_i (s^2_i + B_i)$ is the time at which the last item leaves machine 2.

An order is a permutation $\sigma$, where $\sigma(k)$ is the item in position $k$. The as-soon-as-possible schedule $a_\sigma$ of an order processes the items in the order $\sigma$ on both machines, with no delay on machine 1. Each item starts on machine 2 as soon as it has left machine 1 and machine 2 is free.

Relation (II). Item $i$ is definitely preferred to item $j$ when

$$\min(A_i, B_j) < \min(A_j, B_i),$$

and the two items are indifferent when equality holds. An order is consistent with all the definite preferences when no item is definitely preferred to an item placed earlier.

For an order $\sigma$ the paper uses the quantities

$$K_u = \sum_{l \le u} A_{\sigma(l)} - \sum_{l < u} B_{\sigma(l)}, \qquad F(\sigma) = \max_u K_u .$$

Formalization targets

Goal: Theorem 1 (p. 63)

For positive $A, B$:

$$\exists\, \sigma \text{ consistent with (II)}, \qquad\text{and}\qquad \forall\, \sigma \text{ consistent with (II)},\ \forall\, s \text{ feasible}:\quad a_\sigma \text{ is feasible and } T(a_\sigma) \le T(s).$$

The comparison is against every feasible schedule, including those whose two machines follow different orders.

Milestones

1. Lemma 1 (p. 61). Every feasible schedule can be replaced, at no greater total elapsed time, by a feasible schedule that follows one common order on both machines.
2. As soon as possible (p. 62). For a fixed common order, $a_\sigma$ is feasible and minimizes $T$ among the feasible schedules that follow $\sigma$.
3. Closed form (p. 62). $T(a_\sigma) = \sum_i B_i + F(\sigma)$, i.e. the total idle time of machine 2 is $\max_u K_u$.
4. Adjacent interchange (p. 63). Interchanging the items in positions $j, j+1$ leaves every other $K_u$ unchanged. Moreover, $\max(K_j, K_{j+1}) < \max(K'_j, K'_{j+1})$ holds if and only if (II) holds for the pair.
5. Interchanges do not increase $F$ (p. 63). If the pair in positions $j, j+1$ satisfies (II) non-strictly, then $F(\sigma) \le F(\sigma')$.
6. Lemma 2 (p. 64). Relation (II) is transitive, except when the middle item is indifferent to both others.
7. Worked example (p. 65). For $A = (4,4,30,6,2)$ and $B = (5,1,4,30,3)$, the order $(5,1,4,3,2)$ takes 47 units with 4 units of idle time. The reversed order takes 78 units, and every order takes between 47 and 78 units.

Significance

The theorem reduces an optimization over a continuum of start-time vectors, and over $n!$ orders, to sorting with respect to a pairwise relation. The paper's working rule computes an optimal order in $O(n \log n)$ time. The two-machine rule is the building block of Johnson's three-machine result, of the Campbell–Dudek–Smith heuristic for $m$ machines, and of lower bounds in branch-and-bound methods for flow shops. The closed form $T(a_\sigma) = \sum_i B_i + \max_u K_u$ reappears across flow-shop theory as a longest-path formula.

The result is classical and proved. This mission contributes a machine-checked proof in Lean 4 against Mathlib. As far as a search of the platform shows, no formal statement of the flow-shop model or of Johnson's rule exists there. The mission also fixes a reusable Lean model of a two-machine schedule: start times, feasibility, total elapsed time and the as-soon-as-possible schedule of an order.

Difficulty

The paper's argument leaves two steps informal, and a formal proof must supply both. First, Lemma 1 is justified by a picture and the phrase "successive interchanges". The page does not show that each interchange keeps the schedule feasible and does not delay the last completion on machine 2, and this is where most of the modelling work sits. Second, relation (II) is not a strict weak order when there are ties, so the obvious sorting argument fails. Consistency on adjacent pairs does not imply optimality: the items $(A, B) = (5,2), (1,1), (2,5)$, in that order, satisfy (II) non-strictly on both adjacent pairs, yet take 13 units against an optimum of 10. Lemma 2's exception is exactly this case.

Formalization scope

Items are Fin n (0-based) and times are real numbers. Positivity $A_i > 0$, $B_i > 0$ is a hypothesis of the goal and of Lemma 1, the as-soon-as-possible step and the closed form, as on p. 61. Lemma 2 and the interchange statements are pure min/sum algebra and carry no positivity. An order is σ : Equiv.Perm (Fin n) with σ k the item in position k. Interchanging positions $j, j+1$ is σ * Equiv.swap j (j+1). The total elapsed time is Finset.univ.fold max 0 of the machine-2 completion times, so it is $0$ when $n = 0$. $K_u$ is indexed by 0-based positions (Lean's $K_u$ is the paper's $K_{u+1}$), and $F$ requires $n \ge 1$.

Conventions made explicit or corrected:

• "Consistent with all the definite preferences" is imposed on all pairs of positions $k < l$ as the non-strict inequality $\min(A_{\sigma(k)}, B_{\sigma(l)}) \le \min(A_{\sigma(l)}, B_{\sigma(k)})$. The goal also asserts that such an order exists, so its main clause is not vacuous.
• The display of $K'_u$ on p. 63 prints the upper limit $u$ on the $B'$-sum. The definition of $K_u$ on p. 62 and the reduction of (I) to (II) require $u-1$, and the formalization uses $u-1$.
• Lemma 2 keeps the page's exception (item 2 indifferent to both items); without it the statement is false.

Measuring the objective by $F(\sigma)$, or comparing only against schedules that follow one common order, would drop Lemma 1 and change the theorem. The goal compares against every feasible start-time schedule. The working rule of p. 64 (a procedure) is not formalized.

Proofs of any milestone are welcome, as are further lemmas about the as-soon-as-possible schedule and a formalization of the working rule. The schedule definitions are the basis for the three-machine mission of this series.

Selected references

• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. doi:10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2):117–129, 1976. doi:10.1287/moor.1.2.117
• 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:287–326, 1979. doi:10.1016/S0167-5060(08)70356-X
• H. G. Campbell, R. A. Dudek, M. L. Smith, A heuristic algorithm for the n job, m machine sequencing problem, Management Science 16(10):B630–B637, 1970. doi:10.1287/mnsc.16.10.B630

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

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

Two optimization problems on weighted networks sit at the base of operations research and algorithm design. The first asks for the cheapest way to connect every node of a network, such as a cable, pipeline or communication network. The answer is a minimum weight spanning tree. The second asks for the shortest route from a depot to every other node of a road or data network, the single-source shortest path problem. Chapter 12 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org, CC BY-SA 4.0) treats both. It proves the structural lemmas behind the greedy spanning tree algorithms of Kruskal (1956) and Prim (1957), and the correctness of the shortest path algorithm of Dijkstra (1959).

The minimum spanning tree problem goes back to Borůvka (1926), who designed an electrical network for Moravia. Kruskal and Prim gave the two greedy algorithms taught today, and Dijkstra's 1959 note treated both problems. Dijkstra's shortest path method, with heap-based refinements such as Fredman and Tarjan (1987), remains the standard solver for non-negative lengths and a building block of routing, scheduling and network flow codes.

Setting

A graph $G = (V, E)$ has a finite vertex set $V$ and a set $E$ of 2-element subsets of $V$. A weight $w(e) \in \mathbb N_0$ is attached to each edge, and a set $S$ of edges has weight $w(S) = \sum_{e \in S} w(e)$. A spanning forest of $G$ is an acyclic graph $H = (V, S)$ with $S \subseteq E$. A spanning tree is a spanning forest that is connected. The weight of a spanning tree is the weight of its edge set. In Lean these are SimpleGraph V with [Fintype V], IsSpanningForest G H ($H \le G$ and acyclic), IsSpanningTree G T ($T \le G$ and a tree), and weight w T for a weight w : Sym2 V → ℕ.

A digraph $G = (V, E)$ has $E \subseteq V \times V$ with $x \ne y$ for every directed edge $(x, y)$. Each directed edge has a length $w(x, y) \in \mathbb N_0$. The length is extended by $w(x, y) = \infty$ for non-edges. A directed path from $a$ to $b$ is a sequence $(a = u_0, \dots, u_t = b)$ of distinct vertices in which consecutive pairs are directed edges. Its length is $\sum_{i<t} w(u_i, u_{i+1})$. The distance $\operatorname{dist}(a, b) \in \mathbb N_0 \cup \{\infty\}$ is the minimum length of a directed path from $a$ to $b$, and is $\infty$ when no such path exists. A shortest path is a directed path attaining it. In Lean this is WeightedDigraph V with ext, IsDirPath, pathLength, dist and IsShortestPath.

Dijkstra's algorithm (Algorithm 12.14) with root $r$ and $n = |V|$ keeps a sequence $\sigma$ of permanent vertices, a value $\delta(x) \in \mathbb N_0 \cup \{\infty\}$ and a sequence $P(x)$ for each vertex. Step 1 sets $\delta(r) = 0$, $P(r) = (r)$, $\sigma = (r)$, and $\delta(x) = w(r, x)$, $P(x) = (r, x)$ for $x \ne r$. Step $i$ with $1 < i < n$ scans from the last permanent vertex $v_i$. For every temporary $x$ it sets $\delta(x) \leftarrow \min\{\delta(x), \delta(v_i) + w(v_i, x)\}$, and on a strict decrease it replaces $P(x)$ by $P(v_i)$ followed by $x$. Each step ends by appending to $\sigma$ a temporary vertex of minimum $\delta$, chosen arbitrarily among ties. The algorithm halts at Step $n$. DijkstraRun G r i s holds when some sequence of admissible choices leads to state s at the start of Step $i$.

Formalization targets

Goal: correctness of Dijkstra's algorithm (Theorem 12.18)

For every halted state of every run, and every vertex $x$,

$$\delta(x) = \operatorname{dist}(r, x), \qquad \operatorname{dist}(r, x) < \infty \implies P(x) \text{ is a shortest path from } r \text{ to } x.$$

Milestones

1. Proposition 12.3. A spanning forest $H = (V, S)$ of a graph on $n \ge 1$ vertices has $|S| \le n - 1$ and exactly $n - |S|$ components. It is a spanning tree if and only if $|S| = n - 1$.
2. Proposition 12.4 (Exchange Principle). Let $T$ be a spanning tree and $xy \in E \setminus T$. Then $T$ contains a unique path $x = x_0, \dots, x_t = y$, and replacing any edge $x_i x_{i+1}$ of it by $xy$ gives a spanning tree.
3. Lemma 12.6. In a connected weighted graph, let $F$ be a spanning forest and $C$ a component of $F$. A minimum weight edge leaving $C$ lies in some spanning tree that has minimum weight among the spanning trees containing $F$.
4. Proposition 12.16. Every prefix and every suffix of a shortest path is a shortest path.
5. Proposition 12.17. When the algorithm halts, $\delta(v_1) \le \delta(v_2) \le \cdots \le \delta(v_n)$.

Milestones 4 and 5 are the two statements the book's proof of the goal rests on. Milestones 1–3 are the spanning tree half of the chapter. Lemma 12.6 is the result from which the book derives the correctness of Kruskal's and Prim's algorithms.

Significance

Theorem 12.18 certifies that one pass of $n$ steps computes all distances from $r$ and a shortest path tree, with no condition on the digraph beyond non-negative lengths. Lemma 12.6 is the cut property. Every greedy minimum spanning tree method (Kruskal, Prim, Borůvka) is an instance of it, and the exchange principle is the matroid basis-exchange axiom specialised to the graphic matroid.

All of these results are classical and proved. None is formalized in this form on the platform. Mathlib has spanning trees of connected graphs, uniqueness of paths in acyclic graphs, and the edge count $n - 1$ of a tree. It has no edge–component count for forests, no exchange principle, no weighted spanning trees, and no Dijkstra. On Prove2Me, FamousTheorems.tree_card_edges_6b and ClassicalGaps.isAcyclic_edges_eq_card_sub_one_imp_connected cover only the tree case of Proposition 12.3. KServer.mst_cut_property is a cut property for complete graphs encoded by parent maps, a different statement. The label-correcting algorithm of Dynamic Programming and Optimal Control II (BertsekasDP.label_correcting_*) is a different algorithm: it keeps an open list and scans in arbitrary order, not by minimum label.

Difficulty

The goal is a statement about the final state of a run, but the facts it depends on only become visible across steps: a permanent vertex's $\delta$ and $P$ never change again, and $\delta(x)$ is always the length of the current $P(x)$. None of this is recorded in the final state itself. An argument over the steps of the run has to show that each $P(x)$ remains a path with distinct vertices, including when edges of length $0$ allow ties. It also has to handle the value $\infty$, where $\infty + a = \infty$ and a comparison between two infinite values never counts as a decrease. Tie-breaking is arbitrary, so no argument may depend on which minimum is chosen. For Lemma 12.6 the difficulty is the exchange step: removing an edge of a tree path and adding a crossing edge must again give a tree that still contains the forest $F$, and this is a statement about cycles and components, not about counts.

Formalization scope

• Graphs are SimpleGraph V over a Fintype V. Weights are Sym2 V → ℕ (the book's $w : E \to \mathbb N_0$; values off $E$ are never used). Acyclic, tree and connected components are Mathlib's. In Proposition 12.3, $|S| = n - k$ is written $|S| + k = n$ and $n \ge 1$ is assumed, which the bound $n - 1$ presupposes.
• Lemma 12.6 assumes $G$ connected, the section's standing assumption (p. 239). The page's "to avoid trivialities, we assume $n \ge 3$" is not imposed, because the statement holds for every $n$. The crossing edge may have either endpoint in $C$.
• Lengths in the digraph are ℕ, and $\delta$ and distances are ℕ∞, where $\infty$ is ⊤, never a large finite number. A version with real or ℝ≥0 lengths would be a generalization and is not what is asked.
• Dijkstra's algorithm is defined step by step exactly as on pp. 246–247, including $\delta(x) = w(r, x) = \infty$ and $P(x) = (r, x)$ for non-neighbours at Step 1. The goal quantifies over every halted state, so it holds for every tie-breaking. A halted state always exists; a sorry-free check of this is in the workspace. For a vertex not reachable from $r$ the book is silent. The distance there is read as $\infty$, and the shortest-path conclusion is asserted only at finite distance.
• A trivializing formalization is ruled out: $\delta$ is computed by the update rule of Algorithm 12.14, not defined as the distance, and the theorem is not stated for an arbitrary procedure satisfying its own conclusion.
• The book uses no $O(\cdot)$ bounds or approximate constants in these statements, so there are no constants to instantiate.
• Reusable infrastructure: a list-based theory of directed paths and distances in ℕ∞, the invariants of Dijkstra's algorithm, and forest edge counting. Contributions of general lemmas (walks shortcut to paths without increasing length, component counts under edge insertion) are welcome.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 12. https://www.appliedcombinatorics.org/
• E. W. Dijkstra, "A note on two problems in connexion with graphs", Numerische Mathematik 1 (1959) 269–271. https://doi.org/10.1007/BF01386390
• J. B. Kruskal, "On the shortest spanning subtree of a graph and the traveling salesman problem", Proc. AMS 7 (1956) 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7
• R. C. Prim, "Shortest connection networks and some generalizations", Bell System Technical Journal 36 (1957) 1389–1401. https://doi.org/10.1002/j.1538-7305.1957.tb01515.x
• M. L. Fredman and R. E. Tarjan, "Fibonacci heaps and their uses in improved network optimization algorithms", J. ACM 34 (1987) 596–615. https://doi.org/10.1145/28869.28874
• O. Borůvka, "O jistém problému minimálním", Práce Moravské přírodovědecké společnosti 3 (1926) 37–58. https://dml.cz/handle/10338.dmlcz/500114

Motivation

Counting the objects that avoid every one of a list of conditions is one of the most frequent tasks in enumerative combinatorics: functions that miss no value, permutations that fix no point, integers that share no prime factor with a given number. The Principle of Inclusion-Exclusion converts such a count into an alternating sum of counts of objects that do satisfy prescribed conditions, which are usually far easier to compute. Chapter 7 of Keller and Trotter's Applied Combinatorics (2017 Edition) develops the principle in the abstract language of properties and applies it to three classical questions: the number of surjections, the number of derangements, and Euler's totient function.

This mission formalizes the first two applications, with the chapter's headline result, the closed formula for the number of surjections from an $n$-element set onto an $m$-element set, as its goal. The surjection count answers distribution questions of the form "in how many ways can $n$ distinct objects be handed to $m$ distinct recipients so that every recipient receives at least one", which the book illustrates with fifteen lottery tickets shared among four grandchildren ($S(15,4) = 1016542800$).

Setting

Let $X$ be a finite set and let $\mathcal P = \{P_1, \dots, P_m\}$ be a family of properties: for each $x \in X$ and each $i$, either $x$ satisfies $P_i$ or it does not. For a subset $S \subseteq [m] = \{1, \dots, m\}$ write

$$N(S) = \bigl|\{x \in X : x \text{ satisfies } P_i \text{ for every } i \in S\}\bigr|,$$

so that $N(\emptyset) = |X|$.

Two families of properties are used.

• Functions. $X$ is the set of all functions $f : [n] \to [m]$, and $f$ satisfies $P_i$ when $i$ is not in the range of $f$, i.e. $f(j) \ne i$ for every $j \in [n]$. The functions satisfying none of the properties are the surjections, and their number is written $S(n, m)$.
• Permutations. $X$ is the set of all permutations $\sigma$ of $[n]$, and $\sigma$ satisfies $P_i$ when $\sigma(i) = i$. The permutations satisfying none of the properties are the derangements, and their number is written $d_n$.

In Lean, $X$ is a type with [Fintype X], the properties are a decidable predicate family P : Fin m → X → Prop, and $N(S)$ is AppliedComb.InclExcl.N P S. The two families are AppliedComb.InclExcl.NotInRange n m on Fin n → Fin m and AppliedComb.InclExcl.FixesPoint n on Equiv.Perm (Fin n).

Formalization targets

Goal: Theorem 7.9 (number of surjections)

For all $n, m \ge 0$,

$$S(n, m) = \bigl|\{f : [n] \to [m] \text{ surjective}\}\bigr| = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (m-k)^n .$$

Milestones

1. Theorem 7.7 (Principle of Inclusion-Exclusion). For every finite $X$ and every family of $m$ properties,

$$\bigl|\{x \in X : x \text{ satisfies no } P_i\}\bigr| = \sum_{S \subseteq [m]} (-1)^{|S|} N(S).$$

2. Lemma 7.8. For the function properties, $N(S)$ depends only on $|S|$, and $N(S) = (m-k)^n$ when $|S| = k$.
3. Lemma 7.10. For the permutation properties, $N(S)$ depends only on $|S|$, and $N(S) = (n-k)!$ when $|S| = k$.
4. Theorem 7.11 (number of derangements). For all $n \ge 0$,

$$d_n = \sum_{k=0}^{n} (-1)^k \binom{n}{k} (n-k)! .$$

Milestones 1 and 2 are the two ingredients the book names for the goal; milestones 3 and 4 are the parallel derangement application, which shares the definition of $N(S)$ and milestone 1.

Significance

The result itself. The surjection formula is the standard closed form for $m!\,S_2(n,m)$, where $S_2$ is the Stirling number of the second kind; it gives $S(n, m) = 0$ for $n < m$ and $S(n, n) = n!$ as special cases, and it underlies counts of ordered set partitions, of onto colourings, and of occupancy problems in which every cell is filled. The derangement formula is the standard answer to the hat-check problem and leads directly to the limit $d_n/n! \to 1/e$ (Theorem 7.12 of the book). The Principle of Inclusion-Exclusion in the book's "none of the properties" form is the common tool behind both and behind Möbius inversion in general.

Formalizing it. All results are classical and fully proved in the book. Mathlib contains inclusion-exclusion for unions and intersections of finsets (Finset.inclusion_exclusion_card_biUnion, Finset.inclusion_exclusion_card_inf_compl), the derangement count via its own recurrence (numDerangements, card_derangements_eq_numDerangements, numDerangements_sum), and Stirling numbers of the second kind (Nat.stirlingSecond) with their recurrence, but no closed formula for the number of surjections. The platform has union-form inclusion-exclusion (FamousTheorems.inclusion_exclusion_card_biUnion) and the $1/e$ limit, neither in the property form used here. This mission produces the property-indexed statement of the principle, the two $N(S)$ computations, and the surjection count as a cardinality of surjective functions, in a form that downstream missions of the series (generating functions, Pólya counting) can cite.

Difficulty

The proofs are short on paper, and the work lies in the bookkeeping that the page leaves implicit. Two points stand out. First, the Principle of Inclusion-Exclusion is phrased with properties and $N(S)$ rather than with a union of sets; connecting the two forms, or proving the property form directly, requires handling sums over the power set of $[m]$ together with the sign $(-1)^{|S|}$ in $\mathbb Z$. Second, the step "the result follows immediately, as there are $\binom{m}{k}$ $k$-element subsets of $[m]$" requires regrouping a sum over all subsets $S \subseteq [m]$ by cardinality, which needs Lemma 7.8's statement that $N(S)$ depends only on $|S|$ and a count of the subsets of each size. The book's one-line arguments for Lemmas 7.8 and 7.10 ("a string of length $n$ from an alphabet of $m-k$ letters", "a permutation among the remaining $n-k$ positions") are counting identifications that have to be made precise for subtypes of Fin n → Fin m and of Equiv.Perm (Fin n).

Formalization scope

• The book's $[n] = \{1, \dots, n\}$ is represented by Fin n $= \{0, \dots, n-1\}$; this is an index shift only.
• $S(n, m)$ is Fintype.card {f : Fin n → Fin m // Function.Surjective f} and $d_n$ is Fintype.card {σ : Equiv.Perm (Fin n) // ∀ i, σ i ≠ i}. Defining $S(n, m)$ by the formula, or $d_n$ by the sum, would make the goal hold by rfl; the counts are therefore cardinalities of the sets the book describes. $S(n,m)$ is also not stated through Nat.stirlingSecond, which counts unordered partitions and differs by a factor $m!$.
• All alternating sums are identities in $\mathbb Z$; the natural-number counts are cast. The differences $m - k$ and $n - k$ are computed in $\mathbb N$ where $k$ ranges over $0, \dots, m$ (resp. $0, \dots, n$) or equals $|S|$, so they are exact.
• The book introduces $S(n,m)$ for positive $n, m$ and states Theorem 7.11 for positive $n$. The formal statements are made for all $n, m \ge 0$, where they remain true with Lean's convention $0^0 = 1$ ($S(0,0) = 1$, $S(0,m) = 0$ for $m \ge 1$, $d_0 = 1$). No explicit constants arise: the chapter contains no $O(\cdot)$ or approximate statements among the formalized results.
• The Principle of Inclusion-Exclusion is stated for an arbitrary finite type and an arbitrary decidable family of $m \ge 0$ properties; for $m = 0$ both sides equal $|X|$.

A complete development needs only Mathlib's finite-set, power-set and binomial-coefficient API. The property-form inclusion-exclusion (Theorem 7.7) and the two $N(S)$ lemmas are reusable for other sieve-type counts, for example Euler's totient function (Theorem 7.14 of the book), which is not part of this mission. Proofs of any milestone independently of the others are welcome, as are alternative proofs of the goal (for instance via exponential generating functions) that do not pass through Theorem 7.7.

Selected references

• Mitchel T. Keller and William T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 7 (Theorems 7.7, 7.9, 7.11; Lemmas 7.8, 7.10), CC BY-SA 4.0. https://www.appliedcombinatorics.org/
• Richard P. Stanley, Enumerative Combinatorics, Volume 1, 2nd ed., Cambridge University Press, 2011, Chapter 2 (sieve methods). https://doi.org/10.1017/CBO9781139058520
• The Mathlib Community, The Lean Mathematical Library, CPP 2020. https://doi.org/10.1145/3372885.3373824

Motivation

Insertion heuristics build a traveling salesman tour one city at a time: start from a single city, and at each step choose a city not yet on the subtour and splice it into the subtour where it lengthens the subtour least. Local search heuristics start from a tour and repeatedly replace a few of its edges by others while this shortens the tour. Both families are standard in practice, and a natural engineering idea is to combine them: run an insertion heuristic, then polish the result by local search. The question this mission formalizes is whether local optimality of the insertion tour certifies anything about its quality.

Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) answered this for graphs satisfying the triangle inequality. Their §4 proves that nearest and cheapest insertion always return a tour of length at most $2(1-1/n)$ times the optimal length, and their Theorem 5 shows this bound is attained. Their §7 then shows that the very tour attaining the bound is $k$-optimal for every $k\le n/4$: no exchange of $k$ edges shortens it. So the insertion bound is tight even for tours that local search with $k$-changes cannot improve.

Timeline, as far as this mission is concerned:

• 1965: Lin (Bell System Tech. J. 44) defines $k$-optimal tours and uses 3-optimal local search.
• 1973: Lin and Kernighan (Oper. Res. 21) generalize the edge-exchange neighbourhoods.
• 1977: Rosenkrantz, Stearns and Lewis prove the $2(1-1/n)$ upper bound for nearest and cheapest insertion (Theorem 4 and its corollary), its tightness for $n\ge 6$ (Theorem 5), the existence of $k$-optimal tours with the same ratio (Theorem 6, stated for $n\ge 8$), and the Corollary combining the two.

Setting

A traveling salesman graph on $n$ nodes is the node set $N=\{1,\dots,n\}$ with a distance $d(i,j)\ge 0$ that is symmetric and satisfies the triangle inequality $d(i,k)\le d(i,j)+d(j,k)$. A tour is a Hamiltonian circuit; its length is the sum of its edge lengths; OPTIMAL is the least length of a tour. As in the paper, the identically zero distance is excluded, so OPTIMAL $>0$.

A subtour is a circuit on a subset of the nodes (a single node is a subtour without edges). For a subtour $T$ and a node $k\notin T$, TOUR$(T,k)$ is obtained by deleting an edge $(x,y)$ of $T$ minimizing $d(x,k)+d(k,y)-d(x,y)$ and adding $(x,k)$ and $(k,y)$; COST$(T,k)$ is the resulting increase in length. An insertion method chooses nodes $a_0,a_1,\dots,a_{n-1}$, starts from $T_1=\{a_0\}$ and sets $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$; INSERT is the length of $T_n$. Nearest insertion chooses $a_i$ minimizing $d(T_i,x)=\min_{y\in T_i}d(y,x)$ over $x\notin T_i$; cheapest insertion chooses $a_i$ minimizing COST$(T_i,x)$. Ties are broken arbitrarily.

A $k$-change of a tour deletes $k$ of its edges and adds $k$ other edges so that another tour is obtained. A tour is $k$-optimal if no $k$-change produces a strictly shorter tour.

The extremal instance is the circle $(N_n,d_n)$: $n$ cities equally spaced on a circular road, with $d_n(i,j)$ the smallest $m\ge 0$ with $i-j\equiv m$ or $j-i\equiv m \pmod n$. The insertion run of Theorem 5 inserts the cities in the order $1,2,\dots,n$ and produces the zig-zag tour $T_n$: city 1, then the even cities in increasing order, then the odd cities in decreasing order.

Formalization targets

Goal: the Corollary to Theorem 6

For $n\ge 6$ and $4k\le n$ there is a traveling salesman graph with OPTIMAL $>0$ on which some run of nearest insertion, and some run of cheapest insertion, return a $k$-optimal tour with

$$\frac{\mathrm{INSERT}}{\mathrm{OPTIMAL}}=2\left(1-\frac1n\right).$$

Milestones

1. The insertion run on the circle: the subtours $T_i$ and nodes $a_i=i+1$ form an insertion run that obeys both the nearest and the cheapest rule (proof of Theorem 5).
2. On the circle, $T_n$ has length $2(n-1)$ and OPTIMAL $=n$ (proof of Theorem 5).
3. Theorem 5: for $n\ge 6$ there is a graph with INSERT/OPTIMAL $=2(1-1/n)$ for both methods.
4. Equation (7.4): the length of a tour of the circle is the sum over unit edges $e$ of COUNT$(e,T)$, the number of times $e$ is traversed when each tour edge is replaced by a shortest arc.
5. Every tour of the circle is odd or even (all counts of one parity), eq. (7.5).
6. $T_n$ is the shortest even tour, so every tour shorter than $T_n$ is odd.
7. $T_n$ is $k$-optimal for every $k\le n/4$.
8. Theorem 6: for $n\ge 8$ there is a graph with a tour that is $k$-optimal for all $k\le n/4$ and has LOCALOPT/OPTIMAL $=2(1-1/n)$.

Significance

The result. The Corollary shows that the $2(1-1/n)$ worst-case guarantee of nearest and cheapest insertion cannot be improved by requiring that the returned tour survive $k$-change local search, for $k$ up to a quarter of the number of cities. Theorem 6 says more generally that $k$-optimality with $k\le n/4$ does not bound the ratio to the optimum below $2(1-1/n)$. Together with the paper's upper bound, the insertion guarantee is exact, and it stays exact after local polishing with small neighbourhoods.

Formalizing it. All statements are proved in the paper; none, to our knowledge, has been machine-checked. The platform has an upper bound for nearest insertion (SupplyChainTheory, Theorem 10.7, ratio at most 2) but no tightness example and no notion of $k$-optimality. This mission produces a reusable definition of $k$-changes against arbitrary tours, the circle metric, and the parity-counting argument on a cycle, and it supplies the calculations the paper omits ("We omit these calculations but note that they require the assumption $n\ge 6$").

Difficulty

Two steps carry the weight. First, the omitted calculations for the insertion run: at each stage one must show that inserting $a_i$ between $i-1$ and $i$ minimizes the insertion increase over every edge of the zig-zag subtour, and that no other outside city can be inserted for less than 2; the claim fails for $n=4$ and $n=5$, so the verification must use $n\ge 6$ in an essential way. Second, $k$-optimality is a statement about every tour at edge difference $k$, not about 2-opt segment reversals or any specific move family. A search over moves of a special form does not establish it; the argument must bound the length of an arbitrary tour at edge difference $k$ from below.

Formalization scope

Nodes are Fin n, so the paper's node $m$ is index $m-1$ and $a_i=i+1$ is index $i$; subtour indices stay 1-based ($T_1=[a_0]$, approximation $T_n$). A distance is d : Fin n → Fin n → ℝ with the structure IsTSPDist (symmetric, nonnegative, triangle inequality, and $d(i,i)=0$; the last is a normalization absent from the paper that changes no length). A tour is an Equiv.Perm (Fin n), a subtour a list read cyclically; OPTIMAL is Finset.univ.inf' over permutations, the true minimum. TOUR$(T,k)$ is insertion at a position minimizing the new length; COST is a minimum over positions; the nearest-insertion distance (4.1) takes values in WithTop ℝ, so no junk value arises. $k$-optimality compares the tour with every permutation whose edge set (unordered pairs) misses exactly $k$ of the tour's edges. Ratios are multiplied out.

COUNT$(e,T)$ needs a choice of shortest arc for antipodal pairs when $n$ is even; the formalization takes the arc through $\min(x,y),\dots,\max(x,y)$. The paper's argument does not depend on this choice.

Deviations from the printed text: the Corollary is stated for $n\ge 6$ (the printed statement says only $4k\le n$, but its proof uses the example of Theorem 5, which exists for $n\ge 6$; for $k=0$, $n=3$ the printed statement is false). Theorem 6 keeps its printed $n\ge 8$. In the proof of Theorem 5 the paper writes "(4.2) holds" where the cheapest-insertion condition (4.3) is meant; the formal statement uses (4.3).

The existence statements carry OPTIMAL $>0$, the paper's standing assumption (1.1). Without it, the zero distance would make every length zero and every tour $k$-optimal, which would satisfy the ratio equations trivially; that formalization is ruled out.

Contributions welcome: proofs of any milestone, in particular the omitted insertion calculations and the parity lemma, and reusable lemmas on cyclic lists and edge sets of permutations.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM J. Comput. 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• S. Lin, Computer solutions of the traveling salesman problem, Bell System Tech. J. 44:2245–2269, 1965. https://doi.org/10.1002/j.1538-7305.1965.tb04146.x
• S. Lin, B. W. Kernighan, An effective heuristic algorithm for the traveling-salesman problem, Oper. Res. 21(2):498–516, 1973. https://doi.org/10.1287/opre.21.2.498

Motivation

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

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

Setting

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

Formalization targets

Goal: the directional-derivative/subdifferential correspondence

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

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

MAXIMUM SATISFIABILITY asks for a truth assignment satisfying as many clauses of a given set as possible. It was among the first NP-hard optimization problems for which an approximation algorithm came with a proven worst-case guarantee. In Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 1974, doi:10.1016/S0022-0000(74)80044-9), David S. Johnson set up a framework for measuring such guarantees and analyzed two heuristics for the problem. The second of these, algorithm B2, weights each clause by $2^{-|C|}$ and repeatedly sets a literal so that the heavier side is satisfied. On inputs whose clauses all have at least $k$ literals, it satisfies at least a $1 - 2^{-k}$ fraction of the optimum.

B2 is the ancestor of a line of work on MAX-SAT approximation:

• 1974. Johnson proves the $2^k/(2^k-1)$ bound for B2 on MS(k) and the $(k+1)/k$ bound for the unweighted greedy algorithm B1.
• 1994. Goemans and Williamson (SIAM J. Discrete Math. 7) present Johnson's algorithm as the derandomization, by conditional expectations, of the uniformly random assignment, and combine it with LP rounding to obtain a $3/4$-approximation.
• 1999. Chen, Friesen and Zheng (JCSS 58) show that B2 is a $2/3$-approximation on general inputs, sharper than the $1/2$ that Johnson's bound gives at $k = 1$.

Setting

A literal is a variable $x_i$ or its negation $\bar x_i$. A clause is a finite set of literals. A truth assignment is a set $T$ of literals containing no pair $\{x_i, \bar x_i\}$; it satisfies a clause $C$ when $C \cap T \ne \emptyset$. An input is a finite set $S$ of clauses, and $S^*$ is the largest $|S'|$ over subsets $S' \subseteq S$ satisfied by one truth assignment. MS(k) is the restriction to inputs in which every clause contains at least $k$ distinct literals.

Algorithm B2 keeps a set SUB of satisfied clauses, a set LEFT of unsettled clauses, the literals LIT still available, and a weight $w(C)$ per clause, starting from $w(C) = 2^{-|C|}$, $\mathrm{SUB} = \emptyset$, $\mathrm{LEFT} = S$. While some literal of LIT occurs in a clause of LEFT, it picks any such literal $y$. Let YT be the clauses of LEFT containing $y$ and YF those containing $\bar y$. If $\sum_{\mathrm{YT}} w \ge \sum_{\mathrm{YF}} w$, it makes $y$ true, moves YT to SUB and doubles the weight of each clause of YF; otherwise it does the symmetric move with $\bar y$. Finally it removes $y, \bar y$ from LIT. When no literal of LIT remains in LEFT it returns SUB.

The choice of $y$ is free, so several outputs may be choosable on one input. Johnson measures the algorithm by its worst choosable output, through the ratio $r(B2, S) = S^*/|\mathrm{SUB}|$ and its maximum $R[B2, \mathrm{MS}(k)](n)$ over inputs of size at most $n$.

Formalization targets

Goal: Theorem 3, with the equality range corrected

For every $k \ge 1$, every $S$ in MS(k) and every SUB choosable by B2 on $S$,

$$(2^k - 1)\,S^* \le 2^k\,|\mathrm{SUB}|,$$

and for every $k \ge 2$ there are $S$ in MS(k) and a choosable SUB with $|\mathrm{SUB}| > 0$ and

$$(2^k - 1)\,S^* = 2^k\,|\mathrm{SUB}|.$$

The paper states equality "for all sufficiently large $n$" for every $k \ge 1$. At $k = 1$ this is false: the ratio 2 would require every clause to be a unit clause and all clauses to be jointly satisfiable, and on such inputs B2 satisfies everything. The goal therefore asserts tightness for $k \ge 2$. A separate item states that at $k = 1$ the ratio is never attained.

Milestones

1. Initially, the total weight of LEFT is at most $|S|/2^k$.
2. No iteration increases the total weight of LEFT, so at halting it is still at most $|S|/2^k$.
3. At halting, every clause left in LEFT has weight exactly $1$.
4. At halting, $|\mathrm{LEFT}| \le |S|/2^k$ and $|\mathrm{SUB}| \ge |S|(1 - 2^{-k})$.
5. The eight-clause instance for $k = 3$ has $S^* = 8$ and admits a choosable output of size $7$.

Significance

The bound $1 - 2^{-k}$ is exactly the expected fraction of clauses a uniformly random assignment satisfies on MS(k). B2 attains it deterministically, and the proof bounds $|\mathrm{SUB}|$ against $|S|$ rather than against $S^*$, a feature the paper points out. For $k = 3$ the constant $8/7$ was later shown by Håstad (2001) to be optimal among polynomial-time algorithms unless P = NP, so the guarantee of this 1974 algorithm is best possible for MAX-E3-SAT.

Formalizing the result produces a machine-checked potential-function argument for a nondeterministic algorithm: the invariant links each clause's weight to how many of its literals have been removed. The mission also records a correction to the printed statement at $k = 1$. The paper's proof is complete; to our knowledge no machine-checked version exists.

Difficulty

The obvious argument follows the counting proof for algorithm B1 and compares clauses saved with clauses wounded in each step. It fails here: B2 can wound more clauses than it saves in a step, and the bound holds only in the weighted sense. The weight of a clause is not a static quantity. It is $2^{-|C|}$ times $2$ to the number of its literals already discarded, and this invariant must be carried through every step, including clauses that contain both $y$ and $\bar y$. Tightness needs an explicit input and an explicit adversarial run that exploits the tie in Step 4, and then a proof that every assignment of the remaining variables kills exactly one clause.

Formalization scope

• Literals and clauses. A literal is a pair (variable index in $\mathbb N$, sign). Clauses are Finsets of literals, and an input is a Finset of clauses, so there are no duplicate clauses. Truth assignments are partial and consistent. $S^*$ is a maximum over the finite, nonempty family of satisfiable subsets.
• B2 as a relation. B2 is a nondeterministic run relation, and "choosable" means reachable by finitely many steps from the initial state and halting. Step 3 allows a literal of either sign. The tie in Step 4 goes to $y$, and the comparison and doublings use the weights before the update. Weights are rationals.
• Size-free ratios. The size-dependent $R[B2, \mathrm{MS}(k)](n)$ is replaced by statements about every input (upper bound) and one attaining input (tightness). The two forms are equivalent because $R$ is a maximum over finitely many inputs and nondecreasing in $n$.
• No division. All ratios are multiplied out, so no division by zero can make a bound vacuous.
• Trivializations ruled out. A deterministic tie-break in Step 3 or 4, or tightness at a single fixed $k$, would be a weaker theorem and is not acceptable. So is stating only the upper bound.

The definitions (the MS layer, the run relation) can be reused by other MAX-SAT approximation results, and an identical MS layer appears in the companion mission on algorithm B1. Contributions welcome: proofs of the milestones, of the $k \ge 2$ tightness family, and of the $k = 1$ correction.

Selected references

• D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9 (1974) 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• J. Chen, D. K. Friesen, H. Zheng, Tight bound on Johnson's algorithm for maximum satisfiability, J. Comput. System Sci. 58 (1999) 622–640. https://doi.org/10.1006/jcss.1998.1610
• M. X. Goemans, D. P. Williamson, New 3/4-approximation algorithms for the maximum satisfiability problem, SIAM J. Discrete Math. 7 (1994) 656–666. https://doi.org/10.1137/S0895480192243516
• J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001) 798–859. https://doi.org/10.1145/502090.502098

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.