Operations Research

Motivation

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

Setting

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

Formalization targets

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

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

Setting

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

Formalization targets

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Setting

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

Formalization targets

Goal: The potential criterion for MCFP3 (Theorem 9.4)

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions ("arms") sequentially and must name the arm with the largest mean, with error probability at most a prescribed $\delta$, using as few samples as possible. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) showed that every $\delta$-PAC strategy needs, in expectation, at least $T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta,1-\delta)$ samples, where the characteristic time $T^*(\boldsymbol\mu)$ is the value of a max–min optimization problem over the proportions of draws allocated to the arms. The maximizer of that problem, $w^*(\boldsymbol\mu)$, is the allocation any asymptotically optimal strategy must follow; the Track-and-Stop algorithm of the same paper computes $w^*(\hat{\boldsymbol\mu})$ at plug-in estimates and tracks it.

A strategy can only track $w^*$ if $w^*$ can be computed. This mission formalizes the part of the paper (Section 2.2 and Appendix A) that turns the abstract max–min problem into an explicit recipe: a closed form for the inner infimum, and a characterization of $w^*$ through the root of one increasing scalar function. The problem had been solved in closed form before only for special cases, such as Poisson rewards with all suboptimal arms equal (Vaidhyan and Sundaresan, 2015); the paper's result covers every one-parameter exponential family.

Setting

A canonical one-parameter exponential family is a family of laws $\nu_\theta$, $\theta\in\Theta$, on $\mathbb R$ with density $\exp(\theta x-b(\theta))$ with respect to a reference measure $\xi$. The law $\nu_\theta$ has mean $\dot b(\theta)$; the set of attainable means is the mean space $\dot b(\Theta)$. For means $\mu=\dot b(\theta)$ and $\mu'=\dot b(\theta')$ the Kullback–Leibler divergence is

$$d(\mu,\mu')=\mathrm{KL}(\nu_\theta,\nu_{\theta'})=b(\theta')-b(\theta)-\dot b(\theta)(\theta'-\theta).$$

Bernoulli laws and Gaussian laws with known variance are the standard examples.

A bandit model is identified with its vector of means $\boldsymbol\mu=(\mu_1,\dots,\mu_K)\in\dot b(\Theta)^K$. $\mathcal S$ is the set of models with a unique optimal arm $a^*(\boldsymbol\mu)$, and $\mathrm{Alt}(\boldsymbol\mu)=\{\boldsymbol\lambda\in\mathcal S:a^*(\boldsymbol\lambda)\ne a^*(\boldsymbol\mu)\}$ is the set of alternatives. $\Sigma_K$ is the probability simplex. The transportation cost of proportions $w\in\Sigma_K$ and the objects of the paper are

$$c_{\boldsymbol\mu}(w)=\inf_{\boldsymbol\lambda\in\mathrm{Alt}(\boldsymbol\mu)}\sum_{a=1}^Kw_a\,d(\mu_a,\lambda_a),\qquad T^*(\boldsymbol\mu)^{-1}=\sup_{w\in\Sigma_K}c_{\boldsymbol\mu}(w),\qquad w^*(\boldsymbol\mu)=\operatorname*{argmax}_{w\in\Sigma_K}c_{\boldsymbol\mu}(w).$$

The arms are sorted so that $\mu_1>\mu_2\ge\dots\ge\mu_K$. The parameterized Jensen–Shannon divergence is, for $\alpha\in[0,1]$,

$$I_\alpha(\mu_1,\mu_2)=\alpha\,d\big(\mu_1,\alpha\mu_1+(1-\alpha)\mu_2\big)+(1-\alpha)\,d\big(\mu_2,\alpha\mu_1+(1-\alpha)\mu_2\big).$$

For $a\in\{2,\dots,K\}$ let $g_a(x)=(1+x)I_{1/(1+x)}(\mu_1,\mu_a)$ for $x\ge0$, let $x_a=g_a^{-1}$, and let $x_1\equiv1$. Finally

$$F_{\boldsymbol\mu}(y)=\sum_{a=2}^K\frac{d\big(\mu_1,m_a(y)\big)}{d\big(\mu_a,m_a(y)\big)},\qquad m_a(y)=\frac{\mu_1+x_a(y)\mu_a}{1+x_a(y)}.$$

Formalization targets

Goal: Theorem 5 (p. 5)

With $D=d(\mu_1,\mu_2)$: $F_{\boldsymbol\mu}$ is continuous and strictly increasing on $[0,D[$, $F_{\boldsymbol\mu}(0)=0$, $F_{\boldsymbol\mu}(y)\to\infty$ as $y\to D$, the equation $F_{\boldsymbol\mu}(y)=1$ has a unique solution $y^*\in[0,D[$, and

$$w\in w^*(\boldsymbol\mu)\iff w_a=\frac{x_a(y^*)}{\sum_{i=1}^Kx_i(y^*)}\quad\text{for every arm }a.$$

The equivalence says at once that the argmax exists, that it is a single point, and that it is given by eq. (5).

Milestones

1. Lemma 3 (p. 5): for every $w\in\Sigma_K$,

$$c_{\boldsymbol\mu}(w)=\min_{a\ne1}(w_1+w_a)\,I_{\frac{w_1}{w_1+w_a}}(\mu_1,\mu_a).$$

2. Claim after eq. (4) (p. 5): $g_a$ is a strictly increasing one-to-one mapping from $[0,+\infty[$ onto $[0,d(\mu_1,\mu_a)[$.
3. Lemma 4 (p. 5): for every maximizer $w^*$ and all $a,b\in\{2,\dots,K\}$,

$$(w^*_1+w^*_a)I_{\frac{w^*_1}{w^*_1+w^*_a}}(\mu_1,\mu_a)=(w^*_1+w^*_b)I_{\frac{w^*_1}{w^*_1+w^*_b}}(\mu_1,\mu_b).$$

Significance

The result. Theorem 5 reduces a $(K-1)$-dimensional non-smooth max–min problem to finding the root of one continuous increasing function on a bounded interval, each evaluation of which requires $K-1$ scalar inversions. It gives existence and uniqueness of $w^*(\boldsymbol\mu)$, which the paper's lower bound only presupposes, and it is the computational core of Track-and-Stop: without an explicit, well-posed $w^*$ the tracking strategy is not defined. Lemma 3 alone gives the closed form of the inner infimum used again in the analysis of the stopping rule.

Formalizing it. The results are proved in the paper; nothing here is open. To the best of our knowledge none of them has a machine-checked proof: the platform's existing best-arm-identification rows concern Gaussian arms and state the characteristic time at the level of measures, without this characterization. The mission produces a checked reduction for general one-parameter exponential families, including the edge cases the text passes over (ties among suboptimal arms, zero weights, the behaviour of $x_a$ near the end of its domain).

Difficulty

The infimum in Lemma 3 ranges over $\mathrm{Alt}(\boldsymbol\mu)$, a set of models with a unique best arm, so it is an open condition: the minimizing configuration, in which $\lambda_1$ and $\lambda_a$ coincide, lies outside $\mathrm{Alt}(\boldsymbol\mu)$ and is only approached. Other arms may also compete for the best position. A statement in which the infimum is taken over the closed relaxation $\{\lambda_a\ge\lambda_1\}$ is a lemma of the proof, not Lemma 3.

For Theorem 5, the equalization in Lemma 4 needs an argument that holds for every maximizer, not only for one found by a first-order condition, because the objective is a minimum of functions and is not differentiable. The monotonicity of $F_{\boldsymbol\mu}$ needs the monotonicity of each $x_a$ and of each ratio in the moving point $m_a$, and the limit at $D$ rests on the second-best arm(s) only, which is where the ordering $\mu_1>\mu_2\ge\dots$ enters. Finally the analytic facts about $d$ (continuity, positivity off the diagonal, monotonicity in each argument) must be derived from the exponential family itself.

Formalization scope

Lean represents a model by μ : Fin K → ℝ with 2 ≤ K and every μ a in the mean space deriv F.b '' F.Θ. The paper's arm $1$ is index 0, arm $2$ is index 1. The exponential family is a structure ExpFamily whose parameter set is a nonempty open interval and whose b is twice continuously differentiable with $\ddot b>0$ on $\Theta$. These two conditions are added to the paper's "convex, twice differentiable" and are disclosed: strict convexity is what makes the mean parameterization unique, and openness is what lets alternatives approach the boundary of $\mathrm{Alt}(\boldsymbol\mu)$. The reference measure and normalization are part of the structure but unused here.

The transportation cost is an infimum in EReal, so it is the true infimum of the set of values rather than a default 0. $w^*(\boldsymbol\mu)$ is never defined by choice: "$w$ is optimal" is a predicate, and Theorem 5 characterizes the set of such $w$. The functions $x_a$ are the inverse of $g_a$ on $[0,+\infty[$ and are evaluated only on $[0,d(\mu_1,\mu_2)[$. "Increasing" in Theorem 5 is stated as strictly increasing, as proved in Appendix A.2. Lemmas 3 and 4 and the claim on $g_a$ assume only that arm $1$ is the unique best arm, which is weaker than the paper's standing ordering.

A formalization that replaces $\mathrm{Alt}(\boldsymbol\mu)$ by $\{\lambda_a\ge\lambda_1\}$, assumes the maximizer exists and is unique, or asserts only existence of some $y^*$ without the formula for $w^*$, does not state these results and is ruled out.

A complete development needs: basic calculus of exponential families (the Bregman form of $d$, its continuity and strict positivity off the diagonal, its monotonicity in the second argument), the inverse function of a continuous strictly monotone map on an interval, and compactness of the simplex. The divergence facts are reusable in every bandit mission built on exponential families. Proofs of the milestones, of auxiliary facts about $d$ and $I_\alpha$, and a sorry-free instance of ExpFamily (Bernoulli or unit-variance Gaussian) are welcome.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2. https://arxiv.org/abs/1602.04589
• E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, JMLR 17, 2016. https://arxiv.org/abs/1407.4443
• N. K. Vaidhyan, R. Sundaresan, Learning to detect an oddball target, arXiv:1508.05572, 2015. https://arxiv.org/abs/1508.05572
• O. Cappé, A. Garivier, O.-A. Maillard, R. Munos, G. Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Annals of Statistics 41(3), 2013. https://arxiv.org/abs/1210.1136

Motivation

A false failure return is a product returned by a consumer as defective although it has no functional or cosmetic defect; managers attribute such returns to installation difficulties, a mismatch with the consumer's preferences, and remorse. Ferguson, Guide and Souza report (pp. 376–377) that false failures account for up to 80% of Hewlett-Packard's inkjet printer returns, roughly 5% of sales, and that the per-unit cost of a false failure return to computer manufacturers is around 25% of the product's price. The manufacturer absorbs most of that cost, while the retailer is the party able to prevent the returns in the short term, by spending time with customers before the sale and supporting them after it. The retailer bears the cost of that effort but captures only part of its benefit, so without an incentive it exerts too little.

The paper (Ferguson, Guide & Souza, MSOM 2006) models this as a single-period manufacturer–retailer problem with non-contractible retailer effort, and asks which contracts restore the supply chain's optimal effort and who gains from them. It belongs to the literature on supply chain coordination with contracts (Cachon 2003) and on channel rebates with sales effort (Taylor 2002); its object is a target rebate, a payment to the retailer for every false failure return below a target.

Setting

A manufacturer with unit cost $c$ sells to a retailer at wholesale price $w$, who sells at retail price $p$. Avoiding one false failure return is worth

$$M_m = m + \delta_m(w - c) \ \text{to the manufacturer},\qquad R_r = r + \delta_r(p - w)\ \text{to the retailer},$$

where $m$ and $r$ are the parties' return-processing costs and $\delta_m$, $\delta_r$ are the unit sale impacts of avoiding the return (p. 381). Both are assumed positive.

The retailer chooses an effort $\rho \ge 1$ at cost $a\rho^2/2$, $a > 0$. At effort $\rho$ the number of false failures is a nonnegative random variable $X(\rho)$ with mean $\beta/\rho$, where $\beta > 0$ is the expected number at the minimum effort $\rho = 1$. The coordinated supply chain earns

$$\Pi(\rho) = (M_m + R_r)\,\beta\Big(1 - \frac1\rho\Big) - \frac{a\rho^2}{2},$$

maximized at the coordinated effort $\rho^C = [(M_m + R_r)\beta/a]^{1/3}$. Without a contract the retailer earns $\pi_R(\rho) = -a\rho^2/2 + R_r\beta(1 - 1/\rho)$ and chooses the decentralized effort $\rho^D = \max\{(R_r\beta/a)^{1/3}, 1\}$; the manufacturer then earns $\pi_M(\rho^D) = M_m\beta(1 - 1/\rho^D)$.

Under a target rebate contract $(u, T)$ the retailer receives $u$ for every false failure below the target $T$, so the profits become

$$\pi_R(\rho \mid T, u) = u\,E\{[T - X(\rho)]^+\} - \frac{a\rho^2}{2} + R_r\beta\Big(1 - \frac1\rho\Big),\qquad \pi_M(\rho \mid T, u) = M_m\beta\Big(1 - \frac1\rho\Big) - u\,E\{[T - X(\rho)]^+\}.$$

The contract coordinates the supply chain when $\rho^C$ maximizes $\pi_R(\cdot \mid T, u)$ over $\rho \ge 1$. In the uniform case of §3.1, $X(\rho) \sim \mathrm{Uniform}(0, 2\beta/\rho)$, and the contract must satisfy $T < 2\beta/\rho^C$.

Formalization targets

Goal: Proposition 2 (p. 383)

Assume $a, \beta, M_m, R_r > 0$ and $(M_m + R_r)\beta > a$, and let $X(\rho)$ be uniform. For every coordinating contract $(u, T)$ with $u > 0$, $0 < T < 2\beta/\rho^C$,

$$\pi_R(\rho^C \mid T, u) \ge \pi_R(\rho^D) \qquad\text{and}\qquad \Big(\pi_M(\rho^C \mid T, u) \ge \pi_M(\rho^D) \iff \rho^C \ge 2\rho^D\Big).$$

Milestones

The milestones follow the paper's §3–§3.1 and the appendix proof, in attack order: concavity of $\Pi$ and optimality of $\rho^C$ (Eqs. (1)–(2)); $\rho^C > 1$ in the interesting case; optimality of $\rho^D$ (Eqs. (3)–(4)); $\rho^C \ge \rho^D$; Proposition 1 (concavity of the retailer's rebate profit when $\partial^2 F(x\mid\rho)/\partial\rho^2 \le 0$); its uniform instance; the uniform closed form (8); the first-order condition (9); the coordinating target (10) together with the admissibility condition $u > M_m$; the manufacturer's profit $M_m\beta(\rho^C - 2)/\rho^C$ under a coordinating contract (25); the retailer's profit (27); and the retailer's gain in the two cases $\rho^D > 1$ (30) and $\rho^D = 1$ (31).

Significance

The result divides the effect of the contract between the two parties. The retailer is always at least as well off as without a contract; the manufacturer, who pays the rebate, gains exactly when the supply chain's optimal effort is at least twice what the retailer would exert alone. When $\rho^D > 1$ this is equivalent to $M_m \ge 7R_r$ (p. 383), so a target rebate pays for the manufacturer only when its own stake in avoiding a false failure dwarfs the retailer's. The companion result (10) shows that for every rebate $u > M_m$ exactly one admissible coordinating target exists, and none for $u \le M_m$: a coordinating rebate is always larger than the manufacturer's own cost of a return.

The results are proved in the paper by calculus and algebra. None of them has a machine-checked proof that we know of, and nothing on Prove2Me models non-contractible effort or target rebates. The mission produces a checked version of the paper's model with the expectation taken as a genuine integral against the uniform law, a formal notion of coordination as the retailer's optimization, and statements that make explicit which hypotheses each step of the appendix uses. The definitions of effort-dependent profits and coordination are reusable for other effort-inducing contracts in the same paper and in the sales-effort literature.

Difficulty

The algebra of the appendix is short once the first-order condition (9) holds at $\rho^C$. The substance is getting there. Coordination is defined by optimality of $\rho^C$ for the retailer's profit, and that profit involves the expectation $E\{[T - X(\rho)]^+\}$, which is piecewise in $\rho$: it equals $T^2\rho/4\beta$ only while $T \le 2\beta/\rho$, and $T - \beta/\rho$ beyond. Deriving (9) requires showing that $\rho^C$ is an interior maximizer, that the expectation is differentiable there with the closed-form derivative, and that the side condition $T < 2\beta/\rho^C$ keeps $\rho^C$ in the closed-form region. The converse direction of (10), that the formula for $T$ produces a coordinating contract, needs concavity of the piecewise profit on all of $\rho \ge 1$, which is where Proposition 1 enters.

Replacing the expectation by the global formula $T^2\rho/4\beta$ is the tempting shortcut and it changes the problem: for $\rho > 2\beta/T$ the formula exceeds the true expectation, and the retailer's maximizer, hence the meaning of "coordinates", changes with it.

Formalization scope

All parameters are real numbers, bundled in a structure Params; $M_m$ and $R_r$ are Params.Mm and Params.Rr. Effort ranges over $\rho \ge 1$ (Set.Ici 1); statements the paper makes for every positive effort (concavity of $\Pi$, the closed form (8)) are stated on $\rho > 0$. Cube roots are Real.rpow with exponent $1/3$ on positive bases. The uniform law is Lebesgue measure conditioned on $[0, 2\beta/\rho]$, and the expectation is the Bochner integral against it. Coordination is IsMaxOn of the retailer's profit on Set.Ici 1 at $\rho^C$.

Three conventions differ from the printed text, each recorded in the item's formalization note:

1. The interesting case is printed as $(m + r)\beta > a$; the condition equivalent to the stated consequence $\rho^C > 1$, which the proof uses, is $(M_m + R_r)\beta > a$. The formalization uses the latter.
2. The printed evaluation $E_X\{[T - X(\rho)]^+\} = u\int_0^T (T - x)(\rho/2\beta)\,dx$ carries a stray factor $u$; the expectation is $T^2\rho/4\beta$.
3. Proposition 1 is stated for an arbitrary family of probability laws on $[0,\infty)$ whose distribution functions are $C^2$ in $\rho$ with nonpositive second derivative for $x \in [0,T]$; the paper's further assumptions on $F$ (differentiable, strictly increasing in $x$, mean $\beta/\rho$) are not imposed.

The side condition $T < 2\beta/\rho^C$ of §3.1 is a hypothesis of the goal and of the appendix milestones; without it a coordinating contract with $u = M_m$ exists and the "if" direction fails. The unused page assertion $\delta_r < \delta_m < 1$ is not imposed.

The goal is not trivialized by its coordination hypothesis: coordination is the retailer's optimization over the true profit, and milestone (10) shows that coordinating contracts with $T < 2\beta/\rho^C$ exist for every $u > M_m$, so the hypotheses are satisfiable (Example 1 of the paper, p. 384, is an instance). The retailer half of the goal is comparatively short under this definition of coordination; that is a property of the paper's theorem, not of the encoding. The manufacturer half needs (8), (9) and (25).

The development needs only Mathlib: real calculus (derivatives, concavity, Real.rpow) and Lebesgue integration against a conditioned Lebesgue measure. The model definitions (effort-dependent profits, coordination as the retailer's optimization) are reusable for the paper's other effort-inducing contracts. Contributions welcome: proofs of any milestone, and reusable lemmas on expectations of $[T - X]^+$ under uniform laws.

Selected references

• M. Ferguson, V. D. R. Guide Jr., G. C. Souza, Supply Chain Coordination for False Failure Returns, Manufacturing & Service Operations Management 8(4):376–393, 2006. https://doi.org/10.1287/msom.1060.0112
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, Elsevier, 2003. https://doi.org/10.1016/S0927-0507(03)11006-7
• T. A. Taylor, Supply Chain Coordination Under Channel Rebates with Sales Effort Effects, Management Science 48(8):992–1007, 2002. https://doi.org/10.1287/mnsc.48.8.992.168

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

Network revenue management decides which products to make available to arriving customers when products share scarce resources: an airline sells itineraries (products) that consume seats on flight legs (resources), and each itinerary has a fare. When customers choose among the offered products, rather than asking for one fixed product, the standard planning tool is a deterministic linear program that replaces random choices by their expected values. Gallego, Iyengar, Phillips and Dubey (2004, Columbia CORC technical report TR-2004-01) and Liu and van Ryzin (2008) formulated this choice-based linear program; its solution drives bid-price and offer-set policies used in practice.

The difficulty is size. The choice-based program has one variable for each subset of products, $2^n$ in all, and is solved by column generation, whose pricing subproblem is itself an assortment problem. Feldman and Topaloglu (Oper. Res. 65(5), 2017) show that when customers choose under the Markov chain choice model of Blanchet, Gallego and Goyal (2016), the choice-based program is equivalent to a linear program with only $2n$ variables and $m+n$ constraints. This mission formalizes that equivalence, Theorem 7 of the paper.

Setting

There are $n$ products, $N=\{1,\dots,n\}$. Under the Markov chain choice model a customer first visits product $j$ with probability $\lambda_j$. If the product she visits is offered, she buys it. Otherwise she moves from product $j$ to product $i$ with probability $\rho_{j,i}$, or leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$. The paper assumes throughout that

$$\lambda_j>0\quad\text{and}\quad\sum_{i\in N}\rho_{j,i}<1\qquad\text{for all } j\in N.$$

For an offer set $S\subseteq N$, $P_{j,S}$ is the expected number of visits to product $j$ while it is offered, which is its purchase probability, and $R_{j,S}$ is the expected number of visits to $j$ while it is not offered. The pair $(P_S,R_S)$ is the solution of the (Balance) equations

$$P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S .$$

Dropping the constraints tied to $S$ gives the polyhedron

$$\mathcal H=\Big\{(x,z)\in\mathbb R^{2n}_+ : x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \ \forall j\in N\Big\}.$$

The network has $m$ resources, $M=\{1,\dots,m\}$, with capacities $c_q$; the selling horizon has $T$ periods; product $j$ earns $r_j$ and consumes $a_{q,j}$ units of resource $q$. With $u_S$ the probability of offering $S$ in a period, the (Choice Based) linear program is

$$\max_{u\in\mathbb R^{2^n}_+}\Big\{\sum_{S\subseteq N}\sum_{j\in N}T r_jP_{j,S}u_S:\ \sum_{S\subseteq N}\sum_{j\in N}Ta_{q,j}P_{j,S}u_S\le c_q\ \forall q\in M,\ \sum_{S\subseteq N}u_S=1\Big\},$$

and the (Reduced) linear program is

$$\max_{(x,z)\in\mathbb R^{2n}_+}\Big\{\sum_{j\in N}T r_jx_j:\ \sum_{j\in N}Ta_{q,j}x_j\le c_q\ \forall q\in M,\ x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \forall j\in N\Big\}.$$

In (Reduced), $x_j$ is the expected number of visits to product $j$ while it is available and $z_j$ the expected number of visits while it is not.

Formalization targets

Goal: Theorem 7

Let $(\hat x,\hat z)$ be an optimal solution of (Reduced). Then there are subsets $S^1,\dots,S^K\subseteq N$ and positive scalars $\gamma^1,\dots,\gamma^K$ with $\sum_k\gamma^k=1$ such that

$$\hat x=\sum_{k=1}^K\gamma^kP_{S^k},\qquad \hat z=\sum_{k=1}^K\gamma^kR_{S^k},$$

and for any such subsets and scalars the vector $\hat u$ with $\hat u_{S^k}=\gamma^k$ and $\hat u_S=0$ for $S\notin\{S^1,\dots,S^K\}$ is optimal for (Choice Based), with objective value equal to that of $(\hat x,\hat z)$ in (Reduced). In particular the two programs have the same optimal value.

Milestones

1. (Balance) has a unique and nonnegative solution for every offer set (§2, p. 1325).
2. Lemma 1: an extreme point $(\hat x,\hat z)$ of $\mathcal H$ equals $(P_{S},R_{S})$ for $S=\{j:\hat x_j>0\}$ (p. 1326).
3. Lemma 10: $\mathcal H$ is bounded (quoted on p. 1331; proved in the online appendix).
4. Every point of $\mathcal H$ is a positive convex combination of finitely many extreme points of $\mathcal H$ (proof of Theorem 7, p. 1331).
5. Every feasible $u$ of (Choice Based) yields the feasible point $\tilde x_j=\sum_S P_{j,S}u_S$, $\tilde z_j=\sum_S R_{j,S}u_S$ of (Reduced), with the same objective value (proof of Theorem 7, p. 1332).

Significance

The result. Theorem 7 replaces a program with $2^n$ columns by one with $2n$ variables and $m+n$ constraints, solvable directly by any LP solver, and it returns an optimal solution of the original program, not only its value. The optimal value is the standard upper bound on the optimal expected revenue of a network revenue management policy, and the dual variables of the capacity constraints are the bid prices used to control sales. The decomposition of part 1 is what turns the small program's solution back into offer-set frequencies that a policy can implement; Section 7 of the paper makes that decomposition algorithmic (a separate mission of this series).

Formalizing it. The theorem is proved in the paper; to the best of available knowledge no machine-checked version exists. A formal proof checks the link between polyhedral geometry (extreme points of $\mathcal H$ and the solutions of (Balance)) and linear-programming optimality, and records exactly which properties of the Markov chain choice model are used: the standing assumptions enter through uniqueness and nonnegativity of $(P_S,R_S)$ and through boundedness of $\mathcal H$.

Difficulty

The inequality "(Reduced) $\ge$ (Choice Based)" is a direct computation: averaging the (Balance) equations with weights $u_S$ lands in $\mathcal H$. The reverse direction is where the obvious argument fails. A point of $\mathcal H$ has no offer set attached to it, and a general polyhedron need not be the convex hull of its extreme points: it can contain lines or rays. The argument requires that $\mathcal H$ is bounded, which depends on the substochasticity $\sum_i\rho_{j,i}<1$, and that each extreme point is exactly some $(P_S,R_S)$, which uses the structure of the balance equations and the uniqueness of their solution. Neither follows from general linear-programming facts. In Lean, the finite vertex representation of a bounded polyhedron is also not a one-line consequence of Mathlib's Krein–Milman theorem, which gives only the closure of the convex hull.

Formalization scope

Products are Fin n, offer sets Finset (Fin n), resources Fin m. The model is a structure Model n holding $\lambda$, $\rho$ (rho j i $=\rho_{j,i}$, the transition from $j$ to $i$) and the standing assumptions $\lambda_j>0$ and $\sum_i\rho_{j,i}<1$; the nonnegativity $\rho_{j,i}\ge0$, implicit in the paper because the $\rho_{j,i}$ are probabilities, is an added field. $(P_S,R_S)$ is a solution of (Balance) chosen by Classical.epsilon, and milestone 1 is what identifies it with the paper's unique solution. $\mathcal H$ is a subset of (Fin n → ℝ) × (Fin n → ℝ), extreme points are Mathlib's Set.extremePoints ℝ, and boundedness is Bornology.IsBounded. $T$ is a natural number entering as a real factor exactly where the paper writes it; $c$, $a$, $r$ carry no sign conditions, as in the paper. "Optimal solution" means feasible and at least as good as every feasible point; no supremum is used.

Two conventions are disclosed. The paper defines $\hat u$ by $\hat u_{S^k}=\gamma^k$; the formalization sets $\hat u_S=\sum_{k:S^k=S}\gamma^k$, which agrees when the $S^k$ are distinct and is the only consistent reading otherwise. Milestone 5 is stated for every feasible $u$ of (Choice Based), while the paper applies it to an optimal one; its argument uses only feasibility. No printed statement needed correction.

The goal is not only the decomposition of part 1, which is milestones 2 and 4 combined: it also asserts optimality of $\hat u$ and equality of the optimal values, and a formalization that drops part 2 does not state Theorem 7. Part 2 is required for every decomposition, and part 1 guarantees one exists, so part 2 is not vacuous.

A complete development needs the vertex representation of polytopes (reusable beyond this mission; LinearOptimization.polyhedron_resolution on the platform proves the resolution theorem in another encoding), the theory of substochastic matrices behind (Balance) (invertibility of $I-\bar Q$ with a nonnegative inverse), and finite-sum manipulations over Finset (Fin n). Contributions to any milestone, and bridges to existing polyhedral results, are welcome.

Selected references

• J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
• J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
• Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0172
• G. Gallego, G. Iyengar, R. Phillips, A. Dubey, Managing Flexible Products on a Network, Computational Optimization Research Center Technical Report TR-2004-01, Columbia University, 2004 (technical report; no DOI).
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Airlines, hotels and rental firms sell a fixed stock of capacity (seats on a flight leg, rooms on a night) over a finite selling horizon, and control revenue mainly by deciding which products (fare classes, rate plans) to make available at each moment. When customers substitute between products, the decision in each period is an assortment: a subset of products to offer. Talluri and van Ryzin (Management Science 2004) formulated this single resource revenue management problem as a dynamic program for a general choice model, and showed that structural properties of the optimal policy depend strongly on how customers choose.

The Markov chain choice model of Blanchet, Gallego and Goyal (technical report 2013; Oper. Res. 2016) describes substitution by a Markov chain on the products and approximates a broad class of random-utility models. Feldman and Topaloglu (Oper. Res. 65(5), 2017) study assortment and revenue management problems under this model. This mission formalizes their structural result for the single resource problem (Theorem 5): there is an optimal policy whose offer sets are nested in the remaining capacity and in the remaining time, so that it can be implemented by protection levels, one capacity threshold per product and period.

Setting

There are $n$ products $N=\{1,\dots,n\}$. A customer arrives to purchase product $j$ with probability $\lambda_j$. If $j$ is offered she buys it; otherwise she moves to product $i$ with probability $\rho_{j,i}$, and leaves with probability $1-\sum_{i\in N}\rho_{j,i}$. The paper assumes $\lambda_j>0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j$. For an offer set $S\subseteq N$, the purchase probabilities $P_{j,S}$ and the visit counts $R_{j,S}$ of unavailable products solve the (Balance) equations

$$P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j,\qquad P_{j,S}=0\ \ (j\notin S),\qquad R_{j,S}=0\ \ (j\in S).$$

With product revenues $r_j$, the (Assortment) problem is $\max_{S\subseteq N}\sum_{j}P_{j,S}r_j$, and its (Dual) linear program is

$$\min_{v\in\mathbb R^n}\Big\{\sum_{j}\lambda_jv_j : v_j\ge r_j,\ v_j\ge\sum_{i}\rho_{j,i}v_i\ \ \forall j\Big\}.$$

In the single resource problem there are $T$ periods and $c$ units of capacity. In each period at most one customer arrives; a sale of product $j$ earns $r_j$ and uses one unit. The optimal expected revenue $V_t(x)$ from period $t$ on with $x$ units left satisfies the (Single Resource) dynamic program

$$V_t(x)=\max_{S\subseteq N}\Big\{\sum_{j\in N}P_{j,S}\{r_j+V_{t+1}(x-1)-V_{t+1}(x)\}\Big\}+V_{t+1}(x),$$

with $V_{T+1}(x)=0$ and $V_t(0)=0$. An optimal subset $\hat S_t(x)$ is a maximizer of the problem on the right side. The marginal value of capacity is $\Delta V_t(x)=V_t(x)-V_t(x-1)$.

Formalization targets

Goal: Theorem 5 (p. 1329)

There exists an optimal policy, i.e. a choice of maximizers $\hat S_t(x)$ for all $1\le t\le T$, $1\le x\le c$, such that

$$\hat S_t(x-1)\subseteq \hat S_t(x)\qquad\text{and}\qquad \hat S_{t-1}(x)\subseteq\hat S_t(x).$$

The offer set shrinks as capacity runs down, and it is smaller when more periods remain.

Milestones

1. (§2, p. 1325) The (Balance) equations have a unique nonnegative solution for every $S$.
2. (Theorem 2, p. 1326) If $\hat v$ is optimal for (Dual), then $\{j:\hat v_j=r_j\}$ is optimal for (Assortment).
3. (Lemma 3, p. 1327) For $\eta\ge0$, with $\hat v^\eta$ optimal for (Dual) with revenues $r_j-\eta$,

$$\{j:\hat v^\eta_j=r_j-\eta\}\subseteq\{j:\hat v^0_j=r_j\}.$$

4. ((Single Resource), pp. 1328–1329) The value functions satisfy the printed recursion $V_t(x)=\max_S\{\sum_jP_{j,S}\{r_j+V_{t+1}(x-1)\}+\{1-\sum_jP_{j,S}\}V_{t+1}(x)\}$ and the boundary conditions.
5. (Proof of Theorem 5, p. 1329) $\Delta V_{t+1}(x)\le\Delta V_{t+1}(x-1)$ and $\Delta V_{t+1}(x)\le\Delta V_t(x)$.

Significance

Theorem 5 makes the optimal policy a protection level policy: for each product $j$ and period $t$ there is a threshold $\bar x_{jt}$ such that $j$ is offered exactly when at least $\bar x_{jt}$ units remain. The policy can then be stored as $n\,T$ numbers instead of a table of subsets, and each product can be controlled separately, which is how airline inventory systems are organized. The paper also shows (Table 2, p. 1330) that the products need not be closed in revenue order: a higher-fare product can be closed before a lower-fare one, so the result is genuinely about nested sets, not about nested fare classes. Talluri and van Ryzin (2004) show that under the multinomial logit model an optimal assortment consists of a number of products with the largest revenues; the Markov chain choice model does not have this property (Table 1, p. 1328), so their structure of the optimal policy does not carry over directly.

The result is proved in the paper. No part of it is formalized on Prove2Me. The monotonicity of marginal values for an abstract choice model is published and proved as RevenueManagement.choice_marginal_values, stated over the definitions RevenueManagement_singleResource; milestone 5 is the same statement for this paper's dynamic program and can be bridged to it. A complete development here produces machine-checked Theorem 2 and Lemma 3 for the Markov chain choice model, which are reusable for any assortment problem under this model.

Difficulty

The obvious argument chooses, for each $(t,x)$, any maximizer of the stage problem. This fails: the stage problems have ties, and an arbitrary choice of maximizers need not be nested, so the theorem is an existence statement about a coordinated choice. The dependence of $P_{j,S}$ on $S$ is through the solution of a linear system, so the effect of adding or removing a product on the other purchase probabilities has no simple sign, and optimal assortments need not be nested by revenue (Table 1, p. 1328). The link between two stage problems is that their revenues differ by the same constant for all products, and what has to be shown is that such a uniform shift moves an optimal assortment in a controlled direction. Revenues in the stage problems, $r_j-\Delta V_{t+1}(x)$, can be negative.

Formalization scope

Products are Fin n, offer sets Finset (Fin n), the paper's $\subset$ is non-strict inclusion $\subseteq$. The model is a structure with fields $\lambda$, $\rho$ and the standing assumptions $\lambda_j>0$, $\sum_i\rho_{j,i}<1$; $\rho_{j,i}\ge0$ is added as a field because the $\rho_{j,i}$ are probabilities. $(P_S,R_S)$ is a solution of (Balance) chosen by Classical.epsilon; milestone 1 states that it is the unique nonnegative one. The value function is defined by recursion on the number of periods to go, and $V_t$ is used only for $1\le t\le T+1$. Maxima over $S\subseteq N$ are taken over the finite family of all subsets, so they are attained; dual optimality is "feasible and no worse than every feasible point".

One hypothesis is added to Theorem 5 and milestone 5, and disclosed: $\sum_j\lambda_j\le1$, implied by the paper's description of at most one arrival per period (it makes $1-\sum_jP_{j,S}$ a probability). No sign condition is placed on the revenues, as on the page. Theorem 2 and Lemma 3 are stated for arbitrary real revenues, as the proof of Theorem 5 applies them to $r_j-\Delta V_{t+1}(x)$. The first inclusion of Theorem 5 is stated for $x\ge2$: with $x-1=0$ units there is no decision, and the paper reads $\hat S_t(0)$ as $\emptyset$. The existential requires every $\hat S_t(x)$ in range to be optimal for its stage problem; a statement without that clause would be satisfied by the empty sets and is ruled out.

Theorem 2 and Lemma 3 need LP duality for (Dual) and the (Balance) system; milestone 5 needs the standard induction on the dynamic program, or a bridge to the published choice_marginal_values (with arrival probabilities $1$ and choice model $P_{j,S}$). Proofs of any milestone, and bridges to published Mathlib or platform LP duality results, are welcome.

Selected references

• J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
• J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
• K. Talluri, G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000