Catalog.Sparsity.IterativeBipartiteRamsey
Lemma
Write \(R_d(t, m)\) for \(R(t, \ldots, t, m)\) where the first argument is repeated \(\binom{d-1}{2}\) times. Define \[R^{\star}(s, t, m) \coloneqq \begin{cases} t & \text{if } s = 0; \\ R_k(t, m) & \text{if } s \geq 1, \text{ where } k = R^{\star}(s - 1, t, m). \end{cases}\]
Let \(G\) be a bipartite graph with partitions \(A\) and \(B\). If \(|A| \geq R^{\star}(t, t, m)\), then at least one of the following assertions holds.
- \(A\) contains a set \(A' \subseteq A\) of size \(m\) and \(B\) contains a set \(S\) of size less than \(t\) such that no two vertices of \(A'\) have a common neighbor outside of \(S\);
- in \(G\) there is a \(1\)-subdivision of \(K_t\) with all principal vertices contained in \(A\);
- in \(G\) there is a complete bipartite subgraph \(K_{t,t}\).
Here \(R\) denotes the multicolor Ramsey number and the application of \(R_d\) within the definition of \(R^{\star}\) uses Lemma BipartiteRamsey.
Review notes
The source defines \(R^{\star}(s, t, m)\) as the iterated Ramsey function and states Lemma 3.10 with the bound \(|A| \geq R^{\star}(t, t, m)\). The Lean contract abstracts this into \(\exists N\) depending on \((m, t)\).
Outcome (a): common-neighbor separation.
Compared to Catalog.Sparsity.BipartiteRamsey outcome (a) (“no common
neighbor”), this adds a separator \(S \subseteq B\) with \(|S| < t\) such that no
two vertices of \(A'\) share a neighbor outside \(S\). This relaxation is
what makes the iterative version useful: we allow a bounded number of
“exceptional” common neighbors.
Outcome (c): complete bipartite subgraph. The source states “\(K_{t,t}\) subgraph.” We encode this as: \(\exists X \subseteq A, Y \subseteq B\) with \(|X|, |Y| \geq t\) and every vertex of \(X\) adjacent to every vertex of \(Y\).
Outcome (b): \(1\)-subdivision.
As in Catalog.Sparsity.BipartiteRamsey, the contract now uses an explicit
ShallowTopologicalMinorModel of
\(K_t = \texttt{SimpleGraph.completeGraph (Fin t)}\) at depth \(1\), together with
Set.range M.branchVertex ⊆ ↑A. This restores the actual source
content and is what Catalog.Sparsity.NDImpliesUQW needs in the even step.
The proof (Phase 4) is by iterated application of
Catalog.Sparsity.BipartiteRamsey, following the recursive definition of
\(R^{\star}\).
Catalog/Sparsity/IterativeBipartiteRamsey/Contract.lean (full)
| 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 |