A counterexample to the Erdős--Simonovits compactness conjecture

This file constructs a finite family of connected bipartite cyclic graphs whose family extremal number grows strictly more slowly than that of every member.

structure CompactnessConjecture.FiniteGraph : Type

A finite simple graph packaged with its vertex count.

• order : ℕ

  The number of vertices.

• graph : SimpleGraph (Fin self.order)

  The graph on the standard finite vertex type.

def CompactnessConjecture.FamilyFree (family : Finset FiniteGraph) {n : ℕ} (host : SimpleGraph (Fin n)) : Prop

A host graph contains no member of the forbidden family.

Equations

• CompactnessConjecture.FamilyFree family host = ∀ forbidden ∈ family, forbidden.graph.Free host

noncomputable def CompactnessConjecture.familyExtremal (family : Finset FiniteGraph) (n : ℕ) : ℕ

The maximum edge count of a host avoiding every member of a finite family.

Equations

• CompactnessConjecture.familyExtremal family n = (Finset.filter (CompactnessConjecture.FamilyFree family) Finset.univ).sup fun (host : SimpleGraph (Fin n)) => host.edgeFinset.card

def CompactnessConjecture.IsCompactFamily (family : Finset FiniteGraph) : Prop

The extremal function of one member controls that of the whole family.

Equations

• One or more equations did not get rendered due to their size.

def CompactnessConjecture.CompactnessConjectureStatement : Prop

The Erdős--Simonovits compactness conjecture.

Equations

• One or more equations did not get rendered due to their size.

theorem CompactnessConjecture.free_map_of_no_isolated {U : Type u_1} {V : Type u_2} {W : Type u_3} (forbidden : SimpleGraph U) (hneighbors : ∀ (u : U), ∃ (v : U), forbidden.Adj u v) {host : SimpleGraph V} (embedding : V ↪ W) (hfree : forbidden.Free host) : forbidden.Free (SimpleGraph.map (⇑embedding) host)

Mapping a free graph along an embedding preserves freeness when the forbidden graph has no isolated vertices.

theorem CompactnessConjecture.extremalNumber_monotone_of_no_isolated {U : Type u_1} (forbidden : SimpleGraph U) (hneighbors : ∀ (u : U), ∃ (v : U), forbidden.Adj u v) {m n : ℕ} (hmn : m ≤ n) : SimpleGraph.extremalNumber m forbidden ≤ SimpleGraph.extremalNumber n forbidden

The extremal number of a graph without isolated vertices is monotone in the host order.

def CompactnessConjecture.UniformMemberLower (family : Finset FiniteGraph) (c : ℝ) : Prop

Every member of a forbidden family has a uniform extremal-number lower bound.

Equations

• One or more equations did not get rendered due to their size.

theorem CompactnessConjecture.quantitativeCompactnessCounterexample : ∃ (family : Finset FiniteGraph) (c : ℝ) (C : ℝ), family.Nonempty ∧ (∀ forbidden ∈ family, forbidden.graph.Connected ∧ forbidden.graph.IsBipartite ∧ ¬forbidden.graph.IsAcyclic) ∧ 0 < c ∧ 0 < C ∧ UniformMemberLower family c ∧ (∀ (n : ℕ) (host : SimpleGraph (Fin n)), FamilyFree family host → ↑host.edgeFinset.card ^ 16 ≤ C * ↑n ^ 21) ∧ (∀ (n : ℕ), ↑(familyExtremal family n) ^ 16 ≤ C * ↑n ^ 21) ∧ 0 < 1 / 48 ∧ 21 / 16 = 4 / 3 - 1 / 48 ∧ ¬IsCompactFamily family ∧ ¬CompactnessConjectureStatement

A quantitative counterexample to the Erdős--Simonovits compactness conjecture.