Reduction of Erdős Problem 111 to countable colorings of linear graphs

• Countable deletion. If removing a countable set leaves a countably colorable graph, the graph is countably colorable: give the removed vertices fresh colors.
• Packing. Uncountably many pairwise disjoint finite witnesses with cost above 2 K per vertex include infinitely many with the same size v and cost b, since these are natural numbers. Then ⌊n / v⌋ of them, padded to n vertices, cost at least b ⌊n / v⌋ > K n for n ≥ 2 v.
• The limit. If G is not countably colorable, fix K and take a maximal family of pairwise disjoint witnesses. If it were countable, the remainder would be 2 K-linear by maximality, hence countably colorable, and so would G. So it is uncountable, and packing gives h G n > K n for all large n.

theorem Erdos111.nonempty_coloring_of_countable_compl {V : Type u} {G : SimpleGraph V} {S : Set V} (hS : S.Countable) (h : Nonempty ((SimpleGraph.induce Sᶜ G).Coloring ℕ)) : Nonempty (G.Coloring ℕ)

Countable deletion.

theorem Erdos111.eventually_lt_h_of_uncountable {V : Type u} {G : SimpleGraph V} {ι : Type u_1} [Uncountable ι] (K : ℝ) (s : ι → Finset V) (E : ι → Finset (Sym2 V)) (hdisj : Pairwise fun (i j : ι) => Disjoint (s i) (s j)) (hE : ∀ (i : ι), ↑(E i) ⊆ G.edgeSet) (hEs : ∀ (i : ι), ∀ e ∈ E i, ∀ v ∈ e, v ∈ s i) (hcost : ∀ (i : ι), 2 * K * ↑(s i).card < ↑(edgeCost (E i))) : ∀ᶠ (n : ℕ) in Filter.atTop, K * ↑n < ↑(h G n)

Packing.

theorem Erdos111.tendsto_of_isEmpty_coloring {V : Type u} (hmain : ∀ (W : Type u) (H : SimpleGraph W) (C : NNReal), Linear H C → Nonempty (H.Coloring ℕ)) (G : SimpleGraph V) (hG : IsEmpty (G.Coloring ℕ)) : Filter.Tendsto (fun (n : ℕ) => ↑(h G n) / ↑n) Filter.atTop Filter.atTop

If every linear graph is countably colorable, then h G n / n → ∞ for every graph G that is not countably colorable.

theorem Erdos111.isEmpty_coloring_of_chromaticCardinal {V : Type u} {G : SimpleGraph V} (hG : chromaticCardinal G = Cardinal.aleph 1) : IsEmpty (G.Coloring ℕ)

A graph of chromatic number ℵ₁ is not countably colorable.