OAI/Computability/MinUncut/PCP/Folding.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Hastad.cubeFlip line 15
  2. theorem OAI.MinUncutGames.Foundations.Hastad.cubeFlip_cubeFlip line 18
  3. theorem OAI.MinUncutGames.Foundations.Hastad.bitSign_not line 22
  4. theorem OAI.MinUncutGames.Foundations.Hastad.sum_cubeFlip line 25
  5. theorem OAI.MinUncutGames.Foundations.Hastad.coefficient_zero_of_odd line 37
  6. theorem OAI.MinUncutGames.Foundations.Hastad.coefficient_sign_zero_of_folded line 46
  7. def OAI.MinUncutGames.Foundations.Hastad.representative line 53
  8. theorem OAI.MinUncutGames.Foundations.Hastad.representative_at line 57
  9. theorem OAI.MinUncutGames.Foundations.Hastad.representative_flip line 62
  10. abbrev OAI.MinUncutGames.Foundations.Hastad.HalfCube line 66
  11. def OAI.MinUncutGames.Foundations.Hastad.canonicalInput line 68
  12. theorem OAI.MinUncutGames.Foundations.Hastad.canonicalInput_flip line 72
  13. def OAI.MinUncutGames.Foundations.Hastad.foldedAnswer line 77
  14. theorem OAI.MinUncutGames.Foundations.Hastad.foldedAnswer_flip line 81
  15. theorem OAI.MinUncutGames.Foundations.Hastad.foldedAnswer_zero_coefficient line 89
  16. theorem OAI.MinUncutGames.Foundations.Hastad.foldedAnswer_dictator line 94
  17. def OAI.MinUncutGames.Foundations.Hastad.coordinateMask line 99
  18. def OAI.MinUncutGames.Foundations.Hastad.cubeToggle line 101
  19. theorem OAI.MinUncutGames.Foundations.Hastad.cubeToggle_twice line 105
  20. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_coordinateMask line 111
  21. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_cubeToggle line 121
  22. theorem OAI.MinUncutGames.Foundations.Hastad.sum_cubeToggle line 126
  23. def OAI.MinUncutGames.Foundations.Hastad.restrictQuery line 139
  24. theorem OAI.MinUncutGames.Foundations.Hastad.restrictQuery_cubeToggle line 143
  25. theorem OAI.MinUncutGames.Foundations.Hastad.conditioned_coefficient_zero_invalid line 154
  26. theorem OAI.MinUncutGames.Foundations.Hastad.conditioned_coefficient_support line 164
  27. def OAI.MinUncutGames.Foundations.Hastad.conditionedFoldedAnswer line 174
  28. theorem OAI.MinUncutGames.Foundations.Hastad.conditionedFoldedAnswer_flip line 179
  29. theorem OAI.MinUncutGames.Foundations.Hastad.conditionedFoldedAnswer_zero_coefficient line 186
  30. theorem OAI.MinUncutGames.Foundations.Hastad.conditionedFoldedAnswer_dictator line 193
  31. def OAI.MinUncutGames.Reduction.CloneGap.cart line 205
  32. theorem OAI.MinUncutGames.Reduction.CloneGap.count_const line 208
  33. theorem OAI.MinUncutGames.Reduction.CloneGap.count_cart line 212
  34. theorem OAI.MinUncutGames.Reduction.CloneGap.length_cart line 223
  35. theorem OAI.MinUncutGames.Reduction.CloneGap.count_cart_left line 228
  36. theorem OAI.MinUncutGames.Reduction.CloneGap.count_cart_right line 232
  37. theorem OAI.MinUncutGames.Reduction.CloneGap.count_cart_le line 236
  38. theorem OAI.MinUncutGames.Reduction.CloneGap.count_union_le line 249
  39. theorem OAI.MinUncutGames.Reduction.CloneGap.count_remove line 257
  40. abbrev OAI.MinUncutGames.Reduction.CloneGap.Index line 265
  41. def OAI.MinUncutGames.Reduction.CloneGap.indices line 266
  42. def OAI.MinUncutGames.Reduction.CloneGap.triples line 267
  43. def OAI.MinUncutGames.Reduction.CloneGap.collision line 268
  44. def OAI.MinUncutGames.Reduction.CloneGap.distinctTriples line 270
  45. theorem OAI.MinUncutGames.Reduction.CloneGap.length_indices line 272
  46. theorem OAI.MinUncutGames.Reduction.CloneGap.length_triples line 273
  47. theorem OAI.MinUncutGames.Reduction.CloneGap.count_index_eq_le line 276
  48. theorem OAI.MinUncutGames.Reduction.CloneGap.count_collision_le line 286
  49. theorem OAI.MinUncutGames.Reduction.CloneGap.majority_exists line 315
  50. def OAI.MinUncutGames.Reduction.CloneGap.allAgree line 329
  51. theorem OAI.MinUncutGames.Reduction.CloneGap.count_agree_distinct line 332
  52. structure OAI.MinUncutGames.Reduction.CloneGap.Equation line 349
  53. def OAI.MinUncutGames.Reduction.CloneGap.satisfied line 355
  54. def OAI.MinUncutGames.Reduction.CloneGap.clone line 358
  55. theorem OAI.MinUncutGames.Reduction.CloneGap.lift_preserves line 361
  56. theorem OAI.MinUncutGames.Reduction.CloneGap.clone_names_distinct line 364
  57. theorem OAI.MinUncutGames.Reduction.CloneGap.agree_failure line 375
  58. theorem OAI.MinUncutGames.Reduction.CloneGap.failed_occurrence_clones line 385
  59. def OAI.MinUncutGames.Reduction.CloneGap.majorityBit line 401
  60. theorem OAI.MinUncutGames.Reduction.CloneGap.majorityBit_count line 403
  61. def OAI.MinUncutGames.Reduction.CloneGap.cloneList line 415
  62. theorem OAI.MinUncutGames.Reduction.CloneGap.length_cloneList line 418
  63. theorem OAI.MinUncutGames.Reduction.CloneGap.cloneList_failure_lower line 427
  64. theorem OAI.MinUncutGames.Reduction.CloneGap.clone_gap line 446
  65. theorem OAI.MinUncutGames.Reduction.CloneGap.clone_completeness_count line 465
  66. abbrev OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.Address line 490
  67. def OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.storedAssignment line 492
  68. def OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.rhsCorrection line 496
  69. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.correction_eq line 499
  70. def OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.equation line 506
  71. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.xor_corrections line 513
  72. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.equation_satisfied line 518
  73. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.equation_satisfied_iff line 529
  74. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.equation_indicator line 538
  75. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.satisfied_repeated_right line 549
  76. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.equation_repeated_right line 556
  77. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.restrict_thirdQuery line 565
  78. def OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.conditionedEquation line 571
  79. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.conditionedEquation_rhs line 576
  80. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied line 581
  81. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied_iff line 592
  82. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.conditionedEquation_indicator line 602
  83. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.conditionedEquation_repeated_right line 614
  84. def OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.equationAcceptance line 629
  85. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.equationAcceptance_eq line 635
  86. def OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance line 642
  87. theorem OAI.MinUncutGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance_eq line 649
  88. def OAI.MinUncutGames.Foundations.Hastad.mapEquation line 667
  89. theorem OAI.MinUncutGames.Foundations.Hastad.satisfied_mapEquation line 674
  90. abbrev OAI.MinUncutGames.Foundations.Hastad.EmptyContext.Address line 682
  91. def OAI.MinUncutGames.Foundations.Hastad.EmptyContext.storedAssignment line 684
  92. def OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equation line 687
  93. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equation_second_eq_third line 693
  94. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equation_satisfied line 696
  95. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equation_storedAssignment_satisfied line 704
  96. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equation_flip_first line 709
  97. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equation_flip_rhs line 714
  98. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equation_satisfied_flip line 717
  99. def OAI.MinUncutGames.Foundations.Hastad.EmptyContext.pairedEquations line 723
  100. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.pairedEquations_length line 726
  101. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.pairedEquations_ne_nil line 729
  102. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.pairedEquations_acceptedCount line 732
  103. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.pairedEquations_failureCount line 738
  104. def OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equationAcceptance line 748
  105. def OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equationBias line 751
  106. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.foldedMean_eq_zero line 754
  107. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equation_indicator line 759
  108. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equationAcceptance_eq_half line 765
  109. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.equationBias_eq_zero line 772
  110. theorem OAI.MinUncutGames.Foundations.Hastad.EmptyContext.mapped_equationAcceptance_eq_half line 783