Rota's conjecture: finitely many excluded minors for every finite field

Read-back of the theorem TenChallenges.challenge_02.

The statement is:

$$\forall\, r \in \mathbb{N}\;\; \exists\, B \in \mathbb{N}:\quad \mathrm{statement\_02}(r, B),$$

that is: for every natural number $r$ there exists a natural number $B$ (allowed to depend on $r$) such that for all natural numbers $p, m$ and every proof that $p$ is prime (so: for every prime $p$ and every $m$),

$$0 < m \;\text{ and }\; p^m \le r \quad\Longrightarrow\quad \mathrm{ExcludedMinorsAtMost}(p, m, B).$$

The proof body in the file is sorry (left unproved); this read-back describes only the asserted statement. Everything below unfolds the bundle definitions used.

Matroids. A matroid $M$ on a type $\gamma$ is Mathlib's Matroid γ: a ground set $E(M) \subseteq \gamma$ (possibly infinite or empty) with "base" and "independent" predicates on subsets of $\gamma$, where a set is independent iff it is contained in some base, at least one base exists, bases satisfy the exchange axiom (for bases $B_1, B_2$ and $a \in B_1 \setminus B_2$ there is $b \in B_2\setminus B_1$ with $(B_1\setminus\{a\})\cup\{b\}$ a base), every independent subset of any $X \subseteq E(M)$ is contained in a maximal independent subset of $X$, and every base lies in $E(M)$. Hence every independent set lies in $E(M)$ and $\emptyset$ is independent.

$\mathrm{GF}(p^m)$-representable ($\mathrm{IsGFRepresentable}(p, m, M)$, $M$ a matroid on $\gamma$): there exist a type $W$ in the lowest universe, an additive commutative group structure on $W$, a vector-space structure on $W$ over $\mathrm{GF}(p^m)$ (Mathlib's GaloisField p m, the splitting field of $X^{p^m} - X$ over $\mathbb{Z}/p\mathbb{Z}$; since $m \ge 1$ here, the field with $p^m$ elements), and a function $v : \gamma \to W$ defined on all of $\gamma$, such that for every subset $I \subseteq \gamma$ (not just subsets of $E(M)$)

$$I \text{ is independent in } M \iff (v(x))_{x \in I} \text{ is linearly independent over } \mathrm{GF}(p^m),$$

linear independence of the family indexed by the elements of $I$ meaning that $c \mapsto \sum_{x\in I} c_x\,v(x)$ is injective on finitely supported coefficient functions $c : I \to \mathrm{GF}(p^m)$ (a repeated vector or a zero vector makes the family dependent; the empty family is independent). As independent sets lie in $E(M)$, this forces $v(x) = 0$ for every $x \notin E(M)$. There is no bound on the dimension of $W$, and no finiteness assumption on $M$ inside this definition.

Strict minor. For matroids $N, M$ on the same type $\gamma$, $N <_m M$ (Mathlib's IsStrictMinor) means $N \le_m M$ and not $M \le_m N$, where $N \le_m M$ (Mathlib's IsMinor) means there exist sets $C, D \subseteq \gamma$ (not required to be disjoint or to lie in $E(M)$) with $N = (M / C) \setminus D$; deletion $M \setminus D$ is the restriction of $M$ to $E(M) \setminus D$ (independent sets: the $M$-independent subsets of $E(M)\setminus D$), and contraction $M / C$ is $(M^{*} \setminus C)^{*}$, the dual of deleting $C$ from the dual, with ground set $E(M)\setminus C$. Mathlib documents $N <_m M$ as equivalent to "$N$ is a minor of $M$ and $N \ne M$".

Excluded minor for a property $P$ ($\mathrm{IsExcludedMinorFor}(P, M)$): $\neg P(M)$, and $P(N)$ for every matroid $N$ on the same type with $N <_m M$. If $M$ has no strict minors (for instance $E(M) = \emptyset$), the second clause is vacuous.

Isomorphism ($\mathrm{IsIso}(N, M)$, a definition of this bundle, for $N$ on $\mathbb{N}$ and $M$ on $\beta$): there exists a bijection $e : E(N) \to E(M)$ such that for every $I \subseteq E(N)$, $I$ is independent in $N$ iff $e(I) = \{e(x) : x \in I\}$ is independent in $M$.

$\mathrm{ExcludedMinorsAtMost}(p, m, B)$: there exists a finite set $S$ of matroids on the type $\mathbb{N}$ (each with ground set an arbitrary subset of $\mathbb{N}$, possibly infinite or empty), with

$$|S| \le B,$$

such that for every type $\beta$ in the lowest universe and every matroid $M$ on $\beta$ whose ground set $E(M)$ is finite: if $M$ is an excluded minor for the property $\mathrm{IsGFRepresentable}(p, m, \cdot)$ (so $M$ is not $\mathrm{GF}(p^m)$-representable, while every strict minor of $M$ among matroids on $\beta$ is), then some $N \in S$ satisfies $\mathrm{IsIso}(N, M)$. The members of $S$ need not themselves be excluded minors, finite, or pairwise non-isomorphic, and $S$ may have fewer than $B$ elements; infinite excluded minors are not constrained.

Putting it together, the theorem asserts: for each $r \in \mathbb{N}$ there is one $B \in \mathbb{N}$ such that, for every prime $p$ and every $m \ge 1$ with $p^m \le r$, there is a set of at most $B$ matroids on $\mathbb{N}$ containing, up to the above notion of isomorphism, every finite-ground-set matroid (on any type in the lowest universe) that is not $\mathrm{GF}(p^m)$-representable but all of whose strict minors are.

Edge cases: for $r \le 1$ there is no prime power $p^m \le r$ with $m \ge 1$, so the inner statement is vacuous and any $B$ (e.g. $B = 0$) works. For $r \ge 2$ the single $B$ must work for all prime powers $p^m \le r$ at once; a witness $B = 0$ would assert that no finite excluded minor exists for those fields. The theorem gives no information about $B$ beyond existence, and no uniformity in $r$ is claimed (a separate $B$ for each $r$).