OAI/Computability/BinPacking/PCP/PCPSource.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.output line 9
  2. theorem OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.satisfiable_iff line 12
  3. theorem OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.variable_count line 19
  4. theorem OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.clause_count line 23
  5. theorem OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.nonempty line 27
  6. theorem OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.tableGraph_rejectionCount line 31
  7. theorem OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.tableGraph_count_lower line 41
  8. theorem OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.clauseGap line 50
  9. theorem OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.total_size_le line 60
  10. def OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.sizePolynomial line 67
  11. theorem OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.sizePolynomial_eval line 72
  12. theorem OAI.BinPackingGames.Foundations.PCP.FinalTableFormula.formulaBits_length_le_polynomial line 76
  13. def OAI.BinPackingGames.Foundations.PCP.TableIteration.run line 99
  14. def OAI.BinPackingGames.Foundations.PCP.TableIteration.runTables line 101
  15. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.run_val line 104
  16. def OAI.BinPackingGames.Foundations.PCP.TableIteration.iterationCount line 112
  17. def OAI.BinPackingGames.Foundations.PCP.TableIteration.output line 114
  18. def OAI.BinPackingGames.Foundations.PCP.TableIteration.outputTable line 116
  19. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.output_val line 119
  20. def OAI.BinPackingGames.Foundations.PCP.TableIteration.gapMap line 122
  21. opaque OAI.BinPackingGames.Foundations.PCP.TableIteration.degreeData line 124
  22. def OAI.BinPackingGames.Foundations.PCP.TableIteration.polynomialDegree line 127
  23. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.sizeFactor_le_power line 129
  24. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.run_completeness line 132
  25. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.output_completeness line 136
  26. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.gapMap_completeness line 140
  27. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.output_darts_positive line 146
  28. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.gapMap_nonempty line 150
  29. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.run_size line 153
  30. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.output_size line 157
  31. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.initial_size_le line 162
  32. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.output_size_le_input line 165
  33. def OAI.BinPackingGames.Foundations.PCP.TableIteration.tableSizePolynomial line 173
  34. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.tableSizePolynomial_eval line 176
  35. def OAI.BinPackingGames.Foundations.PCP.TableIteration.tableBitsPolynomial line 181
  36. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.output_bits_le line 184
  37. def OAI.BinPackingGames.Foundations.PCP.TableIteration.formulaBitsPolynomial line 189
  38. theorem OAI.BinPackingGames.Foundations.PCP.TableIteration.gapMap_bits_le line 192
  39. theorem OAI.BinPackingGames.Foundations.PCP.TableGapReduction.run_gap line 209
  40. theorem OAI.BinPackingGames.Foundations.PCP.TableGapReduction.output_gap line 214
  41. theorem OAI.BinPackingGames.Foundations.PCP.TableGapReduction.output_satisfiable_iff line 222
  42. theorem OAI.BinPackingGames.Foundations.PCP.TableGapReduction.gapMap_satisfiable_iff line 232
  43. theorem OAI.BinPackingGames.Foundations.PCP.TableGapReduction.output_count_gap line 236
  44. theorem OAI.BinPackingGames.Foundations.PCP.TableGapReduction.gapMap_clauseGap line 256
  45. theorem OAI.BinPackingGames.Foundations.PCP.TableGapReduction.finalClauseGap_le_one line 262
  46. def OAI.BinPackingCompleteness.PCPSource.baseTable line 278
  47. theorem OAI.BinPackingCompleteness.PCPSource.baseTable_certificate line 281
  48. def OAI.BinPackingCompleteness.PCPSource.rawFormula line 285
  49. def OAI.BinPackingCompleteness.PCPSource.normalizedFormula line 287
  50. theorem OAI.BinPackingCompleteness.PCPSource.rawFormula_nonempty line 289
  51. theorem OAI.BinPackingCompleteness.PCPSource.normalizedFormula_nonempty line 292
  52. theorem OAI.BinPackingCompleteness.PCPSource.normalizedFormula_satisfiable_iff line 295
  53. theorem OAI.BinPackingCompleteness.PCPSource.normalizedFormula_distinct line 300
  54. def OAI.BinPackingCompleteness.PCPSource.baseDenominator line 305
  55. def OAI.BinPackingCompleteness.PCPSource.sourceDenominator line 307
  56. def OAI.BinPackingCompleteness.PCPSource.sourceGap line 309
  57. theorem OAI.BinPackingCompleteness.PCPSource.baseDenominator_pos line 311
  58. theorem OAI.BinPackingCompleteness.PCPSource.sourceDenominator_pos line 314
  59. theorem OAI.BinPackingCompleteness.PCPSource.sourceGap_pos line 317
  60. theorem OAI.BinPackingCompleteness.PCPSource.sourceGap_le_one line 321
  61. theorem OAI.BinPackingCompleteness.PCPSource.finalClauseGap_eq line 326
  62. theorem OAI.BinPackingCompleteness.PCPSource.sourceGap_eq line 329
  63. theorem OAI.BinPackingCompleteness.PCPSource.rawFormula_count_gap line 333
  64. theorem OAI.BinPackingCompleteness.PCPSource.normalizedFormula_count_gap line 355
  65. def OAI.BinPackingCompleteness.PCPSource.clauseFamily line 363
  66. instance OAI.BinPackingCompleteness.PCPSource.clauseCount_neZero line 370
  67. theorem OAI.BinPackingCompleteness.PCPSource.failedCount_eq_fin_sum line 373
  68. theorem OAI.BinPackingCompleteness.PCPSource.violatedCount_eq_failedCount line 380
  69. theorem OAI.BinPackingCompleteness.PCPSource.clauseGap line 387
  70. def OAI.BinPackingCompleteness.PCPSource.source line 400
  71. theorem OAI.BinPackingCompleteness.PCPSource.source_complete line 402
  72. theorem OAI.BinPackingCompleteness.PCPSource.source_sound line 407
  73. def OAI.BinPackingCompleteness.PCPSource.repetitionLength line 411
  74. theorem OAI.BinPackingCompleteness.PCPSource.repetitionLength_positive line 414
  75. def OAI.BinPackingCompleteness.PCPSource.amplifiedSource line 417
  76. theorem OAI.BinPackingCompleteness.PCPSource.amplifiedSource_complete line 420
  77. theorem OAI.BinPackingCompleteness.PCPSource.amplifiedSource_sound line 426
  78. def OAI.BinPackingCompleteness.PCPSource.binarySource line 431
  79. theorem OAI.BinPackingCompleteness.PCPSource.binarySource_complete line 433
  80. theorem OAI.BinPackingCompleteness.PCPSource.binarySource_sound line 437
  81. def OAI.BinPackingCompleteness.PCPSource.binaryAmplifiedSource line 441
  82. theorem OAI.BinPackingCompleteness.PCPSource.binaryAmplifiedSource_complete line 444
  83. theorem OAI.BinPackingCompleteness.PCPSource.binaryAmplifiedSource_sound line 449