Prove2Me

§8 — the rank defined from circuits satisfies (R₁), (R₂), (R₃)

Proved
WhitneyMatroid.RankCircuit.rankSystem_of_circuitSystem

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 MM be divided into circuits and non-circuits so that (C1)(\mathrm C_1) and (C2)(\mathrm C_2) hold, and let r(N)r(N) be the rank of NN defined from circuits (the sum of the Γi\Gamma_i along an enumeration of NN). Then rr satisfies the rank postulates:

  1. (R1)(\mathrm R_1) r(∅)=0r(\emptyset) = 0;
  2. (R2)(\mathrm R_2) for e∉Ne \notin N, r(N+e)=r(N)r(N + e) = r(N) or r(N)+1r(N) + 1;
  3. (R3)(\mathrm R_3) for e1,e2∉Ne_1, e_2 \notin N, if r(N+e1)=r(N+e2)=r(N)r(N + e_1) = r(N + e_2) = r(N), then r(N+e1+e2)=r(N)r(N + e_1 + e_2) = r(N).

This is the deduction of the rank postulates from the circuit postulates, the other half of the equivalence.

Formalization Note The rank of a set is computed along the fixed enumeration N.toList, so this statement holds only if the value is in effect independent of that choice (Lemma 8).

Preamble
import Mathlib
import Definitions.Def_WhitneyMatroid_RankCircuit_IsRankSystem
import Definitions.Def_WhitneyMatroid_RankCircuit_IsCircuitSystem
Formal statement
namespace WhitneyMatroid.RankCircuit

theorem rankSystem_of_circuitSystem {α : Type*} [Fintype α] [DecidableEq α]
    (C : Finset α → Prop) (hC : IsCircuitSystem C) :
    IsRankSystem (rankOfCircuits C) := by sorry

end WhitneyMatroid.RankCircuit
Source
Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), pp. 516–517, §8
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