BG-01 hyperplane separation follows the source's basis construction. ST-02's modular-cut rule is then proved using the exact rank equality.

theorem TutteFormalization.exists_hyperplane_superset_notMem {α : Type u_1} {M : Matroid α} [M.Finite] {F : Set α} (hF : M.IsFlat F) {e : α} (heE : e ∈ M.E) (heF : e ∉ F) : ∃ (H : Set α), IsHyperplane M H ∧ F ⊆ H ∧ e ∉ H

BG-01: extend a basis of F with e, then remove e from a containing base.

theorem TutteFormalization.subset_flat_of_forall_hyperplane {α : Type u_1} {M : Matroid α} [M.Finite] {F : Set α} (hF : M.IsFlat F) {A : Set α} (hAE : A ⊆ M.E) (h : ∀ (H : Set α), IsHyperplane M H → F ⊆ H → A ⊆ H) : A ⊆ F

BG-01: the containing hyperplanes detect containment in a flat.

theorem TutteFormalization.hyperplane_join_eq_ground {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : IsHyperplane M X) (hY : IsHyperplane M Y) (hne : X ≠ Y) : M.closure (X ∪ Y) = M.E

theorem TutteFormalization.hyperplanes_modularPair_of_corankTwo {α : Type u_1} {M : Matroid α} [M.Finite] {X Y : Set α} (hX : IsHyperplane M X) (hY : IsHyperplane M Y) (hne : X ≠ Y) (hc : CorankTwo M (X ∩ Y)) : ModularPair M X Y

ST-02: the precise modular equality, not just distinctness of hyperplanes.

theorem TutteFormalization.ModularCut.hyperplane_inter_mem {α : Type u_1} {M : Matroid α} [M.Finite] {X Y : Set α} {Γ : Set (Set α)} (hΓ : ModularCut M Γ) (hX : IsHyperplane M X) (hY : IsHyperplane M Y) (hne : X ≠ Y) (hc : CorankTwo M (X ∩ Y)) (hXΓ : X ∈ Γ) (hYΓ : Y ∈ Γ) : X ∩ Y ∈ Γ

ST-02 / PT-07: two cut hyperplanes with corank-two intersection put it in the cut.