Catalog.Sparsity.UQWImpliesND
Lemma
If a class \(\mathcal{C}\) is uniformly quasi-wide (Definition UniformQuasiWideness), then \(\mathcal{C}\) is nowhere dense (Definition NowhereDense).
Review notes
The Lean statement directly mirrors the source: uniformly quasi-wide implies nowhere dense. No reformulation is needed.
The proof (Phase 4) argues by contraposition: if \(K_t \preccurlyeq_{2r+1} G\)
for arbitrarily large \(t\), then \(G\) contains arbitrarily large sets whose
pairwise distances are at most \(2(2r+1) + 1\), contradicting uniform
quasi-wideness. The proof imports Catalog.Sparsity.ShallowMinor as a
proof_dep for the shallow-minor machinery.
Catalog/Sparsity/UQWImpliesND/Contract.lean (full)
| 1 | import Catalog.Sparsity.Preliminaries.Contract |
| 2 | import Catalog.Sparsity.UniformQuasiWideness.Contract |
| 3 | import Catalog.Sparsity.NowhereDense.Contract |
| 4 | |
| 5 | namespace Catalog.Sparsity.UQWImpliesND |
| 6 | |
| 7 | open Catalog.Sparsity.Preliminaries Catalog.Sparsity.NowhereDense Catalog.Sparsity.UniformQuasiWideness |
| 8 | |
| 9 | /-- Lemma 3.3: if a class `C` is uniformly quasi-wide, then `C` is nowhere |
| 10 | dense. -/ |
| 11 | axiom uqw_implies_nd (C : GraphClass) : |
| 12 | UniformlyQuasiWide C → IsNowhereDense C |
| 13 | |
| 14 | end Catalog.Sparsity.UQWImpliesND |
| 15 |