§8 — the rank postulates (R) and the circuit postulates (C) are equivalent

Let $M$ be a finite set of elements. Whitney's rank postulates $(\mathrm R_1)$–$(\mathrm R_3)$ and circuit postulates $(\mathrm C_1)$, $(\mathrm C_2)$ define the same structures, through mutually inverse translations:

1. If $r$ satisfies $(\mathrm R_1)$–$(\mathrm R_3)$, then its circuits (minimal sets of positive nullity) satisfy $(\mathrm C_1)$, $(\mathrm C_2)$, the empty set is not a circuit, and the rank defined from these circuits is $r$ again:

2. If a family $\mathcal C$ of nonempty subsets satisfies $(\mathrm C_1)$, $(\mathrm C_2)$, then the rank $r_{\mathcal C}$ defined from it satisfies $(\mathrm R_1)$–$(\mathrm R_3)$, and the circuits of $r_{\mathcal C}$ are exactly the members of $\mathcal C$:

Here $\mathcal C(r)$ denotes the circuits of the rank function $r$, and $r_{\mathcal C}(N) = \sum_i \Gamma_i$ along an enumeration $e_1, \dots, e_p$ of $N$, with $\Gamma_i = 0$ if some member of $\mathcal C$ inside $\{e_1, \dots, e_i\}$ contains $e_i$ and $\Gamma_i = 1$ otherwise. In Whitney's words: the definitions of rank and of circuits under the two systems agree, and hence the systems are equivalent.

Formalization Note The paper takes the circuits to be nonempty tacitly: a circuit of a rank system has positive nullity, so it is never empty, while the family $\{\emptyset\}$ satisfies $(\mathrm C_1)$, $(\mathrm C_2)$ vacuously and its circuit rank has no circuits at all. The hypothesis "$\emptyset$ is not a circuit" is therefore added in part 2, and its counterpart is proved in part 1. The elements form a finite type, subsets are Finsets, ranks are integers, and the rank from circuits is computed along the enumeration N.toList.