Catalog/Sparsity/EvenStepReduction/Contract.lean
| 1 | import Catalog.Sparsity.ShallowMinor.Contract |
| 2 | import Catalog.Sparsity.UniformQuasiWideness.Contract |
| 3 | |
| 4 | namespace Catalog.Sparsity.EvenStepReduction |
| 5 | |
| 6 | open Catalog.Sparsity.ShallowMinor Catalog.Sparsity.UniformQuasiWideness |
| 7 | |
| 8 | /-- Lemma 3.6 (consequence form): given a distance-`(2j+1)` independent set `A` |
| 9 | in `G`, there exists a depth-`j` minor `H` of `G` with a distinguished |
| 10 | independent set `AW` (the image of `A` in `H`) such that for any separator |
| 11 | `S` disjoint from `AW`, distance-`2` independence of a subset of `AW` in |
| 12 | `H - S` lifts to distance-`(2(j+1))` independence of a subset of `A` in |
| 13 | `G - S'` with `|S'| ≤ |S|`. |
| 14 | |
| 15 | The source states an iff for subsets of `A` with `S ⊆ V(H) \ A`; the |
| 16 | consequence form suffices for the densification argument. -/ |
| 17 | axiom evenStepReduction {V : Type} [DecidableEq V] [Fintype V] |
| 18 | (G : SimpleGraph V) (j : ℕ) (A : Finset V) |
| 19 | (hA : DistIndependent G (2 * j + 1) ↑A) : |
| 20 | ∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W) (H : SimpleGraph W) |
| 21 | (AW : Finset W), |
| 22 | IsShallowMinor H G j ∧ |
| 23 | A.card ≤ AW.card ∧ |
| 24 | (↑AW : Set W).Pairwise (fun u v => ¬H.Adj u v) ∧ |
| 25 | (∀ (S : Finset W) (m : ℕ), |
| 26 | Disjoint S AW → |
| 27 | (∃ B : Finset W, B ⊆ AW ∧ m ≤ B.card ∧ |
| 28 | DistIndependent (deleteVerts H ↑S) 2 ↑B) → |
| 29 | ∃ (S' : Finset V) (B' : Finset V), |
| 30 | S'.card ≤ S.card ∧ ↑B' ⊆ ↑A ∧ Disjoint B' S' ∧ m ≤ B'.card ∧ |
| 31 | DistIndependent (deleteVerts G ↑S') (2 * (j + 1)) ↑B') |
| 32 | |
| 33 | end Catalog.Sparsity.EvenStepReduction |
| 34 |