OAI/Computability/MaxCut/PCP/RawInitialPredicate.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Explicit finite predicates and numeric row words of the initial incidence table. Every relation retains all 4096 entries, including repetitions.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.RawInitialRows.Signs line 13
  2. abbrev OAI.MaxCutGames.Foundations.PCP.RawInitialRows.Names line 14
  3. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.clauseSigns line 16
  4. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.clauseNames line 19
  5. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.nameWord line 22
  6. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.decodedLabel line 27
  7. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.incidencePredicate line 30
  8. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.relationPredicate line 38
  9. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.relationWordsFor line 43
  10. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialRows.relationWordsFor_length line 46
  11. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.incidenceWords line 50
  12. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.clauseWords line 56
  13. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.dummyWords line 64
  14. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.orderedList line 77

    Source documentation

    The list induced by an explicit numbering, in increasing numeric order.

    def orderedList {α : Type*} {n : Nat} (e : α ≃ Fin n) : List α :=
…
  15. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialRows.orderedList_cast line 80
  16. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialRows.orderedList_prod line 85
  17. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialRows.orderedList_sum line 109
  18. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.clauseDarts line 123
  19. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialRows.orderedList_dartOrder line 128
  20. def OAI.MaxCutGames.Foundations.PCP.RawInitialRows.rowFor line 141
  21. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialRows.rowList_table line 147
  22. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialRows.rowWords_incidence line 153
  23. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialRows.rowWords_dummy line 173
  24. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialRows.clauseDarts_rowWords line 186
  25. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialRows.tableWords_eq line 193

    Source documentation

    Exact headers and exact clause/slot/orientation order of every emitted word.

    theorem tableWords_eq (F : Formula) :
    tableWords (table F) =
      [F.«variables» + F.clauses.length + 1, 6 * F.clauses.length + 1] ++
      (List.finRange F.clauses.length).flatMap (fun i =>
        clauseWords F.«variables» i.val (clauseNames (clauseAt F i))
          (clauseSigns (clauseAt F i))) ++ dummyWords F.«variables» F.clauses.length := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.RawInitialRows.clauseWords, OAI.MaxCutGames.Foundations.PCP.RawInitialRows.clauseNames, OAI.MaxCutGames.Foundations.PCP.clauseAt, OAI.MaxCutGames.Foundations.PCP.RawInitialRows.clauseSigns, OAI.MaxCutGames.Foundations.PCP.RawInitialRows.dummyWords