Theorem 5 — the nullity counts the steps at which adding an element closes a circuit

Let $r$ be a rank function on the subsets of a finite set $M$ satisfying $(\mathrm R_1)$–$(\mathrm R_3)$, and let $N = e_1 + \cdots + e_p$ be built element by element from distinct elements $e_1, \dots, e_p$. Then

Whitney phrases this as: $n(N)$ is the number of times that adding an element increases the number of circuits present. It shows that the nullity, hence the rank, of a set is determined by the circuits it contains, and it is the model for the definition of rank from circuits in §8.

Formalization Note "Adding an element increases the number of circuits present" is rendered, following the paper's proof, as "there is a circuit in $e_1 + \cdots + e_i$ containing $e_i$": the circuits present in $e_1 + \cdots + e_i$ but not in $e_1 + \cdots + e_{i-1}$ are exactly those containing $e_i$. The ordered set $e_1, \dots, e_p$ is a duplicate-free list l; indices are 0-based in Lean. Nullity is integer valued.