Catalog.Sparsity.NDImpliesUQW
Lemma
If a class \(\mathcal{C}\) is nowhere dense (Definition NowhereDense), then \(\mathcal{C}\) is uniformly quasi-wide (Definition UniformQuasiWideness).
Review notes
The Lean statement directly mirrors the source: nowhere dense implies uniformly quasi-wide. This is the hard direction of the equivalence (Theorem 3.2).
The proof (Phase 4) constructs for each radius \(r\) a threshold function
\(N_r(m)\) and separator bound \(s_r\) via a backward induction on \(i = r, r-1,
\ldots, 1, 0\), alternating between odd steps (applying Ramsey’s theorem via
Catalog.Sparsity.OddStepReduction) and even steps (applying the iterative
bipartite Ramsey lemma via Catalog.Sparsity.EvenStepReduction).
The proof_deps are:
Catalog.Sparsity.OddStepReduction— odd-step neighborhood contractionCatalog.Sparsity.EvenStepReduction— even-step neighborhood contractionCatalog.Sparsity.IterativeBipartiteRamsey— bipartite Ramsey with separatorCatalog.Sparsity.Ramsey— two-color Ramsey for the base case
Catalog/Sparsity/NDImpliesUQW/Contract.lean (full)
| 1 | import Catalog.Sparsity.Preliminaries.Contract |
| 2 | import Catalog.Sparsity.NowhereDense.Contract |
| 3 | import Catalog.Sparsity.UniformQuasiWideness.Contract |
| 4 | |
| 5 | namespace Catalog.Sparsity.NDImpliesUQW |
| 6 | |
| 7 | open Catalog.Sparsity.Preliminaries Catalog.Sparsity.NowhereDense Catalog.Sparsity.UniformQuasiWideness |
| 8 | |
| 9 | /-- Lemma 3.4: if a class `C` is nowhere dense, then `C` is uniformly |
| 10 | quasi-wide. -/ |
| 11 | axiom nd_implies_uqw (C : GraphClass) : |
| 12 | IsNowhereDense C → UniformlyQuasiWide C |
| 13 | |
| 14 | end Catalog.Sparsity.NDImpliesUQW |
| 15 |
Dependencies
Statement