All missions

From feedback to a decision problem

A Mastermind player sees guesses and feedback but cannot inspect the hidden sequence of colors. Before asking which guess to make next, one can ask whether the observations are consistent with any sequence at all. This is the Mastermind satisfiability problem, or MSP. It separates the logical content of the observations from the strategic problem of choosing informative guesses. In their 2005 preprint, Stuckman and Zhang study this decision problem and state that it is NP-complete. The question concerns arbitrarily large boards and alphabets, rather than one commercial game's fixed configuration.

The input is an entire finite collection of observations. Each observation names a guess and its prescribed response. The answer is YES precisely when one hidden sequence explains every observation simultaneously. A transcript need not have arisen from an actual game: inconsistent transcripts are part of the decision problem and must receive the answer NO.

Codes, repeated colors, and scores

Fix a number of colors $\kappa$ and a sequence length $\ell$. A code is an ordered sequence of $\ell$ colors; repetitions are allowed. A guess has the same form. For two codes $x,y$, the black score $b(x,y)$ counts positions containing the same color in both sequences. Let $m_x(j)$ be the number of occurrences of color $j$ in $x$. The total number of color matches, respecting multiplicity but ignoring position, is

$$w(x,y)=\sum_{j<\kappa}\min\{m_x(j),m_y(j)\}.$$

The feedback is the pair

$$\rho(x,y)=(b(x,y),w(x,y)-b(x,y)).$$

Its second component counts the white pegs, which represent matching colors not already counted as black pegs. For example, guesses $(0,0,1)$ and $(0,1,1)$ have score $(2,0)$; sequences $(0,1)$ and $(1,0)$ have score $(0,2)$. Counting only distinct colors would give the wrong model.

An instance consists of these parameters and a finite set of guesses, each with one prescribed feedback pair. It is satisfiable when there is a single code $s$ such that every guess $g$ has precisely its prescribed score against $s$. Neither uniqueness nor prior consistency is assumed. This is the model in Definition 2.1 and §2.1.

Formalization target

Write $L$ for the binary language of satisfiable instances with $\kappa>1$, and $L_\kappa$ for the sublanguage whose encoded color count is exactly $\kappa$. The goal states the two claims together:

$$\operatorname{NPComplete}(L)\quad\land\quad \forall\kappa>1,\ \operatorname{NPComplete}(L_\kappa).$$

NP-completeness includes both membership in NP and hardness under polynomial-time many-one reductions from every NP language. The assertion is unconditional: it assumes neither that P differs from NP nor that a suitable reduction has already been constructed. There is no global bound on the sequence length or number of guesses.

The fixed-color clause retains the stronger reading of the preamble to Theorem 2.1, page 4, which says “for κ > 1.” The printed proof uses a growing color alphabet and therefore does not itself establish this stronger scope. That proof gap is recorded separately; it is not an extra premise of the goal. There are no supporting source milestones in this mission.

What the result establishes

The theorem places consistency of Mastermind feedback among problems that admit short, efficiently checkable certificates and encode the difficulty of every NP problem. It concerns finding whether an explanation exists, rather than efficiently identifying a unique explanation or optimizing a playing strategy. Distinguishing these questions matters because they have different inputs and conclusions.

A formal development makes the score conventions, the quantification over transcripts, and the computational interpretation of input size explicit. The present goal is a statement awaiting proof. Its definitions are concrete, and its complexity notions reuse the published CookPvsNP machine model. The source's independent metric proposition and uniqueness discussion do not appear as assumptions or milestones. Their transcription issues are recorded in the accompanying source findings.

Where the difficulty lies

Trying every hidden code establishes only that each finite instance can be decided. The number of candidates grows exponentially in the board length, so this observation does not establish the required complexity classification. Conversely, rapidly evaluating a proposed code addresses only verification; it says nothing by itself about universal hardness.

The fixed-color claim introduces an additional issue: a construction that increases the alphabet with its input does not automatically settle the problem for two colors or for another prescribed alphabet size. The full statement retains that obligation. Also, the number of guesses is unbounded, so complexity cannot be measured by board length alone while ignoring the cost of reading the transcript.

Formalization scope and encoding

Codes use Fin ℓ → Fin κ, relabeling the source's one-based colors and positions by subtracting one. Empty sequences are permitted. Feedback uses natural numbers; negative feedback has no valid encoding, while impossible nonnegative feedback remains representable and unsatisfiable. Matching-coordinate counts implement the intended reading of the shadowed index in Definition 2.1, as explained by the surrounding text.

A finite guess set is represented by strictly lexicographically increasing rows. This gives one score per guess and rejects duplicates, including conflicting duplicates. Every integer is encoded by canonical little-endian binary digits preceded by their unary digit count and a false separator. Zero has one false digit. The complete string contains the color count, board length, row count, then every color and feedback entry in row order. Membership requires equality with a complete encoding, so extra trailing data and malformed encodings are rejected.

Running time is measured in the length of this complete binary string. An empty transcript can describe a large board compactly and is always satisfiable when $\kappa>1$; it must not force an exponentially long certificate. For nonempty transcripts, a written guess already contains all positions. The mathematical score sums over colors, but the eventual verification algorithm must avoid enumerating exponentially many unused colors. These are proof obligations, not restrictions on instances. No consistency promise or special family of generated instances is hidden in the definitions.

Selected references

• Jeff Stuckman and Guo-Qiang Zhang, Mastermind is NP-Complete, preprint, 2005, arXiv:cs/0512049v1, Definition 2.1 and Theorem 2.1.

Planning a complete Tetris game

Knowing every future piece removes uncertainty from Tetris, but it does not remove the computational difficulty of choosing placements. Offline Tetris asks a player to plan against an entire finite piece sequence revealed in advance. The initial board can already contain occupied cells, and its dimensions are part of the input. Demaine, Hohenberger and Liben-Nowell show that even a coarse multiplicative approximation to the best number of cleared rows is computationally hard. The target here is their exact exponent, rather than only hardness of finding an optimal play (arXiv:cs/0210020v1, Theorem 6.5).

The distinction between input size and piece count matters. A board may contain many occupied cells before any piece arrives. The theorem measures running time in the full explicit input, but its approximation factor depends only on the number of supplied pieces. It therefore connects an operational packing game to the complexity of obtaining even a substantially suboptimal feasible score.

Boards, pieces and legal play

A board is a finite rectangular grid whose cells are occupied or empty. Rows are ordered from bottom to top. An initial legal board has positive height and width, no completely filled row, and no completely empty row below an occupied cell. Cells outside the rectangle count as occupied when testing a move. The input also specifies an ordered list of the seven tetromino types: square, left gun, right gun, left snake, right snake, I and T.

Each piece has a type, one of four orientations, a position and a fixed flag. It enters at the source's prescribed central column, with its highest cells in the top row. The player may rotate, slide by one column, drop by one row, or fix a supported piece. A supported piece can still slide or rotate before fixing. There is no limit on the number of horizontal moves or rotations between drops. Once fixed, it occupies its four cells; every newly full row disappears and the rows above move downward. A blocked spawn ends the game (§2, pp. 4–7).

The rotation rule is fixed before the input game. It examines a fixed finite neighborhood, admits rotation when that neighborhood is empty, and avoids occupied cells. The source's reasonable rotation models additionally preserve connected empty regions and obey three geometric restrictions concerning bucket notches and balconies. The instantaneous model rotates around the precise centers in Figure 2, without requiring a continuously clear swept region. An I piece rotates around its indicated cell, not its geometric midpoint. A square keeps its footprint under rotation.

Formalization targets

Let $G$ be a game, $p$ its number of pieces, and $\operatorname{OPT}(G)$ the greatest attainable cleared-row count. The main target is

$$\text{For every fixed }\varepsilon>0,\qquad \operatorname{OPT}(G)\le p^{1-\varepsilon}v \text{ is NP-hard to achieve with feasible }v.$$

This is Theorem 6.5, p. 21, for every fixed admissible reasonable rotation model. For nonempty piece lists, the displayed factor is unchanged even when it is less than one. An empty list has score zero. The theorem has no assumption that P differs from NP, that 3-Partition is hard, or that a particular reduction is correct.

The fourteen supporting targets are strong NP-completeness of indexed 3-Partition; polynomial size of the concrete base game; completeness; both bucket/lock allocation clauses; exclusion of unfillable buckets; unfillability of the unapproachable shape; reasonability of instantaneous rotation; all eight forbidden configurations; initiator, filler and terminator soundness; confinement of every integer block to one bucket; the final I-piece allocation; and base-game soundness. The geometric statements retain both filler alternatives and both numbered cases of the filler and terminator lemmas. Independent survival, height and tetris-count objectives are outside this mission.

What a formal development establishes

A complete development connects legal movement, row compression, feasible optimization answers and actual polynomial-time computation. The definitions describe a game independently of any partition answer. A future proof must establish the reduction properties; those properties are not built into the game's rules or supplied as premises of the goal.

The paper supplies mathematical proofs. This proposal supplies definitions and compiled statements with proof placeholders, not machine-checked proofs of its fifteen theorems. Cook's published finite-machine and complexity definitions are reused. The local statement audit also records a literal empty-instance counterexample to the printed completeness theorem; that theorem remains stated with its source domain so that a subsequent solver can address the finding explicitly.

Where formal precision is difficult

A final tiling does not by itself establish a legal trajectory. A piece may fit a collection of empty cells while being unable to reach them from its fixed spawn. Row deletion changes coordinates, and a loss check occurs after that deletion. Likewise, a partial sequence being legal does not make it valid in the soundness argument: validity there means extendibility to a strategy clearing the specified number of rows.

The geometric part distinguishes patterns differing by a single cell, including three separate floor patterns and two ceiling-discrepancy patterns. Bucket frames retain the source height and staging space; a notch cannot become an exposed opening at the wall top. The tall-plateau template includes the empty row between its filled plateau and the next notch, as drawn in Figure 8(d). The computational part must distinguish polynomial output size from a polynomial bound on actual machine steps. These distinctions are necessary to preserve what the source claims.

Formalization scope

Boards use finite Boolean arrays. Stored coordinates are zero-based, while signed integer positions handle the exterior sentinels. Each source entry has its own index, even when several integers are equal. The source language uses self-delimiting unary codes over a binary alphabet, preserving the strong-complexity statement and its nonnegative boundary cases. Base-game arithmetic uses the source's three normalization conditions only within reduction lemmas.

Reachable play prefixes include zero score and determine the maximum because continuing cannot decrease the cleared-row count. Approximation compares an attainable answer with every attainable score, avoiding default values of an empty or unbounded supremum. The score is bounded by the initial occupied area plus four times the number of pieces. The general search interface requires instance and answer transformations with Cook-model polynomial running times, correct for every answer satisfying the approximation relation.

The reduction definitions include the concrete bucket board, ordered piece blocks and two-lock reservoir. A fixed explicit staging allowance replaces the source's constant-size staging term. Figure 9(b) determines the four empty cells of the second lock and the empty staging region above the added columns. The source text's conflicting description of those columns is recorded as an insight. Definitions of unfillability use actual trajectories of arbitrarily many permitted pieces, not a list of forbidden patterns or an assumed canonical strategy.

Selected references

• Erik D. Demaine, Susan Hohenberger and David Liben-Nowell, Tetris is Hard, Even to Approximate, preprint arXiv:cs/0210020v1, version identifier dated 21 October 2002. All theorem numbers and printed/PDF pages refer to the checksum-pinned 56-page artifact, whose title-page date differs from its version margin.
• Stephen Cook, The P versus NP Problem, Clay Mathematics Institute problem description. The formal computation interface is the published CookPvsNP_defs definition, id 7c6b3da6-5145-4b2d-9550-f07c61d2c766; it provides finite Turing machines, NP, polynomial-time computation and NP-completeness.

Why multistage programs are discretized

A multi-stage stochastic linear program chooses decisions over $T$ stages while a random process unfolds, each decision depending only on what has been observed so far. Such problems arise in planning under uncertainty, from production and energy systems to asset-liability management. With a non-discrete distribution the unknowns are functions, and the constraints hold almost surely, so the problem has infinitely many variables and constraints. Algorithms therefore work on a finite approximation: a scenario tree carrying a discrete distribution.

The question this mission addresses is what the optimal value of such an approximation says about the original problem. For two-stage programs with complete fixed recourse, replacing the distribution by the conditional means on the cells of a partition gives a lower bound (Jensen's inequality). Kall and Mayer show in Example 3.1 of Chapter 3 that this fails in general for three stages, even with randomness only in the right-hand sides and complete fixed recourse. The discussion goes back to an idea of S. Sen, reported in Fúsek, Kall, Mayer, Sen and Siegrist (2000). Kall and Mayer then isolate an assumption, stagewise independence, under which the lower bound does hold.

This is Mission XII of a series following P. Kall and J. Mayer, Stochastic Linear Programming: Models, Theory, and Computation (Kluwer/Springer, 2005).

The problem and its aggregation

On a probability space, let $\xi_t:\Omega\to\mathbb R^{r_t}$, $t=2,\dots,T$, be random vectors, and let $\zeta_t=(\xi_2,\dots,\xi_t)$ be the state at stage $t$. Problem (3.10) is

$$\min\Big\{c_1^{\mathsf T}x_1+\mathbb E\sum_{t=2}^Tc_t^{\mathsf T}x_t(\zeta_t)\Big\}$$

subject to $A_{11}x_1=b_1$, $A_{t1}x_1+\sum_{\tau=2}^tA_{t\tau}x_\tau(\zeta_\tau)=b_t(\zeta_t)$ a.s., and $x_1\ge0$, $x_t(\zeta_t)\ge0$ a.s. The decisions $x_t$ are square-integrable functions of $\zeta_t$. Only the right-hand sides $b_t$ are random.

Assumption 3.2 asks that the $b_t$ be linear affine in $\zeta_t$, that each $\xi_t$ take its values in a bounded interval $\Xi^t\subset\mathbb R^{r_t}$, that $\xi_2,\dots,\xi_T$ be stochastically independent, and that the $A_{tt}$ be complete recourse matrices: $\{A_{tt}y\mid y\ge0\}$ is the whole space.

A scenario tree has finite node sets $\mathcal N_t$, one root in stage 1, and a parent $h_n$ for each later node. To each node $h$ of a stage below $T$ it attaches a partition of the next interval $\Xi^{t+1}$ into subintervals $\Xi^{t+1}_k$, one for each child $k$; different nodes may use different partitions. Along the history $\{\ell_1,\dots,\ell_t=n\}$ of a node, set

$$\widehat\zeta^n=\big(\mathbb E[\xi_2\mid\xi_2\in\Xi^2_{\ell_2}],\dots,\mathbb E[\xi_t\mid\xi_t\in\Xi^t_{\ell_t}]\big),\qquad p_n=\prod_{\nu=2}^t\mathbb P_{\xi_\nu}(\Xi^\nu_{\ell_\nu}).$$

The fully aggregated problem (3.14) is the finite linear program

$$\min\sum_{m\in\mathcal N}p_mc_{t_m}^{\mathsf T}x_m\quad\text{s.t.}\quad\sum_{m\in\mathcal H(n)}A_{t_nt_m}x_m=b_{t_n}(\widehat\zeta^n)\ \ \forall n,\qquad x_m\ge0\ \ \forall m.$$

Formalization targets

Goal: Lemma 3.1

Under Assumption 3.2, for every scenario tree,

$$\mathrm{val}(3.14)\le\mathrm{val}(3.10).$$

Further results of the section

• Equation (3.13). Under independence, $\mathbb P(\Omega^{(n)})=p_n$, and $\widehat\zeta^n$ is the conditional expectation of the state on $\Omega^{(n)}$.
• The recursions (3.15) and (3.17). Backward recursions $r_t,\Phi_t$ and $q_t,\Psi_t$ compute the optimal values of (3.10) and (3.14).
• Inequality (3.16), with its form for conditional expectations, and the induction $q_t\le r_t$, $\Psi_{t+1}\le\Phi_{t+1}$.
• Proposition 3.1. Splitting a node by the cut and paste procedure, which duplicates its subtree, does not decrease the optimal value: $V^+\ge V$.
• Corollary 3.1. Any sequence of such splits converges to a value $V^*\le\hat V$.
• Example 3.1. With dependent $\xi_2,\xi_3$, the discretized value can exceed the true one: $\bar V=\tfrac34$ against $V^*=\tfrac{5-\varepsilon}{6}$, which is smaller for $\varepsilon>\tfrac12$.

What the results give

Lemma 3.1 turns any scenario tree into a certified lower bound on a problem with a general distribution, computed by one finite linear program. Together with Proposition 3.1 it justifies refining a tree adaptively: every split keeps a valid bound and cannot worsen it. Example 3.1 fixes the limits of this: the bound is a consequence of independence, not of the convexity of the problem alone.

These are textbook results, proved on paper, though the equivalence of (3.10) with its recursion is quoted in the book from Olsen and from Rockafellar and Wets rather than proved. To our knowledge none of this is formalized for general distributions. The platform holds a proved aggregation bound for finite trees (StochasticProg.MultistageBounds.thm1_multistage_jensen_lower_bound_v2, from Birge and Louveaux), which covers a different setting: there both problems live on finite trees. The formalization here adds a statement with arbitrary bounded independent distributions, policies as measurable square-integrable functions, and extended-real optimal values.

Where the difficulty lies

The natural induction backwards through the stages meets the fact that (3.10) lives on a function space while (3.14) is finite. Two gaps must be bridged: the passage between policies and pointwise stage problems, which needs measurable selection and Fubini's theorem under independence; and the behaviour of the stage values, which Assumption 3.2 does not make finite, since it says nothing about dual feasibility.

The obvious transfer of the two-stage argument, conditioning on each cell and applying Jensen's inequality to the whole cost-to-go, does not work without independence: Example 3.1 shows the conclusion is then false. Cells with probability zero, for which the conditional means of (3.13) do not exist, have to be handled throughout.

Formalization scope

Stages keep the book's index $t=1,\dots,T$. Decisions are Fin (n t) → ℝ, and the state space Hist r t is the product over $2\le s\le t$, which is a single point at $t=1$, so stage 1 is covered by the general formulas. The structure MSLP holds the deterministic data, with $b_t$ an affine map. The structure Assumption32 holds the remaining hypotheses. A policy is a family of measurable functions of the state with square-integrable compositions, as the book requires on p.249. The scenario tree ScenarioTree has its nodes indexed by stage.

Both optimal values are infima in EReal, so infeasible and unbounded problems are covered; the recursions are extended-real valued, with expectations given by the published WassersteinDRO.Duality.erealExpectation. On a null cell the conditional mean is 0, a choice that has no effect on the optimal value of (3.14). The complete recourse condition is read for $t=2,\dots,T$, since the book's own Example 3.1 has a first stage that is not complete.

The value of (3.10) is an infimum over policies, not the recursion's $r_1$; identifying the two is a target, not a definition. A statement restricted to finitely supported distributions would be a different theorem, and the goal is stated for every distribution satisfying Assumption 3.2.

A complete development needs conditional expectations on cells of independent vectors, Jensen's inequality for extended-real convex functions, and linear programming on trees. Lemmas on stagewise conditioning are reusable beyond this mission. Contributions on any milestone are welcome.

Selected references

• P. Kall and J. Mayer, Stochastic Linear Programming: Models, Theory, and Computation, International Series in Operations Research & Management Science, Kluwer/Springer, 2005, ISBN 0-387-23385-7.
• P. Fúsek, P. Kall, J. Mayer, S. Sen and S. Siegrist, Multistage stochastic linear programming: Aggregation, approximation, and some open problems, Technical report, Inst. Oper. Res., University of Zurich, 2000. Reference [91] of the book.
• P. Olsen, When is a multistage stochastic programming problem well defined?, SIAM J. Control Optim. 14, 518–527, 1976. Reference [217] of the book.
• R. T. Rockafellar and R. J.-B. Wets, Nonanticipativity and $L^1$-martingales in stochastic optimization problems, Math. Programming Study 6, 170–186, 1976. Reference [254] of the book.

Motivation

A two-stage stochastic linear program asks for a first-stage decision $x$ taken before a random vector $\xi$ is observed, followed by a recourse decision $y$ that corrects for the outcome. Solving it exactly means optimizing an expectation of linear-program values, which is expensive. Practitioners therefore often solve the much cheaper expected value problem, in which $\xi$ is replaced by its mean, and two questions follow at once: how much is lost by doing so, and how much would perfect foresight be worth? The two standard answers are the value of the stochastic solution $VSS$ (Birge, 1982) and the expected value of perfect information $EVPI$ (Avriel and Williams, 1970). This mission formalizes the comparisons between these characteristic values that Kall and Mayer collect in §2.3 of Chapter 3 of Stochastic Linear Programming: Models, Theory, and Computation (2005), the chapter's account of results going back to Madansky (1960).

Timeline:

• Madansky (1960): inequalities between the wait-and-see value, the recourse value and the expected value problem.
• Avriel and Williams (1970): $EVPI = RS - WS$ introduced; bound $EVPI \le EEV - EV$ when only the right-hand side is random.
• Birge (1982): $VSS = EEV - RS$ introduced; bound $VSS \le EEV - EV$ when only the technology matrix and the right-hand side are random.
• Kall (1976) and Birge–Louveaux (1997): counterexamples showing that the bounds need these restrictions on the random data.

Setting

Let $\xi$ be a random vector in $\Xi=\mathbb R^r$ with law $\mu=\mathbb P_\xi$ and $\xi\in L^2$, with mean $\bar\xi=\mathbb E_\xi[\xi]$. The data of the two-stage problem (TwoStageSLP) are a deterministic first stage $A\in\mathbb R^{m_1\times n_1}$, $b\in\mathbb R^{m_1}$, $c\in\mathbb R^{n_1}$, and second-stage arrays that are affine in $\xi$:

$$T(\xi)=T+\sum_j T^j\xi_j,\quad W(\xi)=W+\sum_j W^j\xi_j,\quad h(\xi)=h+\sum_j h^j\xi_j,\quad q(\xi)=q+\sum_j q^j\xi_j .$$

The recourse function is the value of the second-stage linear program,

$$Q(x;\xi)=\inf_y\{q(\xi)^{\mathsf T}y : W(\xi)y=h(\xi)-T(\xi)x,\ y\ge0\}\in[-\infty,+\infty].$$

Writing $\mathcal B_1=\{x: Ax=b,\ x\ge0\}$, the characteristic values are:

• the recourse value $RS=\min_{x\in\mathcal B_1}\{c^{\mathsf T}x+\mathbb E_\xi[Q(x;\xi)]\}$;
• the wait-and-see value $WS=\mathbb E_\xi[\gamma(\xi)]$, where $\gamma(\xi)=\min_{x,y}\{c^{\mathsf T}x+q(\xi)^{\mathsf T}y: Ax=b,\ T(\xi)x+W(\xi)y=h(\xi),\ x,y\ge0\}$;
• the expected value problem value $EV=\gamma(\bar\xi)$;
• for an optimal first-stage solution $\hat x$ of the EV problem, the expected result of the EV solution $EEV=c^{\mathsf T}\hat x+\mathbb E_\xi[Q(\hat x;\xi)]$;
• $EVPI=RS-WS$ and $VSS=EEV-RS$.

The book names two sub-classes by the arguments of the recourse function: $Q(x;T(\xi),h(\xi))$, where only $T$ and $h$ are random, and $Q(x;h(\xi))$, where only $h$ is random.

Formalization targets

Goal: Proposition 2.4 (p.247)

For every optimal first-stage solution $\hat x$ of the EV problem,

$$VSS\le EEV-EV\quad\text{if only }T(\cdot),h(\cdot)\text{ are random},\tag{2.74}$$ $$EVPI\le EEV-EV\quad\text{if only }h(\cdot)\text{ is random}.\tag{2.75}$$

Both bounds use only quantities computable from the expected value problem and one evaluation of the expected recourse.

Milestones

1. Proposition 2.2 (p.245): $WS\le RS\le EEV$ for an arbitrary recourse problem (2.70), and $EV\le RS\le EEV$ when only $T,h$ are random (2.71).
2. Proposition 2.3 (p.245): $EV\le WS$ when only $h$ is random.
3. p.246: $EVPI\ge0$ and $VSS\ge0$ (where the differences are defined).
4. p.246: if $\mathbb P_\xi(\xi=\hat\xi)=1$ for some $\hat\xi$, then $EVPI=VSS=0$.
5. Example 2.2 (pp.247–248): with random $T$, $EVPI=2>EEV-EV=0.75$, so (2.75) needs its restriction.

Significance

The goal gives a priori bounds on two quantities that are otherwise as hard to compute as the recourse problem itself: $EVPI$ requires solving the recourse problem and a continuum of wait-and-see problems, $VSS$ requires the recourse problem. The bound $EEV-EV$ requires only the deterministic expected value problem and one expected recourse evaluation at its solution. A small $EEV-EV$ certifies that solving the stochastic program is not worth the effort; Example 2.2 shows that the certificate is not available for $EVPI$ once the technology matrix is random.

All results are classical and proved in the book. On the platform, the corresponding statements of Birge and Louveaux (Chapter 4, Propositions 1 and 5) exist for finitely many scenarios; this mission states them for a general distribution of $\xi\in L^2$, with extended-real values, which requires the convexity of linear-program values in the right-hand side and Jensen's inequality for extended-real convex functions. These pieces are reusable for every later statement about recourse problems with continuous distributions.

Difficulty

The inequalities $WS\le RS\le EEV$ are order-theoretic: they follow from pointwise inequalities and monotonicity of the expectation. The content is in $EV\le RS$ and $EV\le WS$, which rest on convexity: $\xi\mapsto Q(x;T(\xi),h(\xi))$ for fixed $x$, and $\xi\mapsto\gamma(\xi)$ when only $h$ is random, are convex because a linear program's value is convex in its right-hand side. The obvious argument applies Jensen's inequality to these functions, but they take the values $+\infty$ (infeasible second stage) and $-\infty$ (unbounded second stage), so neither Mathlib's real-valued Jensen inequality nor Bochner integration applies directly. One must show the functions are measurable, bound them below by an integrable affine function where they are finite, and handle infeasibility with positive probability separately. When $W$ or $q$ is random, convexity in $\xi$ fails, and so does the bound; the formal statements must keep the restrictions.

Formalization scope

• $\xi$ is represented by its law, a probability measure $\mu$ on Fin r → ℝ; the standing assumption $\xi\in L^2$ (Chapter 3, Assumption 1.1) is the hypothesis that every coordinate is in $L^2(\mu)$.
• All values lie in EReal. Minima are infima: $+\infty$ for an infeasible problem, $-\infty$ for an unbounded one. The recourse function is the platform's StochasticProg.RecourseKKT.secondStageValue evaluated at the realized data.
• The expectation eExp of an extended-real cost is $\int f^+d\mu-\int f^-d\mu$ with Lebesgue integrals, and $+\infty$ whenever $\int f^+d\mu=+\infty$; this is the book's rule that a decision with infinite or undefined expected recourse is not chosen. No integrability hypothesis is hidden in it.
• $EEV$ and $VSS$ take the EV solution $\hat x$ as an argument, and every statement quantifies over all optimal $\hat x$, because $EEV$ depends on the choice.
• The restrictions "only $T,h$ random" and "only $h$ random" are built by constructors that make the other data deterministic, not by hypotheses.
• $EVPI$ and $VSS$ are EReal differences. Proposition 2.4 holds with no finiteness hypothesis; the nonnegativity statements assume only that the difference is not of the form $\infty-\infty$.

Contributions welcome: Jensen's inequality for convex functions $\mathbb R^r\to[-\infty,+\infty]$ in this expectation; convexity and Borel measurability of linear-program values in the right-hand side; the finite computations of Example 2.2.

Selected references

• P. Kall and J. Mayer, Stochastic Linear Programming: Models, Theory, and Computation, Kluwer/Springer, 2005, Chapter 3, §2.3. https://doi.org/10.1007/b105472
• A. Madansky, Inequalities for stochastic linear programming problems, Management Science 6 (1960) 197–204. https://doi.org/10.1287/mnsc.6.2.197
• M. Avriel and A. C. Williams, The value of information and stochastic programming, Operations Research 18 (1970) 947–954. https://doi.org/10.1287/opre.18.5.947
• J. R. Birge, The value of the stochastic solution in stochastic linear programs with fixed recourse, Mathematical Programming 24 (1982) 314–325. https://doi.org/10.1007/BF01585113
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, Springer, 1997. https://doi.org/10.1007/b97617

Motivation

The traveling salesman problem (TSP) asks for a cheapest circuit through every node of a graph with edge costs. No polynomial-time algorithm is known, and exact codes for large instances depend on strong lower bounds to prune their search. Two lower bounds dominate the classical literature. The first is the subtour bound, the optimal value of the linear programming relaxation of Dantzig, Fulkerson and Johnson (1954). The second is the Held–Karp bound (Held and Karp 1970; 1971), computed from minimum spanning trees after shifting the edge costs by numbers attached to the nodes. The first needs a linear programming solver; the second needs only a spanning-tree routine, iterated.

Chapter 7 of Cook, Cunningham, Pulleyblank and Schrijver, Combinatorial Optimization (Wiley, 1998), presents both bounds in §7.3 and closes the section with Theorem 7.2: the two bounds coincide. This mission formalizes that theorem together with the statements the book uses to reach it.

Timeline:

• 1954: Dantzig, Fulkerson and Johnson solve a 49-city instance with the degree equations, the subtour constraints and cutting planes.
• 1970: Held and Karp introduce 1-trees and node numbers and show that the best bound obtained this way equals the optimal value of the subtour relaxation.
• 1971: Held and Karp give the subgradient ("ascent") method for finding good node numbers.
• 1971: Edmonds describes the forest and spanning-tree polytopes (Edmonds 1971), the polyhedral fact behind the 1-tree linear program.

Setting

A graph $G=(V,E)$ has finite sets of nodes and edges, and every edge has an unordered pair of ends; parallel edges are allowed. A circuit is a closed path $v_0,e_1,v_1,\dots,e_k,v_k=v_0$ with distinct edges, distinct nodes $v_0,\dots,v_{k-1}$ and $k\ge1$. A tour is a circuit meeting every node, and its cost is $c(T)=\sum_{e\in T}c_e$ for edge costs $c\in\mathbb R^E$. A forest is an edge set containing no circuit. For $A\subseteq V$, $\delta(A)$ is the set of edges with one end in $A$ and one outside, $\gamma(A)$ the set of edges with both ends in $A$, $\delta(v)=\delta(\{v\})$, and $x(B)=\sum_{e\in B}x_e$.

Fix a node $v_1$. $G\setminus v_1$ is $G$ with $v_1$ and its incident edges deleted. A 1-tree is a set $\{e,f\}\cup T$ where $e\ne f$ are edges of $\delta(v_1)$ and $T$ is a spanning tree of $G\setminus v_1$. The 1-tree bound is $A+B$, where

$$A=\min\{c_e+c_f : e,f\in\delta(v_1),\ e\ne f\},\qquad B=\text{the cost of a minimum spanning tree of }G\setminus v_1 .$$

For node numbers $y\in\mathbb R^V$, put $\bar c_e=c_e-y_u-y_v$ for an edge $e$ with ends $u,v$. The Held–Karp bound is $2\sum_v y_v + C_y$, where $C_y$ is the 1-tree bound for the costs $\bar c$. The optimal Held–Karp bound is its supremum over $y$, a maximum whenever it is finite.

The subtour bound is the optimal value of

$$\begin{aligned} \text{minimize}\quad & \textstyle\sum_{e\in E}c_ex_e && (7.1)\\ \text{subject to}\quad & x(\delta(v))=2, && v\in V,\\ & x(\delta(S))\ge 2, && \emptyset\ne S\ne V,\\ & 0\le x_e\le 1, && e\in E. \end{aligned}$$

Formalization targets

Goal: Theorem 7.2 (p. 260)

For every finite loopless graph $G$, all edge costs $c$ and every node $v_1$,

$$\min\{c^Tx : x\text{ feasible for (7.1)}\}=\sup_{y\in\mathbb R^V}\Big(2\sum_{v\in V}y_v+C_y\Big),$$

both sides being $+\infty$ when (7.1) is infeasible; and when the left side is not $+\infty$ the supremum is attained by some $y$, which is the book's "maximum". The goal fixes no metric or completeness condition and no lower bound on $|V|$.

Milestones

1. 1-tree Bound (box, p. 253): $A+B\le c(T)$ for every tour $T$.
2. Held–Karp Bound (box, p. 255): $2\sum_v y_v+C_y\le c(T)$ for every tour $T$ and every $y$.
3. (7.1) as (7.2) (p. 259): for a graph all of whose loops are at $v_1$, the constraints of (7.1) have the same solutions as the "inside" system $x(\delta(v))=2$, $x(\gamma(S))\le|S|-1$ for nonempty $S\not\ni v_1$, $x(\gamma(V\setminus\{v_1\}))=|V|-2$, $0\le x\le1$.
4. Theorem 8.8 (p. 280): the convex hull of the characteristic vectors of forests is $\{x\ge0 : x(\gamma(T))\le|T|-1 \text{ for } \emptyset\ne T\subseteq V\}$.
5. (7.7) (p. 260): the cost of a minimum 1-tree equals $\min\{c^Tx : (7.4),(7.5),(7.6),\ x(\delta(v_1))=2\}$.

Significance

The theorem says that the Held–Karp procedure, which only ever computes minimum spanning trees, converges in value to the linear programming relaxation of the TSP. This is why the Held–Karp bound is used inside branch-and-bound codes in place of an LP solver, and why the subtour relaxation is often called the "Held–Karp relaxation" in the approximation literature, where its integrality gap is studied (Wolsey's $3/2$ bound for metric costs; the $4/3$ conjecture).

On the formal side, the platform already has 1-tree and Held–Karp lower bounds and Held–Karp relaxation results, all stated on the complete graph $K_n$ with costs on unordered pairs. Theorem 7.2 itself, the equality of the two bounds, is not on the platform in any form. This mission states it for arbitrary finite graphs with parallel edges and arbitrary real costs, so that sparse instances and negative costs are covered. The forest polytope (Theorem 8.8) is reusable well beyond this mission: it is the polyhedral input to the spanning-tree polytope, to matroid polytopes of graphic matroids, and to the integrality analysis of tree-based relaxations.

Difficulty

Weak duality is easy: each Held–Karp bound is at most the cost of every tour, and the same argument with fractional $x$ bounds it by the subtour bound. The other direction is not a direct computation. It needs LP duality applied to (7.2) with the degree equations at $v\ne v_1$ moved into the objective, plus the fact that the remaining system (7.7) is integral, which is a spanning-tree polytope statement (Theorem 8.8 restricted to a face). Without integrality of (7.7), the dual of (7.2) gives only a fractional 1-tree bound.

The infeasible case needs separate care: when (7.1) has no solution but $G$ has 1-trees, the supremum over $y$ must be shown to be $+\infty$, which is a Farkas-type argument, not an optimal dual solution. In the feasible case the goal also asks for an optimal $y$, so a limiting argument is not enough: the dual optimum must be attained.

Formalization scope

Graphs are a structure Graph V E with ends : E → Sym2 V, so parallel edges and loops are expressible; paths, circuits, forests and tours follow the book's definitions (§2.1, §7.1). Optimal values (the subtour bound, the 1-tree bound, the Held–Karp bound, the value of (7.7)) are in EReal, with $+\infty$ for an empty feasible set; the optimal Held–Karp bound is ⨆ y : V → ℝ, with attainment stated as a second clause of the goal. $|S|-1$ and $|V|-2$ are computed in $\mathbb R$. $G\setminus v_1$ is encoded through edge sets of $G$ avoiding $v_1$.

Section 7.1 models the TSP on a complete graph, while the boxes of §7.3 take "a graph"; the statements here cover every finite graph satisfying the stated loop condition, which includes the complete case. Three printed statements are corrected. Theorem 7.2 assumes $G$ loopless: a loop lies in no cut, so (7.1) can set it to 1, and a loop of negative cost on a triangle makes the subtour bound $-1$ while every Held–Karp bound is $0$. The equivalence of (7.1) with (7.2) assumes every loop is at $v_1$, since (7.4) forces a loop elsewhere to 0. The constraint (7.4) is imposed for nonempty $S$ only, since at $S=\emptyset$ it reads $0\le-1$. The two lower-bound boxes fail only on a single node with a loop, which is a tour of length 1; they assume $G$ has no loop or at least two nodes. (7.7) assumes no loop at $v_1$.

A complete development needs LP duality or Farkas' lemma for finite systems (on the platform as MatousekLP.Duality.duality_theorem), Theorem 8.8, and the graph-theoretic facts that a tour minus the two edges at $v_1$ is a spanning tree of $G\setminus v_1$. Proofs of any milestone, and of the spanning-tree polytope as a face of the forest polytope, are welcome.

Selected references

• W. J. Cook, W. H. Cunningham, W. R. Pulleyblank, A. Schrijver, Combinatorial Optimization, Wiley, 1998, §7.3 and §8.1. https://doi.org/10.1002/9781118033142
• M. Held, R. M. Karp, The traveling-salesman problem and minimum spanning trees, Operations Research 18 (1970), 1138–1162. https://doi.org/10.1287/opre.18.6.1138
• M. Held, R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971), 6–25. https://doi.org/10.1007/BF01584070
• G. Dantzig, R. Fulkerson, S. Johnson, Solution of a large-scale traveling-salesman problem, Operations Research 2 (1954), 393–410. https://doi.org/10.1287/opre.2.4.393
• J. Edmonds, Matroids and the greedy algorithm, Mathematical Programming 1 (1971), 127–136. https://doi.org/10.1007/BF01584082

Limiting the size of a loss, not its probability

A probability constraint in a stochastic linear program asks that a random linear inequality hold with high probability. It counts every violation the same, however large, and the feasible set it defines is in general not convex, as Klein Haneveld's examples show (Klein Haneveld 1986). Integrated chance constraints replace the probability of a shortfall with its expected size. That single change gives convex feasible sets under no distributional assumption beyond existence of expected values. The models are due to Klein Haneveld, and were investigated further by Klein Haneveld and van der Vlerk, whose paper is the source of the polyhedral representations (2006). This mission formalizes the treatment in Kall and Mayer, Stochastic Linear Programming (2005), Chapter 2, §4.1, which is one of a series of missions on that book.

Setting

Let $\xi$ be a random vector with values in $\Xi$ and law $P$. Let $T(\xi)$ be a random $s\times n$ matrix, $h(\xi)\in\mathbb R^s$ a random vector, and, for a decision $x\in\mathbb R^n$,

$$\zeta(x,\xi)=T(\xi)x-h(\xi).$$

Write $z^+=\max\{0,z\}$ and $z^-=\max\{0,-z\}$, componentwise on vectors. Throughout, the expected values of $T(\xi)$ and $h(\xi)$ exist.

When $s=1$, write $\zeta(x,\xi)=t(\xi)^{\mathrm T}x-h(\xi)$. The separate integrated probability functions are

$$K(x)=\mathbb E_\xi[\zeta^+(x,\xi)],\qquad H(x)=\mathbb E_\xi[\zeta^-(x,\xi)].$$

For general $s$, the joint integrated probability functions are

$$K_J(x)=\mathbb E_\xi\big[\max_{1\le i\le s}\zeta_i^+(x,\xi)\big],\qquad H_J(x)=\mathbb E_\xi\big[\max_{1\le i\le s}\zeta_i^-(x,\xi)\big].$$

A variant fixes $\alpha$ and bounds the expected positive part by the fraction $\alpha$ of $\mathbb E_\xi[|\zeta|]$. With $\bar t=\mathbb E_\xi[t(\xi)]$ and $\bar h=\mathbb E_\xi[h(\xi)]$ it leads to the evaluation function

$$K_\alpha(x)=\alpha(\bar t x-\bar h)+(1-2\alpha)\mathbb E_\xi[\zeta^+(x,\xi)].$$

A finite discrete distribution has realizations $\hat\xi^1,\dots,\hat\xi^N$ with probabilities $p_k>0$, $\sum_k p_k=1$. Write $T^k=T(\hat\xi^k)$, $h^k=h(\hat\xi^k)$, let $t^k_i$ be the $i$-th row of $T^k$, and let $\mathcal N=\{1,\dots,N\}$.

Formalization targets

Goal: Theorem 4.3

For a finite discrete distribution and $\gamma\ge 0$, the set $\mathcal S_J(\gamma)=\{x\mid K_J(x)\le\gamma\}$ is polyhedral, and with $\mathcal I=\{1,\dots,s\}$,

$$\{x\mid K_J(x)\le\gamma\}=\bigcap_{\mathcal K\subset\mathcal N}\ \bigcap_{l\in\mathcal I^{\mathcal K}}\Big\{x\ \Big|\ \sum_{k\in\mathcal K}p_k\big(t^k_{l_k}x-h^k_{l_k}\big)\le\gamma\Big\}.$$

Milestones

1. Proposition 4.1. If $\mathbb E[\vartheta]$ exists, then $\mathbb E[(\vartheta-z)^+]=\int_z^\infty(1-F_\vartheta(t))\,dt$ and $\mathbb E[(\vartheta-z)^-]=\int_{-\infty}^zF_\vartheta(t)\,dt$.
2. Proposition 4.2. $H$, $K$ and $\mathbb E_\xi[|\zeta|]=H+K$ are convex on $\mathbb R^n$.
3. Theorem 4.1. For a finite discrete distribution and $\gamma\ge 0$, $\{x\mid K(x)\le\gamma\}=\bigcap_{\mathcal K\subset\mathcal N}\{x\mid\sum_{k\in\mathcal K}p_k(t^kx-h^k)\le\gamma\}$, and this set is polyhedral.
4. (4.13)–(4.15). Three equivalent forms of the $\alpha$-variant, the identity $K_\alpha=(1-\alpha)K-\alpha H$, and convexity for $\alpha<\tfrac12$, concavity for $\alpha>\tfrac12$, affinity for $\alpha=\tfrac12$.
5. Theorem 4.2. For a finite discrete distribution and $\alpha\in[0,\tfrac12]$, the set $\{x\mid K_\alpha(x)\le 0\}$ is polyhedral with the analogous representation.
6. Proposition 4.3. $H_J$ and $K_J$ are convex on $\mathbb R^n$.

Significance

The convexity results say that an expected-shortfall constraint can be added to a convex program with no assumption on the distribution, and with a random technology matrix. This is in sharp contrast with probability functions, whose generalized concavity needs restrictive assumptions and fails for finite discrete distributions in general. The polyhedral representations go further: for scenario models, integrated chance constraints are finitely many linear inequalities, $2^N-1$ in the separate case and $(s+1)^N-1$ in the joint case. Inequalities of this form are what a dual decomposition method generates one at a time.

All results here are proved in the literature. The mission contributes machine-checked versions of them, in a shared development with the other missions on this book. No formalization of integrated chance constraints was found on the platform when this mission was drafted.

Difficulty

The representations rest on one elementary observation: a sum of positive parts is a maximum over subsets, and a maximum over $i$ inside a sum is a maximum over tuples. The work is in the passage from the expectation, which is a Bochner integral against a sum of Dirac measures, to the finite sum, and in exhibiting the intersection as a single matrix inequality.

The tail formulas of Proposition 4.1 require more. The book's proof is an integration by parts for Stieltjes integrals, and it needs the limits $yP(\vartheta>y)\to 0$ and $xF_\vartheta(x)\to 0$ at infinity. Reusing a layer-cake formula on $(\vartheta-z)^+$ avoids this, but it does not avoid working out the two improper integrals and proving that they exist.

The convexity statements are not pointwise statements alone. Passing from pointwise convexity to the expectation needs integrability of each integrand, which has to be derived from integrability of the entries of $T(\xi)$ and $h(\xi)$; the Bochner integral of a non-integrable function is $0$, so this step cannot be skipped.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ, with $0$-based indices. The law of $\xi$ is a probability measure P on a measurable space Ξ. The book's affine form of $T(\xi)$ and $h(\xi)$ is not used in the chapter, so T and h are arbitrary functions with integrable entries; the book's case is Ξ = ℝʳ. Positive and negative parts are written max 0 z and max 0 (-z). The finite discrete law is discreteLaw, the sum of ENNReal.ofReal (p k) • Measure.dirac (ξhat k), and K, KJ, KAlpha are expectations against it: the finite sums (4.8) and (4.20) are consequences, not definitions, which rules out a trivial formalization. The maximum over rows is Finset.sup' over the nonempty Fin s, so $s\ge 1$ has no junk value at $s=0$. A polyhedral set is IsPolyhedron from the published development VanderbeiLP.StrictComp: a finite system $Ax\le b$, with $m=0$ allowed.

Theorem 4.2 is stated with $\alpha\in[0,\tfrac12]$. The book's printed hypothesis "$\gamma\ge 0$, $\mathcal S(\gamma)$" is copied from Theorem 4.1, and the representation fails for $\alpha>\tfrac12$.

A complete development needs a tail formula for expectations, integrability of finite maxima of integrable functions, and integration against finite sums of Dirac measures. Those facts are reusable in the other missions on this book. Contributions of any of the milestones are welcome, in any order; Theorem 4.3 depends on none of the convexity results.

Selected references

• P. Kall and J. Mayer, Stochastic Linear Programming: Models, Theory, and Computation, Kluwer/Springer, 2005, Chapter 2, §4.1. https://doi.org/10.1007/b105472
• W. K. Klein Haneveld, Duality in Stochastic Linear and Dynamic Programming, Lecture Notes in Economics and Mathematical Systems 274, Springer, 1986. https://doi.org/10.1007/978-3-642-51697-9
• W. K. Klein Haneveld and M. H. van der Vlerk, Integrated chance constraints: reduced forms and an algorithm, Computational Management Science 3 (2006), 245–269. https://doi.org/10.1007/s10287-005-0007-3

Motivation

A two-stage stochastic linear program models a decision taken before uncertain data are revealed, followed by a corrective (recourse) decision taken afterwards. Production planning under uncertain demand, capacity expansion under uncertain loads and network design under uncertain traffic all have this form. The first-stage decision $x$ is chosen now; once the random vector $\xi$ is observed, a second-stage linear program repairs any infeasibility at minimal cost. The quantity the planner minimizes is the first-stage cost plus the expected cost of the repair, the expected recourse $\mathcal Q(x)$.

Before any algorithm for such a problem can be justified (cutting planes, decomposition, bounding by discrete approximations), one needs to know that the objective is a sensible function: finite, convex and Lipschitz continuous. For a finite number of scenarios this is classical linear programming. For a general distribution of $\xi$ it requires an integrability argument. This mission formalizes that foundation as it is presented in Chapter 3, §2.1 of Kall and Mayer's textbook (Kall & Mayer 2005, ISBN 0-387-23385-7). The results go back to Wets (Wets 1974) and Walkup and Wets (1967) and are standard material in every stochastic programming textbook.

Setting

Let $\xi$ be a random vector in $\mathbb R^r$ with distribution $\mathbb P_\xi$, and let $\Xi=\operatorname{supp}\mathbb P_\xi$ be its support, the smallest closed set of probability one. The second-stage data depend affinely on $\xi$ (equation (2.1)):

$$T(\xi)=T+\sum_{j=1}^r T^j\xi_j,\qquad h(\xi)=h+\sum_{j=1}^r h^j\xi_j,\qquad q(\xi)=q+\sum_{j=1}^r q^j\xi_j,$$

with $T(\xi)\in\mathbb R^{m_2\times n_1}$, $h(\xi)\in\mathbb R^{m_2}$, $q(\xi)\in\mathbb R^{n_2}$. The recourse matrix $W\in\mathbb R^{m_2\times n_2}$ is deterministic (fixed recourse). For a first-stage decision $x\in\mathbb R^{n_1}$ the recourse function is the optimal value of the second-stage LP

$$Q(x;T(\xi),h(\xi),q(\xi))=\min\{q^{\mathsf T}(\xi)y\mid Wy=h(\xi)-T(\xi)x,\ y\ge 0\},$$

equal to $+\infty$ if the LP is infeasible and $-\infty$ if it is unbounded. The expected recourse is $\mathcal Q(x)=\int_\Xi Q(x;T(\xi),h(\xi),q(\xi))\,\mathbb P_\xi(d\xi)$.

Two assumptions are in force throughout:

• Assumption 2.1 (complete fixed recourse): $\{Wy\mid y\ge 0\}=\mathbb R^{m_2}$, so the second-stage LP is feasible for every $x$ and every $\xi$;
• Assumption 2.2: $\{u\mid W^{\mathsf T}u\le q(\xi)\}\neq\emptyset$ for every $\xi\in\Xi$, so the second-stage LP is dual feasible on the support.

The standing moment assumption is $\xi\in L^2$.

Formalization targets

Goal: Theorem 2.3

Under Assumptions 2.1 and 2.2 and $\xi\in L^2$:

$$\mathcal Q(x)\in\mathbb R\ \text{for every }x,\qquad \mathcal Q\ \text{is convex},\qquad |\mathcal Q(x^{(1)})-\mathcal Q(x^{(2)})|\le L\,\|x^{(1)}-x^{(2)}\|\ \text{for some }L .$$

The constant $L$ is not fixed: the statement asserts only that one exists, so the goal does not depend on any particular bound.

Milestones

1. Lemma 2.1: complete recourse holds if and only if $\operatorname{rank}W=m_2$ and the system $Wy=0$, $y_{i_k}\ge 1$, $y\ge 0$ is feasible for a set of $m_2$ linearly independent columns.
2. Lemma 2.2: for every $x$ there is an optimal recourse $y(\cdot)\in L^2$ with $Q(x;\xi)=q^{\mathsf T}(\xi)y(\xi)$ on $\Xi$.
3. Theorem 2.1: $Q(\cdot;\xi)$ is finite, convex and Lipschitz with a constant $D(\xi)\in L^1$.
4. Lemma 2.3: if $\min\{c^{\mathsf T}x\mid Ax=b,x\ge 0\}$ is solvable for every $b$, its value $\varphi$ is convex and $\partial\varphi(b)$ is the set of optimal dual solutions.
5. Theorem 2.2: $\partial_xQ(\hat x;\xi)=\{-T^{\mathsf T}(\xi)\hat u\mid\hat u\ \text{dual optimal}\}$.
6. Corollary 2.1: the conclusions of Theorem 2.3 hold with $\xi\in L^1$ when $q(\xi)$ and $(h(\xi),T(\xi))$ are independent.
7. Proposition 2.1: with deterministic $q$, $\xi\mapsto Q(x;T(\xi),h(\xi))$ is convex.
8. Theorem 2.4: with deterministic $q$, $Q(x;T(\bar\xi),h(\bar\xi))\le\mathcal Q(x)$ for $\bar\xi=\mathbb E\xi$ (the Jensen lower bound).

Significance

Theorem 2.3 makes the deterministic equivalent $\min\{c^{\mathsf T}x+\mathcal Q(x)\mid Ax=b,\ x\ge 0\}$ a convex program with a Lipschitz objective. Convexity gives that local minima are global and that subgradient-based and cutting-plane methods apply; Lipschitz continuity bounds the subgradients and controls the error of approximating $\mathcal Q$. Theorem 2.2 identifies those subgradients as dual solutions of the second-stage LP, which is how the L-shaped method generates its cuts. Proposition 2.1 and Theorem 2.4 give the Jensen lower bound, the starting point for the successive discrete approximation methods developed later in the chapter.

All results here are classical and proved in the source. None of them, to our knowledge, is formalized for a general (not finitely supported) distribution. Related platform items treat finitely many scenarios or other conventions. The work of this mission is to formalize the known proofs. The parametric LP facts (the value function of an LP is piecewise linear on finitely many bases, the dual characterization of its subdifferential) are reusable far beyond stochastic programming.

Difficulty

For finitely many scenarios, each claim reduces to finitely many LPs. The general case has two obstacles. First, measurability and integrability: $\mathcal Q(x)$ is an integral of an extended-real function. One must show that $\xi\mapsto Q(x;\xi)$ is measurable and that it is integrable, and the second needs a growth bound. On each decision region $Q(x;\xi)=q_B(\xi)^{\mathsf T}B^{-1}(h(\xi)-T(\xi)x)$ is quadratic in $\xi$, so $\xi\in L^1$ is not enough in general; this is why $L^2$ (or independence, Corollary 2.1) is assumed. Second, the Lipschitz constant must be integrable: a constant uniform in $\xi$ does not exist when $q$ and $T$ are random, so the pointwise constant $D(\xi)$ of Theorem 2.1 must itself be shown to be in $L^1$. Lemma 2.2's measurable optimal selection has the same character: an optimal $y(\xi)$ exists for each $\xi$, but building a measurable, square-integrable selection requires the finite partition of $\Xi$ into decision regions.

Formalization scope

Vectors are Fin k → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. The distribution $\mathbb P_\xi$ is a probability measure μ on Fin r → ℝ (the canonical space, $\xi$ the identity), and $\Xi$ is μ.support. $\xi\in L^2$ is MemLp id 2 μ, $\xi\in L^1$ is Integrable id μ. The recourse function is an EReal infimum, so $\pm\infty$ are represented exactly. The expected recourse is the Bochner integral of its real part, and the goal states explicitly that the recourse value is finite almost surely and integrable, so the real-valued encoding hides no divergent integral. Lipschitz bounds use the Euclidean norm. Finiteness in Theorems 2.1 and 2.3 is stated for every $x\in\mathbb R^{n_1}$, which contains the book's $x\in B_1$.

Reused published definitions: KallMayer.Recourse.LPValue (with SolvableEveryRHS, DualOptimizers), CompleteRecourse, PointwiseRecourse, ExpectedRecourse, and the subdifferential StochasticProg.RecourseKKT.subdifferential. The mission adds only the affine data structure (2.1). Contributions of reusable lemmas are welcome: the finite basis decomposition of an LP value function, measurability of LP value functions in the data, and the chain rule for subdifferentials under affine maps.

Selected references

• P. Kall and J. Mayer, Stochastic Linear Programming: Models, Theory, and Computation, Kluwer/Springer, International Series in Operations Research & Management Science 80, 2005, Chapter 3, §2.1, pp.198–211. ISBN 0-387-23385-7
• R. J.-B. Wets, Stochastic programs with fixed recourse: the equivalent deterministic program, SIAM Review 16 (1974), 309–339. https://doi.org/10.1137/1016053
• D. W. Walkup and R. J.-B. Wets, Stochastic programs with recourse, SIAM Journal on Applied Mathematics 15 (1967), 1299–1314. https://doi.org/10.1137/0115113
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Why matroids and the Greedy Algorithm

The Greedy Algorithm builds a set one element at a time, always adding the heaviest element that keeps the set feasible. For the forests of a graph it finds a maximum-weight forest (Kruskal's algorithm), but for the matchings of a graph it can fail: on a 4-cycle with edge weights 9, 7, 8, 3 it picks the edges of weight 9 and 3 when the edges of weight 7 and 8 are better. Matroids are the abstraction of the families on which greedy works. They were introduced by Whitney (1935); the optimality of greedy on matroids is due to Rado (1957) and was rediscovered by Edmonds (1970), who also gave the linear description of the convex hull of independent sets that is the goal of this mission.

This mission formalizes §8.1 of Cook, Cunningham, Pulleyblank and Schrijver, Combinatorial Optimization (Wiley, 1998), pp. 273–280. It is the twelfth mission of a series on the book; later missions treat matroid intersection (§8.3) and the matroid intersection polytope (§8.5), which build on the objects defined here.

Timeline:

• 1935: Whitney defines matroids as an abstraction of linear independence.
• 1957: Rado shows that the greedy algorithm finds a maximum-weight independent set of a matroid.
• 1970–1971: Edmonds proves that the polytope $\{x \ge 0 : x(A) \le r(A)\}$ is the convex hull of independent sets, and that greedy optimality characterizes matroids.

Setting

Let $S$ be a finite set and $\mathcal I$ a family of subsets of $S$, the independent sets. The pair $M=(S,\mathcal I)$ is a matroid if

• (M0) $\emptyset \in \mathcal I$;
• (M1) if $J' \subseteq J \in \mathcal I$ then $J' \in \mathcal I$;
• (M2) for every $A \subseteq S$, every maximal independent subset of $A$ has the same cardinality.

A pair satisfying (M0) and (M1) only is an independence system. A maximal independent subset of $A$ is a basis of $A$; its size is the rank $r(A)$. The bases of $S$ are the bases of $M$.

For weights $c \in \mathbb R^S$ the weight of $J$ is $c(J)=\sum_{e\in J} c_e$, and for $x \in \mathbb R^S$ and $A \subseteq S$, $x(A)=\sum_{e\in A} x_e$. The characteristic vector $\chi^J$ of $J \subseteq S$ has $\chi^J_e = 1$ for $e \in J$ and $0$ otherwise.

The Greedy Algorithm: set $J=\emptyset$; while there is $e \notin J$ with $c_e>0$ and $J\cup\{e\}\in\mathcal I$, choose such an $e$ with $c_e$ maximum and replace $J$ by $J\cup\{e\}$. Ties are broken arbitrarily.

The linear program attached to a matroid with rank function $r$ is

$$\text{maximize } \sum_{e\in S} c_e x_e \quad\text{subject to}\quad x(A)\le r(A)\ (A\subseteq S),\qquad x_e \ge 0\ (e\in S). \tag{8.1}$$

Formalization targets

Goal: Edmonds' Matroid Polytope Theorem (Theorem 8.5)

For every matroid $(S,\mathcal I)$ with rank function $r$,

$$\operatorname{conv}\{\chi^J : J \in \mathcal I\} = \{x \in \mathbb R^S : x \ge 0,\ x(A) \le r(A) \text{ for all } A \subseteq S\}.$$

Both inclusions are part of the goal.

Milestones

• Proposition 8.1 (matching matroid): for a graph $G=(V,E)$, the sets $J\subseteq V$ covered by some matching are the independent sets of a matroid on $V$.
• Theorem 8.2: on a matroid, the Greedy Algorithm returns a maximum-weight independent set, for every $c\in\mathbb R^S$.
• Theorem 8.3: an independence system is a matroid if and only if the Greedy Algorithm returns an optimal independent set for every $c \in \mathbb R^S$.
• Theorem 8.4: the characteristic vector of the greedy set is an optimal solution of (8.1).
• Corollary 8.6: an independent set $J$ is maximum-weight iff (a) $c_e \ge 0$ for $e\in J$, (b) $c_e\le 0$ when $e\notin J$ and $J\cup\{e\}\in\mathcal I$, (c) $c_e\le c_f$ when $e\notin J$, $f\in J$ and $(J\cup\{e\})\setminus\{f\}\in\mathcal I$.
• Corollary 8.7: a basis $J$ is a maximum-weight basis iff condition (c) holds.

Significance

The Matroid Polytope Theorem turns the combinatorial problem of finding a maximum-weight independent set into a linear program over an explicit inequality system, and it is the prototype for the polyhedral descriptions that follow in the book: the forest polytope (Theorem 8.8), from which the spanning-tree description of Theorem 2.8 follows, and the matroid intersection polytope (Theorem 8.20). Theorem 8.3 characterizes matroids by an algorithmic property, which is why matroids appear wherever greedy methods are analysed. Corollaries 8.6 and 8.7 give local certificates of optimality, used in Section 8.5 for weighted matroid intersection.

All results are classical and proved in the book. None is formalized on Prove2Me, and Mathlib, which has a substantial Matroid library (bases, rank, closure, duality), contains neither the greedy theorem nor the matroid polytope. A formalization supplies the polyhedral layer missing from that library and the bridge between the axioms (M0)–(M2) and linear programming.

Difficulty

The inclusion of the convex hull in the polyhedron is immediate: $\chi^J(A)=|J\cap A|\le r(A)$. The reverse inclusion is the content, and the obvious attempt, writing a feasible $x$ directly as a convex combination of characteristic vectors, has no evident inductive structure: the constraint system has one inequality per subset of $S$, and a fractional $x$ can be tight on many overlapping sets at once. Any route has to relate the exponential system $x(A)\le r(A)$ to the combinatorics of (M2), and has to pass from statements about linear objectives to an equality of sets in $\mathbb R^S$; Mathlib contains neither LP duality for such a system nor the polytope-theoretic facts linking optimal vertices to convex hulls in the form needed.

For Theorem 8.3 the nontrivial direction is the converse: if (M2) fails on some set $A$, one must produce weights for which greedy goes wrong, and the formal statement must account for the nondeterminism of tie-breaking.

Formalization scope

• The ground set $S$ is a finite type α; subsets are Finset α; the family $\mathcal I$ is a predicate I : Finset α → Prop. (M0)–(M1) are the published definition SubsamplingSM.Offline.IsIndepSystem; IsMatroid adds (M2) literally (any two bases of the same set have the same size). This is the book's axiom system, not Mathlib's Matroid, to which it can be bridged.
• rank I A is the largest size of an independent subset of $A$, which for a matroid is the size of every basis of $A$.
• Vectors live in α → ℝ; constraints of (8.1) are imposed for every subset $A$; the rank is cast to ℝ.
• The Greedy Algorithm is a relation: GreedyStep allows every admissible choice among ties, and IsGreedyOutput is any set reachable from $\emptyset$ at which the loop stops. Theorems 8.2 and 8.4 are stated for every run. Theorem 8.3 is stated in both readings (every run, some run), which covers every tie-breaking rule.
• Graphs are finite multigraphs (ends : E → Sym2 V), loops and parallel edges allowed; matchings contain no loops.
• Trivial cases are not excluded: the empty ground set and loops of the matroid ($r(\{e\})=0$, forcing $x_e=0$) are covered by the statements.

Useful contributions: a bridge from IsMatroid to Mathlib's IndepMatroid/Matroid (which gives rank submodularity and exchange properties), LP weak duality and complementary slackness for (8.1), and a lemma reducing equality of a polytope with a convex hull to optimality of hull points for every linear objective. These are reusable in the matroid intersection missions of this series.

Selected references

• W. J. Cook, W. H. Cunningham, W. R. Pulleyblank, A. Schrijver, Combinatorial Optimization, Wiley-Interscience, 1998, §8.1. https://doi.org/10.1002/9781118033142
• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications (Gordon and Breach, 1970), 69–87. https://doi.org/10.1007/3-540-36478-1_2
• J. Edmonds, Matroids and the greedy algorithm, Mathematical Programming 1 (1971), 127–136. https://doi.org/10.1007/BF01584082
• R. Rado, A note on independence functions, Proceedings of the London Mathematical Society 7 (1957), 300–320. https://doi.org/10.1112/plms/s3-7.1.300
• H. Whitney, On the abstract properties of linear dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182

Motivation

Many combinatorial optimization problems ask for a largest set that is simultaneously "independent" in two different senses. A matching in a bipartite graph $G=(V,E)$ with bipartition $\{V_1,V_2\}$ is a set of edges in which every node of $V_1$ meets at most one edge and every node of $V_2$ meets at most one edge. A branching of a digraph is an arc set that is a forest in the underlying graph and has each node as the head of at most one arc. Each condition on its own defines a matroid, a structure for which the greedy algorithm is optimal. The matroid intersection problem asks for a maximum common independent set of two matroids on the same ground set.

Edmonds (Edmonds 1970) proved that the maximum size of a common independent set is given by a min–max formula in terms of the two rank functions, and gave a polynomial-time algorithm. The theorem contains König's theorem on bipartite matchings as the special case of two partition matroids. This mission formalizes §8.2–8.3 of Cook, Cunningham, Pulleyblank and Schrijver, Combinatorial Optimization (Wiley, 1998), which develops this result from the matroid axioms. It is the thirteenth mission of a series covering the book's capstone theorems; the twelfth treats the matroid polytope and the fourteenth the matroid intersection polytope.

Timeline:

• 1935: Whitney introduces matroids.
• 1965: Edmonds and Fulkerson show that matching matroids are transversal matroids.
• 1970: Edmonds proves the Matroid Intersection Theorem and the intersection polytope theorem ("Submodular functions, matroids, and certain polyhedra").
• 1975: Lawler's textbook gives the augmenting-path algorithm in the form used here; the auxiliary "exchange" digraph becomes standard.

Setting

Let $S$ be a finite set and $\mathcal I$ a family of subsets of $S$, called independent sets. The pair $M=(S,\mathcal I)$ is a matroid if (M0) $\emptyset\in\mathcal I$; (M1) subsets of independent sets are independent; (M2) for every $A\subseteq S$, every maximal independent subset of $A$ has the same cardinality. A maximal independent subset of $A$ is a basis of $A$, and its size is the rank $r(A)$. A circuit is a minimal dependent set.

For a matroid $M$, a set $B\subseteq S$ and a basis $J$ of $B$, the contraction $M/B$ has ground set $S\setminus B$ and independent sets $\{J'\subseteq S\setminus B : J'\cup J\in\mathcal I\}$.

Two matroids $M_1=(S,\mathcal I_1)$ and $M_2=(S,\mathcal I_2)$ on the same set $S$ have rank functions $r_1,r_2$; a set in $\mathcal I_1\cap\mathcal I_2$ is a common independent set. For $A\subseteq S$ write $\bar A=S\setminus A$.

Given a common independent set $J$, the auxiliary digraph $G(M_1,M_2,J)$ has node set $S\cup\{r,s\}$ and arcs: $es$ for $e\notin J$ with $J\cup\{e\}\in\mathcal I_1$; $re$ for $e\notin J$ with $J\cup\{e\}\in\mathcal I_2$; $ef$ for $e\notin J$, $f\in J$ with $J\cup\{e\}\notin\mathcal I_1$ and $(J\cup\{e\})\setminus\{f\}\in\mathcal I_1$; and $fe$ for $e\notin J$, $f\in J$ with $J\cup\{e\}\notin\mathcal I_2$ and $(J\cup\{e\})\setminus\{f\}\in\mathcal I_2$. A chord of a dipath with node sequence $v_0,\dots,v_k$ is an arc $v_iv_j$ with $i<j-1$.

Formalization targets

Goal: Theorem 8.14 (Matroid Intersection Theorem)

$$\max\{|J| : J\in\mathcal I_1\cap\mathcal I_2\}=\min\{r_1(A)+r_2(\bar A) : A\subseteq S\}.$$

Both matroids are arbitrary (loops allowed, any ranks), and $S$ may be empty.

Milestones

• Theorem 8.9. For $J\in\mathcal I$ and $e\in S$, $J\cup\{e\}$ contains at most one circuit.
• Theorem 8.11. $M/B$ is a matroid, does not depend on the choice of the basis $J$ of $B$, and has rank function $r'(A)=r(A\cup B)-r(B)$ for $A\subseteq S\setminus B$.
• Weak duality (§8.3). For $J\in\mathcal I_1\cap\mathcal I_2$ and $A\subseteq S$, $|J|\le r_1(A)+r_2(\bar A)$.
• Theorem 8.15 (Augmenting Path Theorem). (a) If $G(M_1,M_2,J)$ has no $(r,s)$-dipath, $J$ is maximum, and every $A\subseteq S$ with no arc leaving $A\cup\{r\}$ satisfies $|J|=r_1(A)+r_2(\bar A)$. (b) If there is an $(r,s)$-dipath, $J$ is not maximum, and for a chordless $(r,s)$-dipath $r,e_1,f_1,\dots,e_{m+1},s$, $J\,\triangle\,\{e_1,f_1,\dots,e_{m+1}\}\in\mathcal I_1\cap\mathcal I_2$.
• Lemma 8.16. If $e\in C\subseteq A$ and $C$ is a circuit, then $r(A\setminus\{e\})=r(A)$.

Significance

The Matroid Intersection Theorem is one of the main min–max theorems of combinatorial optimization. It contains König's theorem (two partition matroids), the characterization of maximum branchings, and Rado's theorem on independent transversals, and it is the cardinality case of the weighted matroid intersection theory of §8.5, whose polyhedral form is the subject of the next mission. The Augmenting Path Theorem turns the min–max formula into an algorithm with polynomially many independence tests, and its part (a) gives the optimality certificate $A$ explicitly.

All results of this mission are classical and fully proved in the book. Mathlib has a matroid library (circuits, fundamental circuits, contraction, rank), and it contains the uniqueness of the fundamental circuit (Matroid.IsCircuit.eq_fundCircuit_of_subset), which is Theorem 8.9 in Mathlib's language. To our knowledge Mathlib has neither the matroid intersection theorem nor the augmenting path theorem. The platform has an exchange-graph augmentation statement for shortest walks with oracles (CountingMatroid.Analysis.ShortestExchangeAugmentation.shortest_exchange_augmentation). That is a different statement: it covers shortest walks, while Theorem 8.15 covers chordless dipaths and also the certificate of part (a). The work here is to formalize the book's proofs or to bridge the book's axiomatic matroids to Mathlib's library.

Difficulty

Weak duality takes one line. The other inequality does not follow from any local exchange argument. The book gives two proofs: a short induction on $|S|$ that contracts and deletes one element and then applies submodularity of the rank functions, and the algorithmic proof through Theorem 8.15. In part (b), symmetric difference along an arbitrary augmenting dipath can destroy independence. Chordlessness is what lets the circuit-by-circuit argument with Lemma 8.16 go through, and the book's Exercise 8.37 shows the condition cannot be dropped. Part (a) needs, for each element outside $J$, the unique circuit of Theorem 8.9 to lie inside the right side of the cut.

Formalization scope

The ground set is a finite type S, all of which is the ground set. A matroid is the structure CombOpt.MatroidIntersection.Matroid S: a predicate Indep : Finset S → Prop bundled with the axioms (M0)–(M2) (IsMatroid). (M2), maximal independent subsets (IsMaxIndepIn) and circuits (IsCircuit) reuse the published definitions of the Edmonds matroid-partition mission (EdmondsPartition.Main), which state the same notions. This is the book's axiom system, not Mathlib's _root_.Matroid; on finite ground sets the two describe the same matroids, and a bridge to Mathlib is welcome. rank Indep A is the size of a basis of A with values in ℕ; Ā is the complement Aᶜ. The contraction lives on the subtype {x // x ∉ B}, and its rank formula is stated as $r'(A)+r(B)=r(A\cup B)$, which avoids truncated subtraction. The auxiliary digraph is the arc relation auxArc M₁ M₂ J on nodes AuxNode S (r, s, elem e). A dipath is a node list (IsDipath), chordless means no arc $v_iv_j$ with $i+1<j$ (IsChordless), and the elements visited are innerElems.

The goal states existence of a pair $(J,A)$ with $|J|=r_1(A)+r_2(\bar A)$ together with weak duality for all pairs. A goal stating only one inequality, or only existence of some $J$ and $A$ without the inequality, would not be the theorem.

Contributions welcome: proofs of the milestones, the book's induction proof of Theorem 8.14 (which also needs submodularity of rank, Exercise 8.21), a proof through Theorem 8.15, and an equivalence between CombOpt.MatroidIntersection.Matroid and Mathlib's Matroid on finite types.

Selected references

• W. J. Cook, W. H. Cunningham, W. R. Pulleyblank, A. Schrijver, Combinatorial Optimization, Wiley-Interscience, 1998, §8.2–8.3. https://doi.org/10.1002/9781118033142
• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications (Gordon and Breach, 1970), 69–87; reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, 2003. https://doi.org/10.1007/3-540-36478-1_2
• E. L. Lawler, Matroid intersection algorithms, Mathematical Programming 9 (1975), 31–56. https://doi.org/10.1007/BF01681329
• H. Whitney, On the abstract properties of linear dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182