The OR Formalization Drive

Motivation

The conditional logit model is the workhorse of discrete choice analysis in transportation, marketing, labour and industrial organization. McFadden's 1974 chapter derived it from a theory of population choice behaviour and showed how to estimate it by maximum likelihood; this line of work was recognized by his 2000 Nobel Prize in Economic Sciences, awarded for theory and methods of discrete choice analysis. Every applied logit estimation rests on a basic question: does the maximum likelihood estimate exist for the sample at hand? In small samples it may not. When one alternative is always chosen whenever it is available, the likelihood keeps increasing as a parameter tends to infinity, and numerical optimizers report diverging coefficients. This failure is known in the binary case as complete or quasi-complete separation. McFadden's Lemma 3 gives the exact condition, for the multinomial conditional logit model with general alternative sets, under which a maximizer exists.

Timeline. Berkson (1951, 1955) popularized binomial logit; multinomial versions were developed by Gurland (1960), Bloch (1967), Rassam (1971), McFadden (1968) and Theil (1969, 1970). McFadden (1974) stated the existence criterion for the conditional logit likelihood (Lemma 3) together with a quadratic-programming test for it (Lemma 4). Albert and Anderson (1984) later classified separation patterns for binary and multinomial logistic regression, and Haberman (1974) treated existence for log-linear models.

Setting

A choice experiment has $N \ge 1$ trials. Trial $n$ offers an alternative set of $J_n$ alternatives, indexed $i = 1,\dots,J_n$, each described by an attribute vector $z_{in} \in \mathbb{R}^K$ (the values of $K$ specified functions of the individual's and the alternative's characteristics). Trial $n$ is repeated $R_n \ge 1$ times, and alternative $i$ is chosen $S_{in}$ times, so $R_n = \sum_{j} S_{jn}$.

For a parameter $\theta \in \mathbb{R}^K$, with $z_{in}\theta$ the inner product, the selection probabilities are

and the log-likelihood of the sample is

Write $\bar z_n(\theta) = \sum_i z_{in}P_{in}(\theta)$ for the probability-weighted mean attribute vector of trial $n$.

Axiom 5 (Full Rank). The $\big(\sum_n J_n\big)\times K$ matrix with rows $z_{in} - \bar z_n$ has rank $K$.

Axiom 6. There is no nonzero $\gamma \in \mathbb{R}^K$ with $S_{in}(z_{jn} - z_{in})\gamma \le 0$ for all $i, j = 1,\dots,J_n$ and $n = 1,\dots,N$. Equivalently, no nonzero direction makes every observed choice weakly best in its alternative set.

Formalization targets

Goal: Lemma 3

Under Axiom 5,

Milestones

1. Equation (19): the gradient $\partial L/\partial\theta = \sum_n \sum_j (S_{jn} - R_nP_{jn}) z_{jn}$.
2. Equation (20): the Hessian $\partial^2L/\partial\theta\,\partial\theta' = -\sum_n R_n \sum_j (z_{jn} - \bar z_n)'P_{jn}(z_{jn} - \bar z_n)$.
3. $L$ is concave, and every critical point is a global maximizer.
4. A Hessian that is nonsingular everywhere makes $L$ strictly concave with at most one maximizer.
5. Axiom 5 holds at $\theta$ if and only if the Hessian at $\theta$ is negative definite.
6. Necessity: under Axiom 5, a maximizer forces Axiom 6.
7. Equation (21): under Axiom 6, $b(\gamma) = \max_n \max_{i,j} S_{in}(z_{jn}-z_{in})\gamma$ has a positive lower bound $b^*$ on the unit sphere.
8. The bound $L(\theta) - C \le -b^*|\theta|$ for all $\theta$.
9. Sufficiency: Axiom 6 gives a maximizer.

Significance

Lemma 3 tells the practitioner when the conditional logit maximum likelihood estimate exists, before any numerical optimization is attempted. It is a linear-inequality condition on the data alone, so it can be checked by linear or quadratic programming (Lemma 4 of the same paper). The existence of the estimator is also the first step of McFadden's asymptotic theory: Lemma 5 shows that Axiom 6 holds with probability tending to one, and Lemma 6, consistency and asymptotic normality, concerns the estimator whose existence Lemma 3 characterizes. The concavity and Hessian formulas (19)–(20) are the basis of the Newton–Raphson computation of the estimator and of its asymptotic covariance matrix.

The result has been proved since 1974 and is classical. To our knowledge it has no machine-checked proof; Mathlib has no statement about the existence of logit or softmax-regression maximum likelihood estimates. Formalizing it produces a verified existence criterion for the multinomial logit likelihood, verified gradient and Hessian formulas for log-sum-exp likelihoods with repeated observations, and a verified link between full column rank and strict concavity.

Difficulty

The likelihood is concave, and concave functions on $\mathbb{R}^K$ need not attain their supremum. Concavity alone therefore gives nothing, and existence must come from a growth condition. The obvious approach, "the likelihood is bounded above by $C$, hence attains its maximum", fails: $L$ is bounded but can approach its supremum only at infinity, which is exactly the separation case. Sufficiency needs a quantitative rate at which $L$ decreases, uniform over all directions; a direction-by-direction argument does not suffice. Necessity requires strict concavity, which is where Axiom 5 and the requirement that every trial be observed enter. A trial with $R_n = 0$ can supply the rank of Axiom 5 while contributing nothing to $L$, so with such a trial necessity fails. The calculus part, (19)–(20), involves differentiating sums of log-sum-exp terms over dependent index types and identifying the result with a weighted covariance operator.

Formalization scope

• Representation. $\mathbb{R}^K$ is EuclideanSpace ℝ (Fin K), so $|\theta| = (\theta'\theta)^{1/2}$ is the Euclidean norm and $z\theta$ is the inner product ⟪z, θ⟫. Trials are Fin N, alternatives of trial $n$ are Fin (J n), and the counts $S_{in}$ are natural numbers.
• Data structure. The structure Data K bundles $N$, $J$, $z$, $S$ and the standing assumptions $N \ge 1$ and $R_n = \sum_i S_{in} \ge 1$ for every trial; these make the trial and alternative index sets nonempty.
• Axioms 1–4 are built in. The model is the logit form (16) with $v$ linear in $\theta$ (Axiom 4), so "Suppose Axioms 1–5 hold" becomes "Data plus Axiom 5".
• Axiom 5 is read at every $\theta$. The row space of the matrix does not depend on $\theta$.
• Hessian. The Hessian is the Fréchet derivative of the gradient vector field (19), as a continuous linear map.
• The maximizer is global over all of $\mathbb{R}^K$. Neither a local maximizer nor "$L(\hat\theta) \ge L(0)$" is acceptable as the goal; that would make it trivial.
• Infrastructure. Gradients and Hessians of log-sum-exp with dependent finite index types; positive definiteness from full column rank; attainment of the maximum of a coercive continuous function on a finite-dimensional space. The calculus lemmas are reusable for any multinomial logit or softmax likelihood. Missions 4 and 5 of this series reuse the same model. Contributions of general log-sum-exp lemmas, independent of this mission's definitions, are welcome.

Selected references

• D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf
• A. Albert and J. A. Anderson, On the existence of maximum likelihood estimates in logistic regression models, Biometrika 71(1), 1984, pp. 1–10. https://doi.org/10.1093/biomet/71.1.1
• S. J. Haberman, The Analysis of Frequency Data, University of Chicago Press, 1974.
• J. Berkson, Maximum likelihood and minimum χ² estimates of the logistic function, Journal of the American Statistical Association 50, 1955, pp. 130–162. https://doi.org/10.1080/01621459.1955.10501255

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

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

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$,

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).

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,

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

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

Formalization targets

Goal: §16, pp. 529–530

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

Two-stage adaptive optimization models decisions taken in two rounds: a first-stage decision $x$ is fixed before an uncertain parameter is revealed, and a second-stage decision $y(b)$ is chosen after the parameter $b$ is observed, so that the second stage may depend on $b$ arbitrarily. The objective is the worst case over an uncertainty set $\mathcal U$ of possible parameters. Such models arise in robust network design, capacity planning and two-stage covering problems, and they generalize the two-stage robust combinatorial problems (set cover, facility location) studied by Dhamdhere, Goyal, Ravi and Singh.

Optimizing over all functions $y(\cdot)$ is intractable in general: Bertsimas and Goyal note that the optimal second stage is piecewise linear in $b$ with possibly exponentially many pieces (Bemporad, Borrelli and Morari, 2003). A standard remedy, introduced for robust linear programs by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), restricts the second stage to affine policies (linear decision rules) $y(b)=Pb+q$; the best affine policy is computable by a single convex program and performs well empirically. The question is when this restriction loses nothing.

Timeline of the relevant results:

• 2004. Ben-Tal, Goryashko, Guslitzer and Nemirovski introduce affinely adjustable robust counterparts and show that the best affine policy is tractable for many uncertainty sets (doi:10.1007/s10107-003-0454-y).
• 2010. Bertsimas, Iancu and Parrilo prove that affine policies are optimal for a class of multistage robust problems with one-dimensional uncertainty per stage and box uncertainty sets (doi:10.1287/moor.1100.0444).
• 2012. Bertsimas and Goyal, the source of this mission, prove that an affine policy is optimal for model (1) whenever $\mathcal U$ is a simplex (Theorem 1), and show that this exactness breaks down for slightly larger sets (doi:10.1007/s10107-011-0444-4).

Setting

Let $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$, $c\in\mathbb R^{n_1}_+$ and $d\in\mathbb R^{n_2}_+$. The problem $\Pi_{Adapt}(\mathcal U)$ of model (1) is

where inequalities between vectors are componentwise. A pair $(x,y)$ satisfying the constraints is feasible; its worst-case cost is $c^Tx+\max_{b\in\mathcal U}d^Ty(b)$. A feasible pair is optimal when its worst-case cost equals $z_{Adapt}(\mathcal U)$, and an affine policy is a second stage of the form $y(b)=Pb+q$ with $P\in\mathbb R^{n_2\times m}$, $q\in\mathbb R^{n_2}$, still required to be nonnegative on $\mathcal U$. The value $z_{Aff}(\mathcal U)$ is the same minimum restricted to affine policies.

A simplex in $\mathbb R^m$ is the convex hull

of $m+1$ affinely independent points, that is, points for which $b^1-b^{m+1},\dots,b^m-b^{m+1}$ are linearly independent. The proof works with the $m\times m$ matrix $Q=[(b^1-b^{m+1})\cdots(b^m-b^{m+1})]$, the matrix $Y=[(y^*(b^1)-y^*(b^{m+1}))\cdots(y^*(b^m)-y^*(b^{m+1}))]$ of display (2), and the affine rule $\tilde y(b)=YQ^{-1}(b-b^{m+1})+y^*(b^{m+1})$. In Lean these are Qmat v, Ymat v g and interpolant v g, with vertices v : Fin (m+1) → Fin m → ℝ.

Formalization targets

Goal: Theorem 1

If $\mathcal U=\operatorname{conv}(b^1,\dots,b^{m+1})$ with affinely independent $b^j\in\mathbb R^m_+$ and $\Pi_{Adapt}(\mathcal U)$ is feasible, then there exist $\hat x$, $P\in\mathbb R^{n_2\times m}$ and $q\in\mathbb R^{n_2}$ such that

is an optimal solution of $\Pi_{Adapt}(\mathcal U)$, optimal among all (not only affine) two-stage solutions. In particular $z_{Aff}(\mathcal U)=z_{Adapt}(\mathcal U)$.

Milestones

The proof of Theorem 1 has no numbered lemma; the milestones are its displayed steps, in attack order:

1. $Q$ is invertible (PDF p. 6).
2. For $b=\sum_j\alpha_jb^j$ with $\sum_j\alpha_j=1$: $Q^{-1}(b-b^{m+1})=(\alpha_1,\dots,\alpha_m)^T$ (PDF p. 6).
3. $\tilde y\big(\sum_j\alpha_jb^j\big)=\sum_j\alpha_j\,y^*(b^j)$ (PDF pp. 6–7).
4. Displays (3)–(5): for any feasible $(x^*,y^*)$, the pair $(x^*,\tilde y)$ is feasible and every bound on the worst-case cost of $(x^*,y^*)$ also bounds that of $(x^*,\tilde y)$ (PDF p. 7).

Significance

The result. Theorem 1 identifies a class of uncertainty sets on which the tractable affine restriction is exact, for every constraint matrix $A$ and $B$ and every nonnegative cost. It is the positive anchor of the paper: Sections 3 and 4 show that with $m+3$ extreme points the best affine policy can already be worse by a factor $2-\delta$, and that on sets with exponentially many extreme points the gap can be $\Omega(m^{1/2-\delta})$; Section 6 uses a dominating simplex, on which affine policies are exact, to build an $O(\sqrt m)$-approximation for general $\mathcal U$. The theorem also says that on a simplex the whole adaptive problem reduces to $m+1$ scenario copies of a linear program.

Formalizing it. The result is proved on paper; no machine-checked version is known on Prove2Me. This mission produces the model (1) in Lean, the barycentric-coordinate identity for a simplex in matrix form, and a statement of optimality that asserts attainment of the minimum in (1), which the paper's proof takes for granted.

Difficulty

Two steps are not routine to formalize. First, the paper starts from "an optimal solution $x^*,y^*(b)$", that is, it assumes the minimum in (1) is attained. Over arbitrary functions $y(\cdot)$ this is not automatic; on a simplex it follows because the problem reduces to a finite linear program on the vertices, whose optimum is attained, but Mathlib has no theory of linear-programming attainment, so this reduction has to be built. Second, the affine-independence step needs the passage from affine independence of $m+1$ points to invertibility of the $m\times m$ matrix $Q$, and the identity $Q^{-1}(b-b^{m+1})=\alpha$ requires the barycentric coordinates and the inverse matrix to be matched index by index. The naive idea of comparing $z_{Aff}$ and $z_{Adapt}$ as real infima does not prove the goal: equality of the two infima says nothing about the existence of an optimal solution.

Formalization scope

Vectors in $\mathbb R^m$ are Fin m → ℝ, with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ. The paper's indices start at $1$, Lean's at $0$: $b^j$ is v (j-1) and $b^{m+1}$ is v (Fin.last m). The simplex is convexHull ℝ (Set.range v); it is compact, convex and, by affine independence, full-dimensional, so these standing assumptions of (1) are not stated separately. Nonnegativity of $\mathcal U$ is the hypothesis that all $m+1$ vertices are nonnegative (the page writes $j=1,\dots,m$, a slip for $m+1$). Feasibility of (1) is a hypothesis, as the paper assumes. Optimality (IsOptimalAdapt) means: feasible, and every worst-case cost bound achieved by any feasible two-stage solution is achieved by this one. The values $z_{Adapt}$ and $z_{Aff}$ are infima of the sets of achievable bounds; they are provided for reference and the goal does not depend on them.

The goal must not be replaced by $z_{Aff}(\mathcal U)\le z_{Adapt}(\mathcal U)$, by optimality among affine policies only, or by a version that assumes an optimal solution exists: each of these drops the content "there is an optimal solution and it is affine". The goal does not mention $Q$, $Y$ or the interpolant.