Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `Simultaneous thinning of a semisparse blockade`

groundedproofs/Lax57Proofs/BlockadeThinning.lean · lax-57

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

Description

Select tt vertices from each block in index order. Integer Markov bounds control all pairs involving earlier samples and later blocks. Delete from each sample the vertices whose degree to another sample exceeds t/(2E)t/(2E). The hypothesis P128k3EP\geq 128k^3E ensures that at least half of every sample remains, and the surviving noncomplete pairs are 1/E1/E-sparse in both directions.