OAI/Computability/UniqueGames/PCP/RawInitialTablesLemmas.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

Explicit structural numberings of the raw 3SAT incidence graph. Unused declared variable names are retained; their unary input header pays for them. The graph has one dummy vertex and one tautological loop, even for an empty formula. No input-dependent choice of a finite enumeration is made.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.unitOrder line 27
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.slotOrder line 33
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.binaryOrder line 42
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.labelOrder line 51
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.vertexOrder line 53
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.eventOrder line 57
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.dartOrder line 60
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.raw64 line 64
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.table line 68
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.table_vertices line 71
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.table_darts line 74
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.table_vertices_positive line 76
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.table_darts_positive line 79
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.raw64_satisfiable_iff line 82
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.table_semantics line 87
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.table_satisfiable_iff line 95
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.initial_rejection line 101
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialTables.initial_size line 107
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.nameSum line 121
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.bodyTime line 124
  21. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.loopTime line 128
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.nameSum_le line 132
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.bodyTime_le line 139
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.loopTime_le line 146
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.input_header_bound line 168
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.graph_size_bound line 174
  27. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.fullBudget line 181
  28. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.timePolynomial line 185
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.timePolynomial_eval line 189
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineBudget.fullBudget_le line 193
  31. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.Signs line 218
  32. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.Names line 219
  33. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.clauseSigns line 221
  34. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.clauseNames line 224
  35. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.nameWord line 227
  36. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.decodedLabel line 232
  37. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.incidencePredicate line 235
  38. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.relationPredicate line 243
  39. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.relationWordsFor line 248
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.relationWordsFor_length line 251
  41. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.incidenceWords line 255
  42. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.clauseWords line 261
  43. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.dummyWords line 269
  44. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.orderedList line 276

    Source documentation

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

    def orderedList {α : Type*} {n : Nat} (e : α ≃ Fin n) : List α :=
…
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.orderedList_cast line 279
  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.orderedList_prod line 284
  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.orderedList_sum line 308
  48. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.clauseDarts line 322
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.orderedList_dartOrder line 327
  50. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.rowFor line 340
  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.rowList_table line 346
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.rowWords_incidence line 352
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.rowWords_dummy line 372
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.clauseDarts_rowWords line 385
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.tableWords_eq line 392

    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.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.clauseWords, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.clauseNames, OAI.UniqueGamesTheorem.Foundations.PCP.clauseAt, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.clauseSigns, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.dummyWords

  56. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.BaseTable line 410
  57. opaque OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.fixedWalkParameter line 414

    Source documentation

    Initialized fixed data keep enormous constant powers symbolic in the kernel. The stored equality proves the exact requested parameter; no value is assumed.

    opaque fixedWalkParameter : {n : Nat // n = 2 * FinalConstants.endpointLength} :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.endpointLength

  58. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.walkParameter line 417
  59. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.walkParameter_eq line 419
  60. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.alphabet line 422
  61. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.alphabet_positive line 424
  62. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.powered line 428
  63. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.build line 431
  64. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.sizeFactor line 434
  65. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.degree_positive line 437
  66. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.dartFactor_positive line 441
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.sizeFactor_positive line 445
  68. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.powered_vertices line 452
  69. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.powered_darts line 455
  70. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.build_darts_positive line 459
  71. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.build_size_le line 467
  72. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.build_completeness line 494
  73. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.Input line 503
  74. instance OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.(instance at line 505) line 505
  75. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.step line 507
  76. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.initial line 510
  77. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.size line 513
  78. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.Satisfiable line 515
  79. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.gap line 517
  80. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.size_positive line 519
  81. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.gap_nonnegative line 522
  82. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.gap_eq_zero_iff line 525
  83. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.one_le_size_mul_gap line 528
  84. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.initial_satisfiable_iff line 540
  85. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.step_completeness line 543
  86. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.step_size line 546
  87. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTableGap.powered_count_gap line 564
  88. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTableGap.build_count_gap line 595
  89. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundTableGap.step_gap line 610