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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Numerical classification after a realizable representative replacement. The graph endpoint restrictions are proved separately from this arithmetic.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_classification_weights line 14
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.assignedCount_add_chains_length line 48
  3. theorem OAI.CycleClique.Construction.ExpandedPathSystem.matching_of_incident_eq_twice line 56
  4. theorem OAI.CycleClique.Construction.ExpandedPathSystem.two_chains_of_terminal_two line 100