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

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A finite sequence of locally checked hypothetical attachments builds only sound forbidden entries. Every step reads the preceding matrix.

  1. inductive OAI.CycleClique.Construction.ClosureStep line 9
  2. def OAI.CycleClique.Construction.ClosureStep.source line 18
  3. def OAI.CycleClique.Construction.ClosureStep.target line 22
  4. def OAI.CycleClique.Construction.ClosureStep.parameter line 26
  5. def OAI.CycleClique.Construction.ClosureStep.Check line 30
  6. instance OAI.CycleClique.Construction.ClosureStep.(instance at line 34) line 34
  7. def OAI.CycleClique.Construction.ClosureStep.entryMatrix line 38
  8. def OAI.CycleClique.Construction.ClosureStep.apply line 42
  9. def OAI.CycleClique.Construction.closureMatrix line 49
  10. def OAI.CycleClique.Construction.ClosureCheck line 53
  11. instance OAI.CycleClique.Construction.(instance at line 58) line 58
  12. theorem OAI.CycleClique.Construction.ClosureStep.apply_sound line 68
  13. theorem OAI.CycleClique.Construction.closureMatrix_sound line 93