Unique subgraphs

DefinitionUnique subgraph#✓fully proved

Let \(G\) and \(H\) be graphs on the same vertex set \(V\). Then \(G\) is a unique subgraph of \(H\) if exactly one subgraph of \(H\) is isomorphic to \(G\). Here a subgraph of \(H\) means a spanning subgraph: a graph on \(V\) all of whose edges are edges of \(H\) (not necessarily induced).

def IsUniqueSubgraph (G H : SimpleGraph V) : Prop :=
  ∃! G' : SimpleGraph V, G' ≤ H ∧ Nonempty (G.Iso G')

Used by 1

Used byNumber of unique subgraphs

DefinitionNumber of unique subgraphs#✓fully proved

Let \(H\) be a graph on a finite vertex set \(V\). The number of unique subgraphs of \(H\) is the number of spanning subgraphs \(G\) of \(H\) (graphs on \(V\) all of whose edges are edges of \(H\)) that are unique subgraphs of \(H\), that is, isomorphic to no other spanning subgraph of \(H\).

Equivalently, it is the number of isomorphism classes of graphs on \(V\) that occur exactly once as a spanning subgraph of \(H\): sending each such \(G\) to its isomorphism class is a bijection onto these classes. In particular, isomorphic copies do not inflate the count: if two distinct spanning subgraphs of \(H\) are isomorphic, neither is a unique subgraph of \(H\), so neither is counted.

noncomputable def uniqueSubgraphCount [Finite V] (H : SimpleGraph V) : ℕ :=
  {G : SimpleGraph V | G ≤ H ∧ IsUniqueSubgraph G H}.ncard

Uses 1 · Used by 1

Statement usesUnique subgraph

Used byMany unique subgraphs (Erdős Problem 426)

DefinitionMany unique subgraphs (Erdős Problem 426)#✓fully proved

For a graph \(H\) on a finite vertex set, let \(u(H)\) be the number of spanning subgraphs of \(H\) that are isomorphic to no other spanning subgraph of \(H\) (its unique subgraphs). The statement is that there is a real constant \(c > 0\) such that for infinitely many \(n\) some graph \(H\) on \(n\) vertices has \(u(H) \ge c \cdot 2^{\binom{n}{2}} / n!\).

def conjecture : Prop :=
  ∃ c : ℝ, 0 < c ∧ ∃ᶠ (n : ℕ) in atTop, ∃ H : SimpleGraph (Fin n),
      c * ((2 : ℝ) ^ n.choose 2 / n.factorial) ≤ (uniqueSubgraphCount H : ℝ)

Uses 1 · Used by 2

Statement usesNumber of unique subgraphs

Used byErdős Problem 426 is false (Bradač–Christoph) · Negation of the Erdős Problem 426 statement

DefinitionNegation of the Erdős Problem 426 statement#✓fully proved

For a graph \(H\) on a finite vertex set, let \(u(H)\) be the number of spanning subgraphs of \(H\) that are isomorphic to no other spanning subgraph of \(H\). This is the proposition that there is no real constant \(c > 0\) such that for infinitely many \(n\) some graph \(H\) on \(n\) vertices has \(u(H) \ge c \cdot 2^{\binom{n}{2}} / n!\).

def disprovedForm : Prop := ¬ conjecture

Uses 1

Statement usesMany unique subgraphs (Erdős Problem 426)

TheoremErdős Problem 426 is false (Bradač–Christoph)#●ready to prove

For a graph \(H\) on a finite vertex set, let \(u(H)\) be the number of spanning subgraphs of \(H\) that are isomorphic to no other spanning subgraph of \(H\) (its unique subgraphs). There is no real constant \(c > 0\) such that for infinitely many \(n\) some graph \(H\) on \(n\) vertices has \(u(H) \ge c \cdot 2^{\binom{n}{2}} / n!\).

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• Bradač and Christoph [BrCh24] (f(n) = o(2^C(n,2)/n!)), per erdosproblems.com/426, https://www.erdosproblems.com/426.

Uses 1

Statement usesMany unique subgraphs (Erdős Problem 426)

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.