Proof of `Splitting by a transversal gives a partition homogeneous modulo the pair relation`
groundedproofs/Lax185574Proofs/HomogeneousSplitting.lean · lax-185574
What this proof establishes
- lemâ
Lax185574.BipartiteFlip - lemâ
Lax185574.ComplementDiameter
Assuming the claims on the left, the claim on the right holds â checked by the archive's pipeline. Proof code is not displayed here.
In the paper
- page 34 of this submission's paper
Description
As in the paper, for each pair of parts of we find a flip of
on these parts whose edges lie in . Then the pairs outside
are non-edges of the flip, so they are all edges or all non-edges of
. Two parts of inside one part of : by the diameter lemma,
or áž [X] has diameter at most . In the first case every
non-adjacent pair of is joined by a walk of length at most
between opposite copies in and by an edge in áž [X, X], so it
lies in , and the second case is symmetric. Parts inside different
parts , of : apply the bipartite flip lemma to with
the representatives in . The parts of refine the four parts of
that lemma, so the flip is constant on the pair.