Countable colorings of linear graphs

Theorem. For every C, every C-linear graph has a proper coloring by ℕ.

Proof. Induct on #V; countable graphs are colored injectively. For uncountable V, take a chain. Each layer has fewer than #V vertices and induces a C-linear graph, so it is countably colorable by induction. Proposition L gives a law under which every vertex with infinite trace has trace energy at most C, and Proposition C splits the vertices into countably many classes within which any two signs agree with probability at least η > 0. Within a class, a vertex has only finitely many neighbours in earlier layers: they lie in its trace, which is finite or has energy at most C. Greedy coloring along the layers colors the edges between layers inside each class. The class, the greedy color and the color within the layer together color G.

theorem Erdos111.Linear.induce {V : Type u} {G : SimpleGraph V} {C : NNReal} (hG : Linear G C) (s : Set V) : Linear (SimpleGraph.induce s G) C

Induced subgraphs of a C-linear graph are C-linear.

theorem Erdos111.nonempty_coloring_of_traceBound {V : Type u} {G : SimpleGraph V} {C : NNReal} (c : Chain G) {ν : MeasureTheory.Measure (V → Bool)} [MeasureTheory.IsProbabilityMeasure ν] (hν : ∀ (v : V), (c.trace v).Infinite → TraceBound C ν v (c.trace v)) (hlayer : ∀ (ξ : Ordinal.{u}), Nonempty ((SimpleGraph.induce {v : V | c.layer v = ξ} G).Coloring ℕ)) : Nonempty (G.Coloring ℕ)

Lemma T: the trace bounds of one law and countable colorings of the layers give a countable coloring.

theorem Erdos111.nonempty_coloring_of_linear {V : Type u} (G : SimpleGraph V) {C : NNReal} (hG : Linear G C) : Nonempty (G.Coloring ℕ)

Every C-linear graph has a proper coloring by ℕ.