OAI/Computability/MinUncut/PCP/DegreeReplacement.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.Cloud line 15
  2. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.cloudIndexEquiv line 17
  3. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.cloudRotation line 27
  4. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.cloudRotation_involutive line 32
  5. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.innerRotation line 39
  6. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.innerRotation_involutive line 43
  7. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.innerRotation_tail line 51
  8. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.replacementStep line 57
  9. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.replacementStep_involutive line 64
  10. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.replacementPortGraph line 76
  11. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.replacementGraph line 85
  12. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.liftLabel line 101
  13. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inl line 104
  14. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inr line 114
  15. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.replacement_complete line 120
  16. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.replacement_satisfiable line 130
  17. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.rejectionCount_eq_sum line 136
  18. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.replacement_rejectionCount line 144
  19. abbrev OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.PaddedDart line 155
  20. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.paddedOwner line 158
  21. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.paddedReverse line 163
  22. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.paddedReverse_involutive line 167
  23. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.paddedGraph line 176
  24. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inl line 190
  25. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inr line 195
  26. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.padded_complete line 199
  27. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.padded_satisfiable line 207
  28. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.card_paddedDart line 212
  29. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.padded_rejectionCount line 218
  30. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.paddedReplacementPortGraph line 228
  31. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.paddedReplacementGraph line 233
  32. theorem OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.paddedReplacement_rejectionCount line 239
  33. def OAI.MinUncutGames.Foundations.PCP.DegreeReplacement.noDummyEquiv line 248
  34. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.truth line 275
  35. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.disagree line 277
  36. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.truth_nonneg line 279
  37. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.disagree_nonneg line 281
  38. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.disagree_eq line 284
  39. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.disagree_xor_le line 288
  40. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.parity line 292
  41. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.bitSign_parity line 295
  42. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.bitSign_injective line 303
  43. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.parity_xor line 307
  44. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.cubeXor_comm line 313
  45. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.cubeXor_right_twice line 318
  46. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.expect_cubeXor line 324
  47. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.distance line 339
  48. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.distance_nonneg line 342
  49. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.distance_parity line 348
  50. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.blrReject line 356
  51. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.blrReject_nonneg line 359
  52. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.blr_correlation line 366
  53. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.blrReject_fourier line 385
  54. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.blr_near_parity line 393
  55. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.selfCorrect line 423
  56. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.parity_selfCorrect line 426
  57. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.selfCorrect_error line 431
  58. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.singleMask line 445
  59. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.flipAt line 447
  60. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.flipAt_twice line 451
  61. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.flipAt_eq_xor line 456
  62. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.expect_flipAt line 460
  63. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.walsh_singleMask line 465
  64. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.parity_singleMask line 475
  65. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.parity_flipAt line 479
  66. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.cubeAnd line 484
  67. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.andLawFailure line 486
  68. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.andLawFailure_flipAt_second line 489
  69. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.four_truth_lower line 506
  70. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.parity_and_rejection line 510
  71. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.truth_xor line 539
  72. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.disagree_triangle line 542
  73. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.and_disagree_transfer line 546
  74. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.andReject line 552
  75. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.unitReject line 557
  76. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.inputReject line 562
  77. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.testerReject line 565
  78. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.andReject_nonneg line 568
  79. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.unitReject_nonneg line 581
  80. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.inputReject_nonneg line 587
  81. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.andReject_transfer line 595
  82. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.parity_zero line 619
  83. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.unitReject_zero_parity line 624
  84. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.parity_singleMask_eval line 637
  85. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.inputReject_transfer line 642
  86. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.tester_proximity_soundness line 659
  87. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.selfCorrect_dictator line 707
  88. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.tester_perfect_completeness line 713
  89. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.eventQueries line 725
  90. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.eventAccepts line 741
  91. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.oracleAnswer line 747
  92. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.eventReject line 750
  93. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.truth_not_decide_eq line 755
  94. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.eventReject_blr line 759
  95. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.eventReject_and line 766
  96. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.eventReject_unit line 775
  97. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.eventReject_input line 786
  98. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.event_perfect_completeness line 794
  99. def OAI.MinUncutGames.Foundations.PCP.AssignmentTester.explicitTesterReject line 809
  100. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.explicitTesterReject_eq line 813
  101. theorem OAI.MinUncutGames.Foundations.PCP.AssignmentTester.explicit_proximity_soundness line 820