Independence polynomial of claw-free graphs

10 fully proved

Claw-free graphs and independence polynomials

DefinitionClaw-free finite graph#✓fully proved

A simple graph \(G\) on a finite vertex set \(V\) is claw-free if it has no induced claw \(K_{1,3}\): there are no vertices \(c, \ell_1, \ell_2, \ell_3 \in V\) such that \(\ell_1, \ell_2, \ell_3\) are pairwise distinct, each is adjacent to \(c\) and different from \(c\), and no two of them are adjacent.

public def clawFree {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    [DecidableRel G.Adj] : Prop :=
  ¬ ∃ c l₁ l₂ l₃ : V, c ≠ l₁ ∧ c ≠ l₂ ∧ c ≠ l₃ ∧ l₁ ≠ l₂ ∧ l₁ ≠ l₃ ∧ l₂ ≠ l₃ ∧
    G.Adj c l₁ ∧ G.Adj c l₂ ∧ G.Adj c l₃ ∧ ¬ G.Adj l₁ l₂ ∧ ¬ G.Adj l₁ l₃ ∧ ¬ G.Adj l₂ l₃

Sources

• Moussa Benoumhani, "On the Modes of the Independence Polynomial of the Centipede," Journal of Integer Sequences 15 (2012), Article 12.5.1, unnumbered Chudnovsky–Seymour theorem, lines 142–144, https://cs.uwaterloo.ca/journals/JIS/VOL15/Benoumhani/benoumhani8.tex quoting M. Chudnovsky and P. Seymour, "The roots of the independence polynomial of a clawfree graph," J. Combin. Theory Ser. B 97 (2007), 350–357 (biblio lines 499–501).

Used by 3

Used byThe two definitions of claw-free agree · Claw-free finite graphs have no induced claw · Chudnovsky–Seymour theorem

TheoremChudnovsky–Seymour theorem#✓fully proved

Let \(G\) be a claw-free simple graph on a finite vertex set \(V\), and let \(I(G) = \sum_{k=0}^{|V|} i_k X^k \in \mathbb{Z}[X]\) be its independence polynomial, where \(i_k\) is the number of independent sets of \(G\) with \(k\) vertices. Then \(I(G)\), viewed as a polynomial with real coefficients, splits over \(\mathbb{R}\): it is a constant times a product of linear factors \(X - r\) with \(r \in \mathbb{R}\), so all its roots are real.

public theorem independence_poly_of_claw_free_splits :
    ∀ {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
      clawFree G → ((independencePoly G).map (Int.castRingHom ℝ)).Splits

Sources

• Moussa Benoumhani, "On the Modes of the Independence Polynomial of the Centipede," Journal of Integer Sequences 15 (2012), Article 12.5.1, unnumbered Chudnovsky–Seymour theorem, lines 142–144, https://cs.uwaterloo.ca/journals/JIS/VOL15/Benoumhani/benoumhani8.tex quoting M. Chudnovsky and P. Seymour, "The roots of the independence polynomial of a clawfree graph," J. Combin. Theory Ser. B 97 (2007), 350–357 (biblio lines 499–501).

Uses 1

Statement usesClaw-free finite graph

TheoremClaw-free finite graphs have no induced claw#✓fully proved

Let \(G\) be a simple graph on a finite vertex set. Then \(G\) is claw-free if and only if the claw \(K_{1,3}\), the star graph on four vertices whose center is adjacent to the other three, is not an induced subgraph of \(G\), that is, there is no injective map from its vertices to those of \(G\) that preserves both adjacency and nonadjacency.

public theorem clawFree_iff_not_isIndContained {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] :
    clawFree G ↔ ¬ (SimpleGraph.starGraph (0 : Fin 4)).IsIndContained G

Uses 1

Statement usesClaw-free finite graph

TheoremCoefficients of the independence polynomial#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\), and let \(I(G) = \sum_{k=0}^{|V|} i_k X^k \in \mathbb{Z}[X]\) be its independence polynomial, where \(i_k\) is the number of independent sets of \(G\) with \(k\) vertices. Then for every natural number \(k\), the coefficient of \(X^k\) in \(I(G)\) is the number of independent sets of \(G\) with exactly \(k\) vertices.

public theorem independencePoly_coeff {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) :
    (independencePoly G).coeff k = ((G.indepSetFinset k).card : ℤ)

Used by 2

Used byIndependence polynomial of the edgeless graph · Independence polynomial of the complete graph

TheoremEvaluating the independence polynomial#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\), and let \(I(G) = \sum_{k=0}^{|V|} i_k X^k \in \mathbb{Z}[X]\) be its independence polynomial, where \(i_k\) is the number of independent sets of \(G\) with \(k\) vertices. Then for every element \(x\) of a commutative ring \(R\), the value of \(I(G)\) at \(x\) is \(\sum_S x^{|S|}\), the sum running over all independent sets \(S \subseteq V\) of \(G\), the empty set included.

public theorem aeval_independencePoly {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type*} [CommRing R] (x : R) :
    Polynomial.aeval x (independencePoly G)
      = ∑ s ∈ Finset.univ.filter (fun s : Finset V => G.IsIndepSet (s : Set V)),
        x ^ s.card

TheoremIndependence polynomial of the edgeless graph#✓fully proved

Let \(V\) be a finite set. For a simple graph \(G\) on \(V\), let \(I(G) = \sum_{k=0}^{|V|} i_k X^k \in \mathbb{Z}[X]\) be its independence polynomial, where \(i_k\) is the number of independent sets of \(G\) with \(k\) vertices. If \(G\) is the graph on \(V\) with no edges, then \(I(G) = (1 + X)^{|V|}\).

public theorem independencePoly_bot {V : Type*} [Fintype V] [DecidableEq V] :
    independencePoly (⊥ : SimpleGraph V) = (1 + Polynomial.X) ^ Fintype.card V

Uses 1

Proof usesCoefficients of the independence polynomial

TheoremIndependence polynomial of the complete graph#✓fully proved

Let \(V\) be a finite set. For a simple graph \(G\) on \(V\), let \(I(G) = \sum_{k=0}^{|V|} i_k X^k \in \mathbb{Z}[X]\) be its independence polynomial, where \(i_k\) is the number of independent sets of \(G\) with \(k\) vertices. If \(G\) is the complete graph on \(V\), then \(I(G) = 1 + |V|\,X\).

public theorem independencePoly_top {V : Type*} [Fintype V] [DecidableEq V] :
    independencePoly (⊤ : SimpleGraph V)
      = 1 + Polynomial.C (Fintype.card V : ℤ) * Polynomial.X

Uses 1

Proof usesCoefficients of the independence polynomial

Simple Graph

DefinitionClaw-free graph#✓fully proved

A simple graph \(G\) on a vertex set \(V\), not necessarily finite, is claw-free if it has no induced claw \(K_{1,3}\): there are no vertices \(c, \ell_1, \ell_2, \ell_3 \in V\) such that \(\ell_1, \ell_2, \ell_3\) are pairwise distinct, each is adjacent to \(c\) and different from \(c\), and no two of them are adjacent.

public def IsClawFree {V : Type*} (G : SimpleGraph V) : Prop :=
  ¬ ∃ c l₁ l₂ l₃ : V, c ≠ l₁ ∧ c ≠ l₂ ∧ c ≠ l₃ ∧ l₁ ≠ l₂ ∧ l₁ ≠ l₃ ∧ l₂ ≠ l₃ ∧
    G.Adj c l₁ ∧ G.Adj c l₂ ∧ G.Adj c l₃ ∧ ¬ G.Adj l₁ l₂ ∧ ¬ G.Adj l₁ l₃ ∧ ¬ G.Adj l₂ l₃

Used by 2

Used byThe two definitions of claw-free agree · Claw-free graphs have no induced claw

TheoremClaw-free graphs have no induced claw#✓fully proved

Let \(G\) be a simple graph on an arbitrary vertex set. Then \(G\) is claw-free if and only if the claw \(K_{1,3}\), the star graph on four vertices whose center is adjacent to the other three, is not an induced subgraph of \(G\), that is, there is no injective map from its vertices to those of \(G\) that preserves both adjacency and nonadjacency.

public theorem isClawFree_iff_not_isIndContained {V : Type*} (G : SimpleGraph V) :
    G.IsClawFree ↔ ¬ (starGraph (0 : Fin 4)).IsIndContained G

Uses 1

Statement usesClaw-free graph

Equivalence of the definitions

TheoremThe two definitions of claw-free agree#✓fully proved

A simple graph on a finite vertex set is a claw-free finite graph if and only if it is a claw-free graph in the sense defined for graphs on arbitrary vertex sets.

public theorem clawFree_iff_isClawFree {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] :
    clawFree G ↔ G.IsClawFree

Uses 2

Statement usesClaw-free finite graph · Claw-free graph

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.