prop:indecomposable-step: the source maximal-intersection construction.

theorem TutteFormalization.exists_crossing_hyperplane {α : Type u_1} {M : Matroid α} [M.Finite] {S T : Set α} (hS : M.IsFlat S) (hT : Indecomposable M T) (hTS : T ⊂ S) (hSE : S ≠ M.E) : ∃ (H : Set α), IsHyperplane M H ∧ T ⊆ H ∧ ¬S ⊆ H ∧ S ∪ H ≠ M.E

theorem TutteFormalization.exists_indecomposable_step {α : Type u_1} {M : Matroid α} [M.Finite] {S T : Set α} (hS : Indecomposable M S) (hT : Indecomposable M T) (hTS : T ⊂ S) : ∃ (U : Set α), Indecomposable M U ∧ T ⊆ U ∧ U ⊂ S ∧ natRank M U + 1 = natRank M S

Source rank-one downward step; the maximized quantity is literally |H ∩ S|.