Local rank arguments for adjacency and hyperplane intersections in the path proof. All contextual hypotheses are explicit. No structural existence theorem is assumed globally, and none of these results depends on the path theorem.
theorem
TutteFormalization.tutteAdjacent_of_corankTwo
{α : Type u_1}
{M : Matroid α}
[M.Finite]
{F X Y : Set α}
(hF : Indecomposable M F)
(hc : CorankTwo M F)
(hX : IsHyperplane M X)
(hY : IsHyperplane M Y)
(hXY : X ≠ Y)
(hFX : F ⊆ X)
(hFY : F ⊆ Y)
:
TutteAdjacent M X Y
After the nested-flat equality, indecomposability gives the Tutte edge.
theorem
TutteFormalization.corankTwo_inter_eq_of_join_eq_ground
{α : Type u_1}
{M : Matroid α}
[M.Finite]
{F L U : Set α}
(hF : M.IsFlat F)
(hL : CorankTwo M L)
(hU : M.IsFlat U)
(hFL : F ⊆ L)
(hFU : F ⊆ U)
(hUr : natRank M U = natRank M F + 2)
(hjoin : M.closure (L ∪ U) = M.E)
:
The source's submodularity argument for the complementary intersection. The rank equation for U and the join condition are explicit premises supplied by the structural constructions in the other project modules.
theorem
TutteFormalization.path_join_rank_bounds
{α : Type u_1}
{M : Matroid α}
[M.Finite]
{F L U P : Set α}
(hL : M.IsFlat L)
(hP : M.IsFlat P)
(hLU : L ∩ U = F)
(hFP : F ⊂ P)
(hPU : P ⊆ U)
(hPr : natRank M P = natRank M F + 1)
:
Apply with P=V or P=W. Derives the intersection and strict containment before proving both rank bounds. No corank hypothesis is needed here.
theorem
TutteFormalization.path_join_isHyperplane
{α : Type u_1}
{M : Matroid α}
[M.Finite]
{F L U P : Set α}
(hL : CorankTwo M L)
(hP : M.IsFlat P)
(hLU : L ∩ U = F)
(hFP : F ⊂ P)
(hPU : P ⊆ U)
(hPr : natRank M P = natRank M F + 1)
:
IsHyperplane M (M.closure (L ∪ P))
With L of corank two, the two bounds give the constructed hyperplane's rank.