Proof of `Nowhere dense classes have subpolynomial weak coloring numbers`

groundedproofs/Lax12Proofs/NowhereDenseWcol.lean · lax-12

What this proof establishes

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Every nowhere dense graph class has subpolynomial weak coloring numbers: for every radius rr and every ε>0ε > 0 there is a constant cc such that every subgraph HH of a member, on mm vertices, satisfies wcolr(H)cmεwcol_r(H) ≤ c * m^ε.

Proof strategy

This is a glue proof: it assumes the four preceding statements of the submission and does nothing but compose them, so the proof network is visible on the archive rather than buried inside a single derivation.

Fix rr and εε, and set ε1=ε/(3r2+1)ε₁ = ε / (3r² + 1). Subpolynomial density, applied to the closure of the class under subgraph copies — which is nowhere dense whenever the class is — gives a constant cc bounding the edges of every depth-rr minor of a subgraph HH of a member by ck(1+ε1)c · k^(1+ε₁) in its own vertex count kk. Since a shallow minor has no more vertices than its host, kmk ≤ m, so that bound rewrites as the per-graph density bound d=cm1εd = ⌈c · m^ε₁⌉ for HH: k(1+ε1)=kk1εkm1εk^(1+ε₁) = k · k^ε₁ ≤ k · m^ε₁. A depth-rr topological minor is in particular a depth-rr minor, so dd bounds the topological density as well, and the admissibility bound yields admr+1(H)1+6(r+1)d3adm_{r+1}(H) ≤ 1 + 6(r+1)d³; admissibility is monotone in the radius, so the same bound holds at radius rr. The two coloring-number links then give wcolr(H)1+r(scolr(H)1)r1+r(admr(H)1)(r2)1+r(6(r+1)d3)(r2)wcol_r(H) ≤ 1 + r·(scol_r(H) - 1)^r ≤ 1 + r·(adm_r(H) - 1)^(r²) ≤ 1 + r·(6(r+1)d³)^(r²) — the arithmetic of Corollary 2.7 of the notes, which has no concept of its own.

What remains is real arithmetic. From d(c+1)m1εd ≤ (c+1)·m^ε₁ and ε13r2εε₁ · 3r² ≤ ε one gets d(3r2)(c+1)(3r2)mεd^(3r²) ≤ (c+1)^(3r²) · m^ε, so wcolr(H)1+Kmε(K+1)mεwcol_r(H) ≤ 1 + K·m^ε ≤ (K+1)·m^ε with K=r(6(r+1))(r2)(c+1)(3r2)K = r·(6(r+1))^(r²)·(c+1)^(3r²), using mε1m^ε ≥ 1. The degenerate case m=0m = 0 is separate: there wcolr(H)=0wcol_r(H) = 0 and mε=0m^ε = 0.

Attribution

The statement is Theorem 3.4 of Chapter 2 of the sparsity lecture notes of Pilipczuk and Siebertz (numbering of the 2019/20 edition). The composition reproduces that derivation at the level of the submitted concepts.