Theorems

Same-phase stability for graph polynomials

A multivariate polynomial is same-phase stable when every nonnegative one-dimensional specialization is real-rooted. Leake and Ryder proved that the multivariate independence polynomial is same-phase stable exactly for claw-free graphs. Their result also gives same-phase stability of the edge-variable matching polynomial and recovers the Chudnovsky–Seymour theorem by setting every variable equal to the same univariate variable.

References

J. D. Leake and N. R. Ryder, “Generalizations of the matching polynomial to the multivariate independence polynomial,” Algebraic Combinatorics 2 (2019), 781–802. See the discussion of same-phase stability on symmetricfunctions.com.

Definitions

  • Same-phase stability

    RealRooted.SamePhaseStablesource
    def SamePhaseStable {sigma : Type*} (P : MvPolynomial sigma ℝ) : Prop :=
  ∀ wt : sigma → ℝ, (∀ i, 0 ≤ wt i) → (commonPhaseRestriction wt P).Splits

  • Multivariate independence polynomial

    RealRooted.Graph.multivariateIndepPolysource
    def multivariateIndepPoly {V : Type u} [Fintype V]
    (G : _root_.SimpleGraph V) : MvPolynomial V ℝ := by
  classical
  exact ∑ s ∈ indepSetsOn G Finset.univ,
    ∏ v ∈ s, MvPolynomial.X v

  • Edge-variable matching polynomial

    RealRooted.Graph.multivariateMatchingPolynomialByEdgessource
    def multivariateMatchingPolynomialByEdges {V : Type u} [Fintype V]
    (G : _root_.SimpleGraph V) : MvPolynomial G.edgeSet ℝ := by
  classical
  exact ∑ M ∈ (Finset.univ.filter fun M : Finset G.edgeSet =>
      IsMatchingEdgeFinset G M),
    ∏ e ∈ M, MvPolynomial.X e

Theorems

  • Leake–Ryder: same-phase stable if and only if claw-free

    RealRooted.Graph.multivariateIndepPoly_samePhaseStable_iff_clawFreesource
    theorem multivariateIndepPoly_samePhaseStable_iff_clawFree
    {V : Type u} [Fintype V] (G : _root_.SimpleGraph V) :
    SamePhaseStable (multivariateIndepPoly G) ↔ ClawFree G

  • Chudnovsky–Seymour via Leake–Ryder

    RealRooted.Graph.ClawFree.indepPoly_splits_of_leakeRydersource
    theorem ClawFree.indepPoly_splits_of_leakeRyder
    {V : Type u} [Fintype V] [DecidableEq V]
    {G : _root_.SimpleGraph V} (hG : ClawFree G) :
    (indepPoly G).Splits

  • The matching polynomial is same-phase stable

    RealRooted.Graph.multivariateMatchingPolynomialByEdges_samePhaseStablesource
    theorem multivariateMatchingPolynomialByEdges_samePhaseStable
    {V : Type u} [Fintype V]
    (G : _root_.SimpleGraph V) :
    SamePhaseStable (multivariateMatchingPolynomialByEdges G)

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