Graph saturation

DefinitionSaturating non-edge#✓fully proved

Let \(F\) and \(G\) be simple graphs. A pair of vertices \(x, y\) of \(G\) is an \(F\)-saturating non-edge of \(G\) if \(x \ne y\), \(x\) and \(y\) are not adjacent in \(G\), and the graph \(G + xy\) obtained from \(G\) by adding the edge \(xy\) contains a copy of \(F\) (a subgraph isomorphic to \(F\), not necessarily induced).

def IsSaturatingNonedge (x y : W) : Prop :=
  x ≠ y ∧ ¬G.Adj x y ∧ IsContained F (G ⊔ edge x y)

Used by 2

Used byA saturating non-edge of an \(F\)-free graph creates a copy of \(F\) · Graph of saturating non-edges

TheoremA saturating non-edge of an \(F\)-free graph creates a copy of \(F\)#✓fully proved

Let \(F\) and \(G\) be simple graphs, and let \(xy\) be an \(F\)-saturating non-edge of \(G\). If \(G\) is \(F\)-free, that is, \(G\) contains no copy of \(F\), then the graph \(G + xy\) obtained from \(G\) by adding the edge \(xy\) contains a copy of \(F\), and \(G\) does not.

theorem IsSaturatingNonedge.newCopy_of_free {x y : W} (h : IsSaturatingNonedge F G x y)
    (hfree : Free F G) :
    IsContained F (G ⊔ edge x y) ∧ ¬IsContained F G

Uses 1

Statement usesSaturating non-edge

DefinitionGraph of saturating non-edges#✓fully proved

Let \(F\) and \(G\) be simple graphs. The graph of \(F\)-saturating non-edges of \(G\) is the simple graph on the vertices of \(G\) whose edges are exactly the \(F\)-saturating non-edges of \(G\).

def saturatingNonedgeGraph : SimpleGraph W :=
  fromRel (IsSaturatingNonedge F G)

Uses 1 · Used by 1

Statement usesSaturating non-edge

Used byNumber of saturating non-edges

DefinitionNumber of saturating non-edges#✓fully proved

Let \(F\) and \(G\) be simple graphs such that \(G\) has only finitely many \(F\)-saturating non-edges. Then \(f_F(G)\) is the number of \(F\)-saturating non-edges of \(G\), counted as unordered pairs \(\{x, y\}\), that is, the number of edges of the graph of \(F\)-saturating non-edges of \(G\).

def numSaturatingNonedges : ℕ :=
  #(saturatingNonedgeGraph F G).edgeFinset

Uses 1

Statement usesGraph of saturating non-edges

Definition\(H\)-saturated graphs#✓fully proved

Let \(H\) be a simple graph. A simple graph \(G\) is \(H\)-saturated if \(G\) is \(H\)-free (it contains no copy of \(H\) as a subgraph) and is maximal with this property: every \(H\)-free simple graph \(G'\) on the same vertex set as \(G\) with \(G \subseteq G'\) equals \(G\).

def IsSaturated (G : SimpleGraph W) : Prop :=
  Maximal H.Free G

Used by 6

Used bySaturation number is attained by a saturated graph · Saturation via strict supergraphs · Saturation via missing edges · Saturation of complete graphs · Edge counts of saturated graphs · Saturated graphs bound the saturation number

TheoremSaturation via strict supergraphs#✓fully proved

Let \(H\) be a simple graph. A simple graph \(G\) is \(H\)-saturated if and only if \(G\) is \(H\)-free and every simple graph \(G'\) on the same vertex set with \(G \subsetneq G'\) contains a copy of \(H\).

theorem isSaturated_iff_forall_gt (G : SimpleGraph W) :
    H.IsSaturated G ↔ H.Free G ∧ ∀ ⦃G' : SimpleGraph W⦄, G < G' → ¬ H.Free G'

Uses 1 · Used by 1

Statement uses\(H\)-saturated graphs

Used bySaturation via missing edges

TheoremSaturation via missing edges#✓fully proved

Let \(H\) be a simple graph. A simple graph \(G\) is \(H\)-saturated if and only if \(G\) is \(H\)-free and, for all distinct vertices \(s\) and \(t\) of \(G\) that are not adjacent in \(G\), the graph \(G + st\) obtained from \(G\) by adding the edge \(st\) contains a copy of \(H\).

This is the usual missing-edge definition of \(H\)-saturation.

theorem isSaturated_iff_missing_edge (G : SimpleGraph W) :
    H.IsSaturated G ↔
      H.Free G ∧ ∀ s t : W, s ≠ t → ¬ G.Adj s t → ¬ H.Free (G ⊔ edge s t)

Uses 2

Statement uses\(H\)-saturated graphs

Proof usesSaturation via strict supergraphs

TheoremSaturation of complete graphs#✓fully proved

Let \(H\) be a simple graph. The complete graph on any vertex set is \(H\)-saturated if and only if it is \(H\)-free.

A complete graph has no missing edge, so only \(H\)-freeness matters. The vertex set of the complete graph is independent of that of \(H\), so this condition is not vacuous: \(H\) need not embed in a complete graph with fewer vertices.

theorem isSaturated_top : H.IsSaturated (⊤ : SimpleGraph W) ↔ H.Free (⊤ : SimpleGraph W)

Uses 1

Statement uses\(H\)-saturated graphs

DefinitionEdge counts of saturated graphs#✓fully proved

Let \(H\) be a simple graph and \(n\) a natural number. The set of saturated edge counts of \(H\) on \(n\) vertices is the set of natural numbers \(m\) such that some \(H\)-saturated simple graph on the vertex set \(\{0, 1, \dots, n - 1\}\) has exactly \(m\) edges.

def satCounts (n : ℕ) : Set ℕ :=
  { m | ∃ G : SimpleGraph (Fin n), ∃ _ : DecidableRel G.Adj, H.IsSaturated G ∧
    G.edgeFinset.card = m }

Uses 1 · Used by 4

Statement uses\(H\)-saturated graphs

Used bySaturation number is attained by a saturated graph · Saturation number · The saturation number is zero when no saturated graph exists · Saturated graphs bound the saturation number

DefinitionSaturation number#✓fully proved

Let \(H\) be a simple graph and \(n\) a natural number. The saturation number \(\operatorname{sat}(n, H)\) is the minimum number of edges of an \(H\)-saturated simple graph on the vertex set \(\{0, 1, \dots, n - 1\}\), and is \(0\) when no such graph exists.

noncomputable def sat (n : ℕ) : ℕ :=
  sInf (H.satCounts n)

Uses 1 · Used by 3

Statement usesEdge counts of saturated graphs

Used bySaturation number is attained by a saturated graph · The saturation number is zero when no saturated graph exists · Saturated graphs bound the saturation number

TheoremThe saturation number is zero when no saturated graph exists#✓fully proved

Let \(H\) be a simple graph, \(n\) a natural number, and \(\operatorname{sat}(n, H)\) the saturation number of \(H\) on \(n\) vertices. If the set of saturated edge counts of \(H\) on \(n\) vertices is empty, that is, no \(H\)-saturated simple graph on the vertex set \(\{0, 1, \dots, n - 1\}\) exists, then \(\operatorname{sat}(n, H) = 0\).

theorem sat_eq_zero_of_counts_empty (n : ℕ) (h : H.satCounts n = ∅) : H.sat n = 0

Uses 2

Statement usesSaturation number · Edge counts of saturated graphs

TheoremSaturated graphs bound the saturation number#✓fully proved

Let \(H\) be a simple graph, \(n\) a natural number, and \(\operatorname{sat}(n, H)\) the saturation number of \(H\) on \(n\) vertices. Every \(H\)-saturated simple graph on the vertex set \(\{0, 1, \dots, n - 1\}\) has at least \(\operatorname{sat}(n, H)\) edges.

theorem sat_le_card_of_isSaturated (n : ℕ) (G : SimpleGraph (Fin n))
    [DecidableRel G.Adj] (h : H.IsSaturated G) :
    H.sat n ≤ G.edgeFinset.card

Uses 3

Statement uses\(H\)-saturated graphs · Saturation number

Proof usesEdge counts of saturated graphs

TheoremSaturation number is attained by a saturated graph#✓fully proved

Attainment: when a saturated graph exists, some saturated graph has exactly sat(n, H) edges.

theorem exists_isSaturated_card_eq_sat (n : ℕ) (h : (H.satCounts n).Nonempty) :
    ∃ G : SimpleGraph (Fin n), ∃ _ : DecidableRel G.Adj, H.IsSaturated G ∧
      G.edgeFinset.card = H.sat n

Uses 3

Statement uses\(H\)-saturated graphs · Saturation number · Edge counts of saturated graphs

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.