Combinatorics

Motivation

Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract notion of dependence that captures what linearly dependent columns of a matrix and cycles of a graph have in common. A distinctive feature of the paper is that it gives several independent axiom systems for the same structure: one in terms of rank, one in terms of independent sets, one in terms of bases, and one in terms of circuits (minimal dependent sets). It then proves they are interchangeable. These equivalences, now called cryptomorphisms, are what allow matroid theory to move freely between the algebraic picture (rank of a set of vectors) and the combinatorial one (cycles of a graph, minimal dependent column sets). Every textbook on the subject relies on them, for example J. Oxley, Matroid Theory, Chapter 1.

This mission treats one of them: the equivalence of Whitney's rank postulates (§2) and circuit postulates (§8). The circuit side is the one used in combinatorial optimization, where circuits appear as cycles in network flows, as minimal infeasible subsystems, and in the exchange arguments behind the greedy algorithm.

Setting

Let $M$ be a finite set of elements. For subsets we write $N + e$ for $N \cup \{e\}$ and $P_1 + P_2$ for $P_1 \cup P_2$.

Rank system. A function $r$ assigning an integer $r(N)$ to each $N \subseteq M$ satisfies the rank postulates if

• $(\mathrm R_1)$ the rank of the null subset is zero;
• $(\mathrm R_2)$ for any subset $N$ and any element $e$ not in $N$, $r(N+e) = r(N) + k$ with $k = 0$ or $1$;
• $(\mathrm R_3)$ for any subset $N$ and elements $e_1, e_2$ not in $N$, if $r(N+e_1) = r(N+e_2) = r(N)$, then $r(N+e_1+e_2) = r(N)$.

With $\rho(N)$ the number of elements of $N$, the nullity is $n(N) = \rho(N) - r(N)$. An element $e$ is dependent on $N$ if $r(N+e) = r(N)$. A circuit of $r$ is a minimal dependent set: a subset $P$ with $n(P) > 0$ such that $n(N) = 0$ for every proper subset $N$ of $P$. In Lean these are IsRankSystem r, nullity r N, IsDependentOn r e N and circuitsOfRank r P.

Circuit system. A family of subsets, called circuits, satisfies the circuit postulates (§8, p. 516) if

(C₁) No proper subset of a circuit is a circuit.

(C₂) If P₁ and P₂ are circuits, e₁ is in both P₁ and P₂, and e₂ is in P₁ but not in P₂, then there is a circuit P₃ in P₁ + P₂ containing e₂ but not e₁.

In Lean this is IsCircuitSystem C for a predicate C : Finset α → Prop.

Rank from circuits. Whitney defines (p. 516):

Let e₁, ⋯, e_p be any ordered set of elements of M. Set Γᵢ = 0 if there is a circuit in e₁ + ⋯ + eᵢ containing eᵢ, and set Γᵢ = 1 otherwise (compare Theorem 5). Let the "rank" of (e₁, ⋯, e_p) be r(e₁, ⋯, e_p) = Σ_{i=1}^{p} Γᵢ.

In Lean, rankSeq C l is this sum for a list l, and rankOfCircuits C N is its value on the enumeration N.toList of a subset $N$.

Formalization targets

Goal: the two systems are equivalent

For every finite set $M$:

$$\text{(1)}\quad r \text{ satisfies } (\mathrm R) \;\Longrightarrow\; \mathcal C(r) \text{ satisfies } (\mathrm C),\ \emptyset \notin \mathcal C(r),\ r_{\mathcal C(r)} = r;$$ $$\text{(2)}\quad \mathcal C \text{ satisfies } (\mathrm C),\ \emptyset \notin \mathcal C \;\Longrightarrow\; r_{\mathcal C} \text{ satisfies } (\mathrm R),\ \mathcal C(r_{\mathcal C}) = \mathcal C,$$

where $\mathcal C(r)$ is the family of circuits of $r$ and $r_{\mathcal C}$ is the rank defined from $\mathcal C$. This is Whitney's closing sentence of §8 (p. 517): "The definitions of rank and of circuits under the two systems (R), (C) agree, and hence the systems are equivalent."

Milestones, in the order the argument uses them

• Lemma 5 (p. 512): each element of a circuit is dependent on the rest of the circuit.
• Lemma 6 (p. 512): if $e \notin P_1$ is dependent on $P_1$ but on no proper subset of $P_1$, then $P_1 + e$ is a circuit.
• Theorem 4 (p. 512): for $e \notin N$, some circuit in $N + e$ contains $e$ if and only if $e$ is dependent on $N$.
• Theorem 5 (p. 513): if $N = e_1 + \cdots + e_p$ is formed element by element, $n(N)$ is the number of indices $i$ for which some circuit in $e_1 + \cdots + e_i$ contains $e_i$.
• §5 (pp. 512–513): the circuits of a rank system satisfy $(\mathrm C_1)$ and $(\mathrm C_2)$.
• Lemma 7 (p. 516): $r(e_1, \dots, e_{q-2}, e_{q-1}, e_q) = r(e_1, \dots, e_{q-2}, e_q, e_{q-1})$ under $(\mathrm C_1)$, $(\mathrm C_2)$.
• Lemma 8 (p. 517): the rank of a subset defined from circuits does not depend on the ordering of its elements.
• §8 (p. 517): the rank defined from circuits satisfies $(\mathrm R_1)$–$(\mathrm R_3)$.

Significance

The equivalence makes the circuit postulates a complete description of a matroid: everything stated about rank, nullity, independence and bases can be phrased through circuits and back. Downstream in the same paper, the fundamental sets of circuits of §9 (Theorem 9) and the binary-matroid characterization of the Appendix are stated in terms of circuits, and they depend on circuits and rank being interchangeable. Theorem 5, read on its own, expresses the nullity of a set as a count of circuit-closing steps. This is the abstract form of the fact that the cycle space of a graph has dimension equal to the number of non-tree edges.

On the formal side, Mathlib's Matroid is built on the base axioms and proves circuit elimination (Matroid.IsCircuit.strong_elimination) as a theorem about that structure. Whitney's own route is different: rank defined from circuits by an ordered sum of $\Gamma_i$, with order-independence (Lemmas 7 and 8) as the central step. That route has no machine-checked version that we know of, on Prove2Me or elsewhere. This mission formalizes the 1935 argument as stated: the rank and circuit systems as Whitney wrote them, and the two translations between them.

Difficulty

The obvious definition of the rank of a set from its circuits enumerates the set and counts the elements that do not close a circuit with their predecessors. This definition depends on the enumeration, and nothing in $(\mathrm C_1)$, $(\mathrm C_2)$ obviously prevents two orderings from giving different counts. Lemma 7, the swap of two adjacent elements, is where $(\mathrm C_2)$ does real work, through a case analysis on which of the two swapped elements closes a circuit. In the other direction, $(\mathrm C_2)$ for circuits of a rank function requires turning the local postulate $(\mathrm R_3)$ into a statement about unions of two circuits. Defining the circuit rank as a maximum over orderings, or as the size of a largest circuit-free subset, sidesteps exactly the step the paper proves and is not this mission.

Formalization scope

• The elements form a finite type α with [Fintype α] [DecidableEq α]. The ground set is all of α, and subsets are Finset α. Whitney's matroid is a finite set $e_1, \dots, e_n$.
• Ranks and nullities are integers (ℤ), so that $n(N) = \rho(N) - r(N)$ is a true difference.
• Ordered sets of elements are lists. Lemmas 7, 8 and Theorem 5 assume the list has no repetitions, as Whitney's "ordered set of elements" means. "A circuit in $e_1 + \cdots + e_i$" means a circuit contained in $\{e_1, \dots, e_i\}$.
• The rank of a subset from circuits is computed along one fixed enumeration N.toList. Its independence from the enumeration is Lemma 8, and the definition does not build it in.
• Tacit hypothesis made explicit. Whitney's circuits are nonempty, since a circuit of a rank system has positive nullity. The family $\{\emptyset\}$ satisfies $(\mathrm C_1)$, $(\mathrm C_2)$ vacuously, but its circuit rank is $\rho$, which has no circuits, so the round trip fails. Part (2) of the goal therefore assumes $\emptyset \notin \mathcal C$, and part (1) asserts $\emptyset \notin \mathcal C(r)$.
• Lemma 6 assumes $e \notin P_1$, which the paper leaves tacit.
• Ruled out. Neither system may be encoded as Mathlib's Matroid in the statements. Doing so would turn the equivalence into a library lemma. The statements are about Whitney's postulates on bare functions and predicates.

The development needs only finite sets, lists and permutations from Mathlib. The definitions IsRankSystem and IsCircuitSystem can be reused for the other cryptomorphisms of the paper. Contributions are welcome on any milestone, and so are local helper lemmas, such as monotonicity of rank under $(\mathrm R_1)$–$(\mathrm R_3)$ or invariance of rankSeq under prefix-preserving changes.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), no. 3, 509–533. https://doi.org/10.2307/2371182
• J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• Mathlib, Mathlib/Combinatorics/Matroid/Circuit.lean (circuits of Mathlib's Matroid). https://github.com/leanprover-community/mathlib4

Motivation

Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a $d$-regular graph is governed by the Alon–Boppana bound $2\sqrt{d-1}$, and graphs attaining it, Ramanujan graphs, were constructed explicitly by Lubotzky, Phillips and Sarnak (LPS 1988) and by Margulis. These constructions exist only for special degrees ($d = p+1$ with $p$ prime) and special numbers of vertices (orders of $PSL(2,\mathbb F_q)$ or $SL(2,\mathbb F_q)$). Applications often need a graph of a prescribed size $n$.

N. Alon's paper Explicit expanders of every degree and size (arXiv:2003.11673v1; Combinatorica 41, 2021) shows how to obtain explicit near-Ramanujan graphs on exactly $n$ vertices. This mission formalizes the spectral core of its Theorem 1.2: a Ramanujan graph on $m$ vertices can be enlarged to $n = m + r$ vertices, with degree raised by one, while the nontrivial eigenvalues stay within a constant factor of optimal.

Setting

Let $V$ be a finite set of $m \ge 1$ vertices. A $(n,d,\lambda)$-graph is a $d$-regular graph on $n$ vertices whose adjacency matrix $A$ satisfies $|\mu| \le \lambda$ for every nontrivial eigenvalue $\mu$, that is, every eigenvalue other than the top eigenvalue $d$ of the constant vector $\mathbf 1$. For a symmetric $A$ with $A\mathbf 1 = d\,\mathbf 1$, the nontrivial eigenvalues are those with an eigenvector $f \ne 0$ satisfying $\sum_v f(v) = 0$. Graphs may carry loops, at most one per vertex, and a loop adds one to the degree: it is a diagonal entry $1$ of $A$.

Fix an integer $p \ge 0$ and let $H$ be an $(m, p+1, 2\sqrt p)$-graph on $V$, a $(p+1)$-regular Ramanujan graph. Let $R = \{u_1, \dots, u_r\}$ be $r$ new vertices and let $W_1, \dots, W_r \subseteq V$ be pairwise disjoint sets of $p+2$ vertices each. Put $W = \bigcup_i W_i$ and $L = V \setminus W$. The graph $G$ on $U = V \cup R$ is obtained from $H$ by joining each $u_i$ to every vertex of $W_i$ and adding one loop at each vertex of $L$. Its adjacency matrix is

$$A_G = A_H + A_R + A_L,$$

where $A_H$ is the adjacency matrix of $H$ (zero on $R$), $A_R$ that of the stars joining $u_i$ to $W_i$, and $A_L$ the diagonal matrix of the loops. Every vertex of $G$ has degree $p+2$.

Formalization targets

Goal: Theorem 1.2, spectral core

$$A_G \text{ is an } \Big(m+r,\; p+2,\; \sqrt{2(p+1)} + \sqrt p + \frac{(p+1)\,r}{m}\Big)\text{ matrix.}$$

The paper states $\lambda \le \sqrt{2(d-1)} + \sqrt{d-1} + o(1)$ for $d = p+2$; its proof gives $\sqrt{2(p+1)} + \sqrt p + o(1)$, which is stronger, and the error term it produces is $(p+1)r/m$. The goal is parametrised by $H$, $r$ and the sets $W_i$, so it does not depend on how $m$ and $r$ are chosen.

Milestones

1. The variational characterization of the nontrivial eigenvalues: for a symmetric matrix with constant row sums and $\lambda \ge 0$, $|\mu| \le \lambda$ for every nontrivial eigenvalue if and only if $|f^tAf| \le \lambda\|f\|^2$ whenever $\sum f = 0$.
2. The Cauchy–Schwarz display: $\sum_U f = 0$ implies $|\sum_V f|^2 = |\sum_R f|^2 \le |R| \sum_R f^2$.
3. Inequality (3): $|f^tA_Hf| \le b^2(p+1) + c^2\, 2\sqrt p$ with $b^2 = (\sum_V f)^2/m$ and $c^2 = \sum_V f^2 - b^2$.
4. Display (4): $f^tA_Lf = \sum_{v\in L} f^2(v)$.
5. Inequality (5): $|f^tA_Rf| \le \frac{p+2}{x}\sum_R f^2 + x\sum_W f^2$ for every $x > 0$.
6. Inequality (6): for $\sum_U f = 0$ and $x > 0$,

$$|f^tA_Gf| \le (2\sqrt p+1)\sum_L f^2 + (2\sqrt p+x)\sum_W f^2 + \frac{p+2}{x}\sum_R f^2 + (p+1)\frac rm \sum_R f^2.$$

Significance

With $H$ the Lubotzky–Phillips–Sarnak graph on $m = |SL(2,\mathbb F_q)|$ vertices for the largest suitable prime $q$ with $m \le n$, and $r = n - m$, the distribution of primes in arithmetic progressions gives $r = o(m)$, and the goal yields an explicit $(n, p+2, \lambda)$-graph with $\lambda \le (1+\sqrt2)\sqrt{d-1} + o(1)$ for every sufficiently large $n$. This is within a factor of about $1.21$ of the Ramanujan bound $2\sqrt{d-1}$, for every number of vertices, by an elementary modification of an existing graph. The statement is useful independently of LPS: any Ramanujan graph, or any graph with a bound on its nontrivial eigenvalues, can be padded to a nearby size in the same way.

The result is proved in the paper. No formalization of it, of the $(n,d,\lambda)$ notion, or of the variational characterization of nontrivial eigenvalues for regular graphs exists on the platform. The mission produces a checked version of the spectral argument, and the variational characterization (milestone 1) is a general fact about symmetric matrices with constant row sums that applies to any spectral expander argument.

Difficulty

The vertices of $W$ and $L$ lie in the old graph $H$, whose spectrum is controlled, but the new vertices of $R$ are not; and a vector orthogonal to $\mathbf 1$ on $U$ need not be orthogonal to the constant vector on $V$. Bounding $f^tA_Gf$ by applying the Ramanujan bound for $H$ to $f$ restricted to $V$ therefore fails: the restriction has a component along the trivial eigenvector of $H$, whose eigenvalue $p+1$ is large. The argument must show that this component is small, of order $r/m$, and must balance the star edges between $R$ and $W$ against the loops on $L$ so that every vertex class gets the same coefficient. The naive bound $|f^tA_Rf| \le \|A_R\|\,\|f\|^2 = \sqrt{p+2}\,\|f\|^2$ added to $2\sqrt p$ for $H$ and $1$ for $L$ gives a constant larger than $\sqrt{2(p+1)}+\sqrt p$; the stated constant needs the weighted estimate.

On the Lean side, milestone 1 concerns the spectrum of a symmetric matrix on the invariant subspace $\mathbf 1^\perp$, while Mathlib states the spectral theorem for the whole space.

Formalization scope

• Vertices of $G$ are the disjoint union $V \oplus \mathrm{Fin}\, r$. $G$ is represented by its real adjacency matrix, since it has loops; $H$ is a Mathlib SimpleGraph with adjMatrix.
• The $(n,d,\lambda)$ predicate is stated for matrices: $|V| = n$, symmetry, $A\mathbf 1 = d\,\mathbf 1$, and $|\mu| \le \lambda$ for every eigenpair $(\mu, f)$ with $f \ne 0$ and $\sum f = 0$. For simple graphs, $d$-regularity is added.
• The paper's $o(1)$ terms are replaced by the explicit quantities its proof produces: $(p+1)r/m$ in the goal, and $(p+1)\frac rm\sum_R f^2$ in (6). Inequality (3) is stated with the corrected relation $b^2 + c^2 = \sum_V f^2$; the paper's "$b^2 + c^2 = 1$" holds only for unit restrictions.
• The bound uses $\sqrt p = \sqrt{d-2}$, as in the proof and the abstract, which implies the printed $\sqrt{d-1}$.
• $p$ is any natural number. The hypothesis "$p$ prime, $p \equiv 1 \pmod 4$" serves only to obtain $H$ from LPS, and $H$ is a hypothesis here. The sets $W_i$ are arbitrary pairwise disjoint sets of size $p+2$, not the paper's consecutive blocks of a numbering of $SL(2,\mathbb F_q)$.
• Out of scope: the existence of the prime $q$ and the estimate $n - m = o(m)$; the numbering of $SL(2,\mathbb F_q)$; the "strongly explicit" and polynomial-time claims; the LPS construction (Theorem 2.1, cited); the variant that replaces loops by a matching for even $n$.
• The goal cannot be satisfied trivially: dropping the condition $\sum f = 0$ makes it false, since $p+2$ is always an eigenvalue, and for $p \ge 2$ and small $r/m$ the bound is below $p + 2$ (for $p = 5$ it is about $5.70 + 6r/m$). At $p = 1$ the bound $3 + 2r/m$ is at least the degree $3$, so that case holds trivially; it is the paper's statement there as well.
• Contributions welcome: proofs of each milestone, especially the variational characterization, which is reusable for mission 3 of this series and for any regular-graph spectral argument.

Selected references

• N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673
• A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988) 261–277. https://doi.org/10.1007/BF02126799
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8

Motivation

An $(n,d,\lambda)$-graph is a $d$-regular graph on $n$ vertices in which every eigenvalue of the adjacency matrix other than the top eigenvalue $d$ has absolute value at most $\lambda$. Graphs of this kind with $\lambda$ small compared with $d$ are expanders. They are used in derandomization, error-correcting codes, sorting networks and many other constructions in theoretical computer science. A Ramanujan graph achieves $\lambda\le 2\sqrt{d-1}$, which is asymptotically optimal.

The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (LPS, 1988) exist only for special vertex counts, such as $q(q^2-1)/2$ for a prime $q$ or the size of a quaternion group modulo $m$. N. Alon, in Explicit expanders of every degree and size (arXiv:2003.11673, 2020; Combinatorica 41, 2021), asks for explicit $(n,d,\lambda)$-graphs with $\lambda\le(2+o(1))\sqrt d$ for every degree $d$ and every number of vertices $n$. His Proposition 1.1 builds such graphs out of LPS graphs, and one ingredient is purely arithmetic. If the available vertex counts of an LPS family are dense enough, so that for every large $n$ one is within a factor $1+o(1)$ of $n$, then a few vertices can be added or removed while keeping the spectral bound.

This mission formalizes that ingredient, Lemma 2.2 of the paper (p. 7). It concerns the vertex counts of the LPS graphs $H(p,q_1^sq_2^t)$ for two fixed primes $q_1,q_2$ and all exponents $s,t\ge1$. With $q_1,q_2$ fixed, the construction needs no large primes, which is why Proposition 1.1 is strongly explicit for every fixed degree.

Setting

Fix natural numbers $q_1,q_2$. For natural numbers $s,t$ define the LPS vertex count

$$Q(q_1,q_2,s,t)=q_1^{3(s-1)}\,q_2^{3(t-1)}\cdot\frac{q_1(q_1-1)(q_1+1)}{2}\cdot\frac{q_2(q_2-1)(q_2+1)}{2}.$$

When $q_1,q_2$ are distinct primes congruent to $1$ modulo $4p$ and $s,t\ge1$, this is the number of vertices of the LPS Cayley graph $H(p,q_1^sq_2^t)$ (§2.3, p. 6). Lemma 2.2 itself only requires $q_1,q_2$ to be distinct primes. Both fractions are integers, because $q(q-1)(q+1)$ is a product of three consecutive integers.

The proof uses the real number $\alpha=\log q_1/\log q_2$, and the fractional part $\{x\}=x-\lfloor x\rfloor\in[0,1)$, written $x \bmod 1$ in the paper.

Formalization targets

Goal: Lemma 2.2

For distinct primes $q_1,q_2$ there is a function $g:\mathbb N\to\mathbb R$ with $g(n)=o(n)$ such that for all sufficiently large $n$ there are integers $s,t\ge1$ with

$$n\le Q(q_1,q_2,s,t)\le n+g(n).$$

Equivalently, the ratio between consecutive elements of $\{Q(q_1,q_2,s,t):s,t\ge1\}$ tends to $1$. The statement fixes no rate for $g$, matching the paper's $o(n)$.

Milestones, in the order the proof of Lemma 2.2 uses them (p. 7)

1. For distinct primes $q_1,q_2$, $\alpha=\log q_1/\log q_2$ is irrational.
2. For irrational $\alpha$ and every $\delta>0$ there is $k_1\ge1$ with $0<\{k_1\alpha\}<\delta$.
3. For distinct primes $q_1,q_2$ and every $\mu>0$ there are $k_1\ge1$, $k_2\ge0$ with

$$1\le \frac{q_1^{k_1}}{q_2^{k_2}}\le 1+\mu .$$

4. For distinct primes, $\mu>0$ and $k_1\ge1$, if $1\le q_1^{k_1}/q_2^{k_2}\le1+\mu$, then for $s>k_1$ and $t\ge1$

$$1\le\frac{Q(q_1,q_2,s,t)}{Q(q_1,q_2,s-k_1,t+k_2)}\le(1+\mu)^3 .$$

Significance

The result. Lemma 2.2 is the step of Proposition 1.1 that turns a family of Ramanujan graphs with sparse vertex counts into a family whose vertex counts approximate every large $n$ up to a factor $1+o(1)$. The deviation from $n$ can then be absorbed by the general packing argument of §2.1 of the paper. Without it, the construction would have to search for large primes depending on $n$, and the result would be explicit but not strongly explicit.

The formalization. The lemma is proved in the paper, in one paragraph. To our knowledge no machine-checked proof exists, and the platform has no statement of it. The only related platform item is the irrationality of $\log 2/\log 3$, the case $q_1=2$, $q_2=3$ of milestone 1. Formalizing the lemma requires a quantitative inhomogeneous step that the paper leaves implicit ("implying the desired result"). Its last sentence also contains a misprint that the formalization corrects (see below). The Diophantine milestones 1–3 are reusable for any argument about the multiplicative density of $\{q_1^a q_2^b\}$, for instance the ratio of consecutive elements of $\{2^a3^b\}$.

Difficulty

Each milestone is short. The difficulty is in making the paper's last sentence ("implying the desired result") into a proof. Taking $s$ or $t$ large separately does not work: changing $s$ or $t$ by one multiplies $Q$ by $q_1^3$ or $q_2^3$, a fixed factor larger than $1$, so the values obtained by varying one exponent leave gaps of a constant ratio. The bound must hold for every large $n$, not just along a subsequence, and the exponents must stay positive throughout. Milestone 2 is the classical fact that the multiples of an irrational number are dense modulo $1$. It needs a pigeonhole argument, not just the irrationality.

Formalization scope

• Representation. $Q$ is a natural-number-valued Lean definition given by the explicit formula above, not the cardinality of a quaternion group. The graph-count interpretation needs the section's congruence conditions on $p,q_1,q_2$; Lemma 2.2 is an arithmetic statement for all distinct primes $q_1,q_2$. Every use of $Q$ in the theorems has positive $s,t$, so natural-number subtraction $s-1$ is exact, and the division by $2$ is exact since $q(q-1)(q+1)$ is even. Ratios and the bound $n+g(n)$ are computed in $\mathbb R$ after casting. The logarithm is Real.log, and the fractional part is Int.fract.
• o(n). The paper writes $n\le Q\le n+o(n)$ for every large $n$. The goal states it literally: $\exists g,\ g=o(n)$ (Mathlib IsLittleO along atTop) and, eventually in $n$, $\exists s,t\ge1$ with $n\le Q\le n+g(n)$. This is equivalent to the form "for every $\mu>0$, every large $n$ has $s,t\ge1$ with $n\le Q\le(1+\mu)n$". The paper's proof yields the second form, with the factor $(1+\mu)^3$ for arbitrary $\mu$.
• Misprint. The paper's last sentence compares $Q(q_1,q_2,s,t)$ with $Q(q_1,q_2,s-k_1,t-k_2)$ for $s,t\ge\max\{k_1,k_2\}$. As printed the ratio is $q_1^{3k_1}q_2^{3k_2}$, which is not close to $1$. Milestone 4 uses the intended pair $(s-k_1,t+k_2)$, with $s>k_1$ so that $s-k_1\ge1$.
• Ruling out a trivial reading. The lower bound $n\le Q(q_1,q_2,s,t)$ alone holds for every $n$ by taking $s$ large. The content of the goal is the upper bound with a sublinear excess, and $s,t$ must be positive. In milestone 3 the condition $k_1\ge1$ excludes the trivial witness $k_1=k_2=0$.
• Out of scope. The derivation of $Q$ as the vertex count of $H(p,q_1^sq_2^t)$ (Hensel's lemma and the Chinese remainder theorem, pp. 6–7), Theorem 2.1 (the LPS graphs are Ramanujan, cited from Lubotzky–Phillips–Sarnak), Proposition 1.1, the §2.1 packing argument, and every running-time ("explicit", "strongly explicit") claim.
• Infrastructure. Only Mathlib is needed: unique factorization for milestone 1, Int.fract and a pigeonhole or Dirichlet-approximation argument for milestone 2, and real exponentiation and asymptotics for the goal. Contributions of alternative proofs of milestone 2, for instance via Mathlib's Dirichlet approximation theorem, are welcome.

Selected references

• N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673 , https://doi.org/10.1007/s00493-020-4429-x
• A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988) 261–277. https://doi.org/10.1007/BF02126799
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

Formalization targets

Goal: §16, pp. 529–530

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

Formalization targets

Goal: Theorem 37 (p. 533)

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

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

for the nullity of $N$.

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

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

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

Formalization targets

Goal: Theorem 19

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

In 1935 Hassler Whitney asked which properties of linear dependence among the columns of a matrix can be stated without reference to the matrix at all. His answer, On the Abstract Properties of Linear Dependence (American Journal of Mathematics 57, 1935), introduced the matroid: a finite set together with a rank function obeying three short postulates. The notion now underlies combinatorial optimization (the greedy algorithm is optimal exactly on matroids, and matroid intersection and partition generalize bipartite matching and arborescence packing), graph theory (graphic and cographic matroids), coding theory and the study of linear representations over finite fields.

A defining feature of the subject is that the same structure can be axiomatized in several apparently unrelated ways: by rank, by independent sets, by bases, by circuits. Each axiom system is convenient for different arguments, and passing between them, a so-called cryptomorphism, is routine in practice. Whitney's paper is where these equivalences first appear. Part I, §§2–4 and §6 (pp. 510–514), derives the basic properties of rank from the rank postulates, deduces from them the postulates for independent sets, and shows that the two systems are equivalent. This mission formalizes that first equivalence.

Setting

Let $M$ be a finite set of elements $e_1, \dots, e_n$. Following Whitney, write $N + e$ for $N \cup \{e\}$, $M_1 + M_2$ for the union and $M_1 M_2$ for the intersection of subsets; $\rho(N)$ is the number of elements of $N$.

A rank system is a function $r$ on the subsets of $M$ satisfying

• (R₁) $r(\emptyset) = 0$;
• (R₂) for every subset $N$ and element $e \notin N$, $r(N + e) = r(N)$ or $r(N + e) = r(N) + 1$;
• (R₃) for every subset $N$ and elements $e_1, e_2 \notin N$, if $r(N + e_1) = r(N + e_2) = r(N)$ then $r(N + e_1 + e_2) = r(N)$.

The nullity of $N$ is $n(N) = \rho(N) - r(N)$, and $N$ is independent when $n(N) = 0$. The increment of (3.1) is $\Delta(M', N) = r(M' + N) - r(M')$, written $\Delta(M', e)$ when $N = \{e\}$.

An independence system is a predicate "independent" on the subsets of $M$ satisfying

• (I₁) any subset of an independent set is independent;
• (I₂) if $N$ and $N'$ are independent and $N'$ has exactly one element more than $N$, then $N + e'$ is independent for some $e' \in N'$ with $e' \notin N$.

From an independence system one recovers a rank by letting $r(N)$ be the number of elements in a largest independent subset of $N$. In the Lean development these objects are IsRankSystem, nullity, Delta, indepOfRank, IsIndepSystem and rankOfIndep, all in the namespace WhitneyMatroid.RankIndep.

Formalization targets

Goal: (R) and (I) are equivalent (§6, p. 514)

1. If $r$ satisfies (R₁)–(R₃), then $\{N : \rho(N) = r(N)\}$ satisfies (I₁), (I₂), contains $\emptyset$, and

$$r(N) = \max\{\rho(I) : I \subseteq N,\ \rho(I) = r(I)\} \quad \text{for every } N.$$

2. If "independent" satisfies (I₁), (I₂) and $\emptyset$ is independent, then $r(N) = \max\{\rho(I) : I \subseteq N \text{ independent}\}$ satisfies (R₁)–(R₃), and $N$ is independent if and only if $\rho(N) = r(N)$.

Both translations and both round trips are part of the goal: Whitney's conclusion is not only that each system implies the other but that "the definitions of the rank and the independence or dependence of any subset of $M$ agree under the two systems".

Milestones

• Lemma 1 (p. 510): $r(N) \ge 0$, $n(N) \ge 0$, and $N \subseteq M'$ implies $r(N) \le r(M')$, $n(N) \le n(M')$.
• Lemma 2 (p. 510): any subset of an independent set is independent, which is (I₁).
• Lemma 3 (p. 511): $\Delta(M + e_2, e_1) \le \Delta(M, e_1)$.
• Lemma 4 (p. 511): $\Delta(M + N, e) \le \Delta(M, e)$.
• Theorem 3 (p. 511): $\Delta(M + N_2, N_1) \le \Delta(M, N_1)$; equivalently

$$r(M + N_1 + N_2) \le r(M + N_1) + r(M + N_2) - r(M), \qquad r(M_1 + M_2) \le r(M_1) + r(M_2) - r(M_1 M_2).$$

• §4 (pp. 511–512): the independent sets of a rank system satisfy (I₂).

Significance

The equivalence makes the rank function and the family of independent sets two descriptions of one object. Every later result of Whitney's paper, and of matroid theory generally, moves between them without comment: the circuit postulates of §5 and §8, the base postulates of §7 and the duality of §§11–13 are all phrased through rank or independence as convenient. Theorem 3 is the submodularity of rank, the property that connects matroids to submodular function minimization and polymatroids; here it is derived from the purely local postulates (R₁)–(R₃), which constrain the rank only under the addition of one or two elements.

On the formal side, Mathlib defines Matroid through independent sets (with constructors from other axiom systems) and proves submodularity of its rank; the platform has submodularity for Mathlib matroids (FamousTheorems.matroid_rank_submodular_7a). Neither starts from Whitney's local rank postulates. What this mission adds is a machine-checked derivation of the global properties of rank from (R₁)–(R₃) and of Whitney's original equivalence, stated for his own postulates, so that the later missions of this series, which work from the same postulates, rest on a verified foundation. The result itself has been settled since 1935; the open work is the formal proof.

Difficulty

The postulates (R₂) and (R₃) are local: they speak about adding at most two elements to a set. Monotonicity and the bound $r(N) \le \rho(N)$ follow by adding elements one at a time, but the submodular inequality relates arbitrary sets, and nothing in (R₃) mentions more than two new elements. The gap between the local and the global statement is the substance of Lemmas 3, 4 and Theorem 3, and the deduction of (I₂) depends on it.

In the converse direction the rank is defined as a maximum over independent subsets, while (I₂) only augments a set from an independent set with exactly one element more; (R₃) for the derived rank is a statement about three sets that are not given in that form. The round trips are where the two halves meet, and each depends on the global properties of the first half rather than on the postulates alone.

Formalization scope

Elements form a type α with [Fintype α] [DecidableEq α]; subsets are Finset α, and the matroid $M$ is the whole type. Ranks, nullities and increments take values in ℤ, so differences never truncate; Whitney allows any number, but (R₁) and (R₂) force nonnegative integers. Postulate (I₂) is stated in Whitney's form with N'.card = N.card + 1, not the general augmentation for $\rho(N) < \rho(N')$. Postulates (R₂), (R₃) keep their hypotheses $e, e_1, e_2 \notin N$. Lemmas 3, 4 and Theorem 3 are stated for arbitrary subsets $M, N, N_1, N_2$; Lemma 1's monotonicity for arbitrary $N \subseteq M'$, the form in which the paper uses it. rankOfIndep is the supremum of cardinalities over the independent members of the powerset.

The paper takes for granted that the empty set is independent in system (I). Without that hypothesis, the predicate declaring nothing independent satisfies (I₁) and (I₂) vacuously, the supremum defining the rank returns $0$, and the round trip fails; the goal therefore assumes $\emptyset$ independent in part 2 and proves it in part 1. A formalization in terms of Mathlib's Matroid would make the goal a restatement of library facts, since Mathlib's matroids are independence systems by construction; the goal is deliberately about the postulates as predicates on functions and on families of sets.

A complete development needs only finite set combinatorics (Finset.card, induction on finite sets, Finset.sup). The derived lemmas (monotonicity, submodularity, (I₂)) are reusable for any later work from Whitney's rank postulates, including the circuit-postulate equivalence of the companion mission. A bridge from rank systems to Mathlib's Matroid (via IndepMatroid.ofFinset) would be a welcome addition but is not part of the goal. Proofs of the milestones in any order are welcome; Theorem 3 and the §4 deduction are the natural first targets.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), no. 3, 509–533. https://doi.org/10.2307/2371182
• J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• J. Kung (ed.), A Source Book in Matroid Theory, Birkhäuser, 1986. https://doi.org/10.1007/978-1-4684-9199-9
• Mathlib, Mathlib.Data.Matroid (matroids via independent sets; IndepMatroid.ofFinset). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matroid/Basic.html