Combinatorics

Motivation

A matching in a graph is a set of edges no two of which share a vertex. Finding a matching of maximum cardinality is one of the basic problems of combinatorial optimization: it models pairing tasks (workers to shifts, kidney donors to recipients, players to rounds), it is a subroutine of algorithms for the travelling salesman and Chinese postman problems, and it was the first problem shown to need more than linear programming over the obvious constraints to be solved exactly.

For bipartite graphs, König's theorem (1931) gives a min–max formula: the maximum size of a matching equals the minimum size of a set of vertices meeting every edge. In general graphs this fails already for a triangle, where a single edge is a maximum matching but two vertices are needed to meet all three edges. Jack Edmonds' paper Paths, trees, and flowers (1965) gave both a polynomial-time algorithm for maximum matching in general graphs, the blossom algorithm, and, as a by-product of its analysis, the correct min–max theorem for general graphs.

Timeline.

• 1891: Petersen uses alternating paths to prove the existence of factors in certain graphs.
• 1947: Tutte characterizes graphs with a perfect matching.
• 1957: Berge proves that a matching is maximum if and only if there is no augmenting path, and derives the deficiency formula now called the Tutte–Berge formula (Berge 1957).
• 1965: Edmonds shrinks odd circuits ("blossoms") to search for augmenting paths in polynomial time and proves the matching-duality theorem in terms of odd-set covers (Edmonds 1965); the companion paper on the matching polyhedron extends this to weighted matching.

Setting

A graph $G$ is a finite set of vertices and a finite set of edges, each edge meeting exactly two distinct vertices, its end-points. Several edges may join the same two vertices; this is needed because shrinking creates parallel edges. A matching $M$ is a set of edges no two of which meet the same vertex; a vertex is exposed if it meets no edge of $M$. "Maximum" refers to cardinality.

An odd set is a set $U$ of vertices with an odd number of elements. Its capacity is

$$\operatorname{cap}(U) = \begin{cases} 1 & |U| = 1,\\ k & |U| = 2k+1,\ k \ge 1.\end{cases}$$

A one-vertex set covers the edges meeting its vertex; a set of $2k+1 \ge 3$ vertices covers the edges with both end-points in it. An odd-set cover is a family $\mathcal S$ of odd sets such that every edge is covered by some member, and its capacity-sum is $\operatorname{cap}(\mathcal S) = \sum_{U \in \mathcal S} \operatorname{cap}(U)$.

The proof uses the following objects of §3–§4 of the paper. An alternating path is a simple path whose edges alternate between $M$ and the non-matching edges $\bar M$. An alternating tree is a tree whose vertices are split into inner and outer vertices, every edge joining an inner to an outer vertex and every inner vertex meeting exactly two tree edges; it is planted if $M$ restricted to the tree is a maximum matching of the tree whose one exposed vertex (the root) is exposed in $G$, and Hungarian if its outer vertices are adjacent only to its inner vertices. A blossom is an odd circuit on which $M$ is a maximum matching, leaving one vertex $b$ exposed; with a stem (an alternating path from an exposed vertex ending in a matching edge at $b$) it forms a flower. Shrinking a vertex set $U$ replaces it by a single vertex $U/U$, deletes the edges inside $U$ and keeps all other edges; $G/B$ and $M/B = M \cap (G/B)$ denote the result for a blossom $B$.

Formalization targets

Goal: the matching-duality theorem (5.6, p. 462)

$$\max\{|M| : M \text{ a matching of } G\} \;=\; \min\{\operatorname{cap}(\mathcal S) : \mathcal S \text{ an odd-set cover of } G\}.$$

It is stated as: there are a maximum matching $M$ and a minimum odd-set cover $\mathcal S$ with $|M| = \operatorname{cap}(\mathcal S)$.

Milestones (attack order)

1. Weak duality: $|M| \le \operatorname{cap}(\mathcal S)$ for every matching and odd-set cover.
2. 3.7 (Berge): $M$ is not maximum iff an alternating path joins two exposed vertices.
3. 4.1–4.2: maximum matchings of an alternating tree.
4. 4.14 and 4.15: the two directions of 4.12, in stronger form.
5. 4.12: for the blossom $B$ of a flower, $M$ is maximum in $G$ iff $M/B$ is maximum in $G/B$.
6. 4.17: removing a Hungarian tree preserves maximality.
7. 5.7: the theorem for graphs with at most one exposed vertex.
8. 5.8: the configuration produced by the algorithm on a maximum matching, and the odd sets $\mathcal S_J$ it yields, which reduce the theorem to a graph with one exposed vertex fewer.

Significance

The matching-duality theorem gives a certificate of optimality: a matching and an odd-set cover of equal size prove each other optimal, and the blossom algorithm produces both. It is equivalent to the Tutte–Berge formula $\nu(G) = \min_{X} \tfrac12\bigl(|V| + |X| - \operatorname{odd}(G - X)\bigr)$, it contains König's theorem as the case where all members of the cover are singletons, and it is the cardinality case of Edmonds' description of the matching polytope by odd-set constraints, which underlies weighted matching, $b$-matching and the polyhedral approach to combinatorial optimization.

The theorem has been proved since 1965, with several independent proofs (via Tutte's theorem, via the Gallai–Edmonds decomposition, via linear programming). Mathlib contains Tutte's perfect-matching theorem for simple graphs, but neither the Tutte–Berge formula nor odd-set covers, alternating trees, blossom shrinking or Berge's augmenting-path theorem in a multigraph setting. This mission produces a machine-checked version of Edmonds' statement together with the lemmas of his algorithmic proof (4.12, 4.14, 4.15, 4.17), which are the correctness core of the blossom algorithm.

Difficulty

Weak duality and Berge's theorem are elementary. The difficulty is the strong direction. The obvious argument, a search for augmenting paths from an exposed vertex, fails because an alternating search tree in a non-bipartite graph can close an odd circuit, after which a vertex is reachable both by an even and by an odd alternating path; a naive search either misses augmenting paths or must back-track exponentially. The proof therefore has to work in shrunken graphs, whose vertices are nested sets of original vertices, and transfer maximality and covers back through every shrinking (4.12–4.15). Keeping track of nested blossoms, of the identity of edges under shrinking and of the parity bookkeeping of 5.8 is the main formal burden.

Formalization scope

• Graphs are the published EdmondsMatching65.Polyhedron.Graph V E (a map from edges to unordered pairs of distinct vertices) with finite V, E; parallel edges are allowed and loops are not. Matchings are Finset E. Maximum and minimum are by cardinality, stated with explicit comparisons rather than sSup/sInf.
• A family of odd sets is a Finset (Finset V); repeating a member only adds capacity, so this does not change the minimum. The capacity of a singleton is $1$, not $(1-1)/2$.
• Paths and circuits are lists of vertices and edges; subgraphs are vertex and edge sets; a matching of a subgraph is a matching of $G$ using only its edges.
• Shrinking is contraction along a partition of the vertices: the vertex type of $G/\mathcal P$ is the set of parts, the edge type is the set of edges not inside a part. Nested blossom shrinking is encoded by an inductive predicate of blossom sets (the complete expansions of pseudovertices), not by a tower of quotient types. Statements that shrink a set other than a circuit assume its induced subgraph connected, the standing assumption of 4.9.
• 5.7 is stated as the existence of a cover: the page's explicit families fail for the two-vertex graph with one edge and for the one-vertex graph, where the claim still holds.
• 5.8 is stated through the configuration the algorithm outputs (blossom sets, a planted Hungarian tree in $G'$, pseudovertices outer), not through the algorithm as a procedure.
• A trivializing formalization is excluded: the goal asserts the equality of the maximum and the minimum, not weak duality and not the separate existence of an optimal matching and an optimal cover.

Reusable beyond this mission: the multigraph shrinking construction, blossom sets, alternating and Hungarian trees, and Berge's theorem in the multigraph setting; these are shared with the companion mission on the invariance of the dual (Gallai–Edmonds). Proofs of any milestone, and alternative proofs of the goal (e.g. through Mathlib's Tutte theorem), are welcome.

Selected references

• J. Edmonds, Paths, trees, and flowers, Canadian Journal of Mathematics 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
• C. Berge, Two theorems in graph theory, Proceedings of the National Academy of Sciences USA 43 (1957), 842–844. https://doi.org/10.1073/pnas.43.9.842
• W. T. Tutte, The factorization of linear graphs, Journal of the London Mathematical Society 22 (1947), 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
• L. Lovász and M. D. Plummer, Matching Theory, North-Holland, 1986. https://doi.org/10.1090/chel/367

Motivation

Online bipartite matching asks an algorithm to assign arriving requests to resources it cannot reassign later. In display advertising, the requests are page views (impressions) and the resources are advertisers who have bought a fixed number of impressions in advance; each impression must be served immediately or lost. In the adversarial model, Karp, Vazirani and Vazirani (STOC 1990) showed that the RANKING algorithm achieves a $1 - 1/e$ fraction of the optimum in expectation, and that no online algorithm does better. Advertising systems, however, have historical traffic data, which motivates the i.i.d. model: the impression types are drawn independently from a distribution that is known in advance.

Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) were the first to beat $1 - 1/e$ in this model, with an algorithm that achieves $\approx 0.67$ with high probability. Their Section 3 asks the complementary question: how close to $1$ can any online algorithm get when the distribution is known? Their Theorem 3 answers that the expected approximation factor of every online algorithm is bounded strictly away from $1$, already on a graph with six vertices. Later work in the same model (Manshadi, Oveis Gharan and Saberi, SODA 2011, arXiv:1007.1673) sharpened both the algorithmic and the hardness side.

Setting

An instance consists of a bipartite graph $G = (A, I, E)$ between a finite set $A$ of advertisers and a finite set $I$ of impression types, a distribution $D$ on $I$, and a number $n$ of arrivals. In this mission $D$ is the uniform distribution on $I$. Online, $n$ impressions arrive one at a time; their types $\omega(0), \dots, \omega(n-1)$ are independent draws from $D$. When impression $t$ arrives, the algorithm must immediately either assign it to an advertiser $a$ with $(a, \omega(t)) \in E$ that has not yet been used, or leave it unassigned. Each advertiser can be used at most once, and decisions are final.

A deterministic online algorithm decides what to do with arrival $t$ from the types $\omega(0), \dots, \omega(t)$ seen so far; it knows $G$, $D$ and $n$, but not the future. A randomized online algorithm is a probability distribution over deterministic ones. $\mathrm{ALG}(\omega)$ is the number of impressions the algorithm assigns on the arrival sequence $\omega$. $\mathrm{OPT}(\omega)$ is the size of a maximum matching of the realization graph, which has one node per arrival $t$, joined to every advertiser adjacent to $\omega(t)$: the most impressions that could have been assigned with hindsight. The expected approximation factor of an algorithm is

$$\mathbb E\!\left[\frac{\mathrm{ALG}(\omega)}{\mathrm{OPT}(\omega)}\right],$$

the expectation taken over the algorithm's randomness and the arrivals.

The 6-cycle instance has $A = \{a, b, c\}$, $I = \{x, y, z\}$ and $E = \{(x,a),(y,a),(y,b),(z,b),(z,c),(x,c)\}$, with the uniform distribution and $n = 3$. The family $\Gamma_k$ consists of $k$ disjoint copies of the 6-cycle, with the uniform distribution on its $3k$ impression types and $n = 3k$ arrivals.

Formalization targets

Goal: Theorem 3

On the 6-cycle, every randomized online algorithm satisfies

$$\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le \frac{26}{27},$$

and there are a constant $c < 1$ and a threshold $K_0$ such that for every $k \ge K_0$ and every randomized online algorithm on $\Gamma_k$,

$$\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le c .$$

The second part is the paper's "there exists a family of instances with $n \to \infty$ for which no algorithm can achieve an expected approximation of $1 - o(1)$", stated on the paper's own family. It leaves $c$ unspecified: Appendix B estimates $c \approx 0.9898$ through approximate counts, and a sharper constant would not invalidate the goal.

Milestones

1. The $(x, y, y)$ scenario (§3, p. 4). For every deterministic online algorithm on the 6-cycle and every type $u$ of the first arrival there is a type $v$ with $\mathrm{ALG}(u, v, v) \le 2$ and $\mathrm{OPT}(u, v, v) = 3$.
2. Theorem 3, first sentence (p. 4). The bound $26/27$ on the 6-cycle, for every randomized online algorithm.

Significance

Theorem 3 sets the ceiling against which algorithms in the i.i.d. model are measured. It rules out an online algorithm with expected factor arbitrarily close to $1$, even though the distribution is known and the instance is tiny, so a constant-factor gap between online and offline matching is intrinsic to the model and not an artefact of adversarial arrivals. The paper's positive results ($1 - 1/e$ for the Suggested Matching algorithm, $\approx 0.67$ for Two Suggested Matchings) sit between $1 - 1/e$ and this ceiling.

The single-instance bound has a short counting proof. The family statement is argued in the paper only in outline: Appendix B approximates the fractions of copies receiving $1$, $2$, $3$ or more impressions, assumes the most favourable outcome on each, and reports the resulting ratio as approximately $0.9898$. A machine-checked proof of the family statement would turn that sketch into a theorem with an explicit constant. To our knowledge neither part has been formalized before.

Difficulty

The single-cycle bound reduces to a finite check, but the paper's "without loss of generality (from the symmetry of the 6-cycle)" hides the cases the algorithm can choose: assigning the first impression to either neighbour, or not assigning it at all. Each case needs its own bad continuation. The passage from deterministic to randomized algorithms is an averaging step.

The family bound is harder. On $\Gamma_k$ the algorithm sees all arrivals in all copies and may coordinate its decisions across copies, so the per-copy loss of the single cycle does not transfer by independence. Moreover the target is the expectation of a ratio, $\mathbb E[\mathrm{ALG}/\mathrm{OPT}]$, not a ratio of expectations: a bound on the expected loss must be combined with concentration of the number of copies that receive exactly three impressions, and with a lower bound on $\mathrm{OPT}$ that holds with high probability. The approximations "$\simeq 3/e^3$, $9/(2e^3)$, $27/(6e^3)$" of Appendix B have unquantified errors and cannot be used as they stand.

Formalization scope

The model is formalized for general finite $A$ and $I$ with uniform arrivals. Arrival sequences are functions Fin n → I. A deterministic online algorithm is a function that receives the time $t$, the prefix of the first $t$ types (Fin t → I) and the current type, and returns an advertiser or none; it cannot read later arrivals. A proposal of a non-adjacent or already used advertiser leaves the impression unassigned, so the encoding covers all online algorithms, including ones that skip an impression while a neighbour is free. A randomized online algorithm is a probability distribution (PMF) on the finite type of deterministic algorithms; by Kuhn's theorem this is equivalent to fresh random choices at each step. $\mathrm{OPT}$ is the maximum size of an injective, edge-respecting partial assignment of arrivals to advertisers. The expected approximation factor is a finite average over all $|I|^n$ arrival sequences, weighted by the algorithm distribution.

The explicit instantiations of the paper's asymptotic wording are as follows:

• "no algorithm can achieve an expected approximation of $1 - o(1)$" becomes $\exists\, c < 1,\ \exists K_0,\ \forall k \ge K_0,\ \forall P:\ \mathbb E[\mathrm{ALG}/\mathrm{OPT}] \le c$ on $\Gamma_k$, with $n = 3k$ tied to $k$, and with $c$ and $K_0$ chosen before $k$ and before the algorithm.
• The paper's constant $0.9898$ is not part of the statement.

Lean's division sets $x/0 = 0$. A formalization of the form "there is an instance on which every algorithm has expected factor at most $26/27$" would be satisfied trivially by a graph without edges, where $\mathrm{OPT} = 0$; the statements here are on the paper's explicit instances, where every impression type has an adjacent advertiser and $\mathrm{OPT} \ge 1$ on every arrival sequence.

A complete development needs finite case analysis on runs of online algorithms, averaging over mixed strategies, and, for the family, concentration inequalities for occupancy counts (Azuma or McDiarmid, both available on the platform) together with bounds on maximum matchings of disjoint unions. The online-algorithm model and the averaging lemmas are reusable for other lower bounds in the i.i.d. model. Proofs of either milestone, and independent proofs of the family statement with any explicit $c < 1$, are welcome.

Selected references

• J. Feldman, A. Mehta, V. Mirrokni, S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, FOCS 2009; arXiv:0905.4100v1. https://arxiv.org/abs/0905.4100
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
• V. H. Manshadi, S. Oveis Gharan, A. Saberi, Online Stochastic Matching: Online Actions Based on Offline Statistics, SODA 2011; arXiv:1007.1673. https://arxiv.org/abs/1007.1673

Motivation

Single-machine scheduling with precedence constraints asks for an order in which one machine processes jobs while respecting prescribed comparisons between them. For the objective of minimizing total weighted completion time, the structure of the precedence order can influence the quality of approximation algorithms. Ambühl, Mastrolilli, Mutsanas, and Svensson connect one such approach to coloring a graph built from the order's incomparable pairs. A bounded number of colors would make a certain class of coloring-based guarantees uniform over the class of precedence orders. Their Theorem 4.3 shows that canonical interval orders have no such uniform bound for this particular graph. Ambühl et al., §4.2, p. 658

An interval order is a partial order whose elements can be represented by closed real intervals, with one element strictly before another when the first interval ends before the second begins. Interval orders are a familiar restriction of general precedence systems. The paper distinguishes them from semiorders, represented by intervals of equal length, for which it reports a three-element realizer bound and a corresponding scheduling guarantee. The chromatic obstruction here explains why that particular bounded-color route cannot be extended uniformly from semiorders to all interval orders. It does not assert that every scheduling approach to interval orders fails. Ambühl et al., §§3–4.2, pp. 656–658

Setting

For an integer $n\ge2$, let $[n]$ be a linearly ordered set with $n$ points. The canonical interval order $I_n$ has one element for every pair of distinct points $a<b$ in $[n]$, viewed as the closed interval $[a,b]$. For two such intervals, write $S\le_{I_n}T$ when $S=T$ or the right endpoint of $S$ is strictly less than the left endpoint of $T$. Thus intervals that touch at an endpoint remain incomparable. The formalization represents each interval by its two-element endpoint set, and its order relation is equivalent to this endpoint rule. Ambühl et al., §4.2, p. 658

For any partial order $P$ on a ground set $N$, an ordered incomparable pair is $(x,y)$ with neither $x\le_P y$ nor $y\le_P x$. Both $(x,y)$ and $(y,x)$ are vertices when $x$ and $y$ are incomparable. A linear extension of $P$ is a linear order on the same elements that contains all comparisons of $P$. It reverses $(x,y)$ if it places $y$ before $x$. The graph $G_P$ has the ordered incomparable pairs as vertices. Two distinct vertices form an edge when no linear extension reverses both, while each singleton can be reversed by some linear extension. This singleton condition is the minimality clause in the paper's definition through its hypergraph of incomparable pairs. Ambühl et al., §2.1, p. 655, §3, p. 656

A proper $k$-coloring assigns one of $k$ colors to every vertex of $G_P$ so that endpoints of an edge have different colors. The graph's chromatic number $\chi(G_P)$ is the least positive number of colors that works, when the graph is nonempty. The mission uses the equivalent predicate that no proper map into a fixed $k$-element color set exists once $n$ is large enough. This also gives a clear interpretation at $k=0$.

Formalization targets

The goal is Theorem 4.3: for each fixed integer $k$, all sufficiently large canonical interval orders have incomparable-pairs graphs with chromatic number greater than $k$. With $k\ge0$, the Lean target is

$$\forall k\in\mathbb N,\ \exists n_0\ge2,\ \forall n\ge n_0,\quad G_{I_n}\text{ is not $k$-colorable}.$$

The paper states $k$ as an integer. Its negative cases are immediate from nonnegativity of chromatic numbers; the target states the substantive range. The threshold $n_0$ may depend on $k$, while $I_n$ and $G_{I_n}$ are constructed from $n$ rather than supplied as arbitrary objects. Ambühl et al., Theorem 4.3, p. 658

Two assertions from the theorem's proof serve as milestones. First, $\chi(G_{I_n})$ is nondecreasing as $n$ increases. Second, for four endpoints $i<j<\ell<m$, the vertices $(\{i,j\},\{j,\ell\})$ and $(\{j,\ell\},\{\ell,m\})$ are adjacent in $G_{I_n}$. They are recorded with their wording and provenance from §4.2. A separately published theorem on hypergraph Ramsey numbers is included as a reference because the source uses that theorem in its large-$n$ argument. Ambühl et al., proof of Theorem 4.3, p. 658

Significance

The result provides a precise structural limitation: across the canonical interval orders, the chromatic numbers of $G_{I_n}$ cannot be bounded by one constant. The graph $G_P$ is a specific graph of ordered incomparable pairs, distinct from other graphs that can be associated with a scheduling instance. Thus the conclusion addresses the bounded-color approach attached to this graph, without asserting an algorithmic impossibility for interval-order scheduling. The paper contrasts this limitation with the bounded-realizer situation for semiorders. Ambühl et al., §§3–4.2, pp. 656–658

The theorem is proved in the 2011 paper. The remaining work in this mission is a machine-checked development of its definition layer, its two stated supporting assertions, and the unbounded-color conclusion. The partial-order property of $I_n$ is already proved in the definition file; the three theorem statements are open proof targets in the proposal. A completed formalization would also give reusable components for finite interval orders, ordered incomparable pairs, and coloring arguments in dimension theory.

Difficulty

A pair of intervals overlapping or touching is easy to recognize as incomparable, but graph adjacency has a stronger meaning: it quantifies over every linear extension of the entire partial order. A local test based only on the four displayed intervals would silently change the graph. Likewise, the fact that two vertices have different endpoint descriptions does not by itself make them adjacent. The formal argument must connect the canonical interval representation to the global extension-based edge condition, then show that a bounded coloring cannot persist as the endpoint set grows. Ambühl et al., proof of Theorem 4.3, p. 658

Formalization scope

The endpoint set is Fin n, hence indexed $0,\ldots,n-1$ rather than the paper's $1,\ldots,n$; the shift preserves order. Elements of $I_n$ are exactly two-element subsets of this set. The order relation includes equality and strict separation of endpoint sets and is proved to be a partial order. The graph is defined for an arbitrary binary relation so it can be reused, but every target here applies it to the concrete partial order $I_n$. Vertices are ordered incomparable pairs, and adjacency retains both singleton reversibility and failure of simultaneous reversibility. Defining adjacency directly from the desired four-point pattern would trivialize the target and is excluded.

Colorable n k means existence of a proper function from all vertices of $G_{I_n}$ to Fin k. For an empty graph, zero-colorability is allowed by this representation. The theorem therefore includes a threshold $n_0\ge2$ and quantifies over every $n\ge n_0$; the assertion itself forces the threshold past any empty-graph exceptions. The formal target uses natural $k$; the paper's negative integer values need no separate theorem. No asymptotic notation or unspecified constants occur. The source's Ramsey number $R(3:4,\ldots,4)$ is not hard-coded into the goal, because the source asserts existence of a suitable threshold, not that the least threshold equals that value.

The printed adjacency justification names an alternating-cycle pair set different from the two adjacent vertices in the preceding sentence. The milestone formalizes the adjacency assertion itself and records the printed explanation verbatim for review; it does not turn the mismatched pair set into a hypothesis. The mission needs finite order embeddings, linear extensions, graph colorings, and a finite Ramsey theorem. The existing published Ramsey theorem is referenced as a reusable result. No scheduling approximation algorithm, polynomial-time statement, or numerical scheduling guarantee is formalized in this mission.

Selected references

• Christoph Ambühl, Monaldo Mastrolilli, Nikolaos Mutsanas, and Ola Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4), 653–669, 2011. DOI: 10.1287/moor.1110.0512

Motivation

MAXCUT asks for a partition of the vertices of a weighted graph into two sets that maximizes the total weight of the edges between them. It is one of Karp's original NP-hard problems, so no polynomial-time exact algorithm is expected, and the natural question is how close a polynomial-time algorithm can come to the optimum. Sampling a uniformly random partition already achieves, in expectation, half of the optimal value. For two decades this factor $1/2$ was essentially the best known.

Goemans and Williamson (J. ACM 42(6), 1995) replaced the combinatorial problem by a semidefinite relaxation, solvable in polynomial time by interior point methods, and rounded its solution with a random Gaussian hyperplane. They proved that the resulting cut has expected weight at least $0.878$ times the maximum. The technique founded the use of semidefinite programming in approximation algorithms. Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 37(1), 2007) showed that, assuming the Unique Games Conjecture, no polynomial-time algorithm achieves a better constant. Nesterov (Optim. Methods Softw. 9, 1998) extended the rounding analysis to maximizing any positive semidefinite quadratic form over the hypercube, with the constant $2/\pi$.

This mission formalizes the presentation of these results in §6.6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 343–347.

Setting

Let $n\ge 0$ and let $A\in\mathbb R^{n\times n}$ be a symmetric matrix with non-negative entries; $A_{i,j}$ is the weight between points $i$ and $j$. The graph Laplacian is $L=D-A$, where $D$ is the diagonal matrix with entries $\sum_{j=1}^n A_{i,j}$. For $x\in\{-1,1\}^n$ the vector $x$ encodes a partition, and MAXCUT is (6.7)

$$\max_{x\in\{-1,1\}^n} x^\top L x .$$

Write $\langle M,X\rangle=\operatorname{Tr}(M^\top X)$ for the Frobenius inner product and $\mathbb S^n_+$ for the symmetric positive semidefinite matrices. Since $x^\top Lx=\langle L,xx^\top\rangle$ and $xx^\top\in\mathbb S^n_+$ has unit diagonal, MAXCUT is bounded above by the SDP relaxation

$$\max\bigl\{\langle L,X\rangle : X\in\mathbb S^n_+,\ X_{i,i}=1,\ i\in[n]\bigr\}.$$

A solution $\Sigma$ of the relaxation is any feasible matrix attaining this maximum. The rounding draws $\xi\sim\mathcal N(0,\Sigma)$, a centered Gaussian vector with covariance $\Sigma$, and outputs $\zeta=\operatorname{sign}(\xi)\in\{-1,1\}^n$ coordinatewise.

Formalization targets

Goal: Theorem 6.11 (Goemans–Williamson)

For $A$ symmetric with non-negative entries, $L=D-A$, $\Sigma$ any solution of the relaxation, $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$:

$$\mathbb E\,\zeta^\top L\zeta\ \ge\ 0.878\max_{x\in\{-1,1\}^n}x^\top Lx.$$

Milestones

1. Bounded entries. If $\Sigma\in\mathbb S^n_+$ and $\Sigma_{i,i}=1$, then $|\Sigma_{i,j}|\le 1$ (remark in the proof of Lemma 6.12).
2. Lemma 6.12 (Sheppard's formula). If $\xi\sim\mathcal N(0,\Sigma)$ with $\Sigma_{i,i}=1$ and $\zeta=\operatorname{sign}(\xi)$, then $\mathbb E\,\zeta_i\zeta_j=\frac{2}{\pi}\arcsin(\Sigma_{i,j})$.
3. Inequality (6.8). $1-\frac{2}{\pi}\arcsin(t)\ge 0.878(1-t)$ for all $t\in[-1,1]$.
4. Relaxation inequality. $\max_{x}x^\top Lx=\max_x\langle L,xx^\top\rangle\le\langle L,\Sigma\rangle$ for every solution $\Sigma$.

The separately stated Laplacian identity on p. 346 is also included as a theorem item: if $X_{i,i}=1$ for all $i$, then $\langle L,X\rangle=\sum_{i,j}A_{i,j}(1-X_{i,j})$; for $x\in\{-1,1\}^n$, $x^\top Lx=\sum_{i,j}A_{i,j}(1-x_ix_j)$.

Companion: Theorem 6.13 (Nesterov)

For $B\in\mathbb S^n_+$, $\Sigma$ a solution of $\max\{\langle B,X\rangle : X\in\mathbb S^n_+,\ X_{i,i}=1\}$, $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$:

$$\mathbb E\,\zeta^\top B\zeta\ \ge\ \frac{2}{\pi}\max_{x\in\{-1,1\}^n}x^\top Bx.$$

Significance

The result. Theorem 6.11 is a polynomial-time randomized $0.878$-approximation for MAXCUT: the relaxation is a semidefinite program, and sampling a Gaussian vector and taking signs is cheap. Repeated sampling turns the bound in expectation into a cut of value close to $0.878$ times the optimum with high probability. The same scheme of relaxation followed by randomized rounding underlies approximation algorithms for MAX-2SAT, correlation clustering and quadratic programs over the hypercube, and Nesterov's Theorem 6.13 is the version for an arbitrary positive semidefinite objective.

Formalizing it. Both theorems were proved long ago. To our knowledge neither has a machine-checked proof in Mathlib. The platform has related statements from other books, in different forms: Grothendieck's identity for a standard Gaussian and two unit vectors, and the relaxation guarantee with a Grothendieck constant. This mission states the textbook's results for a Gaussian with a possibly singular covariance matrix, which is the form the rounding uses. A complete development needs Sheppard's formula for a degenerate bivariate Gaussian, an elementary but careful real-variable inequality, and a link between Mathlib's multivariate Gaussian and Gram factorizations of $\Sigma$. All three are reusable.

Difficulty

The algebra (the Laplacian identity and milestone 4) is routine. The probabilistic core is Lemma 6.12. The textbook argument reduces it to the probability that a uniformly random direction separates two unit vectors, which is "a quick picture" on paper. In Lean this requires showing that the pair $(\xi_i,\xi_j)$ has the law of $(\langle V_i,\varepsilon\rangle,\langle V_j,\varepsilon\rangle)$ for a standard Gaussian $\varepsilon$, and then computing an angular measure in the plane, including the degenerate cases $\Sigma_{i,j}=\pm1$, where the pair is supported on a line. A density-based argument fails there, because $\mathcal N(0,\Sigma)$ has no density when $\Sigma$ is singular, and singular solutions of the relaxation occur (for instance $\Sigma=xx^\top$). Inequality (6.8) is a statement about a transcendental function on a closed interval with a tight constant ($0.878$ against the true minimum $\approx0.87856$), so crude estimates do not suffice near the minimizer $t\approx-0.689$.

Formalization scope

• Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin n → ℝ. $\mathbb S^n_+$ is Matrix.PosSemidef, which includes symmetry, and $\langle M,X\rangle$ is trace (Mᵀ * X).
• $\mathcal N(0,\Sigma)$ is Mathlib's ProbabilityTheory.multivariateGaussian 0 Σ on EuclideanSpace ℝ (Fin n), defined for every positive semidefinite $\Sigma$, singular ones included. Expectations are Bochner integrals against it, and each theorem also asserts integrability of its (bounded) integrand.
• The sign is $\{-1,1\}$-valued: $\operatorname{sign}(r)=1$ for $r\ge0$ and $-1$ for $r<0$. Mathlib's Real.sign would give $\operatorname{sign}(0)=0$, which takes $\zeta$ out of $\{-1,1\}^n$; the two agree almost surely because $\Sigma_{i,i}=1$.
• The maximum over the hypercube is a finite maximum (Finset.sup') over the $2^n$ Boolean vectors read as $\pm1$ vectors, so it is never a junk value. "The solution" of the relaxation means any maximizer, and maximizers exist since the feasible set is compact and contains the identity.
• Standing hypotheses: in Theorem 6.11, $A$ symmetric with non-negative entries (the book's MAXCUT setting); in Lemma 6.12, $\Sigma$ positive semidefinite (implicit in "$\xi\sim\mathcal N(0,\Sigma)$"); in Theorem 6.13, $B$ positive semidefinite. The identities of milestones 4 and 5 hold for every real matrix $A$ and are stated without hypotheses on $A$.
• Ruled out: tying $\xi$'s law to anything other than $\Sigma$, or dropping optimality of $\Sigma$, would make the goal false or vacuous; here the law is exactly $\mathcal N(0,\Sigma)$ and $\Sigma$ is a maximizer.
• Welcome contributions: Sheppard's formula in Mathlib's multivariate Gaussian language, a proof of (6.8), and the Schur product theorem ($A,B\succeq0\Rightarrow A\circ B\succeq0$) used in Theorem 6.13.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42(6):1115–1145, 1995. doi:10.1145/227683.227684
• Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optim. Methods Softw. 9(1–3):141–160, 1998. doi:10.1080/10556789808805690
• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37(1):319–357, 2007. doi:10.1137/S0097539705447372
• W. F. Sheppard, On the application of the theory of error to cases of normal distribution and normal correlation, Phil. Trans. R. Soc. A 192:101–167, 1899. doi:10.1098/rsta.1899.0003

Motivation

Single-machine scheduling with precedence constraints, written $1|\mathrm{prec}|\sum w_jC_j$ in the notation of Graham et al., asks for an order of $n$ weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph built from the precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain $(2-2/f)$-approximations for orders of fractional dimension at most $f$. This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.

Setting

An instance $S$ consists of a finite set $N$ of jobs, a partial order $P$ on $N$ (reflexive, antisymmetric, transitive; $(i,j)\in P$ with $i\ne j$ means job $i$ finishes before job $j$ starts), processing times $p_j\ge 0$ and weights $w_j\ge 0$.

Two jobs $x,y$ are incomparable, $x\parallel y$, when neither $(x,y)$ nor $(y,x)$ lies in $P$. The set $\operatorname{inc}(P)$ of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of $P$ is a linear order $L\supseteq P$ on $N$; it reverses $(x,y)\in\operatorname{inc}(P)$ when $y<x$ in $L$. A nonempty multiset $L_1,\dots,L_t$ of linear extensions is a $k:t$-realizer if every incomparable pair is reversed by at least $k$ of them. The fractional dimension $\operatorname{fdim}(P)$ is the least ratio $t/k$ over all $k:t$-realizers.

The vertex cover graph $G^S_P$ has the incomparable pairs as nodes; nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell),(k,j)\in P$ (symmetrically closed). Node $(i,j)$ has weight $w_{(i,j)}=p_iw_j$, and $w(C)=\sum_{u\in C}w_u$. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$. The LP relaxation [CS-LP] asks for $x\in[0,1]^{\operatorname{inc}(P)}$ with $x_u+x_v\ge1$ on every edge, minimizing $\sum_u w_ux_u$. For a solution $x$ write $V_a=\{u: x_u=a\}$, and for a linear extension $L$ let $I_{1/2}(L)$ be the pairs of $V_{1/2}$ reversed in $L$.

The graph of incomparable pairs $G_P$ (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.

Formalization targets

Goal: Theorem 5.1 (p. 658)

For an instance $S$, a $k:t$-realizer $L_1,\dots,L_t$ of $P$, and a half-integral optimal solution $x$ of [CS-LP], put $C_i=V_1\cup\bigl(V_{1/2}\setminus I_{1/2}(L_i)\bigr)$. Then every $C_i$ is a vertex cover of $G^S_P$, and

$$\frac1t\sum_{i=1}^t w(C_i)\;\le\;\Bigl(2-\frac{2}{t/k}\Bigr)\mathrm{OPT}.$$

Milestones

• Proposition 3.2 (p. 657): $G^S_P=G_P$.
• Footnote 4 (p. 659): the pairs reversed by a linear extension are independent in $G^S_P$.
• Eq. (4): $\frac1t|\{i: L_i\text{ reverses }u\}|\ge k/t$ for every incomparable pair $u$.
• Eq. (5): $\frac1t\sum_i w(I_{1/2}(L_i))\ge \frac kt\,w(V_{1/2})$.
• Hochbaum's observation (§5, p. 659): for half-integral feasible $x$, $V_1\cup C$ covers $G^S_P$ whenever $C$ covers $G^S_P[V_{1/2}]$.
• Eqs. (6)–(8): $\frac1t\sum_iw(C_i)\le w(V_1)+(1-\frac kt)w(V_{1/2})\le 2(1-\frac kt)(w(V_1)+\frac12w(V_{1/2}))\le(2-\frac2{t/k})\mathrm{OPT}$ when $P$ is not a linear order.

Significance

The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an $\alpha$-approximate vertex cover of $G^S_P$ into an $\alpha$-approximate schedule, Theorem 5.1 gives a $(2-2/f)$-approximation for $1|\mathrm{prec}|\sum w_jC_j$ whenever the precedence order has an efficiently samplable realizer with $t/k\le f$. The paper applies it to interval orders ($3/2$), convex bipartite orders and semiorders ($4/3$), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, $k$-fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.

Difficulty

Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion $G_P\subseteq G^S_P$ in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of $P$ by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality $t\ge 2k$ used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of $(x,y)$ and $(y,x)$.

Formalization scope

• Jobs form a finite type N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.
• $\operatorname{inc}(P)$ is the subtype IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a $k:t$-realizer is a family Fin t → LinearExtension P with $t>0$. Reversal of $(x,y)$ means $y<x$ in $L$ throughout; the page's "$y>x$" in Eq. (4) and "$\mathrm{Prob}[j>i]$" in Eq. (5) are the same family of inequalities because $\operatorname{inc}(P)$ is symmetric.
• $G^S_P$ is the symmetric closure of the printed three-case rule on distinct nodes. $G_P$ is defined through linear extensions and hyperedge minimality, never through the three-case rule, so Proposition 3.2 is a genuine statement and not a definitional equality.
• [CS-LP] drops the constant term $\sum_jp_jw_j+\sum_{(i,j)\in P}p_iw_j$ of [CS-IP], which does not affect optimality. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$, taken over a finite nonempty family.
• Not formalized: "efficiently samplable", "polynomial time" and "randomized algorithm". The expectation over a uniformly sampled $L_i$ is stated as the average $\frac1t\sum_{i=1}^t$, which is equivalent to it and stronger than the existence of one good index. The existence of a half-integral optimal [CS-LP] solution (Nemhauser–Trotter, cited) is a hypothesis on $x$. The conversion of a vertex cover into a schedule (Theorem 2.1, cited) is not formalized; the goal is stated for vertex covers of $G^S_P$.
• Constants: $2-2/(t/k)$ in real arithmetic; it equals $2-2k/t$, and equals $2$ when $k=0$.
• The paper assumes $\operatorname{fdim}(P)\ge2$, i.e. $P$ is not a linear order. Eqs. (6)–(8) carry that hypothesis as the paper does; the goal omits it because for a linear order both sides are $0$.
• Conclusion (a), that each $C_i$ is a vertex cover, is part of the goal and is not assumed.

Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the approximability of single-machine scheduling with precedence constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4), 2009 (reference [2] of the paper).
• J. R. Correa, A. S. Schulz, Single-machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992 (reference [7]).
• S. Felsner, W. T. Trotter, Dimension, graph and hypergraph coloring, Order 17(2):167–177, 2000 (reference [13]).
• D. S. Hochbaum, Efficient bounds for the stable set, vertex cover and set packing problems, Discrete Appl. Math. 6(3):243–254, 1983 (reference [20]).
• G. L. Nemhauser, L. E. Trotter, Vertex packings: structural properties and algorithms, Math. Programming 8(1):232–248, 1975 (reference [29]).

Motivation

Hassler Whitney introduced matroids in On the Abstract Properties of Linear Dependence (Amer. J. Math. 57, 1935, doi:10.2307/2371182) to capture what linear dependence among the columns of a matrix and the circuit structure of a graph have in common. One of the central constructions of the paper is duality. For graphs, duality exists only for planar graphs (Whitney, Non-separable and planar graphs, Trans. AMS 34, 1932); for matroids Whitney showed that every matroid has a dual, and that duality has a direct linear-algebra model: the matroid of a subspace of $\mathbb R^n$ and the matroid of its orthogonal complement are duals.

Matroid duality underlies much of combinatorial optimization: the duality between cycles and cuts in graphs, the relation between a linear code and its dual code, the exchange of rank and corank in matroid intersection and partition, and the treatment of network flows as duals of potential problems. Whitney's §§11–13 are where this structure is first defined and where its linear-algebra meaning (Theorem 28) is established.

Setting

A matroid $M$ is a finite set of elements $e_1,\dots,e_n$ with a rank function $r$ on its subsets; equivalently, a family of independent sets, or of bases (maximal independent sets). For a subset $N$ write $\rho(N)$ for its number of elements and

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

for its nullity; $r(M)$ and $n(M)$ are the rank and nullity of the whole set of elements.

Duality (§11). Let $M$ and $M'$ be matroids and $\sigma$ a one-to-one correspondence between their elements. $M'$ is a dual of $M$ (via $\sigma$) if, for every subset $N$ of $M$, with $N'$ the complement in $M'$ of $\sigma(N)$,

$$r(N') = r(M') - n(N). \tag{11.1}$$

The matroid of a subspace (§12). Let $E_n$ be $n$-dimensional Euclidean space with coordinates $x_1,\dots,x_n$, and let $H$ be a hyperplane through the origin, which in Whitney's usage is a linear subspace of any dimension. For a set $S$ of coordinates, project $H$ onto the coordinate subspace $E'_S$ spanned by the axes $x_i$, $i\in S$. The matroid associated with $H$ has elements $e_1,\dots,e_n$, one per coordinate, and gives the set $\{e_i: i\in S\}$ the rank

$$r_H(S) = \dim \pi_S(H).$$

If $H$ is the row space of a matrix $\mathbf M$, then $r_H(S)$ is the rank of the columns of $\mathbf M$ indexed by $S$, so the associated matroid is the column matroid of $\mathbf M$.

In the Lean development these objects are WhitneyMatroid.Components.nullity (shared), IsDualVia M M' σ, IsDual M M', subspaceRank H S and IsAssociated M H.

Formalization targets

Goal: Theorem 28

Let $H$ be a subspace of $E_n$ and $H' = H^\perp$ its orthogonal complement. If $M$ and $M'$ are the matroids associated with $H$ and $H'$, then $M$ and $M'$ are duals under the correspondence of equal coordinates:

$$\forall N\subseteq\{e_1,\dots,e_n\}:\qquad r_{M'}(\overline N) = r(M') - n_M(N).$$

Milestones

1. Theorem 27. For every subspace $H$ there is exactly one matroid associated with $H$.
2. Theorem 6 (already proved on the platform). All bases have the same number of elements.
3. Theorem 7. $B$ is a base iff $r(B)=r(M)$ and $n(B)=0$.
4. Theorem 8. If $B$ is a base and $N$ is independent, then $N\cup N'$ is a base for some $N'\subseteq B$.
5. Theorem 20. If $M'$ is a dual of $M$, then $r(M') = n(M)$ and $n(M') = r(M)$.
6. Theorem 23. $M'$ is a dual of $M$ via $\sigma$ iff, for every $B$, $B$ is a base of $M$ exactly when the complement of $\sigma(B)$ is a base of $M'$.
7. Theorem 21. Duality is symmetric.
8. Theorem 22. Every matroid has a dual.

Significance

The result. Theorem 28 identifies abstract duality with orthogonal complementation. With Theorem 23 it says that the column matroid of a real matrix whose rows span $H$ and the column matroid of a matrix whose rows span $H^\perp$ have complementary bases. This is the basis of the standard representation of the dual of a represented matroid ($[I_r\mid A]$ and $[-A^{\mathsf T}\mid I_{n-r}]$), of the cycle/cocycle duality of graphs viewed through incidence matrices, and of the fact that a matroid representable over a field has a dual representable over the same field. Theorems 20–23 are the basic facts every later treatment of matroid duality starts from: duality exchanges rank and nullity, is symmetric, always exists, and is characterized by base complements.

Formalizing it. All of these results are classical and proved in Whitney's paper; what this mission adds is a machine-checked development of Whitney's own definition of duality, the rank identity (11.1), rather than the base-complement definition used in modern libraries. Mathlib defines the dual matroid $M^*$ by base complements and proves that it is a matroid; it does not, at the pinned revision, contain the rank formula (11.1) for $M^*$, the matroid of a real subspace, or Theorem 28. Theorem 6 is already proved on the platform and enters as a reference. Theorems 7 and 8 are close to Mathlib lemmas and are footholds rather than new content.

Difficulty

The difficulty of the goal is not in the combinatorics but in the passage between the two descriptions of a subspace. The natural first idea is to compare the ranks $r_H(S)$ and $r_{H^\perp}(\overline S)$ directly by counting dimensions of $H$ and $H^\perp$. This does not close: $r_H(S)$ is the dimension of a projection of $H$ onto coordinates, while $\dim H^\perp = n - \dim H$ only controls $H^\perp$ as a whole, and the rank of a complementary coordinate set in $M'$ is not determined by the dimensions of $H$ and $H^\perp$ alone. Some relation between coordinate projections of $H$ and the structure of $H^\perp$ on the complementary coordinates has to be established. Theorem 27 is itself nontrivial in Lean: the rank function $r_H$ has to be shown to satisfy the matroid axioms, which needs a careful treatment of coordinate projections and of submodularity of dimension. On the abstract side, Theorem 23 needs both directions of the passage between the rank identity and base complements, including the counting step $r(M) + r(M') = \rho(M)$.

Formalization scope

• Matroids are Mathlib Matroid α on a finite type α whose ground set is all of α (Whitney's matroid is its finite set of elements). This finiteness and the ground set convention are part of the definitions; all theorems are stated under them.
• Ranks and nullities. Ranks are Mathlib's eRk, finite on a finite type and converted to integers; the nullity $n(N)=\rho(N)-r(N)$ and the identity (11.1) are computed in $\mathbb Z$. No truncated subtraction appears.
• Duality is Whitney's rank identity (11.1) for every subset, for a fixed bijection σ : α ≃ β (IsDualVia) or some bijection (IsDual). It is deliberately not defined as Mathlib's M✶: with that definition Theorem 23 would be nearly definitional and Theorem 28 would lose the rank identity. A formalization that replaces (11.1) by the base-complement condition, or states Theorem 28 only for bases, is not this mission's goal.
• Euclidean space is EuclideanSpace ℝ (Fin n) with its standard inner product; the orthogonal hyperplane is Hᗮ. The field is $\mathbb R$, as in the paper; the analogous statement over other fields with the dot-product annihilator is a generalization and not part of this mission.
• The associated matroid is a predicate (IsAssociated M H): ground set Fin n, and the rank of every set $S$ of coordinates equals the finrank of the image of $H$ under the coordinate projection onto $S$ (not of $H\cap E'_S$, a different set function). Existence and uniqueness is Theorem 27.
• Implicit hypotheses made explicit: the ground sets are finite and equal to the whole element type; Whitney's "dimension $r$" and "dimension $n-r$" in Theorem 28 are consequences of $H'=H^\perp$ and are not hypotheses. The goal covers $n=0$, $H=\{0\}$ and $H=E_n$.
• Infrastructure needed and reusable: the matroid of a real subspace (equivalently the column matroid of a real matrix), with its rank function in terms of coordinate projections; the rank formula of the dual matroid; the dimension identity relating projections of $H$ and sections of $H^\perp$. All are reusable for the other missions of this series (the Fano matroid and binary matroids) and for any later work on represented matroids. Proofs of the milestones, alternative proofs of Theorem 28 through Mathlib's M✶, and supporting lemmas on coordinate projections are 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
• J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011, Chapter 2 (duality). https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• Mathlib, Mathlib.Combinatorics.Matroid (Dual, Rank). https://github.com/leanprover-community/mathlib4

Motivation

Assortment optimization asks which set of products a firm should offer when customers choose among the offered products according to a discrete choice model; it underlies shelf-space planning in retail and fare-class control in airline revenue management (Talluri and van Ryzin, 2004). Under the nested logit model products are grouped into nests, and a customer first picks a nest and then a product inside it. Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) map out how hard this problem is across variants of the model.

When every nest dissimilarity parameter is at most one and a customer who chose a nest always buys there, offering the top-revenue products of each nest is optimal (Theorem 4 of the paper, the subject of an earlier mission of this series). Once a customer may leave a nest without buying — a partially-captured nest — that structure breaks and the problem becomes NP-hard (Theorem 8). This mission targets the paper's response: a small, explicitly constructed family of candidate assortments per nest from which a linear program recovers a solution within a factor of two of optimal.

Setting

There are $m$ nests $M$ and, in each nest, $n$ products $N = \{1, \dots, n\}$. Product $j$ of nest $i$ has a revenue $r_{ij} \ge 0$ and a preference weight $v_{ij} > 0$, with $r_{i1} \ge \dots \ge r_{in}$. Nest $i$ has a dissimilarity parameter $\gamma_i > 0$ and a within-nest no-purchase weight $v_{i0} \ge 0$; $v_0 \ge 0$ is the weight of choosing no nest. For an assortment $S_i \subseteq N$,

$$V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j \in S_i} r_{ij} v_{ij}}{V_i(S_i)},\quad R_i(\emptyset)=0,$$

and the expected revenue of $(S_1, \dots, S_m)$ is $\Pi = \sum_i V_i(S_i)^{\gamma_i} R_i(S_i) / (v_0 + \sum_i V_i(S_i)^{\gamma_i})$. The optimal expected revenue $Z^*$ is the optimal value of the linear program

$$\text{(3)}\quad \min\ x \quad\text{s.t.}\quad v_0 x \ge \sum_{i \in M} y_i,\qquad y_i \ge V_i(S_i)^{\gamma_i}\big(R_i(S_i) - x\big)\ \ \forall S_i \subseteq N,\ i \in M,$$

and problem (4) is the same program with the second family of constraints imposed only for a chosen collection of candidate assortments in each nest.

Throughout, $\gamma_i \le 1$ for every nest and the $v_{i0}$ are arbitrary. For a capacity $\epsilon_i \ge 0$, the knapsack value $K_i(\epsilon_i)$ is the largest $\sum_{j \in S} r_{ij} v_{ij}$ over assortments $S$ with $\sum_{j \in S} v_{ij} \le \epsilon_i$ (display (9)). Its continuous relaxation (11) allows fractional $z_{ij} \in [0, \mathbf 1(v_{ij} \le \epsilon_i)]$ under the same capacity. The greedy solution $\hat z_i(\epsilon_i)$ of (11) fills the capacity with the products of weight at most $\epsilon_i$ in revenue order, each fully while it fits and the next one fractionally, and

$$\hat S_i(\epsilon_i) = \{ j \in N : \hat z_{ij}(\epsilon_i) = 1 \}.$$

Problem (10) replaces the per-assortment constraints of (3) by $y_i \ge \max_{\epsilon_i \ge 0} (v_{i0}+\epsilon_i)^{\gamma_i}[K_i(\epsilon_i)/(v_{i0}+\epsilon_i) - x]$.

Formalization targets

Goal: Theorem 10 (p. 24)

Let $(\hat x, \hat y)$ be an optimal solution of (4) with candidate collections $\{\hat S_i(\epsilon_i) : \epsilon_i \in [0,\infty]\} \cup \{\{j\} : j \in N\}$. Then

$$(2\hat x,\ 2\hat y) \ \text{ is feasible for (3).}$$

Milestones

1. Per-nest identity (proof of Lemma 9, p. 23). For $x \ge 0$, $\max_{S_i} V_i(S_i)^{\gamma_i}(R_i(S_i) - x) = \max_{\epsilon_i \ge 0}(v_{i0}+\epsilon_i)^{\gamma_i}[K_i(\epsilon_i)/(v_{i0}+\epsilon_i) - x]$.
2. Lemma 9 (p. 23). Problems (3) and (10) have the same optimal solutions.
3. Relaxation (p. 23). Every feasible point of (9) is feasible for (11), so $\hat K_i(\epsilon_i) \ge K_i(\epsilon_i)$.
4. Greedy solution (pp. 23–24). $\hat z_i(\epsilon_i)$ is optimal for (11) and has at most one fractional component.
5. Sign (A.3, p. 45). $\hat x \ge 0$.
6. Inequalities (28) and (29) (A.3, pp. 45–46). In both cases — $\hat z_i(\epsilon)$ with and without a fractional component — $2\hat y_i \ge (v_{i0}+\epsilon)^{\gamma_i}[K_i(\epsilon)/(v_{i0}+\epsilon) - 2\hat x]$.

Two further statements accompany the goal: the factor-two revenue guarantee obtained from Theorem 10 and Theorem 1 of the paper, and the fact that every $\hat S_i(\epsilon_i)$ is one of the at most $1 + n^2$ assortments $N^k_{ij}$, the first $j$ products by revenue among the $k$ lightest.

Significance

Theorem 10 turns an NP-hard assortment problem into a linear program with $1 + m$ variables and $1 + m(1 + n + n^2)$ constraints whose solution is within a factor of two of optimal. The construction is explicit: the candidates are defined by a greedy rule, not by an optimization oracle. The same template, a restricted linear program whose doubled optimum is feasible for the full one, is reused in §6 of the paper for the most general instances, and Lemma 9's knapsack reformulation is the link to the classical approximation theory of knapsack problems (Williamson and Shmoys, 2011).

The theorem is proved in the paper. No machine-checked proof of it, of Lemma 9, or of greedy optimality for the continuous knapsack with an eligibility bound exists on the platform. Formalizing it yields a checked factor-two guarantee and a reusable fractional-knapsack development.

Difficulty

The obvious argument would compare the restricted program (4) with (3) constraint by constraint. That fails: (3) has one constraint per subset of products, and most subsets are not candidates. The comparison has to pass through the knapsack reformulation (10), which requires showing that a maximum over all subsets equals a maximum over a one-dimensional capacity parameter, using $\gamma_i \le 1$ and $x \ge 0$ in an essential way. The second obstacle is that the greedy assortment $\hat S_i(\epsilon_i)$ keeps only the fully taken products, so its value can fall short of the continuous knapsack value, and no single candidate assortment need attain the knapsack bound. With dissimilarity parameters above one the monotonicity behind the reformulation is lost, and §6 of the paper needs a different factor.

Formalization scope

Products are Fin n (indices $0, \dots, n-1$), nests a finite type, and every quantity is real. Powers are Real.rpow; $x/0 = 0$, which gives $R_i(\emptyset) = 0$. An optimal solution of a linear program is a feasible pair whose $x$ is minimal among feasible pairs. The constraint "$y_i \ge \max_{\epsilon_i \ge 0}(\dots)$" of (10) is stated in constraint form, for every $\epsilon_i \ge 0$, so no real supremum is taken. $K_i(\epsilon)$ is defined for $\epsilon \ge 0$ only; its placeholder value for $\epsilon < 0$ is never used. Ties in revenue (and, for $N^k_{ij}$, in weight) are broken by index. The candidate collection is taken over real $\epsilon_i \ge 0$; $\epsilon_i = \infty$ adds nothing, since every capacity of at least $\sum_j v_{ij}$ already gives $\hat S_i = N$.

Standing assumptions and added hypotheses: $\gamma_i \le 1$ for every nest (the section's assumption) on the goal and on every model milestone; the pins $v_{ij} > 0$, $r_{ij} \ge 0$, $\gamma_i > 0$ and the revenue ordering, shared by the series; $n \ge 1$ on Lemma 9, on $\hat x \ge 0$ and on (28)/(29), the paper's nonempty $N$; and $v_0 > 0$ on the factor-two revenue guarantee, where Theorem 1 of the paper fails without it.

The greedy assortments $\hat S_i(\epsilon_i)$ are defined explicitly. Quantifying over arbitrary optimal solutions of (11) instead would change the candidate collection and is not the paper's theorem. The goal states feasibility for the full program (3) and does not mention knapsack values, the greedy solution or the case split. A formalization that weakens the conclusion to feasibility for (10), or that drops the singletons from the candidate collection, is not a solution.

Needed infrastructure: fractional knapsack optimality of the greedy rule with an eligibility bound, monotonicity of $t \mapsto t^{\gamma}$ and $t \mapsto t^{\gamma - 1}$ for $\gamma \le 1$, and finite maximization over subsets. The fractional-knapsack lemmas are reusable beyond this mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment Optimization under Variants of the Nested Logit Model, Operations Research 62(2), 2014 (revised manuscript of June 18, 2013, cited here). DOI 10.1287/opre.2014.1256
• K. T. Talluri, G. J. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 15–33, 2004. DOI 10.1287/mnsc.1030.0147
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. DOI 10.1017/CBO9780511921735