OAI/Combinatorics/Ramsey/CycleClique/Construction/RepresentativePacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two nonclique first balls improve the separated packing from 2t to 2t+2, finishing the parity boundary once the path-system exclusions apply.

  1. theorem OAI.CycleClique.Construction.exists_short_path_of_two_noncliques line 13