Catalog.Sparsity.EvenStepReduction
Lemma
Let \(A\) be a distance-\((2j+1)\) independent set in \(G\). Let \(H \preccurlyeq_j G\) be the depth-\(j\) minor (Definition ShallowMinor) of \(G\) obtained by contracting the disjoint distance-\(j\) neighborhoods \(N_j^G[v]\) for \(v \in A\) to single vertices. Identify the vertex of \(H\) resulting from contracting \(N_j^G[v]\) with the original vertex \(v\) of \(G\), so that \(A\) is a subset of vertices of both \(G\) and \(H\). Then, for any \(S \subseteq V(H) - A = V(G) - \bigcup_{v \in A} N_j(v)\), a subset of \(A\) is distance-\((2j+2)\) independent in \(G - S\) if and only if it is distance-\(2\) independent in \(H - S\).
Review notes
The source states Lemma 3.6 as an iff: for a distance-\((2j+1)\) independent set \(A\) in \(G\), contracting distance-\(j\) neighborhoods gives a depth-\(j\) minor \(H\) such that for any \(S \subseteq V(H) - A\), a subset of \(A\) is distance-\((2j+2)\) independent in \(G - S\) iff it is distance-\(2\) independent in \(H - S\).
The Lean contract uses a consequence form and adds an explicit AW : Finset W representing the image of \(A\) in \(W = V(H)\). Three additional
conditions beyond the original statement:
Disjoint S AW– matches the source restriction \(S \subseteq V(H) \setminus A\).B\(\subseteq\)AW– matches the source biconditional being about subsets of \(A\).(\(\uparrow\)AW).Pairwise (\(\lambda\)u v\(\Rightarrow\)H.Adj u v)– \(A\)-vertices are independent in \(H\), needed by the downstream bipartite construction.
These restrictions are necessary for the lifting proof and are satisfied by the downstream use in NDImpliesUQW (the bipartite Ramsey produces \(S\) from the non-\(A\) side and the independent set from the \(A\) side).
The separator \(S'\) in \(G\) is the image of \(S\) under Subtype.val and
satisfies \(|S'| = |S|\).
Catalog/Sparsity/EvenStepReduction/Contract.lean (full)
| 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 |