Proof of `Weakly sparse monadically dependent classes are nowhere dense`
groundedproofs/Lax5Proofs/Corollary6a.lean · lax-5
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.
Description
Every weakly sparse monadically dependent graph class is nowhere dense: Corollary 6a of Dreier, Mählmann, McCarty, Pilipczuk and Toruńczyk, by way of Lemma 13.7 of Mählmann's thesis.
Proof strategy
Suppose is weakly sparse and monadically dependent but not nowhere dense. Passing to the closure of the class under graph copies and to the shallow-minor formulation, some radius admits -subdivided cliques of every order as subgraphs of members. At these are cliques, which contain large bicliques, contradicting weak sparseness. At a subdivided clique contains a subdivided biclique of half the order, and the Ramsey-theoretic extraction of Lemma 13.8 of Mählmann's thesis turns those into either large bicliques — again contradicting weak sparseness — or induced -subdivided bicliques with . A pigeonhole fixes one occurring at unbounded orders, and the star-crossing transduction then transduces all graphs from , contradicting monadic dependence.
The two Ramsey inputs are assumed from the Finite Ramsey submission rather than reproved: the monochromatic-subset extraction inside the nowhere-dense bridge is the multicolour Ramsey statement, and the order-type homogeneity behind Lemma 13.8 is the tuple Ramsey statement.
Attribution
Corollary 6a of Dreier, Mählmann, McCarty, Pilipczuk and Toruńczyk, Neighborhood Complexity and Radius-1 Merge-Width in Monadically Dependent Graph Classes (2026). The argument is Lemma 13.7 of Mählmann's thesis, through its Lemma 13.8, with the forbidden-pattern endpoint replaced by a transduction of all graphs.