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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A required-path certificate is simply a finite simple path. Its complementary outside parameter is forbidden by the exact cycle length.

  1. structure OAI.CycleClique.Construction.RequiredPathData line 9
  2. def OAI.CycleClique.Construction.RequiredPathData.support line 19
  3. def OAI.CycleClique.Construction.RequiredPathData.parameter line 21
  4. def OAI.CycleClique.Construction.RequiredPathData.Check line 23
  5. instance OAI.CycleClique.Construction.RequiredPathData.(instance at line 26) line 26
  6. theorem OAI.CycleClique.Construction.RequiredPathData.forbids line 32
  7. def OAI.CycleClique.Construction.requiredEntryMatrix line 53
  8. def OAI.CycleClique.Construction.requiredMatrix line 56
  9. theorem OAI.CycleClique.Construction.requiredMatrix_sound line 62