Theorems

Claw-free independence polynomials

The independence polynomial counts independent vertex sets by cardinality. Chudnovsky and Seymour proved that it is real-rooted for every finite claw-free graph.

References

M. Chudnovsky and P. Seymour, “The roots of the independence polynomial of a clawfree graph,” Journal of Combinatorial Theory, Series B 97 (2007), 350–357. See also the graph-polynomial context on symmetricfunctions.com.

Definitions

  • Claw-free graph

    RealRooted.Graph.ClawFreesource
    def ClawFree {V : Type u} (G : _root_.SimpleGraph V) : Prop :=
  ∀ v : V, ∀ s : Finset V, (∀ w ∈ s, G.Adj v w) → ¬ G.IsNIndepSet 3 s

  • Independence polynomial

    RealRooted.Graph.indepPolysource
    def indepPoly {V : Type u} [Fintype V] [DecidableEq V]
    (G : _root_.SimpleGraph V) : ℝ[X] := by
  classical
  exact ∑ s ∈ (Finset.univ.powerset.filter fun s : Finset V =>
      G.IsIndepSet (s : Set V)),
    (X : ℝ[X]) ^ s.card

Theorems

  • Chudnovsky–Seymour: claw-free graphs have real-rooted independence polynomials

    RealRooted.Challenges.ChudnovskySeymour.clawFree_indepPoly_splitssource
    theorem clawFree_indepPoly_splits :
    ∀ {V : Type u} [Fintype V] [DecidableEq V]
      (G : _root_.SimpleGraph V),
      RealRooted.Graph.ClawFree G → (RealRooted.Graph.indepPoly G).Splits

Lean source RealRooted/Challenges/ChudnovskySeymour.lean at revision 5827550b.