The limit law (Proposition L)

For a linear graph and a chain, there is one law of the signs under which every vertex with infinite trace has trace energy at most C.

Proof. By induction on ξ, there is a law satisfying J over every N ζ with ζ ≤ ξ and the trace bound at every vertex of layer below ξ with infinite trace. Any law satisfies J over N 0 = ∅. The successor step applies Lemma S to N ξ ⊆ N (ξ + 1); the new law has the old marginals on N ξ, which carry J over each earlier N ζ and the earlier trace bounds. At a limit, every condition is closed and finite-dimensional, and holds from some stage on, so a limit along an ultrafilter keeps them all; a pattern over the union has its finitely many roots in an earlier set. At (#V).ord every vertex has its layer below.

theorem Erdos111.exists_traceBound_law {V : Type u} {G : SimpleGraph V} {C : NNReal} (hG : Linear G C) (c : Chain G) : ∃ (ν : MeasureTheory.Measure (V → Bool)), MeasureTheory.IsProbabilityMeasure ν ∧ ∀ (v : V), (c.trace v).Infinite → TraceBound C ν v (c.trace v)

Proposition L: one law gives every vertex with infinite trace trace energy at most C.