Catalog/Sparsity/OddStepReduction/Contract.lean
| 1 | import Catalog.Sparsity.ShallowMinor.Contract |
| 2 | import Catalog.Sparsity.UniformQuasiWideness.Contract |
| 3 | |
| 4 | namespace Catalog.Sparsity.OddStepReduction |
| 5 | |
| 6 | open Catalog.Sparsity.ShallowMinor Catalog.Sparsity.UniformQuasiWideness |
| 7 | |
| 8 | /-- Lemma 3.5 (consequence form): given a distance-`2j` independent set `A` in |
| 9 | `G`, there exists a depth-`j` minor `H` of `G` such that any independent |
| 10 | set of size `m` in `H` lifts to a distance-`(2j+1)` independent subset of |
| 11 | `A` of the same size. |
| 12 | |
| 13 | The full statement is an iff (distance-`(2j+1)` independence in `G` ↔ |
| 14 | distance-`1` independence in `H`), but the consequence form suffices for |
| 15 | the densification argument. -/ |
| 16 | axiom oddStepReduction {V : Type} [DecidableEq V] [Fintype V] |
| 17 | (G : SimpleGraph V) (j : ℕ) (A : Finset V) |
| 18 | (hA : DistIndependent G (2 * j) ↑A) : |
| 19 | ∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W) (H : SimpleGraph W), |
| 20 | IsShallowMinor H G j ∧ |
| 21 | A.card ≤ Fintype.card W ∧ |
| 22 | (∀ m : ℕ, (∃ B : Finset W, m ≤ B.card ∧ DistIndependent H 1 ↑B) → |
| 23 | ∃ B' : Finset V, ↑B' ⊆ ↑A ∧ m ≤ B'.card ∧ |
| 24 | DistIndependent G (2 * j + 1) ↑B') |
| 25 | |
| 26 | end Catalog.Sparsity.OddStepReduction |
| 27 |