Matching cuts

DefinitionAverage degree of a finite graph#✓fully proved

For a simple graph \(G\) on a finite vertex set \(V\) with edge set \(E\), the average degree of \(G\) is the rational number \(2|E|/|V|\); it equals \(0\) when \(V\) is empty.

noncomputable def avgDegree {V : Type*} [Fintype V]
    (G : SimpleGraph V) [DecidableRel G.Adj] : ℚ :=
  (2 * G.edgeFinset.card : ℚ) / Fintype.card V

Used by 1

Used byMatching cut and girth question, affirmative form

DefinitionMatching cut#✓fully proved

A simple graph \(G\) has a matching cut if some matching \(M\) of \(G\), that is, a set of pairwise disjoint edges of \(G\), is such that deleting the edges of \(M\) from \(G\) leaves two vertices \(u\) and \(v\) that are not joined by any path. The matching may be empty, in which case this says that \(G\) itself has two vertices not joined by any path.

def HasMatchingCut {V : Type*} (G : SimpleGraph V) : Prop :=
  ∃ H : G.Subgraph, H.IsMatching ∧
    ∃ u v : V, ¬ (G.deleteEdges H.edgeSet).Reachable u v

Used by 1

Used byMatching cut and girth question, affirmative form

DefinitionMatching cut and girth question, affirmative form#✓fully proved

For every real number \(d\) there is a natural number \(g\) such that every simple graph \(G\) on a finite vertex set with at least two vertices, whose average degree is less than \(d\) and whose girth is at least \(g\), has a matching cut. An acyclic graph has infinite girth, so it meets the girth bound for every \(g\).

def conjecture : Prop :=
  ∀ d : ℝ, ∃ g : ℕ, ∀ (V : Type*) [Fintype V] [Nontrivial V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj],
    (avgDegree G : ℝ) < d →
    ((g : ℕ∞) ≤ G.egirth) →
    HasMatchingCut G

Sources

• [OPG-37364], Open Problem Garden, "Matching cut and girth".

Uses 2 · Used by 1

Statement usesMatching cut · Average degree of a finite graph

Used byNegative answer to the matching cut and girth question

TheoremNegative answer to the matching cut and girth question#●ready to prove

It is not the case that for every real number \(d\) there is a natural number \(g\) such that every simple graph on a finite vertex set with at least two vertices, average degree less than \(d\) and girth at least \(g\) has a matching cut. That is, there is a real number \(d\) such that for every natural number \(g\) some simple graph on a finite vertex set with at least two vertices, average degree less than \(d\) and girth at least \(g\) has no matching cut.

Feghali, Lucke, Paulusma and Ries (Lemma 5) construct, for every \(g\), a connected 14-regular bipartite graph of girth at least \(g\) with no matching cut; these graphs give \(d = 15\).

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• C. Feghali, F. Lucke, D. Paulusma and B. Ries, Matching Cuts in Graphs of High Girth and H-Free Graphs, ISAAC 2023, arXiv:2212.12317, https://arxiv.org/abs/2212.12317.

Uses 1

Statement usesMatching cut and girth question, affirmative form

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.