Operations Research

Motivation

Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision $x$ is fixed before an uncertain right-hand side $b$ is revealed, and a second-stage decision $y(b)$ is chosen after it, as a function of $b$. The objective protects against the worst $b$ in an uncertainty set $\mathcal U$. Computing an optimal fully adaptable solution is intractable in general (Feige, Jain, Mahdian and Mirrokni, IPCO 2007), so practitioners restrict the second stage to affine policies $y(b)=Pb+q$, introduced in robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004). An optimal affine policy is computed by a single convex program, but its cost may exceed the adaptive optimum.

Bertsimas and Goyal (Math. Program. Ser. A, 2012) quantify this loss. Earlier, Bertsimas, Iancu and Parrilo (Math. Oper. Res. 2010) proved affine policies optimal for a class of one-dimensional multistage problems. The present paper shows that affine policies are optimal when $\mathcal U$ is a simplex (Theorem 1), that they can lose a factor $\Omega(m^{1/2-\delta})$ in general (Theorem 3), and — the subject of this mission — that when the first-stage constraint matrix is nonnegative they never lose more than $3\sqrt m$ (Theorem 4). Nonnegative first-stage matrices occur in network design, facility location, capacity planning and other covering problems.

Setting

Let $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$, $c\in\mathbb R^{n_1}_+$, $d\in\mathbb R^{n_2}_+$, and let $\mathcal U\subseteq\mathbb R^m_+$ be convex, compact and full-dimensional. The problem $\Pi_{Adapt}(\mathcal U)$ is

$$z_{Adapt}(\mathcal U)=\min\; c^Tx+\max_{b\in\mathcal U}d^Ty(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ \ x\ge0,\ \ y(b)\ge0\quad\forall b\in\mathcal U,$$

where the minimum is over first-stage vectors $x$ and arbitrary maps $b\mapsto y(b)$. The problem is assumed feasible. The value $z_{Aff}(\mathcal U)$ is the same minimum restricted to affine second stages $y(b)=Pb+q$, which must still satisfy $Pb+q\ge0$ on $\mathcal U$.

For each coordinate $j$ put $\mu_j=\max\{b_j : b\in\mathcal U\}$ and fix a maximizer $\beta^j\in\mathcal U$ with $\beta^j_j=\mu_j$ (display (38)). The scaled sum of $b$ over an index set $J$ is $\sum_{j\in J}b_j/\mu_j$.

Algorithm $\mathcal A$ (Fig. 1 of the paper) starts with $J_1=\{1,\dots,m\}$ and $b^0=0$. While some $b\in\mathcal U$ has scaled sum over $J_1$ larger than $\sqrt m$, it picks a maximizer $u^k\in\mathcal U$ of that scaled sum, adds $u^k$ to the running vector on the coordinates of $J_1$, and moves to $J_2$ every coordinate $j$ whose running value has reached $\mu_j$. It returns the number of iterations $K$, the vectors $u^1,\dots,u^K$, their sum $\beta=u^1+\dots+u^K$, and the partition $J_1,J_2$.

In the $k$-uncertain variant (60)–(63), only $k$ right-hand sides $b\in\mathcal U\subseteq\mathbb R^k_+$ are uncertain and the remaining $m-k$ are fixed at $b^0$; all data are nonnegative. Its values are $z^k_{Adapt}(\mathcal U)$ and $z^k_{Aff}(\mathcal U)$.

Formalization targets

Goal: Theorem 4

If $A\ge0$ entrywise, then a feasible affine solution exists and

$$z_{Aff}(\mathcal U)\le 3\sqrt m\cdot z_{Adapt}(\mathcal U).$$

Milestones

1. $\mu_j>0$ for every $j$ (after (38)).
2. Lemma 9. For every complete run of Algorithm $\mathcal A$: $\sum_{j\in J_1}b_j/\mu_j\le\sqrt m$ for all $b\in\mathcal U$, and $b_j\le\beta_j$ for all $j\in J_2$ and $b\in\mathcal U$.
3. Lemma 10. Algorithm $\mathcal A$ executes at most $K\le2\sqrt m$ iterations.
4. Feasibility (48)–(55). For any feasible $(x^*,y^*)$, the solution $\tilde x=3\sqrt m\,x^*$, $\tilde y(b)=\sum_{j\in J_1}\frac{b_j}{\mu_j}y^*(\beta^j)+\hat y$ with $\hat y=\frac{2\sqrt m}{K}\sum_{k=1}^Ky^*(u^k)$ is feasible.
5. Cost (56)–(59). If $t$ bounds the worst-case cost of $(x^*,y^*)$, then $3\sqrt m\cdot t$ bounds that of $(\tilde x,\tilde y)$.

Companion results

• Algorithm $\mathcal A$ has a complete run when $\mathcal U$ is compact.
• Lemma 11. $z(\Pi_1)\le z^k_{Adapt}(\mathcal U)$ and $z(\Pi_2)\le z^k_{Adapt}(\mathcal U)$ for the uncertain and deterministic parts of the $k$-uncertain problem.
• Theorem 5. $z^k_{Aff}(\mathcal U)\le(3\sqrt k+1)\cdot z^k_{Adapt}(\mathcal U)$, the paper's $O(\sqrt k)$ bound with its proof's constant.
• Special case (39)–(45). If $\sum_{j=1}^m b_j/\mu_j\le\sqrt m$ on $\mathcal U$, then $z_{Aff}(\mathcal U)\le\sqrt m\cdot z_{Adapt}(\mathcal U)$.

Significance

Theorem 4 is an upper bound on the price of restricting to affine policies, and Theorem 3 of the same paper shows it is tight up to a constant factor: for every $\delta>0$ there are instances with $A\ge0$ where the gap is $\Omega(m^{1/2-\delta})$. Together they settle the order of the approximation ratio of affine policies for covering-type two-stage problems. Theorem 5 refines the bound to $O(\sqrt k)$ when only $k$ of the $m$ right-hand sides are uncertain, which is the regime of many applications. The construction is also the template for the paper's Theorem 6, a $4\sqrt m$-approximation for general $A$ obtained from a single dominating simplex.

The results are proved in the paper. To the knowledge of this mission, none of them has a machine-checked proof. Formalizing them produces a reusable model of two-stage adaptive linear programs with affine policies, a verified analysis of a greedy covering procedure (Algorithm $\mathcal A$), and an explicit-constant version of an $O(\cdot)$ statement.

Difficulty

The obvious attempt scales the fully adaptable solution at the extreme points $\beta^j$ linearly in $b$: $\tilde y(b)=\sum_j (b_j/\mu_j)\,y^*(\beta^j)$. This is feasible at cost factor $\sqrt m$ only when the scaled sums $\sum_j b_j/\mu_j$ stay below $\sqrt m$ on $\mathcal U$ (condition (39)); in general they can reach $m$, and the linear rule then costs a factor $m$. The difficulty is to handle the coordinates where $\mathcal U$ has large scaled mass. Algorithm $\mathcal A$ isolates them, and the delicate point is the iteration count: each round must add scaled mass above $\sqrt m$, while the total scaled mass that can be absorbed before every coordinate leaves $J_1$ is at most $2m$. A formal proof must also track the algorithm's state through its recursion, because the argmax choices are not unique and the statements must hold for every run.

Formalization scope

Vectors are Fin m → ℝ with the componentwise order, indices are 0-based, and matrices are Matrix (Fin m) (Fin n) ℝ. Nonnegativity of a matrix is stated entrywise. $z_{Adapt}$ and $z_{Aff}$ are infima of the set of worst-case cost bounds achieved by feasible solutions; the goal and Theorem 5 assert the existence of a feasible affine solution, which rules out the trivializing reading in which $z_{Aff}$ is the infimum of an empty set (Lean's junk value $0$) and the inequality holds for free. The goal does not mention $\mu$, $\beta^j$ or Algorithm $\mathcal A$; these appear only in milestones.

$\mu$ and $\beta^j$ are given with their defining properties ($\mu_j$ is the greatest value of $b_j$ on $\mathcal U$, and $\beta^j\in\mathcal U$ with $\beta^j_j=\mu_j$). Algorithm $\mathcal A$ is encoded as a recursion on a choice sequence $u$, with step 2(d) read as $J_1^k=\{j\in J_1^{k-1}: b^k_j<\mu_j\}$. A complete run requires the loop test and the argmax property at each iteration and the failure of the loop test at the end. The milestones on the constructed policy are stated for every feasible $(x^*,y^*)$ and every cost bound $t$, so that no attainment of the optimum is assumed.

Standing assumptions of (1) carried by the goal: $c,d\ge0$; $\mathcal U\subseteq\mathbb R^m_+$ convex, compact, with nonempty interior; feasibility. Milestones drop the ones they do not use. Theorem 5 carries compactness and full-dimensionality of $\mathcal U$, which §5.1 does not repeat but its proof uses through Theorem 4. Lemma 11 assumes that $z^k_{Adapt}(\mathcal U)$ is finite, since the paper's inequality is between extended reals.

A complete development needs: finite-dimensional linear programming facts (existence of optimal solutions is not needed), compactness arguments for the argmax in Algorithm $\mathcal A$, and manipulation of finite sums over Finset. The model of (1) and the analysis of Algorithm $\mathcal A$ are reusable by the companion mission on Theorem 6. Contributions of proofs of any milestone, and of supporting lemmas about the recursion of Algorithm $\mathcal A$, are welcome.

Selected references

• D. Bertsimas and V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Math. Program. Ser. A, 2012. https://doi.org/10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer and A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99(2), 351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu and P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Math. Oper. Res. 35(2), 363–394, 2010.
• U. Feige, K. Jain, M. Mahdian and V. Mirrokni, Robust combinatorial optimization with exponential scenarios, Lect. Notes Comput. Sci. 4513, 439–453, 2007.

Motivation

Two-stage adaptive optimization models decisions made in two steps: a first-stage decision is fixed before an uncertain parameter is revealed, and a second-stage (recourse) decision may then depend on the realized value. In the robust version, the uncertain parameter ranges over an uncertainty set and the objective is the worst-case cost. Such models arise in capacity planning, network design and inventory problems with uncertain demand, where the demand is the right-hand side of the constraints.

Computing an optimal fully adaptable second-stage policy is intractable in general: the recourse is an arbitrary function of the uncertain parameter. The standard tractable surrogate, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004), restricts the recourse to an affine policy $y(b) = Pb + q$, whose optimization is a finite convex program. Practitioners report that affine policies often perform well, which raises the question of when they are optimal and how much they can lose.

Bertsimas and Goyal (Math. Program. Ser. A, 2012) answer this for problems with an uncertain right-hand side. Their Theorem 1 shows that affine policies are optimal when the uncertainty set is a simplex, that is, the convex hull of $m+1$ affinely independent points of $\mathbb R^m_+$. Their Theorem 2, the subject of this mission, shows that this is almost tight: one additional extreme point can make the best affine policy almost twice as expensive as the optimum.

Setting

Let $A \in \mathbb R^{m\times n_1}$, $B \in \mathbb R^{m\times n_2}$, $c \in \mathbb R^{n_1}_+$, $d \in \mathbb R^{n_2}_+$ and let $\mathcal U \subseteq \mathbb R^m_+$ be an uncertainty set. The problem $\Pi_{\mathrm{Adapt}}(\mathcal U)$ is

$$z_{\mathrm{Adapt}}(\mathcal U)=\min\ c^{T}x+\max_{b\in\mathcal U} d^{T}y(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ \ x\ge 0,\ \ y(b)\ge 0\quad\forall b\in\mathcal U .$$

Here $x$ is the first-stage decision and $y : \mathcal U \to \mathbb R^{n_2}$ is the second-stage policy; all inequalities between vectors are componentwise. The value $z_{\mathrm{Aff}}(\mathcal U)$ is the same minimum restricted to affine policies $y(b) = Pb + q$ with $P \in \mathbb R^{n_2\times m}$ and $q \in \mathbb R^{n_2}$; an affine policy must still satisfy $Pb + q \ge 0$ for every $b \in \mathcal U$. Always $z_{\mathrm{Adapt}}(\mathcal U) \le z_{\mathrm{Aff}}(\mathcal U)$.

The instance $\mathcal I$ of (6) is defined for $\delta > 0$ and an even integer $m > 200/\delta^2$. It has $n_1 = n_2 = m$, $c = 0$, $d = (1,\dots,1)^T$, $A = 0$, and

$$B_{ij}=\begin{cases}1,& i=j,\\ 1/\sqrt m,& i\ne j,\end{cases}\qquad \mathcal U=\operatorname{conv}\{b^0,b^1,\dots,b^{m+2}\},$$

where $b^0 = 0$, $b^j = e_j$ is the $j$-th unit vector for $j = 1,\dots,m$, $b^{m+1}$ has entries $1/\sqrt m$ in its first $m/2$ coordinates and $0$ in the others, and $b^{m+2}$ has $0$ in its first $m/2$ coordinates and $1/\sqrt m$ in the others. Thus $\mathcal U$ is generated by $m+2$ nonzero points. The last two are also extreme points when $m\ge 6$; for $m=2$ or $4$ they lie in the convex hull of $0,e_1,\dots,e_m$.

For a permutation $\tau$ of $\{1,\dots,m\}$, write $x^\tau = (x_{\tau(1)},\dots,x_{\tau(m)})$. A set $U$ is permutation-invariant with respect to $\tau$ if $x \in U \iff x^\tau \in U$ (Definition 2), and $\Gamma$ is the set (10) of permutations with $i \le m/2 \iff \tau(i) \le m/2$.

Formalization targets

Goal: Theorem 2

$$z_{\mathrm{Aff}}(\mathcal U)>(2-\delta)\cdot z_{\mathrm{Adapt}}(\mathcal U)\qquad\text{for the instance }\mathcal I\text{ of (6), every }\delta>0\text{ and every even }m>200/\delta^2 .$$

Milestones

1. Lemma 1. On $\mathcal I$ there is a feasible fully adaptable solution with worst-case cost $1$, so $z_{\mathrm{Adapt}}(\mathcal U) \le 1$.
2. Lemma 2. The set $\mathcal U$ of (6) is permutation-invariant with respect to every $\tau \in \Gamma$.
3. Lemma 3. There is an optimal affine solution $\hat y(b) = \hat Pb + \hat q$ whose intercept is constant: $\hat q_i = \hat q_j$ for all $i, j$.
4. First Claim of the proof of Theorem 2. For any feasible affine solution with intercept $\hat q \equiv \beta$ and worst-case cost at most $2-\delta$: $\beta \le (2-\delta)/m$.
5. Second Claim. Under the same assumption, $\hat P_{jj} \ge 1 - 2/\sqrt m - 2/m$ for every $j$.
6. Third Claim. Under the same assumption, $\hat P_{ij} \ge -(2-\delta)/m$ for all $i, j$.

Significance

Together with Theorem 1 of the same paper, Theorem 2 delimits exactly where affine policies are optimal for right-hand-side uncertainty: for a simplex they are, and with one more nonzero extreme point the gap can approach $2$. The ratio is measured against the fully adaptable optimum, which is the quantity a practitioner gives up by choosing affine recourse. Later sections of the paper push the same construction to $m^{1/2-\delta}$ for sets with polynomially many extreme points and prove a matching $O(\sqrt m)$ upper bound; Theorem 2 is the simplest member of this family and isolates the mechanism.

The result is proved in the paper; to our knowledge it has not been machine-checked. The mission produces a formal model of two-stage adaptive linear optimization with uncertain right-hand side, the values $z_{\mathrm{Adapt}}$ and $z_{\mathrm{Aff}}$, and a verified lower-bound instance. The symmetrization statement (Lemma 3) is an instance of a general principle, that a convex problem invariant under a group has an invariant optimum, which is reusable well beyond this paper.

Difficulty

The upper bound $z_{\mathrm{Adapt}} \le 1$ requires a feasible policy, which can be written down. The lower bound on $z_{\mathrm{Aff}}$ is a statement about all affine policies, an $m^2 + m$ dimensional family, and cannot be checked policy by policy. The obvious attempt, testing an arbitrary affine policy against a few extreme points, fails because an asymmetric policy can trade cost between coordinates. The argument needs an optimal policy that is symmetric, which in turn needs both the existence of an optimal affine solution (attainment of a minimum over a non-compact set of policies) and the invariance of the instance under the permutations of $\Gamma$ and the swap of the two halves. Without the attainment step, a contradiction for every policy of cost at most $2-\delta$ yields only $z_{\mathrm{Aff}} \ge 2-\delta$, not the strict inequality.

Formalization scope

Vectors are Fin m → ℝ with the componentwise order, matrices are Matrix (Fin m) (Fin n) ℝ, $Bx$ is B *ᵥ x and $d^Ty$ is d ⬝ᵥ y. Indices are 0-based: the paper's coordinate $i$ is index $i - 1$, so "$i \le m/2$" is (i : ℕ) < m / 2, with natural-number division (exact since $m$ is even). $x^\tau$ is x ∘ τ for τ : Equiv.Perm (Fin m).

$z_{\mathrm{Adapt}}$ and $z_{\mathrm{Aff}}$ are the infima of the sets of real numbers $t$ for which some feasible (respectively feasible affine) solution satisfies $c^Tx + d^Ty(b) \le t$ for all $b \in \mathcal U$. This epigraph form avoids a supremum of a possibly unbounded function; on an infeasible instance the infimum would be Lean's junk value $0$, which is why Lemma 1 also asserts the existence of the feasible solution of cost $1$. Optimal solutions are stated by IsOptimalAff: feasible, with worst-case cost bounded by every bound achieved by any feasible affine solution. Affine policies must be nonnegative on $\mathcal U$, as in (1).

The instance is concrete, so the standing assumptions of (1) (nonnegative costs, compact convex full-dimensional $\mathcal U \subseteq \mathbb R^m_+$, feasibility) are properties of the data rather than hypotheses. The goal adds no hypothesis to the page: $\delta > 0$, $m$ even and $m > 200/\delta^2$. For $\delta \ge 2$ the statement is easy but still true. The three Claims are stated for any feasible affine solution with constant intercept and worst-case cost at most $2-\delta$, which is exactly what the paper's proof uses about the symmetric optimal solution under its contradiction hypothesis (12). Lemma 1 drops the unused hypothesis $m > 200/\delta^2$. Definition 2 prints "$x \in P \iff x^\tau \in P$"; the formalization reads $P$ as the set $U$.

Replacing $z_{\mathrm{Aff}}$ by the cost of one particular affine policy, stating the goal with $\ge$, or bounding only policies with constant intercept would not be Theorem 2, and is ruled out: the goal compares the two optimal values with a strict inequality.

A complete development needs convex hulls of finite point sets in Fin m → ℝ, the existence of a minimizer for the affine problem (a linear program in $(x, P, q)$ with infinitely many constraints indexed by $\mathcal U$, reducible to the extreme points), averaging of optimal solutions over a permutation group, and elementary estimates with $\sqrt m$. Contributions of general lemmas on attainment of semi-infinite linear programs and on symmetrization of convex programs are welcome.

Selected references

• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming Ser. A (online first 2011; received 31 Oct 2009, accepted 17 Jan 2011). https://doi.org/10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Mathematics of Operations Research 35 (2010) 363–394. https://doi.org/10.1287/moor.1100.0444

Motivation

A linear program is solved with data that, in practice, is rarely known exactly: coefficients come from measurements, estimates or forecasts. Robust optimization asks for a solution that remains feasible for every realization of the data in a prescribed uncertainty set, and among those the one with the best guaranteed objective value. Ben-Tal and Nemirovski introduced this framework for linear programming in Robust solutions of uncertain linear programs (Oper. Res. Lett. 25, 1999), following their treatment of robust convex optimization (Math. Oper. Res. 23, 1998) and Soyster's earlier work on inexact linear programming (Oper. Res. 21, 1973). The robust counterpart has since become the starting point of a large literature on uncertainty sets, budgets of uncertainty and adjustable policies.

A natural first objection is that the robust counterpart might be needlessly conservative: by demanding feasibility for all realizations simultaneously, it could be infeasible, or have a worse value, even when every individual realization is perfectly well behaved. This mission formalizes the paper's answer (§2.2): under two structural hypotheses, the robust counterpart is no worse than the worst realization.

Setting

Fix $c, f \in \mathbb R^n$ and write a linear program in the homogeneous form (6)

$$(P)\qquad \min\{c^{T}x \mid Ax \ge 0,\ f^{T}x = 1\},$$

where $A$ is a real $m\times n$ matrix and $Ax\ge0$ is componentwise. Every linear program can be put in this form. The matrix $A$ is uncertain: it is only known to lie in an uncertainty set $\mathcal U$ of $m\times n$ matrices. Each $A\in\mathcal U$ gives an instance $(P)$ with feasible set $\{x\mid Ax\ge0,\ f^{T}x = 1\}$ and optimal value $c^*(P)$; the family of instances is $\mathcal P$. The robust counterpart (7) is

$$(P_{\mathcal U})\qquad \min\{c^{T}x \mid x \in G_{\mathcal U}\},\qquad G_{\mathcal U} = \{x\mid Ax\ge0\ \ \forall A\in\mathcal U;\ f^{T}x = 1\},$$

and its optimal value is $c^*$. Since $G_{\mathcal U}$ does not change when $\mathcal U$ is replaced by its closed convex hull, the paper assumes throughout that $\mathcal U$ is convex and closed.

Let $\mathcal U_i\subseteq\mathbb R^n$ be the set of all realizations of the $i$-th row, the projection of $\mathcal U$ onto the data of the $i$-th constraint. The uncertainty is constraint-wise if $\mathcal U = \mathcal U_1\times\dots\times\mathcal U_m$: the rows vary independently. The Boundedness Assumption asks for a convex compact set $Q\subseteq\mathbb R^n$ that contains the feasible set of every instance.

Formalization targets

Goal: Proposition 2.1 (p. 5)

If the uncertainty is constraint-wise and the Boundedness Assumption holds, then

1. $(P_{\mathcal U})$ is infeasible if and only if some instance is infeasible:

$$G_{\mathcal U} = \emptyset \iff \exists A\in\mathcal U:\ \{x\mid Ax\ge0,\ f^{T}x=1\}=\emptyset;$$

2. if $(P_{\mathcal U})$ is feasible with optimal value $c^*$, then

$$c^* = \sup\{c^*(P)\mid (P)\in\mathcal P\}. \tag{9}$$

Milestones

The milestones follow the paper's proof: the row-wise description (8) of robust feasibility; the inclusion of $G_{\mathcal U}$ in every instance's feasible set; the reduction of the semi-infinite system (8) on $Q$ to a finite subsystem; the statement that the finite system (10) $A_1x\ge0,\dots,A_Nx\ge0,\ f^{T}x=1$ then has no solution at all; the Farkas certificate (11); the construction of one infeasible instance from it; and part (i) alone, which part (ii) uses for an augmented program.

Companions

The §2.2 example (every instance has optimal value 1, the robust counterpart is infeasible), and the two invariance remarks: $G_{\mathcal U}$ is unchanged under passing to the closed convex hull of $\mathcal U$ (§2.1) or to the product $\mathcal U_1\times\dots\times\mathcal U_m$ of its projections (§2.2).

Significance

Proposition 2.1 says that, for constraint-wise uncertainty, robustness costs nothing beyond what the worst realization already costs: the robust counterpart is feasible exactly when every instance is, and its optimal value equals the worst instance value. The §2.2 example shows the hypothesis cannot be dropped: there, correlated uncertainty in two rows makes every instance solvable with value 1 while the robust counterpart is infeasible. Together with the invariance of $G_{\mathcal U}$ under passing to the product of projections, this explains why row-wise (constraint-wise) uncertainty sets are the standard modelling choice in robust linear optimization.

The result is proved in the paper; no machine-checked version is known to exist. Formalizing it produces a reusable development of semi-infinite linear systems: the compactness reduction to finite subsystems, a homogeneous Farkas alternative, and the row-averaging argument that uses convexity and the product structure of $\mathcal U$.

Difficulty

The robust counterpart has a continuum of constraints, one for each $A\in\mathcal U$, so Farkas' Lemma cannot be applied to it directly. The step that requires care is passing from infeasibility of this semi-infinite system to infeasibility of a single instance. Compactness yields only finitely many instances whose joint system has no solution in $Q$; those instances are in general all feasible individually, and the infeasible instance has to be manufactured from their rows. Without constraint-wise uncertainty the manufactured matrix need not lie in $\mathcal U$, which is exactly what the §2.2 example exploits. Part (ii) needs the optimal values of the instances to be attained on compact feasible sets, which is where the Boundedness Assumption enters again.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and $Ax\ge0$ is 0 ≤ A *ᵥ x in the componentwise order. The $i$-th row of $A$ is A i and $a^{T}x$ is a ⬝ᵥ x. The projections $\mathcal U_i$ are the images of $\mathcal U$ under $A\mapsto A_i$, not free sets, and constraint-wise uncertainty is the inclusion $\mathcal U_1\times\dots\times\mathcal U_m\subseteq\mathcal U$ (the reverse inclusion always holds). The Boundedness Assumption keeps both convexity and compactness of $Q$, as on the page.

Optimal values are infima: $c^*$ is the greatest lower bound (IsGLB) of $c^{T}x$ over $G_{\mathcal U}$, and (9) states that $c^*$ is the least upper bound (IsLUB) of the set of real optimal values of the instances. No real sInf/sSup is used, so no junk value can make the statement true.

The goal carries the paper's standing assumption that $\mathcal U$ is convex and closed, and one disclosed addition: $\mathcal U$ is nonempty. The paper takes this for granted; without it part (i) fails for $f = 0$ and the supremum in (9) ranges over the empty set. The goal does not assume that the robust counterpart or any instance attains its optimum, and it does not mention finite subsystems, multipliers or the averaged matrix; those appear only in the milestones. A formalization in which the uncertainty sets $\mathcal U_i$ are arbitrary sets with $\mathcal U = \prod_i\mathcal U_i$, or in which optimal values are taken as sInf without boundedness, would not be faithful and is ruled out.

A complete development needs: compactness arguments for families of closed half-spaces, a Farkas alternative for homogeneous systems with one normalizing equation, and elementary convexity of linear images. These pieces are general and reusable beyond robust optimization. Proofs of the milestones, alternative arguments (for instance via LP duality for part (ii)) and proofs of the companion statements are welcome.

Selected references

• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/s0167-6377(99)00016-4 (cited here by the pages of the authors' manuscript).
• A. Ben-Tal, A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Operations Research 21(5):1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154

Motivation

Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets equipped with a rank function, or equivalently a family of independent sets, obeying a few postulates abstracted from the linear dependence of the columns of a matrix. The obvious first question about such an abstraction is whether it is genuinely more general than its model, that is, whether there are matroids that do not arise from any matrix. Section 16 of the paper answers it with a seven-element example, now called the Fano matroid $F_7$, and proves that no real matrix corresponds to it.

The question has had a long life. Representability of matroids over a given field is a central theme of matroid theory: Tutte (1958) characterized the matroids representable over the field with two elements by a single excluded minor, the four-point line $U_{2,4}$, and the regular matroids by three excluded minors, $U_{2,4}$, $F_7$ and its dual; and Seymour's decomposition of regular matroids (1980) rests on the same objects. Whitney's §16 is the starting point of this line: the first proof that the abstract postulates admit matroids outside linear algebra over $\mathbb R$.

Timeline:

• 1935. Whitney defines matroids, the circuit matrix of a matrix, and proves (§16) that the seven-element matroid $M'$ corresponds to no real matrix; in a footnote he credits Saunders MacLane with finding that $M'$ corresponds to no matrix and identifying it with a finite projective geometry. On p. 533 he exhibits a matrix of integers mod 2 for $M'$.
• 1958. Tutte characterizes binary and regular matroids by excluded minors; $F_7$ appears as an excluded minor for regularity (Tutte 1958).

Setting

Let $\mathbf M=(a_{ij})$ be an $m\times n$ matrix with columns $C_1,\dots,C_n$. For a set $N$ of columns, let $r(N)$ be the rank of the submatrix formed by those columns. Regarding the columns as abstract elements gives a matroid $M$ on $\{C_1,\dots,C_n\}$ with rank function $r$: the matroid of $\mathbf M$. A matroid corresponds to $\mathbf M$ if it is the matroid of $\mathbf M$, with elements matched to columns.

A circuit of a matroid is a minimal dependent set. For a circuit $P=\{i_1,\dots,i_p\}$ of the matroid of $\mathbf M$, there are numbers $b_1,\dots,b_n$ with $\sum_j a_{ij}b_j=0$ for every row $i$, and $b_j\neq 0$ exactly for $j\in P$; the set of such vectors is written $Z_{i_1\cdots i_p}$ when only the support condition is meant. Stacking one such row per circuit gives the circuit matrix $\mathbf M'$ of $\mathbf M$, determined up to nonzero factors on its rows.

A fundamental set of circuits of a matroid $M$ with nullity $n(M)=\rho(M)-r(M)$ ($\rho$ the number of elements) is a family of circuits $P_1,\dots,P_q$ with $q=n(M)$ such that the elements can be ordered $e_1,\dots,e_n$ with $e_{n-q+i}\in P_i$ and $e_{n-q+j}\notin P_i$ for $j>i$; it is strict if $e_{n-q+j}\notin P_i$ for every $j\neq i$.

The matroid $M'$ of §16 has elements $1,\dots,7$; its bases (maximal independent sets) are all three-element sets except

$$124,\quad 135,\quad 167,\quad 236,\quad 257,\quad 347,\quad 456. \qquad (16.1)$$

Formalization targets

Goal: §16, pp. 529–530

$$\exists\,M' \quad\text{and}\quad \forall m\ \forall\,\mathbf M\in\mathbb R^{m\times 7}:\ M' \text{ is not the matroid of } \mathbf M .$$

The number of rows is arbitrary; the existence clause makes the non-existence statement non-vacuous.

Milestones

1. §12. Every real matrix has a matroid: the ranks of column submatrices satisfy the rank postulates.
2. §14, (14.1). Every real matrix has a circuit matrix.
3. Theorem 29. The rows of a fundamental set of circuits form a base for the rows of the circuit matrix, so $r(\mathbf M')=q=n(\mathbf M)$.
4. Lemma 10. The support of a vector in the row space $H$ of a circuit matrix is a union of circuits.
5. Lemma 11. Two vectors of $H$ with the same circuit as support are proportional.
6. Theorem 32. For a circuit matrix normalised along a strict fundamental set, a minor $D$ vanishes iff an associated $q\times q$ minor $D'$ vanishes, iff some circuit avoids a prescribed set of columns.
7. §16, rank of $M'$. The rank of a $k$-set is $k$ for $k\le 2$, $3$ for $k\ge 4$, and for $k=3$ it is $2$ on (16.1) and $3$ otherwise.
8. p. 533. $M'$ is the matroid of an explicit $3\times 7$ matrix of integers mod 2.

Significance

The result. The theorem separates the abstract notion of matroid from linear dependence over $\mathbb R$: some matroids are not real-representable. It also exhibits that representability depends on the field, because the same matroid is the matroid of a matrix over the integers mod 2 (milestone 8). Everything later written about representability over particular fields, excluded-minor characterizations, and the gap between abstract and linear matroids starts from this distinction. Theorem 32 is of independent interest: it translates statements about circuits of a represented matroid into the vanishing of minors of a normalised circuit matrix.

Formalizing it. The result is classical and its proof is short on paper, but it is not formalized in Mathlib, which has matroids (Matroid, circuits, ranks) but no column matroid of a matrix with a rank-of-submatrix characterization, no circuit matrix, and no Fano matroid. The mission produces those objects and the bridge lemmas (Theorem 29, Lemmas 10–11, Theorem 32) that connect matroid circuits with linear algebra of the circuit matrix. No machine-checked proof of the non-representability of the Fano matroid over $\mathbb R$ in Lean is known to the curators.

Difficulty

The obvious attempt is a direct search: suppose a real $m\times 7$ matrix has $M'$ as its matroid and derive a contradiction from the seven dependent triples. This does not work as stated. Each rank condition is a determinantal (nonlinear) condition on the entries, the number of rows $m$ is unbounded, and a representation is determined only up to row operations and column scalings, so there is no finite case check and no single linear computation that settles the question. The contradiction has to come from an argument that is invariant under these symmetries, and the milestones (circuit vectors determined up to scaling, fundamental sets spanning, circuits detected by minors) are what such an argument needs to be stated in. The field also matters: the argument must use that $2\neq 0$ in $\mathbb R$, since over a field of characteristic 2 the statement is false (milestone 8).

Formalization scope

• Elements and matrices. Matroids are Mathlib Matroids whose ground set is the whole (finite) type. The Fano matroid lives on Fin 7, Whitney's element $k$ being k - 1; the seven triples are written out literally. Matrices are Matrix (Fin m) ι K; "the matroid of $\mathbf M$" means: ground set everything, and the rank M.eRk N of every finite set $N$ of columns equals Matrix.rank of the column submatrix.
• Field. The goal and Lemmas 10–11, Theorems 29 and 32 are stated over $\mathbb R$, as in the paper; the predicate "matroid of a matrix" is stated over any field so that the mod-2 milestone uses the same notion.
• Circuit matrix. Rows are determined up to nonzero factors, so "circuit matrix" is a predicate on a matrix together with a bijection between its rows and the circuits; every theorem holds for every such choice.
• Nullity and indices. $q=n(M)$ is written $q+r(M)=\rho(M)$ in extended naturals, with no truncated subtraction. In Theorem 32, $n=p+q$, the complement of $i_1,\dots,i_s$ is given as an order embedding of Fin t with $s+t=q$, and determinants are of square submatrices in the paper's row and column order.
• Ruling out trivial readings. The goal includes the existence of $M'$; without it "every matroid with these bases has no real matrix" could hold vacuously. The goal quantifies over every number of rows; fixing $m=3$ would be a weaker statement.

Reusable beyond this mission: the matroid of a matrix over a field, the circuit matrix, fundamental sets of circuits, and the Fano matroid. Contributions welcome: proofs of the milestones, and a proof of the goal by any route, including one that does not go through Theorem 32.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
• W. T. Tutte, A homotopy theorem for matroids, I, II, Transactions of the American Mathematical Society 88 (1958), 144–174. https://doi.org/10.2307/1993244
• J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• O. Veblen and J. W. Young, Projective Geometry, Vol. I, Ginn, 1910 (cited by Whitney for the finite projective geometry).

Motivation

Whitney's 1935 paper introduced matroids as an abstraction of linear dependence among the columns of a matrix. Most of the paper works over the real numbers; its appendix asks which matroids arise from matrices of integers mod 2, that is, matrices with entries 0 and 1 in which rank and dependence are computed over the two-element field. These are today's binary matroids. They include the cycle matroids of graphs (Whitney closes the paper by noting that graphs correspond to mod-2 matrices with exactly two ones in each column) and they are the setting of several later structure theorems: Tutte's excluded-minor characterization of binary matroids (Tutte 1958), Seymour's decomposition of regular matroids (Seymour 1980) and Seymour's theory of binary clutters and max-flow min-cut (Seymour 1977), which underlies parts of combinatorial optimization.

Whitney's answer is an intrinsic postulate, (C*), on the circuits of the matroid, stated without reference to any matrix, and a constructive representation theorem (Theorem 37): a matroid satisfying (C*) is the matroid of a mod-2 matrix, and the matrix is unique once the columns of one base are fixed.

Setting

A matroid $M$ on elements $e_1, \dots, e_n$ is given by its independent sets; its circuits are its minimal dependent sets, its rank $r(M)$ is the size of a base, and its nullity is $n(M) = n - r(M)$. Here $M$ is a Mathlib Matroid (Fin n) whose ground set is all of Fin n.

Subsets of the elements are added mod 2: a sum of finitely many sets is the set of elements lying in an odd number of them (for two sets, the symmetric difference). A cycle is a sum mod 2 of circuits; the empty sum is the null cycle $\emptyset$. A set is a true sum of sets that have no common elements and whose union it is. Postulate (C*) requires that each cycle be a true sum of circuits.

With $n = r + q$, a family $P_1, \dots, P_q$ is a strict fundamental set of circuits with respect to $e_{n-q+1}, \dots, e_n$ if $q = n(M)$, each $P_i$ is a circuit, and $P_i$ contains $e_{n-q+i}$ but no other $e_{n-q+j}$.

For a matrix $\mathbf M$ over the integers mod 2 with columns $C_1, \dots, C_n$, columns are independent (mod 2) if no non-null subset of them sums to the zero column. The matroid corresponding to $\mathbf M$ has the column indices as elements and these independent sets.

Formalization targets

Goal: Theorem 37 (p. 533)

Let $M$ satisfy (C*), with elements $e_1, \dots, e_n$ and base $\{e_1, \dots, e_{n-q}\}$. For every matrix $\mathbf M_1$ mod 2 (any number of rows) whose $n - q$ columns are independent mod 2,

$$\exists!\ \mathbf M = (\mathbf M_1 \mid C_{n-q+1} \cdots C_n) \ \text{ whose corresponding matroid is } M.$$

Milestones

1. Theorem 9 (p. 517): if $e_1, \dots, e_{n-q}$ is a base, there is a unique strict fundamental set of circuits with respect to $e_{n-q+1}, \dots, e_n$.
2. Appendix, p. 531: (C*) implies the circuit postulate (C₂), for any family of sets.
3. Theorem 33: under (C*), the circuits are exactly the minimal non-null cycles.
4. Theorem 34: under (C*), the cycles are exactly the $2^q$ sums mod 2 of a strict fundamental set.
5. Theorem 35: two (C*)-matroids with a common strict fundamental set have the same circuits.
6. Theorem 36: any $P_1, \dots, P_q$ with $e_{n-q+i} \in P_i \subseteq \{e_1, \dots, e_{n-q}, e_{n-q+i}\}$ is the strict fundamental set of exactly one (C*)-matroid.
7. Appendix, p. 532: the matroid of a matrix mod 2 exists, satisfies (C*), and its cycles are the supports of the mod-2 dependencies among the columns.

Milestone 7 and the goal together characterize binary matroids as the matroids satisfying (C*).

Significance

The result. Theorem 37 and the p. 532 claim give an intrinsic, matrix-free description of the matroids representable over the two-element field, and Theorem 36 parametrizes all of them by $q$ arbitrary subsets of a base. Uniqueness in Theorem 37 says that a binary representation is determined by the columns of one base; in modern terms, binary matroids are uniquely representable over GF(2) up to row operations. Every later theory of binary matroids, including graphic and cographic matroids, Tutte's excluded-minor theorem and Seymour's decomposition, starts from this equivalence.

Formalizing it. The results are proved in the paper and in textbooks (e.g. Oxley, Matroid Theory, Ch. 9) but, at the Mathlib revision used here, there is no notion of a matroid represented by a matrix over a field, and no binary-matroid theory. On Prove2Me, the existing binary objects (SeymourMFMC.Binary.*) are binary clutters defined through blockers, not matroids represented by mod-2 matrices. This mission produces the representation predicate for mod-2 matrices, the cycle space of a matroid, and the equivalence between (C*) and binary representability.

Difficulty

Writing down candidate columns is not the hard part; showing that the matroid of the completed matrix is $M$ itself, and not merely a matroid sharing some of its circuits, is. Whitney's example at the end of §9 exhibits two different matroids with a common strict fundamental set, so agreement on fundamental circuits does not by itself identify a matroid; any argument must use (C*) on both the given matroid and the matroid of the matrix. A naive comparison of independent sets column by column does not close this gap. Uniqueness likewise depends on the independence mod 2 of the prescribed columns: without it, different completions can give the same matroid.

Formalization scope

• Matroids are Mathlib Matroid (Fin (r + q)) with ground set Set.univ; Whitney's $e_k$ is k - 1, his $e_1, \dots, e_{n-q}$ is the range of Fin.castAdd q, and $e_{n-q+i}$ is Fin.natAdd r (i - 1). Writing $n = r + q$ removes natural-number subtraction; $q$ is not a free parameter, since $\{e_1, \dots, e_r\}$ is required to be a base.
• Sums mod 2 count parity of membership (sumMod2); cycles are sums over finite sets of circuits; true sums are unions over finite pairwise-disjoint sets of circuits; (C*) is SatisfiesCStar on the circuit family {C | M.IsCircuit C}. These definitions take the circuit family as a parameter, so that the (C₂) milestone is posed for an arbitrary family of sets, as Whitney poses it.
• A strict fundamental set includes the nullity condition $r(M) + q = \rho(M)$, stated in $\mathbb N_\infty$.
• Matrices are Matrix (Fin m) (Fin n) (ZMod 2) with any $m$; independence mod 2 of columns is LinearIndepOn (ZMod 2) of the columns (the rows of the transpose). IsMatroidOf M A compares all independent sets, not only bases.
• Ruled out: the goal is not satisfied by any statement that compares only the bases of one size, by an existence-only statement without uniqueness, or by real (instead of mod-2) independence.
• Tacit hypotheses made explicit: the matroid's ground set is exactly $e_1, \dots, e_n$ ($\rho(M) = n$); the elements and matroids are finite.

Contributions welcome: the general fact that the matroid of a vector family over a field exists (a reusable Matroid.ofFun-style construction over any field), the cycle-space lemmas, and proofs of the milestones in any order.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
• W. T. Tutte, A homotopy theorem for matroids, I, II, Transactions of the AMS 88 (1958), 144–174. https://doi.org/10.2307/1993244
• P. D. Seymour, The matroids with the max-flow min-cut property, Journal of Combinatorial Theory Ser. B 23 (1977), 189–222. https://doi.org/10.1016/0095-8956(77)90031-4
• P. D. Seymour, Decomposition of regular matroids, Journal of Combinatorial Theory Ser. B 28 (1980), 305–359. https://doi.org/10.1016/0095-8956(80)90075-1
• J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001

Motivation

Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract rank function that behaves like the rank of a set of vectors. Part II of the paper opens with the decomposition of a matroid into components. The question it answers is basic to every later use of matroids: when does a matroid split into independent pieces, and how can the pieces be recognized?

For the matroid of a graph (elements = edges, rank = number of vertices minus number of connected pieces spanned) the components are the 2-connected blocks of the graph, and Whitney's theorem recovers the classical fact that two edges lie in a common block exactly when they lie on a common cycle. Whitney had studied separability of graphs in Non-separable and planar graphs (1932), and footnote 11 of the 1935 paper points out that the theorem identifies König's "Glieder" of a graph with components. Matroid connectivity built on this notion runs through later structure theory: Tutte's higher connectivity, Seymour's decomposition of regular matroids, and the matroid minors project all start from the separation of a matroid into components.

Setting

A matroid $M$ on a finite ground set $E$ is given here by Mathlib's Matroid structure, with rank function $r(X)$ for $X\subseteq E$ (Mathlib's M.eRk X) and circuits, the minimal dependent sets (M.IsCircuit). Whitney treats every subset $X\subseteq E$ as a matroid in its own right, a submatroid, with the rank function of $M$ restricted to subsets of $X$. For sets he writes $M_1+M_2$ for the union, $\rho(N)$ for the number of elements of $N$, and

$$n(N) = \rho(N) - r(N)$$

for the nullity of $N$.

Rank is subadditive: $r(X_1+X_2)\le r(X_1)+r(X_2)$. A submatroid $X$ is separable if it can be divided into two disjoint groups $X_1, X_2$, each containing at least one element, with

$$r(X) = r(X_1) + r(X_2),$$

and non-separable otherwise. Every single element is non-separable. A component of $M$ is a maximal non-separable part of $M$: a nonempty non-separable set $K\subseteq E$ contained in no strictly larger non-separable subset of $E$.

Formalization targets

Goal: Theorem 19

For two distinct elements $e_1\neq e_2$ of $E$,

$$\bigl(\exists K \text{ component of } M:\ e_1, e_2\in K\bigr) \iff \bigl(\exists P \text{ circuit of } M:\ e_1, e_2\in P\bigr).$$

Components are defined by the rank function, circuits by dependence; the goal asserts that the two descriptions agree.

Milestones (§10, in the paper's order)

• Theorem 11. If $r(M_1+M_2)=r(M_1)+r(M_2)$, $M_1'\subseteq M_1$ and $M_2'\subseteq M_2$, then $r(M_1'+M_2')=r(M_1')+r(M_2')$.
• Theorem 12. Under the same rank additivity, a non-separable $M'\subseteq M_1+M_2$ lies in $M_1$ or in $M_2$.
• Theorem 13. Two non-separable sets with a common element have a non-separable union.
• Theorem 14. Distinct components are disjoint.
• Theorem 15. The components cover $E$, and no other family of components does.
• Theorem 16. A set is non-separable of nullity $1$ if and only if it is a circuit.
• Lemma 9. If $M_1+M_2$ is non-separable, with $M_1, M_2$ nonempty and disjoint, some circuit inside $M_1+M_2$ meets both.
• Theorem 17. A non-separable set of nullity $n>0$ is built from a circuit by $n-1$ steps, each adding a set of elements that forms a circuit with elements already present, through non-separable sets of nullity $1,2,\dots,n$.
• Theorem 18. For distinct nonempty non-separable $M_1,\dots,M_p$ covering $E$, the following are equivalent: they are the components; they are pairwise disjoint and no circuit meets two of them; $r(E)=\sum_i r(M_i)$.

Significance

The result. Theorem 19 makes the component decomposition computable from circuits alone and shows that "lying on a common circuit" is an equivalence relation on distinct elements, a fact that is not evident from the circuit axioms. Theorem 18 adds that the decomposition is the unique one with additive rank. Together they are the starting point of matroid connectivity: the direct-sum decomposition of a matroid, the reduction of many matroid problems (representability, duality of components, Whitney's own Theorems 24–26 on duals of components) to the connected case, and the higher-connectivity theory that followed.

Formalizing it. The results are classical and proved in the paper; nothing here is open. To our knowledge Mathlib at the pinned revision has no notion of matroid connectivity or components, so this mission produces the first machine-checked development of Whitney's §10: the rank-based definition of separability, the disjoint decomposition into components, the circuit characterization, and the ear-type construction of non-separable matroids (Theorem 17). These are reusable for any later formalization of matroid connectivity, including Whitney's results on duals of components.

Difficulty

The two directions of Theorem 19 rest on different machinery. That two elements on a common circuit lie in one component follows from the rank theory (Theorems 13 and 16). The converse is the substantial direction: a component is defined by the failure of rank additivity, which only says that every division of the component is crossed by some circuit (Lemma 9). It does not directly give one circuit through two prescribed elements. Combining circuits that cross different divisions into a single circuit through both $e_1$ and $e_2$ requires the circuit elimination property together with a minimality argument over subsets of the component; the naive attempt of chaining overlapping circuits from $e_1$ to $e_2$ gives a connected chain of circuits, not one circuit.

Formalization scope

• Representation. A matroid is Mathlib's Matroid α with [M.Finite]; Whitney's matroids are finite. A submatroid is a subset $X\subseteq$ M.E with the rank M.eRk restricted to its subsets; results that Whitney states for "a matroid $M = M_1 + M_2$" are stated for subsets of an ambient finite matroid, which is the same statement applied to the submatroid $M_1+M_2$.
• Ranks are Mathlib's ℕ∞-valued M.eRk, finite on a finite matroid, so (10.1) is an equation of natural numbers. Nullity is computed in $\mathbb Z$ as the number of elements minus the rank.
• Definitions. IsSeparable M X requires two nonempty, disjoint groups with union $X$ and additive rank; without nonemptiness every set would be separable. IsNonSeparable M X adds $X\subseteq$ M.E. IsComponent M K requires $K$ nonempty, non-separable, and maximal; nonemptiness excludes the empty set, which is vacuously non-separable.
• Tacit hypotheses made explicit. In Theorem 19 the two elements are distinct: for $e_1=e_2$ a coloop is its own component and lies on no circuit. In Theorem 18 the sets $M_1,\dots,M_p$ are distinct and nonempty: a loop listed twice would satisfy (3) but not (2), and an empty set would satisfy (2) and (3) but not (1). In Theorems 11 and 12 the two parts need not be disjoint, as Whitney's use of $M_1+M_2$ for overlapping sets in Theorem 13 indicates; the statements hold in that generality.
• Ruled out. Components must not be defined as the classes of the relation "lie on a common circuit": that would make the goal a tautology. Here they are the rank-defined maximal non-separable sets of §10, and circuits are Mathlib's Matroid.IsCircuit.
• Infrastructure. Solvers will need submodularity of M.eRk and circuit elimination (both in Mathlib), the relation between circuits of M ↾ X and circuits of M inside $X$ (Matroid.restrict_isCircuit_iff), and finiteness arguments for maximal non-separable sets. Proofs of the milestones, alternative proofs of the goal, and lemmas relating components to Mathlib's direct sums of matroids are all welcome.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
• H. Whitney, Non-separable and planar graphs, Transactions of the American Mathematical Society 34 (1932), 339–362. https://doi.org/10.1090/S0002-9947-1932-1501641-2
• D. König, Acta Litterarum ac Scientiarum Szeged, vol. 6, pp. 155–179, as cited by Whitney in footnote 11 (p. 159 for the notion of "Glied").
• J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011, Chapter 4 (connectivity).