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

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Natural-number masks provide a compact, checked representation of finite forbidden matrices. The supplied masks are validated separately.

  1. def OAI.CycleClique.Construction.decode line 12

    Source documentation

    Decode the first w bits of a natural-number mask.

    def decode (w b : ℕ) : Finset ℕ :=
…
  2. theorem OAI.CycleClique.Construction.decode_zero line 15
  3. theorem OAI.CycleClique.Construction.decode_or line 18
  4. def OAI.CycleClique.Construction.templateMaskEntry line 22
  5. def OAI.CycleClique.Construction.templateMaskMatrix line 26
  6. theorem OAI.CycleClique.Construction.templateMaskMatrix_append line 31
  7. theorem OAI.CycleClique.Construction.decode_templateMaskEntry line 43
  8. theorem OAI.CycleClique.Construction.decode_templateMaskMatrix line 51
  9. def OAI.CycleClique.Construction.requiredMaskEntry line 67
  10. def OAI.CycleClique.Construction.requiredMaskMatrix line 71
  11. theorem OAI.CycleClique.Construction.requiredMaskMatrix_append line 76
  12. theorem OAI.CycleClique.Construction.decode_requiredMaskEntry line 88
  13. theorem OAI.CycleClique.Construction.decode_requiredMaskMatrix line 96