GraphCylinderCover.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Turn a countable base-ball cover of a scalar level slab into an explicit small-diameter graph cover, retaining the quadratic cost.