Catalog/Sparsity/IterativeBipartiteRamsey/Contract.lean
| 1 | import Catalog.Sparsity.BipartiteRamsey.Contract |
| 2 | import Catalog.Sparsity.ShallowTopologicalMinor.Contract |
| 3 | |
| 4 | namespace Catalog.Sparsity.IterativeBipartiteRamsey |
| 5 | |
| 6 | open Catalog.Sparsity.ShallowTopologicalMinor |
| 7 | |
| 8 | /-- Lemma 3.10: iterative version of bipartite Ramsey. In a bipartite graph with |
| 9 | sides `A` and `B`, if `|A|` is large enough, then at least one of: |
| 10 | (a) `A` contains `m` vertices and `B` contains a small separator `S` of size |
| 11 | `< t` such that no two vertices of `A'` have a common neighbor outside `S`, |
| 12 | (b) `G` contains a `1`-subdivision of `K_t` with principal vertices in `A`, |
| 13 | (c) `G` contains a complete bipartite subgraph `K_{t,t}`. -/ |
| 14 | axiom iterativeBipartiteRamsey (m t : ℕ) : |
| 15 | ∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V] |
| 16 | (G : SimpleGraph V) [DecidableRel G.Adj] |
| 17 | (A B : Finset V), |
| 18 | Disjoint A B → |
| 19 | (∀ u v, G.Adj u v → (u ∈ A ∧ v ∈ B) ∨ (u ∈ B ∧ v ∈ A)) → |
| 20 | N ≤ A.card → |
| 21 | (∃ (A' : Finset V) (S : Finset V), |
| 22 | A' ⊆ A ∧ S ⊆ B ∧ m ≤ A'.card ∧ S.card < t ∧ |
| 23 | (↑A' : Set V).Pairwise (fun u v => |
| 24 | ∀ w, w ∉ (S : Set V) → ¬(G.Adj u w ∧ G.Adj v w))) ∨ |
| 25 | (∃ M : ShallowTopologicalMinorModel |
| 26 | (SimpleGraph.completeGraph (Fin t)) G 1, |
| 27 | Set.range M.branchVertex ⊆ ↑A) ∨ |
| 28 | (∃ (X : Finset V) (Y : Finset V), |
| 29 | X ⊆ A ∧ Y ⊆ B ∧ t ≤ X.card ∧ t ≤ Y.card ∧ |
| 30 | ∀ x ∈ X, ∀ y ∈ Y, G.Adj x y) |
| 31 | |
| 32 | end Catalog.Sparsity.IterativeBipartiteRamsey |
| 33 |