Catalog.Sparsity.BipartiteRamsey
Lemma
Let \(G\) be a bipartite graph with sides \(A\) and \(B\). Let \(m, t, d \in \mathbb{N}\). If \(|A| \geq R(t, \ldots, t, m)\), where \(t\) is repeated \(\binom{d-1}{2}\) times, then at least one of the following assertions holds.
- \(A\) contains a set \(A' \subseteq A\) of size \(m\) such that no two vertices of \(A'\) have a common neighbor;
- in \(G\) there is a \(1\)-subdivision of \(K_t\) with all principal vertices contained in \(A\); or
- \(B\) contains a vertex of degree at least \(d\).
Review notes
The source states Lemma 3.9 with the explicit bound \(|A| \geq R(t, \ldots, t, m)\) where \(t\) is repeated \(\binom{d-1}{2}\) times. The Lean contract abstracts this into an existential \(\exists N\) depending on \((m, t, d)\). The specific Ramsey bound is internal to the proof.
Bipartite encoding. The bipartite structure is encoded as:
Disjoint A B: the two sides are disjoint.- The bipartite condition: every edge has one endpoint in \(A\) and the other in \(B\).
Outcome (a): no common neighbor.
(↑A’ : Set V).Pairwise (fun u v => ∀ w, ¬(G.Adj u w ∧ G.Adj v w))
states that no two vertices of \(A'\) share a neighbor. This is equivalent to
distance-\(2\) independence when \(A'\) is an independent set (which it is, being a
subset of one side of a bipartite graph).
Outcome (b): \(1\)-subdivision of \(K_t\).
The Lean contract now exposes outcome (b) as an explicit
ShallowTopologicalMinorModel of
\(K_t = \texttt{SimpleGraph.completeGraph (Fin t)}\) at depth \(1\), together with
Set.range M.branchVertex ⊆ ↑A. This is the mathematically correct
formal analogue of a \(1\)-subdivision with all principal vertices in \(A\) and is
the shape needed downstream in Catalog.Sparsity.NDImpliesUQW.
Outcome (c): high-degree vertex.
A vertex in \(B\) with at least \(d\) neighbors in \(A\):
d ≤ (G.neighborFinset v ∩ A).card.
Catalog/Sparsity/BipartiteRamsey/Contract.lean (full)
| 1 | import Mathlib.Combinatorics.SimpleGraph.Clique |
| 2 | import Catalog.Sparsity.ShallowTopologicalMinor.Contract |
| 3 | |
| 4 | namespace Catalog.Sparsity.BipartiteRamsey |
| 5 | |
| 6 | open Catalog.Sparsity.ShallowTopologicalMinor |
| 7 | |
| 8 | /-- Lemma 3.9: in a bipartite graph with sides `A` and `B`, if `|A|` is large |
| 9 | enough (as a function of `m`, `t`, `d`), then at least one of the following |
| 10 | holds: |
| 11 | (a) `A` contains `m` vertices with no common neighbor, |
| 12 | (b) `G` contains a `1`-subdivision of `K_t` with principal vertices in `A`, |
| 13 | (c) `B` contains a vertex of degree at least `d`. -/ |
| 14 | axiom bipartiteRamsey (m t d : ℕ) : |
| 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, A' ⊆ A ∧ m ≤ A'.card ∧ |
| 22 | (↑A' : Set V).Pairwise (fun u v => |
| 23 | ∀ w, ¬(G.Adj u w ∧ G.Adj v w))) ∨ |
| 24 | (∃ M : ShallowTopologicalMinorModel |
| 25 | (SimpleGraph.completeGraph (Fin t)) G 1, |
| 26 | Set.range M.branchVertex ⊆ ↑A) ∨ |
| 27 | (∃ v ∈ B, d ≤ (G.neighborFinset v ∩ A).card) |
| 28 | |
| 29 | end Catalog.Sparsity.BipartiteRamsey |
| 30 |