Challenge 2: the scaled excluded-minor statement $S(r,B)$

Read-back of TenChallenges.statement_02 r B (a proposition depending on two natural numbers $r$ and $B$).

The definition asserts: for all natural numbers $p$ and $m$, and for every proof that $p$ is prime (a typeclass hypothesis Fact p.Prime bound inside the universal quantifier, so in effect: for every prime $p$ and every natural $m$),

where $\mathrm{ExcludedMinorsAtMost}(p, m, B)$ is the bundle definition from item TenChallenges_MatroidRepresentability, which unfolds as follows.

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$ such that a set is independent iff it lies in some base, some base exists, bases satisfy the exchange axiom, every independent subset of any $X \subseteq E(M)$ extends to a maximal independent subset of $X$, and bases lie in $E(M)$; hence independent sets lie in $E(M)$ and $\emptyset$ is independent.

$\mathrm{GF}(p^m)$-representability ($\mathrm{IsGFRepresentable}(p,m,M)$ for a matroid $M$ 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}$; for $m \ge 1$ 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 only subsets of $E(M)$),

where linear independence of the family indexed by the elements of $I$ means that $c \mapsto \sum_{x \in I} c_x v(x)$ is injective on finitely supported coefficient functions (repeated vectors or a zero vector make the family dependent; the empty family is independent). Since independent sets lie in $E(M)$, this forces $v(x)=0$ for all $x \notin E(M)$. No bound on $\dim W$.

Excluded minor ($\mathrm{IsExcludedMinorFor}(P, M)$ for $P = \mathrm{IsGFRepresentable}(p,m,\cdot)$): $\neg P(M)$, and for every matroid $N$ on the same type $\gamma$ with $N <_m M$, $P(N)$ holds. Here $N <_m M$ is Mathlib's strict minor relation: $N \le_m M$ and not $M \le_m N$, where $N \le_m M$ means $N = (M/C)\setminus D$ for some sets $C, D \subseteq \gamma$ (not required disjoint or inside $E(M)$), with $M \setminus D$ the restriction of $M$ to $E(M)\setminus D$ and $M/C = (M^*\setminus C)^*$ the contraction (ground set $E(M) \setminus C$). Mathlib documents $N <_m M$ as equivalent to "$N$ is a minor of $M$ and $N \ne M$". If $M$ has no strict minors (e.g. $E(M)=\emptyset$), the second clause is vacuous.

Isomorphism ($\mathrm{IsIso}(N, M)$, a bundle definition): there is a bijection $e : E(N) \to E(M)$ such that for every $I \subseteq E(N)$, $I$ is independent in $N$ iff $e(I)$ is independent in $M$.

$\mathrm{ExcludedMinorsAtMost}(p, m, B)$: there exists a finite set $S$ of matroids on the type $\mathbb{N}$ (ground sets arbitrary subsets of $\mathbb{N}$) with $|S| \le B$ such that for every type $\beta$ in the lowest universe and every matroid $M$ on $\beta$ with $E(M)$ finite, if $M$ is an excluded minor for $\mathrm{GF}(p^m)$-representability (as unfolded above, with minors taken among matroids on $\beta$), then some $N \in S$ satisfies $\mathrm{IsIso}(N, M)$. Members of $S$ need not be excluded minors, finite, or pairwise non-isomorphic; $B=0$ forces $S=\emptyset$ and then asserts that no finite excluded minor exists; infinite excluded minors are unconstrained.

Edge cases of $\mathrm{statement\_02}$ itself: the hypothesis $0 < m$ excludes $m = 0$ (so $\mathrm{GF}(p^m)$ always has $p^m \ge 2$ elements here). For $r \le 1$ no pair $(p, m)$ with $p$ prime, $m \ge 1$, $p^m \le r$ exists, so $\mathrm{statement\_02}(r, B)$ holds vacuously for every $B$. For $r \ge 2$ the single number $B$ must serve simultaneously as the bound for every prime power $p^m \le r$ with $m \ge 1$ (e.g. for $r = 4$: $2^1, 3^1, 2^2$). The hypotheses mention only $p^m \le r$; nothing depends on $r$ otherwise.