ComplexGraphUpper.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The complete uncut complex graph is small: the retained graph and the two endpoint deletion errors share the same exponential saving.