OriginalCoarsePackets.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Cell-dependent packets retain original fine tubes, and both their total size and their common coarse cover are bounded by the original configuration.