Dev.MonadicDependence.Biclique
Definition
The biclique of order \(k\) is the complete bipartite graph \(K_{k,k}\): the bipartite graph with sides \(a_1, \ldots, a_k\) and \(b_1, \ldots, b_k\), where \(a_i\) and \(b_j\) are adjacent for all \(i, j \in [k]\).
Let \(G\) be a graph and \(k \in \mathbb{N}\). We say that \(G\) contains the biclique of order \(k\) as a subgraph if there exist pairwise distinct vertices \(a_1, \ldots, a_k, b_1, \ldots, b_k \in V(G)\) such that \(a_i b_j \in E(G)\) for all \(i, j \in [k]\). No conditions are imposed on the remaining adjacencies between these vertices.
Review notes
The thesis does not give a standalone definition of “biclique”. We introduce one here because the term is used in the definition of weakly sparse (Definition WeaklySparse) and in Lemma SubdividedBicliqueRamsey (Mählmann’s Lemma 13.8) without further explanation. Our reading follows Mählmann’s convention on p. 22: the biclique of order \(k\) is \(K_{k,k}\) with explicitly labelled sides of size \(k\) each, not \(K_{k}\)’s bipartite complement or any other bipartite variant.
We define “contains as a subgraph” in the standard sense: existence of \(2k\) distinct vertices forming the required bipartite edge pattern, with no constraint on edges between the \(a_i\), between the \(b_j\), or with the rest of \(G\). This matches Mählmann’s usage in Definition 13.5 and throughout Chapter 13.
Lean encoding. biclique k is an abbrev for
Mathlib’s completeBipartiteGraph (Fin k) (Fin k) on the
vertex type Fin k ⊕ Fin k. “Contains as a subgraph” is
SimpleGraph.IsContained (Mathlib; scoped notation
⊑): existence of an injective graph homomorphism
biclique k →g G. Mathlib supplies the finset-level
characterization completeBipartiteGraph_isContained_iff,
useful downstream in Phase 3.
Dev/MonadicDependence/Biclique/Contract.lean (full)
| 1 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 2 | |
| 3 | namespace Dev.MonadicDependence.Biclique |
| 4 | |
| 5 | /-- The biclique of order `k` is the complete bipartite graph `K_{k,k}` |
| 6 | on vertex set `Fin k ⊕ Fin k`: sides `a_1,…,a_k` (the `Sum.inl i`) and |
| 7 | `b_1,…,b_k` (the `Sum.inr j`), with `a_i` adjacent to `b_j` for all |
| 8 | `i, j ∈ Fin k`. |
| 9 | |
| 10 | "`G` contains the biclique of order `k` as a subgraph" (Mählmann, p. 22; |
| 11 | see `statement.tex`) is `(biclique k).IsContained G` — i.e., an injective |
| 12 | graph homomorphism `biclique k →g G`, equivalently `2k` distinct vertices |
| 13 | of `G` forming the bipartite edge pattern, with no constraint on other |
| 14 | adjacencies. Mathlib exposes this relation via the scoped notation |
| 15 | `biclique k ⊑ G` and supplies `completeBipartiteGraph_isContained_iff` |
| 16 | for a finset-level characterization. -/ |
| 17 | abbrev biclique (k : ℕ) : SimpleGraph (Fin k ⊕ Fin k) := |
| 18 | completeBipartiteGraph (Fin k) (Fin k) |
| 19 | |
| 20 | end Dev.MonadicDependence.Biclique |
| 21 |