Finite rank compatibility for contraction. The pinned API defines contraction by dual deletion; its dual and restriction rank formulas therefore suffice to derive the paper's contraction rank formula without adding an assumption.

theorem TutteFormalization.natRank_dual_add {α : Type u_1} (M : Matroid α) [M.Finite] (X : Set α) (hX : X ⊆ M.E) : natRank M✶ X + natRank M M.E = natRank M (M.E \ X) + X.ncard

theorem TutteFormalization.natRank_delete {α : Type u_1} (M : Matroid α) (C X : Set α) (hX : X ⊆ M.E \ C) : natRank (M.delete C) X = natRank M X

theorem TutteFormalization.natRank_contract_add {α : Type u_1} {M : Matroid α} [M.Finite] (F X : Set α) (hF : F ⊆ M.E) (hX : X ⊆ M.E \ F) : natRank (M.contract F) X + natRank M F = natRank M (X ∪ F)

BG-01: the exact additive form of the contraction rank formula on its ground set.

theorem TutteFormalization.contract_empty_isFlat {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) : (M.contract F).IsFlat ∅

BG-01: contracting a flat makes the empty set a flat (the quotient is loopless).

theorem TutteFormalization.natRank_empty {α : Type u_1} (M : Matroid α) : natRank M ∅ = 0

theorem TutteFormalization.natRank_pos_of_empty_isFlat {α : Type u_1} {M : Matroid α} [M.Finite] (h0 : M.IsFlat ∅) {A : Set α} (hAE : A ⊆ M.E) (hA : A.Nonempty) : 0 < natRank M A

A nonempty ground subset of a loopless matroid has positive rank.

theorem TutteFormalization.connected_of_empty_isFlat_of_rank_le_one {α : Type u_1} {M : Matroid α} [M.Finite] (h0 : M.IsFlat ∅) (hr : natRank M M.E ≤ 1) : Connected M

Source connectedness for loopless matroids of rank at most one, including rank zero.

theorem TutteFormalization.hyperplane_indecomposable {α : Type u_1} {M : Matroid α} [M.Finite] {H : Set α} (hH : IsHyperplane M H) : Indecomposable M H

def:indecomposable: every hyperplane is indecomposable.