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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Realize numerical canonical profiles by independently orienting and reordering the actual chains, preserving the full raw vertex set.

  1. def OAI.CycleClique.Construction.ChainOrientation line 14
  2. theorem OAI.CycleClique.Construction.chainOrientations_flatten line 16
  3. theorem OAI.CycleClique.Construction.chainOrientations_source line 25
  4. theorem OAI.CycleClique.Construction.orient_chain_profiles line 37
  5. def OAI.CycleClique.Construction.RawPathSystem.reorient line 57
  6. theorem OAI.CycleClique.Construction.RawPathSystem.reorient_vertices line 84
  7. theorem OAI.CycleClique.Construction.RawPathSystem.reorient_amount line 90
  8. theorem OAI.CycleClique.Construction.RawPathSystem.reorient_assignedCount line 95
  9. theorem OAI.CycleClique.Construction.RawPathSystem.canonical_profile line 108