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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The complete main formula for cycle length at least nineteen, conditional on the precisely stated published Hamiltonicity input. No finite search is needed in this range.

  1. theorem OAI.CycleClique.Construction.no_expanded_largeCycle_counterexample line 15
  2. theorem OAI.CycleClique.Construction.cycle_clique_large_upper line 33
  3. theorem OAI.CycleClique.Construction.cycle_clique_ge_nineteen line 41