Combinatorics

Motivation

Many assignment questions reduce to one combinatorial question: given finitely many sets, can one choose a different element from each? Workers are matched to jobs they are qualified for, rows of a matrix to columns with nonzero entries. The criterion for when this is possible is Hall's marriage theorem, first stated and proved by P. Hall in a five-page note in 1935 (DOI 10.1112/jlms/s1-10.37.26). It underlies bipartite matching, the integrality of the assignment polytope, the Birkhoff–von Neumann theorem on doubly stochastic matrices, and transversal theory in matroids.

Hall's note was written with a second question in view. In 1916 D. König proved, in the language of bipartite graphs, that if a set of $mn$ things is divided into $m$ classes of $n$ things in two ways, then one can choose $m$ things that represent every class of both divisions at once ("Über Graphen und ihre Anwendungen", Math. Annalen 77 (1916), 453). Van der Waerden (1927) and Sperner (1927) gave the set-theoretic form and a short proof. Hall's contribution was a criterion for a common system of representatives of two divisions in which the classes need not have equal sizes, obtained from the marriage theorem in two short steps.

Setting

Let $S$ be any set, finite or infinite, and let

$$T_1, T_2, \dots, T_m \tag{1}$$

be a finite system of subsets of $S$. The sets $T_i$ may be infinite and need not be distinct; when one speaks of $k$ of the sets, $k$ indices are meant, so a repeated set is counted with multiplicity. A complete set of distinct representatives, or C.D.R., of (1) is a choice of pairwise distinct elements $a_1, \dots, a_m$ of $S$ with

$$a_i \in T_i \qquad (i = 1, \dots, m).$$

The system satisfies Hall's condition when any $k$ of the sets contain between them at least $k$ elements of $S$, for $k = 1, \dots, m$. The meet of all C.D.R.s, written $R$, is the set of elements of $S$ that occur as a representative in every C.D.R. of (1).

A division of $S$ into classes is a family of pairwise disjoint sets $S_1, S_2, \dots$ whose union is $S$. The paper writes $A \wedge B$ and $A \vee B$ for intersection and union; this mission writes $A \cap B$ and $A \cup B$.

In Lean the system is T : ι → Set α over a finite index type, a C.D.R. is an injective a : ι → α with a i ∈ T i (IsCDR), Hall's condition is HallCondition, and the meet of all C.D.R.s is cdrMeet, all in the namespace HallReps.CDR.

Formalization targets

Goal: Theorem 3 (pp. 29–30)

Let $S$ be divided into $m$ classes in two ways, $S = S_1 \cup \dots \cup S_m = S_1' \cup \dots \cup S_m'$, each a division into pairwise disjoint classes. If, for each $k$, any $k$ of the classes $S_j'$ contain between them elements from at least $k$ of the classes $S_i$, then for some permutation $\sigma$ of $\{1, \dots, m\}$ there are elements

$$a_i \in S_i \cap S'_{\sigma(i)} \qquad (i = 1, \dots, m).$$

The set $S$ and the classes may be infinite, and no class is assumed non-empty.

Milestones

1. Lemma (p. 27). If $a$ is a C.D.R. of (1) and $R$ is the meet of all C.D.R.s, the sets $T_i$ whose representative $a_i$ lies in $R$ contain between them exactly the elements of $R$, and there are $|R|$ of them.
2. Induction step, p. 28. With (4) the system $T_1, \dots, T_{m-1}$ and $R^*$ the meet of its C.D.R.s: if $T_m \not\subseteq R^*$, then (1) has a C.D.R.
3. Induction step, p. 29. If (4) has a C.D.R. and $T_m \subseteq R^*$, then some $\rho + 1$ of the sets, including $T_m$, have union exactly $R^*$, where $\rho = |R^*|$.
4. Theorem 1 (p. 27). Hall's condition is sufficient for a C.D.R. of (1).
5. Theorem 2 (p. 29). If $S$ is divided into any number of classes and any $k$ of the sets $T_i$ contain between them elements from at least $k$ classes, there are $a_i \in T_i$ lying in pairwise different classes.

A companion item states König's theorem (§1, p. 26), which the paper deduces from Theorem 3 on p. 30.

Significance

Theorem 3 gives a necessary and sufficient criterion for two partitions of a set into $m$ classes to admit a common system of representatives. Necessity is immediate, and the paper proves sufficiency. It contains König's theorem, and through it the statement that a regular bipartite multigraph has a perfect matching, as the case of equal class sizes. Hall remarks that R. Rado's generalization of König's theorem (1933) also follows. Theorem 2, the passage from "distinct elements" to "elements of distinct classes", is the form used for transversals of partitions and is the first instance of what later became the theory of common transversals and matroid intersection.

On the formal side, Hall's theorem for finite sets is in Mathlib as Finset.all_card_le_biUnion_card_iff_existsInjective' (in Mathlib/Combinatorics/Hall/Finite.lean), and the platform already has a proved equivalence for arbitrary sets with a finite index type (YogeshwaranDM.sdr_iff, included in this mission as a reference item) as well as finite bipartite-graph forms. For that reason Theorem 1 is a milestone and not the goal. What this mission adds is Hall's own proof structure, namely the meet of all C.D.R.s and the Lemma about it, which has not been formalized; Theorems 2 and 3 for divisions of a possibly infinite set; and König's theorem in its set-partition form. To our knowledge none of these statements has a machine-checked proof on the platform.

Difficulty

Theorem 3 does not follow from Theorem 1 applied to the classes $S_j'$ directly. Theorem 1 produces distinct elements, but the conclusion needs elements in distinct classes $S_i$, and two distinct elements of $S_j'$ may lie in the same $S_i$. The paper's route goes through Theorem 2, which allows any number of classes. That route needs Theorem 1 for systems whose sets can be infinite, because a single $T_i$ may meet infinitely many classes, so the finite-set version of Hall's theorem in Mathlib is not enough on its own. In Hall's own proof of Theorem 1, the work lies in the Lemma. It is an exchange statement about all C.D.R.s at once, whose object $R$ is defined by a universal quantifier over C.D.R.s, and it must be established over an arbitrary finite index type with possibly infinite sets.

Formalization scope

• The ground set is a type α, with no finiteness or decidability assumed. The system (1) is T : ι → Set α with [Finite ι] (or Fin (m + 1) in the two induction steps, where the paper's $m$ is the Lean m + 1, its last set is T (Fin.last m), and (4) is fun i : Fin m => T i.castSucc).
• Cardinalities of unions of the $T_i$ are Set.encard in ℕ∞, so an infinite union counts as infinite. Set.ncard is used only for subsets of Fin m, for the finite set $R^*$ (with its finiteness stated), and in König's theorem.
• "$k$ of the sets" is a Finset ι of indices, so repeated sets count with multiplicity.
• Divisions into classes are class maps: cls : α → κ in Theorem 2, with κ arbitrary, and p q : α → Fin m in Theorem 3 and König's theorem. A class map makes the classes cover $S$ and be pairwise disjoint by construction. Empty classes are allowed.
• In Theorem 3 the permutation is existential and chosen together with the representatives. $a_i \in S_i \cap S'_{\sigma(i)}$ is p (a i) = i ∧ q (a i) = σ i.
• Added or dropped hypotheses: the Lemma assumes a C.D.R. exists, as the page does (without one, cdrMeet is all of α). The first induction step omits the page's C.D.R. of (4), because its hypothesis already implies one. König's theorem adds $0 < n$, which the page presumes and without which the statement is false.
• The trivializing formalizations are ruled out. Typing the $T_i$ as Finset α would reduce Theorem 1 to Mathlib and lose the page's "It is not necessary that the sets $T_i$ shall be finite". Measuring unions by ncard would make Hall's condition fail exactly when a union is infinite. An infinite index type would make Theorem 1 and the Lemma false. None of these is used.
• Useful contributions include proofs of the Lemma and of the induction steps, a proof of Theorem 1 either from them or from Mathlib's Hall theorem via a reduction to finite sets, and the reductions Theorem 1 → Theorem 2 → Theorem 3 → König.

Selected references

• P. Hall, On representatives of subsets, J. London Math. Soc. 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
• D. König, Über Graphen und ihre Anwendungen auf Determinantentheorie und Mengenlehre, Math. Annalen 77 (1916), 453–465. https://doi.org/10.1007/BF01456961
• B. L. van der Waerden, Ein Satz über Klasseneinteilungen von endlichen Mengen, Abh. Math. Sem. Hamburg 5 (1927), 185–188. https://doi.org/10.1007/BF02952519
• R. Rado, Bemerkungen zur Kombinatorik im Anschluss an Untersuchungen von Herrn D. König, Sitzungsber. Berliner Math. Ges. 32 (1933), 60–75.
• Mathlib, Mathlib/Combinatorics/Hall/Finite.lean and Mathlib/Combinatorics/Hall/Basic.lean. https://github.com/leanprover-community/mathlib4

Motivation

Chordal graphs (graphs in which every long cycle has a shortcut edge) appear wherever a sparse symmetric structure has to be eliminated without creating new interactions: Gaussian elimination on sparse symmetric matrices (Rose 1970), acyclic database schemes, junction trees for probabilistic graphical models, and phylogenetic and scheduling problems. In all of these applications the useful object is not the graph itself but a tree representation of it: a tree on which every vertex of the graph is a connected piece, and adjacency is overlap.

The theorem of this mission says that such tree representations exist exactly for chordal graphs. It extends the theory of interval graphs (intersection graphs of intervals on a line, i.e. of subpaths of a path), whose characterization was asked by Hajós (1957) and given by Lekkerkerker–Boland (1962), Gilmore–Hoffman (1964) and Fulkerson–Gross (1965), from paths to arbitrary trees.

Timeline. Dirac (1961) proved that every chordal graph has a simplicial vertex, a vertex whose neighbourhood is a complete subgraph. Rose (1970) used this to recognize chordal graphs efficiently, and Gavril (1972) showed that a chordal graph has at most as many maximal cliques as vertices. Renz (1970) studied intersection graphs of arcs in trees. Gavril (1974), together with Buneman (1974) and Walter (1972/1978) independently, proved that the intersection graphs of subtrees of trees are exactly the chordal graphs, and gave an algorithm that builds such a representation.

Setting

All graphs are finite and simple: a graph $G$ has a finite vertex set $V$ and a symmetric irreflexive adjacency relation. A completely connected set is a set of pairwise adjacent vertices, and a clique is a maximal completely connected set. The set of cliques of $G$ is $\mu(G)$, and $\mu_v(G) \subseteq \mu(G)$ is the set of cliques containing the vertex $v$. For a vertex $v$, $\Gamma v$ is the set of its neighbours; $v$ is simplicial if $\Gamma v$ is completely connected.

$G$ is chordal if every simple circuit $v_1, \dots, v_k, v_1$ with $k > 3$ vertices has a chord: an edge of $G$ joining two vertices of the circuit that are not consecutive on it.

A tree $T$ is a connected graph without simple circuits. A subtree of $T$ is a nonempty set of tree vertices that induces a connected subgraph of $T$. A family $(\bar v)_{v \in V}$ of subtrees of $T$ represents $G$ if, for all distinct $u, v \in V$,

$$u \sim_G v \iff \bar u \cap \bar v \neq \varnothing.$$

$G$ is a subtree graph if it has such a representation on some tree, and a proper subtree graph if it has one in which no subtree is contained in another.

Formalization targets

Goal: Theorem 3 (p. 51)

$$G \text{ is a subtree graph} \iff G \text{ is chordal}$$

for every finite simple graph $G$. The paper calls this "the main theorem of this paper".

Milestones

1. The three-point remark (p. 50): subtrees of a tree that each contain two of three given points have a common point.
2. Lemma 1 (p. 50): for every completely connected set $A$ of a subtree graph, $\bigcap_{v \in A} \bar v \neq \varnothing$.
3. For two different cliques $A_1 \neq A_2$, $\big(\bigcap_{v\in A_1}\bar v\big) \cap \big(\bigcap_{v \in A_2} \bar v\big) = \varnothing$ (p. 50).
4. Theorem 2 (p. 51): $G$ is a subtree graph if and only if there is a tree $T$ with vertex set $\mu(G)$ such that $T(\mu_v(G))$ is connected for every $v \in V$ (a clique tree).
5. Subtree graphs are chordal (proof of Theorem 3, p. 51).
6. Dirac–Rose (cited, p. 48): every nonempty finite chordal graph has a simplicial vertex.
7. For a simplicial vertex $v$, $\{v\} \cup \Gamma v$ is a clique (p. 52).
8. Induced subgraphs of chordal graphs are chordal (p. 52).
9. Every finite chordal graph has a clique tree (pp. 51–52).

Companion statements (§3 and §1)

$$G \text{ subtree graph} \implies G \text{ proper subtree graph}, \qquad \text{subtree} \iff \text{proper subtree} \iff \text{chordal},$$

and, cited on p. 49, $|\mu(G)| \le |V|$ for a nonempty finite chordal graph.

Significance

The result. The theorem turns a forbidden-structure condition (no chordless cycle of length at least four) into a constructive geometric one (a tree model), and Theorem 2 makes the tree canonical: its vertices are the maximal cliques. Clique trees are the data structure behind junction-tree inference, multifrontal sparse Cholesky factorization, and dynamic programming over tree decompositions; the treewidth of a graph is defined through chordal supergraphs and their clique trees. The proper-subtree result of §3 shows a contrast with interval graphs, where proper interval graphs form a strictly smaller class.

Formalizing it. The theorem is classical and fully proved in the literature, but Mathlib has no notion of chordal graph, no Helly property for subtrees, no clique trees and no simplicial-vertex theorem. This mission produces those definitions together with the characterization, the Helly property for finite families of subtrees, the Dirac–Rose theorem under the cycle–chord definition, and closure of chordality under induced subgraphs. As far as is known, none of these results has a machine-checked proof in Lean under the cycle–chord definition.

Difficulty

The "only if" direction is short on paper but rests on tree facts that are not packaged in Mathlib: a connected vertex set of a tree contains the unique path between any two of its vertices, and three pairwise paths of a tree meet. The "if" direction must produce a tree on the set $\mu(G)$ of maximal cliques, and the maximal cliques of a graph are not stable under passing to induced subgraphs: a clique of a subgraph need not be a clique of $G$, and two cliques of $G$ may restrict to the same set. Relating $\mu(G)$ to $\mu(G_1)$ for a smaller graph $G_1$ is the step where informal arguments are routinely loose, and it is where a formal proof spends most of its effort. The Dirac–Rose theorem is cited rather than proved in the paper and needs a separate development.

A tempting shortcut is to define chordality as the existence of a perfect elimination ordering. This builds the Dirac–Rose theorem into the definition and changes the theorem being proved; it is excluded here.

Formalization scope

• Graphs are G : SimpleGraph V with [Fintype V] in the goal, Theorem 2, the clique-tree claim, Dirac–Rose and the clique count. Milestones whose claims hold for infinite graphs (Lemma 1 for finite $A$, the three-point remark, the clique-disjointness claim, subtree ⇒ chordal, induced chordality, the simplicial clique, subtree ⇒ proper subtree) are stated without finiteness, which makes them stronger. $V$ may be empty in the goal and in Theorem 2; Dirac–Rose and the clique count assume $V$ nonempty, which they need.
• Chordality is the cycle–chord definition: for every cycle walk c of length at least 4 there are vertices x, y on c with G.Adj x y and s(x, y) not an edge of c.
• The paper's trees are topological and its subtrees connected closed portions that may end inside an edge. Here a tree is a combinatorial tree T : SimpleGraph β with T.IsTree (not necessarily finite), and a subtree is a vertex set s with (T.induce s).Connected; subdividing the topological tree at all end-points shows the class of subtree graphs is the same. The tree type lives in the same universe as V.
• The representing family is indexed by V; adjacency is compared only for distinct vertices. A clique is Maximal G.IsClique s; $\mu(G)$ is the subtype of such sets.
• Two trivializing formalizations are ruled out: chordality as a perfect elimination ordering, and representations by sets that need not be connected (with arbitrary sets every graph is an intersection graph, and the "only if" half would be false).
• Needed infrastructure: paths and connected sets in trees, Helly's property for subtrees, maximal cliques and their behaviour under induced subgraphs, and simplicial vertices. The tree lemmas and the Dirac–Rose theorem are reusable well beyond this mission. Proofs of any milestone, alternative routes (for example via perfect elimination orderings proved equivalent to the cycle–chord definition), and the clique-count bound are all welcome.

Selected references

• F. Gavril, Algorithms for minimum coloring, maximum clique, minimum covering by cliques, and maximum independent set of a chordal graph, SIAM J. Comput. 1 (1972) 180–187. https://doi.org/10.1137/0201013
• F. Gavril, The intersection graphs of subtrees in trees are exactly the chordal graphs, J. Combin. Theory Ser. B 16 (1974) 47–56. https://doi.org/10.1016/0095-8956(74)90094-X
• G. A. Dirac, On rigid circuit graphs, Abh. Math. Sem. Univ. Hamburg 25 (1961) 71–76. https://doi.org/10.1007/BF02992776
• D. J. Rose, Triangulated graphs and the elimination process, J. Math. Anal. Appl. 32 (1970) 597–609. https://doi.org/10.1016/0022-247X(70)90282-9
• P. Buneman, A characterisation of rigid circuit graphs, Discrete Math. 9 (1974) 205–212. https://doi.org/10.1016/0012-365X(74)90002-8
• J. R. Walter, Representations of chordal graphs as subtrees of a tree, J. Graph Theory 2 (1978) 265–267. https://doi.org/10.1002/jgt.3190020311
• D. R. Fulkerson and O. A. Gross, Incidence matrices and interval graphs, Pacific J. Math. 15 (1965) 835–855. https://doi.org/10.2140/pjm.1965.15.835

Motivation

A postman, a snowplough or a street sweeper must traverse every street of a district and return to the depot. When some streets are one-way, the street network is a mixed graph: some edges are directed and must be traversed in a prescribed direction, the others are undirected and may be traversed either way. The first question about such a route is whether a closed route exists that traverses every street exactly once, an Euler tour of the mixed graph. When one exists, it is an optimal postman route; when none exists, the postman problem asks which streets to repeat.

J. Edmonds and E.L. Johnson treat this question in §6 of Matching, Euler tours and the Chinese postman (Mathematical Programming 5, 1973), the paper that solved the undirected Chinese postman problem by matching. Section 6 gives an algorithm that finds an Euler tour in any mixed graph that is connected, of even degree and symmetric, and §7 uses it for the mixed postman problem.

Timeline.

• 1736: Euler's condition for undirected graphs (even degrees, connectivity).
• 1951: T. van Aardenne-Ehrenfest and N.G. de Bruijn enumerate the Euler tours of a symmetric directed graph through spanning arborescences ("circuits and trees in oriented linear graphs"). Edmonds and Johnson cite this as the source of their arborescence rule.
• 1962: L.R. Ford and D.R. Fulkerson (Flows in Networks, §II.7) characterize, by a flow argument, when a mixed graph has an Euler tour without assuming symmetry.
• 1973: Edmonds and Johnson give the combined orientation and Rule algorithm of §6 for connected, even, symmetric mixed graphs, and the existence criterion of §7 for mixed postman tours.
• 1976: C.H. Papadimitriou shows the mixed postman problem NP-hard, so the polynomial-time picture of §6 does not extend to its optimization version.

Setting

A mixed graph $G$ has a finite set $N$ of nodes and a finite set $E$ of edges. Each edge $e$ meets two distinct nodes; several edges may meet the same pair of nodes. Some edges are directed: an edge directed away from node $i$ toward node $j$ must be traversed from $i$ to $j$. In Lean an edge has a tail, a head (distinct) and a Boolean directed; for an undirected edge the order of the two ends carries no meaning.

• The degree of a node is the total number of edges, regardless of direction, meeting it. $G$ is even if every degree is even.
• $\operatorname{out}(n)$ and $\operatorname{in}(n)$ count the directed edges directed away from and toward $n$. $G$ is symmetric if $\operatorname{out}(n)=\operatorname{in}(n)$ for every node $n$.
• $G$ is connected if it is connected when the directions on the edges are ignored.
• A mixed walk is a sequence $(n_1,e_1,n_2,\dots,e_l,n_{l+1})$ in which each directed $e_i$ goes from its tail $n_i$ to its head $n_{i+1}$ and each undirected $e_i$ meets $n_i$ and $n_{i+1}$. It is a tour if $n_{l+1}=n_1$, an Euler tour if it contains every edge exactly once, and a postman tour if it contains every edge at least once.
• An arborescence with root $r$ is a tree $T$ of directed edges in which every node $n\neq r$ of $T$ has precisely one edge of $T$ directed away from $n$. Following those edges from any node of $T$ leads to $r$. It is spanning if it contains every node.

Formalization targets

Goal: the mixed Euler tour theorem (§6, pp. 115–118)

If $G$ is connected, even and symmetric, then for every node $r$

$$\exists\ (r=n_1,e_1,\dots,e_l,n_{l+1}=r)\ \text{a mixed Euler tour of } G .$$

Milestones

1. Cut balance (p. 116). If $G$ is symmetric, every node set $S$ has as many directed edges leaving it as entering it.
2. Maximal arborescences span (pp. 115–116). Suppose the directed edges form a symmetric, connected spanning subgraph. Then an arborescence of directed edges to which no directed edge entering it from outside can be added contains every node.
3. The Rule (pp. 116–117). Suppose the directed edges form a symmetric connected spanning subgraph and the undirected edges have even degree. Fix a spanning arborescence with root $r$ and order the directed edges leaving each node $n\neq r$ so that the arborescence edge comes last. Then the following traversal from $r$ is an Euler tour: leave by the next unused undirected edge if there is one, otherwise by the next unused directed edge.
4. The assignment outcome (p. 118). If $G$ is connected, even and symmetric, directions can be assigned to some undirected edges so that the result is symmetric, its directed edges form a connected spanning subgraph, and the unassigned edges have even degree.
5. Mixed postman criterion (§7, p. 120). A connected mixed graph has a postman tour if and only if no nonempty proper node set $S$ has every boundary edge directed away from $S$.

Significance

The goal contains two classical theorems as special cases. With every edge undirected it is Euler's theorem for connected even multigraphs. With every edge directed it is the theorem that a connected balanced digraph is Eulerian. The milestones connect the two cases: an orientation reduces the mixed case to one the Rule can handle. The Rule itself is the van Aardenne-Ehrenfest–de Bruijn construction, which underlies the BEST theorem counting Euler tours. Milestone 5 decides whether the mixed postman problem has any feasible solution. The mixed postman problem is the standard model for routing on one-way street networks.

All results here are proved in the paper, so none is open. No Lean proof of any of them in this form is known. Mathlib's Eulerian walks are for simple graphs; it has no multigraph or mixed-graph Euler theorem, no directed Euler theorem and no arborescence-based traversal. The mission produces these, together with a reusable vocabulary of mixed multigraphs, walks that respect directions, and arborescences given by parent edges.

Difficulty

The obvious approach to the goal is to forget the directions and apply Euler's theorem. This fails because the tour it produces may traverse a directed edge backwards. Orienting all undirected edges at once also fails: an arbitrary orientation of the undirected edges need not keep every node balanced.

The difficult part of the Rule is showing that the greedy traversal does not get stuck before using every edge. It cannot stop at a node other than $r$ because of the degree conditions. The hard step is showing that no edge is left unused when it stops at $r$. The answer depends on the ordering condition: without the arborescence edge last at every node, the Rule can return to $r$ with edges still unused. The assignment step needs an invariant: the orientation must keep every node symmetric while it extends a spanning structure of directed edges.

Formalization scope

• Graphs. Nodes and edges are finite types (Fintype V, Fintype E). Parallel edges are allowed, including a directed and an undirected edge on the same pair. Loops are excluded (tail e ≠ head e), following the paper's standing setting of §2 (p. 91: edges meet two different nodes). Edges are a type, not a relation on nodes, so parallel edges stay distinct in every walk.
• Hypotheses as on p. 115. "Even" counts all edges, directed or undirected. "Symmetric" counts only directed edges. "Connected" ignores directions. Strong connectivity is not assumed. "Symmetric" does not mean that every node has even in-degree, and an Euler tour of the underlying undirected multigraph does not satisfy the goal: the tour must traverse each directed edge from its tail to its head.
• Walks are a node list and an edge list of length one less. The one-node walk is allowed, so the graph with one node and no edges satisfies the goal.
• Arborescences are given by an optional edge $a_n$ at each node, with an edge required for each non-root node of $W$; following those edges leads to $r$. A maximal arborescence is one where no directed edge enters $W$ from outside. The optional choice represents the root-only arborescence when the graph has no edges.
• The Rule is computed by a fuel-bounded traversal (at most $|E|$ steps) that keeps a global list of used edges. Its conclusion is that the computed sequences form a mixed Euler tour from $r$.
• The assignment is an existential statement over a second mixed graph $G'$ on the same edges, with the same unordered ends and every directed edge kept. The paper's algorithm (Steps 0–3) is not formalized.
• Postman criterion. "Proper subset" means nonempty and proper. Connectivity is assumed, as throughout §7, and the node set is nonempty (with no nodes there is no tour, while the criterion holds vacuously).
• Not formalized. The §7 evenness argument (p. 122) and the min-cost flow formulations are outside the scope.

Contributions are welcome at every level: proofs of the milestones, a direct proof of the goal, and general lemmas about mixed multigraph walks.

Selected references

• J. Edmonds and E.L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973) 88–124. https://doi.org/10.1007/BF01580113
• T. van Aardenne-Ehrenfest and N.G. de Bruijn, Circuits and trees in oriented linear graphs, Simon Stevin 28 (1951) 203–217.
• L.R. Ford and D.R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• C.H. Papadimitriou, On the complexity of edge traversing, Journal of the ACM 23 (1976) 544–554. https://doi.org/10.1145/321958.321974

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