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

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Computable validation of explicit initial-rule templates. Validation checks paths and disjointness directly rather than trusting a forest search.

  1. theorem OAI.CycleClique.Construction.chainCliqueCount_filter line 12
  2. theorem OAI.CycleClique.Construction.chainOutsideCount_filter line 20
  3. def OAI.CycleClique.Construction.RawChainsValid line 29
  4. instance OAI.CycleClique.Construction.(instance at line 35) line 35
  5. def OAI.CycleClique.Construction.RawPathSystem.ofValid line 39
  6. structure OAI.CycleClique.Construction.TemplateData line 47
  7. def OAI.CycleClique.Construction.TemplateData.oldVertices line 61
  8. def OAI.CycleClique.Construction.TemplateData.amount line 64
  9. def OAI.CycleClique.Construction.TemplateData.assignedCount line 67
  10. def OAI.CycleClique.Construction.TemplateData.incidentBound line 71
  11. def OAI.CycleClique.Construction.TemplateData.Valid line 74
  12. instance OAI.CycleClique.Construction.TemplateData.(instance at line 82) line 82
  13. def OAI.CycleClique.Construction.TemplateData.toTemplate line 85
  14. theorem OAI.CycleClique.Construction.TemplateData.toTemplate_amount line 98
  15. theorem OAI.CycleClique.Construction.TemplateData.toTemplate_incidentBound line 102
  16. theorem OAI.CycleClique.Construction.TemplateData.toTemplate_assignedCount line 107
  17. def OAI.CycleClique.Construction.TemplateData.Check line 114
  18. instance OAI.CycleClique.Construction.TemplateData.(instance at line 119) line 119
  19. theorem OAI.CycleClique.Construction.TemplateData.forbids line 125