Dev/MonadicDependence/SubdividedBicliqueRamsey/Contract.lean
| 1 | import Mathlib.Combinatorics.SimpleGraph.Copy |
| 2 | import Mathlib.Order.Monotone.Basic |
| 3 | import Catalog.Sparsity.Preliminaries.Contract |
| 4 | import Dev.MonadicDependence.Biclique.Contract |
| 5 | import Dev.MonadicDependence.Subdivision.Contract |
| 6 | |
| 7 | namespace Dev.MonadicDependence.SubdividedBicliqueRamsey |
| 8 | |
| 9 | open Dev.MonadicDependence.Biclique |
| 10 | open Dev.MonadicDependence.Subdivision |
| 11 | |
| 12 | /-- Mählmann Lemma 13.8. For every `r : ℕ` there is a monotone, |
| 13 | unbounded function `U : ℕ → ℕ` (depending only on `r`) such that for |
| 14 | every graph `G` and every `n`, if `G` contains the `r`-subdivided |
| 15 | biclique of order `n` as a subgraph, then at least one of: |
| 16 | |
| 17 | * `G` contains the biclique of order `U n` as a subgraph, or |
| 18 | * there exists `r' ∈ [r]` (i.e. `1 ≤ r' ≤ r`) such that `G` contains |
| 19 | the `r'`-subdivided biclique of order `U n` as an induced subgraph. -/ |
| 20 | axiom subdividedBicliqueRamsey (r : ℕ) : |
| 21 | ∃ U : ℕ → ℕ, Monotone U ∧ (∀ N : ℕ, ∃ n : ℕ, N ≤ U n) ∧ |
| 22 | ∀ {V : Type} [DecidableEq V] [Fintype V] |
| 23 | (G : SimpleGraph V) (n : ℕ), |
| 24 | (subdividedBiclique n r).IsContained G → |
| 25 | (biclique (U n)).IsContained G ∨ |
| 26 | ∃ r' : ℕ, 1 ≤ r' ∧ r' ≤ r ∧ |
| 27 | (subdividedBiclique (U n) r').IsIndContained G |
| 28 | |
| 29 | end Dev.MonadicDependence.SubdividedBicliqueRamsey |
| 30 |