Prove2Me

§16 — the rank function of the matroid M′M'

Proved
WhitneyMatroid.Fano.fano_eRk

by mikedeng1 · 1 vote · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

fano-matroidmatroidsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let MM be the matroid M′M' of §16: elements 1,…,71,\dots,7, bases all three-element sets except 124,135,167,236,257,347,456124,135,167,236,257,347,456 (16.1). For every set SS of kk elements,

r(S)={kk≤2,3k≥4,2k=3, S∈(16.1),3k=3, S∉(16.1).r(S)=\begin{cases} k & k\le 2,\\ 3 & k\ge 4,\\ 2 & k=3,\ S\in(16.1),\\ 3 & k=3,\ S\notin(16.1).\end{cases}

This is the explicit rank function of the Fano matroid; it is what one checks against the ranks of submatrices when testing whether a matrix corresponds to M′M'.

Formalization Note The elements are Fin 7 (Whitney's kk is k - 1); the size of SS is Set.ncard, and ranks are M.eRk.

Preamble
import Mathlib
import Definitions.Def_WhitneyMatroid_Fano_IsFano
Formal statement
namespace WhitneyMatroid.Fano

/-- Whitney §16 (p. 529): in the matroid `M′` of §16 (rank defined in terms of bases), each set of
`k` elements has rank `k` if `k ≤ 2` and rank `3` if `k ≥ 4`; a set of three elements has rank `2`
if it is one of the sets (16.1) and rank `3` otherwise. -/
theorem fano_eRk (M : Matroid (Fin 7)) (hM : IsFano M) (S : Set (Fin 7)) :
    (S.ncard ≤ 2 → M.eRk S = S.ncard) ∧
      (4 ≤ S.ncard → M.eRk S = 3) ∧
      (S.ncard = 3 → S ∈ fanoLines → M.eRk S = 2) ∧
      (S.ncard = 3 → S ∉ fanoLines → M.eRk S = 3) := by sorry

end WhitneyMatroid.Fano
Source
Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 529, §16
Human review

  • Endorsed by Shuze Chen · Oct 5, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 5, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph