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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A weighted packing witness is validated by finite arithmetic and pairwise matrix lookups. Its soundness needs only the established matrix.

  1. def OAI.CycleClique.Construction.PackingCheck line 11
  2. instance OAI.CycleClique.Construction.(instance at line 17) line 17
  3. theorem OAI.CycleClique.Construction.packingCheck_false line 22