This file states the Seymour decomposition theorem. Proving hardSeymour is the ultimate goal of this project.

def StandardRepresentation.IsGraphic {α : Type} [DecidableEq α] (M : StandardRepresentation α) : Prop

TODO define graphics matroids.

Equations

• M.IsGraphic = sorryAx Prop

def StandardRepresentation.IsCographic {α : Type} [DecidableEq α] (M : StandardRepresentation α) : Prop

TODO define cographics matroids.

Equations

• M.IsCographic = sorryAx Prop

def MatroidR10 {α : Type} [DecidableEq α] : StandardRepresentation α

TODO define R10.

Equations

• MatroidR10 = sorryAx (StandardRepresentation α)

inductive StandardRepresentation.IsGood {α : Type} [DecidableEq α] : StandardRepresentation α → Prop

Given matroid can be constructed from graphic matroids, cographics matroids, and R10 using 1-sums, 2-sums, and 3-sums.

• graphic: ∀ {α : Type} [inst : DecidableEq α] {M : StandardRepresentation α}, M.IsGraphic → M.IsGood
• cographic: ∀ {α : Type} [inst : DecidableEq α] {M : StandardRepresentation α}, M.IsCographic → M.IsGood
• theR10: ∀ {α : Type} [inst : DecidableEq α] {M : StandardRepresentation α} {e : α ≃ Fin 10}, M.toMatroid.mapEquiv e = MatroidR10.toMatroid → M.IsGood
• is1sum: ∀ {α : Type} [inst : DecidableEq α] {M M₁ M₂ : StandardRepresentation α}, M.Is1sumOf M₁ M₂ → M.IsGood
• is2sum: ∀ {α : Type} [inst : DecidableEq α] {M M₁ M₂ : StandardRepresentation α}, M.Is2sumOf M₁ M₂ → M.IsGood
• is3sum: ∀ {α : Type} [inst : DecidableEq α] {M M₁ M₂ : StandardRepresentation α}, M.Is3sumOf M₁ M₂ → M.IsGood

theorem hardSeymour {α : Type} [DecidableEq α] {M : StandardRepresentation α} (hM : M.IsRegular) : M.IsGood