Proof of `Splitting by a transversal gives a partition homogeneous modulo the pair relation`

groundedproofs/Lax185574Proofs/HomogeneousSplitting.lean · lax-185574

What this proof establishes

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

  • page 34 of this submission's paper

Description

As in the paper, for each pair of parts of 𝒬=đ’«âˆ§T𝒬 = đ’« ∧ T we find a flip of GG on these parts whose edges lie in RR. Then the pairs outside RR are non-edges of the flip, so they are all edges or all non-edges of GG. Two parts of 𝒬𝒬 inside one part XX of đ’«đ’«: by the diameter lemma, G[X]G[X] or áž [X] has diameter at most 33. In the first case every non-adjacent pair of XX is joined by a walk of length at most 44 between opposite copies in G[X,X]G[X, X] and by an edge in áž [X, X], so it lies in RR, and the second case is symmetric. Parts inside different parts XX, YY of đ’«đ’«: apply the bipartite flip lemma to G[X,Y]G[X, Y] with the representatives in TT. The parts of 𝒬𝒬 refine the four parts of that lemma, so the flip is constant on the pair.