Lemma 7 — interchanging the last two elements does not change the circuit rank

Proved

WhitneyMatroid.RankCircuit.rankSeq_swap_last

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

circuitsmatroidsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1rank-function

Let the subsets of a finite set $M$ be divided into circuits and non-circuits so that $(\mathrm C_1)$ and $(\mathrm C_2)$ hold, and let $r(e_1, \dots, e_q) = \sum_i \Gamma_i$ be the rank of an ordered list defined from circuits ( $\Gamma_i = 0$ if some circuit inside $\{e_1, \dots, e_i\}$ contains $e_i$ , else $\Gamma_i = 1$ ). For distinct elements $e_1, \dots, e_q$ ,

r(e_1, \dots, e_{q-2}, e_{q-1}, e_q) = r(e_1, \dots, e_{q-2}, e_q, e_{q-1}).

This is the key step toward Lemma 8, that the circuit rank of a set does not depend on how its elements are ordered.

Formalization Note The list $(e_1,\dots,e_{q-2})$ is l, and $e_{q-1}, e_q$ are a, b; the whole list l ++ [a, b] is required to have no repetitions, as the paper's "ordered set of elements" implies.

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_RankCircuit_IsCircuitSystem

Formal statement

namespace WhitneyMatroid.RankCircuit

theorem rankSeq_swap_last {α : Type*} [Fintype α] [DecidableEq α]
    (C : Finset α → Prop) (hC : IsCircuitSystem C) (l : List α) (a b : α)
    (hnd : (l ++ [a, b]).Nodup) :
    rankSeq C (l ++ [a, b]) = rankSeq C (l ++ [b, a]) := by sorry

end WhitneyMatroid.RankCircuit

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 516, Lemma 7

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