Tutte's theorem (work in progress)

Main definitions

• SimpleGraph.TutteViolator G u is a set of vertices u which certifies non-existence of a perfect matching.

def SimpleGraph.IsTutteViolator {V : Type u} (G : SimpleGraph V) (u : Set V) : Prop

A set certifying non-existence of a perfect matching.

Equations

• G.IsTutteViolator u = (u.ncard < (⊤.deleteVerts u).coe.oddComponents.ncard)

theorem SimpleGraph.Subgraph.IsPerfectMatching.exists_of_isClique_supp {V : Type u} {G : SimpleGraph V} [Fintype V] (hveven : Even (Nat.card V)) (h : ¬G.IsTutteViolator G.universalVerts) (h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp) : ∃ (M : G.Subgraph), M.IsPerfectMatching

Given a graph in which the universal vertices do not violate Tutte's condition, if the graph decomposes into cliques, it has a perfect matching.

theorem SimpleGraph.IsTutteViolator.empty {V : Type u} {G : SimpleGraph V} [Fintype V] (hodd : Odd (Fintype.card V)) : G.IsTutteViolator ∅

theorem SimpleGraph.not_isTutteViolator_of_isPerfectMatching {V : Type u} {G : SimpleGraph V} [Fintype V] {M : G.Subgraph} (hM : M.IsPerfectMatching) (u : Set V) : ¬G.IsTutteViolator u

Proves the necessity part of Tutte's theorem