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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

After the proved large-clique contradiction, every remaining expanded counterexample lies in the finite parameter range used by the certificates.

  1. theorem OAI.CycleClique.Construction.finite_range_clique_bounds line 12