Additive-rank partitions and their restrictions, the elementary direct-sum background used in lem:separation. These lemmas use the actual partition and rank equations rather than assuming a decomposition theorem.

theorem TutteFormalization.natRank_submodular_sets {α : Type u_1} (M : Matroid α) [M.Finite] (X Y : Set α) : natRank M (X ∩ Y) + natRank M (X ∪ Y) ≤ natRank M X + natRank M Y

theorem TutteFormalization.natRank_partition {α : Type u_1} {M : Matroid α} [M.Finite] {A B X : Set α} (hd : Disjoint A B) (hu : A ∪ B = M.E) (hr : natRank M A + natRank M B = natRank M M.E) (hX : X ⊆ M.E) : natRank M X = natRank M (X ∩ A) + natRank M (X ∩ B)

BG-01/BG-02: ranks in an additive ground partition add on every subset.

theorem TutteFormalization.natRank_inter_lt_of_not_subset_flat {α : Type u_1} {M : Matroid α} [M.Finite] {X H : Set α} (hH : M.IsFlat H) (hXE : X ⊆ M.E) (hn : ¬X ⊆ H) : natRank M (X ∩ H) < natRank M X

A set losing an element outside a flat loses rank when intersected with it.

theorem TutteFormalization.hyperplane_contains_partition_side {α : Type u_1} {M : Matroid α} [M.Finite] {A B H : Set α} (hd : Disjoint A B) (hu : A ∪ B = M.E) (hr : natRank M A + natRank M B = natRank M M.E) (hH : IsHyperplane M H) : A ⊆ H ∨ B ⊆ H

BG-01: a hyperplane in an additive ground partition contains one entire side.

theorem TutteFormalization.natRank_contract_partition {α : Type u_1} {M : Matroid α} [M.Finite] {A B : Set α} (hd : Disjoint A B) (hu : A ∪ B = M.E) (hr : natRank M A + natRank M B = natRank M M.E) (F : Set α) (hF : F ⊆ M.E) : natRank (M.contract F) (A \ F) + natRank (M.contract F) (B \ F) = natRank (M.contract F) (M.E \ F)

BG-01: contraction preserves the additive rank of the two residual sides.

theorem TutteFormalization.natRank_eq_ncard_of_isBasis {α : Type u_1} {M : Matroid α} {I S : Set α} (hI : M.IsBasis I S) : natRank M S = I.ncard

BG-01: a basis computes natural rank by its finite cardinality.

theorem TutteFormalization.natRank_add_of_hyperplane_sides {α : Type u_1} {M : Matroid α} [M.Finite] {A B : Set α} (hd : Disjoint A B) (hu : A ∪ B = M.E) (hh : ∀ (H : Set α), IsHyperplane M H → A ⊆ H ∨ B ⊆ H) : natRank M A + natRank M B = natRank M M.E

Direct-sum background: the hyperplane-side property implies rank additivity. Extend a basis of A to a ground basis; the remaining basis elements span B, since otherwise a hyperplane containing them would contain neither full side.