Finite-flat rank tools using Mathlib's rank and closure API. Natural ranks are an internal arithmetic interface to finite eRk. The structural lemmas do not depend on the path theorem.

theorem TutteFormalization.contraction_finite {α : Type u_1} (M : Matroid α) [M.Finite] (F : Set α) : (M.contract F).Finite

Mathlib infers finiteness after arbitrary contraction.

noncomputable def TutteFormalization.natRank {α : Type u_1} (M : Matroid α) (F : Set α) : ℕ

Engineering interface; only used with a finite-ground-set matroid below.

Equations

• TutteFormalization.natRank M F = (M.eRk F).toNat

theorem TutteFormalization.cast_natRank {α : Type u_1} (M : Matroid α) [M.Finite] (F : Set α) : ↑(natRank M F) = M.eRk F

theorem TutteFormalization.natRank_mono {α : Type u_1} {M : Matroid α} [M.Finite] {F G : Set α} (hFG : F ⊆ G) : natRank M F ≤ natRank M G

theorem TutteFormalization.natRank_closure {α : Type u_1} (M : Matroid α) (F : Set α) : natRank M (M.closure F) = natRank M F

theorem TutteFormalization.natRank_submodular {α : Type u_1} (M : Matroid α) [M.Finite] (F G : Set α) : natRank M (F ∩ G) + natRank M (M.closure (F ∪ G)) ≤ natRank M F + natRank M G

Convert Mathlib's submodular rank inequality to finite natural ranks.

theorem TutteFormalization.flat_eq_of_subset_of_natRank_le {α : Type u_1} {M : Matroid α} [M.Finite] {F G : Set α} (hF : M.IsFlat F) (hG : M.IsFlat G) (hFG : F ⊆ G) (hr : natRank M G ≤ natRank M F) : F = G

BG-01: nested flats cannot have nonincreasing rank unless they are equal.

theorem TutteFormalization.natRank_lt_of_flat_ssubset {α : Type u_1} {M : Matroid α} [M.Finite] {F G : Set α} (hF : M.IsFlat F) (hG : M.IsFlat G) (hFG : F ⊂ G) : natRank M F < natRank M G

theorem TutteFormalization.flat_inter {α : Type u_1} {M : Matroid α} {F G : Set α} (hF : M.IsFlat F) (hG : M.IsFlat G) : M.IsFlat (F ∩ G)

BG-01: intersection of flats, via closure monotonicity and extensivity.

theorem TutteFormalization.hyperplane_natRank {α : Type u_1} {M : Matroid α} [M.Finite] {H : Set α} (hH : IsHyperplane M H) : natRank M H + 1 = natRank M M.E

BG-01: adjoining one element outside a hyperplane spans the ground set.

theorem TutteFormalization.isHyperplane_of_natRank {α : Type u_1} {M : Matroid α} [M.Finite] {H : Set α} (hH : M.IsFlat H) (hr : natRank M H + 1 = natRank M M.E) : IsHyperplane M H

theorem TutteFormalization.hyperplane_inter_eq_of_corankTwo {α : Type u_1} {M : Matroid α} [M.Finite] {F : Set α} (hF : CorankTwo M F) {X Y : Set α} (hX : IsHyperplane M X) (hY : IsHyperplane M Y) (hXY : X ≠ Y) (hFX : F ⊆ X) (hFY : F ⊆ Y) : X ∩ Y = F

Strict containment below a hyperplane gives the upper rank bound.