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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Soundness of the checker's hypothetical zero/one attachment rules. Each local contradiction is witnessed by explicit required paths and a checked bad state; inherited constraints refer only to earlier states.

  1. structure OAI.CycleClique.Construction.EdgeAttachmentData line 10
  2. structure OAI.CycleClique.Construction.FreshAttachmentData line 17
  3. def OAI.CycleClique.Construction.EdgeAttachmentData.Check line 26
  4. def OAI.CycleClique.Construction.FreshAttachmentData.Check line 32
  5. instance OAI.CycleClique.Construction.(instance at line 38) line 38
  6. instance OAI.CycleClique.Construction.(instance at line 42) line 42
  7. theorem OAI.CycleClique.Construction.EdgeAttachmentData.forbids line 48
  8. theorem OAI.CycleClique.Construction.FreshAttachmentData.forbids line 64