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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A complete finite obstruction certificate: verified indexed layout, initial templates, required paths, closure steps, and final contradiction.

  1. structure OAI.CycleClique.Construction.LayoutCertificate line 10
  2. def OAI.CycleClique.Construction.LayoutCertificate.graph line 23
  3. instance OAI.CycleClique.Construction.LayoutCertificate.(instance at line 25) line 25
  4. def OAI.CycleClique.Construction.LayoutCertificate.initialMatrix line 28
  5. def OAI.CycleClique.Construction.LayoutCertificate.matrix line 31
  6. def OAI.CycleClique.Construction.LayoutCertificate.Check line 34
  7. instance OAI.CycleClique.Construction.LayoutCertificate.(instance at line 43) line 43
  8. theorem OAI.CycleClique.Construction.LayoutCertificate.false_of_check line 50