Proof of `Splitting by a transversal keeps few parts in flip-metric balls`

groundedproofs/Lax185574Proofs/SplitBalls.lean · lax-185574

What this proof establishes

no assumptions

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 32 of this submission's paper

Description

Let BB be the radius-rr ball and B′B' the radius-(r+1)(r+1) ball of the 𝒬𝒬-flip metric around vv, and T′=T∩B′T' = T ∩ B'. The transversal has one vertex in each part of 𝒫𝒫, so ∣T′∣≤∣B′/𝒫∣≤k|T'| ≤ |B'/𝒫| ≤ k. Take u∈Bu ∈ B and t∈T∖B′t ∈ T ∖ B'. Some 𝒬𝒬-flip HH has no short walk from vv to tt, so uu and tt are distinct and non-adjacent in HH. Hence the adjacency of tt in GG is the same for all vertices of BB in the part 𝒬(u)𝒬(u), which contains 𝒫(u)𝒫(u). So the part of uu in 𝒫∧T𝒫 ∧ T is determined by its part in 𝒫𝒫 and its trace on T′T'. There are at most kk parts of 𝒫𝒫 meeting BB, and at most πG(k)π_G(k) traces on T′T'.