OAI/Computability/DirectedFeedback/Encoding/PortTables.lean

GitHub source file

132 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.PCP.PortTables.Label line 11
  2. def OAI.DFVSGames.Foundations.PCP.PortTables.rowIndex line 13
  3. theorem OAI.DFVSGames.Foundations.PCP.PortTables.rowIndex_val line 16
  4. structure OAI.DFVSGames.Foundations.PCP.PortTables.Table line 19
  5. def OAI.DFVSGames.Foundations.PCP.PortTables.rotation line 30
  6. def OAI.DFVSGames.Foundations.PCP.PortTables.accepts line 33
  7. theorem OAI.DFVSGames.Foundations.PCP.PortTables.rowIndex_rotation line 36
  8. theorem OAI.DFVSGames.Foundations.PCP.PortTables.rotation_involutive line 40
  9. theorem OAI.DFVSGames.Foundations.PCP.PortTables.accepts_rotation line 46
  10. def OAI.DFVSGames.Foundations.PCP.PortTables.portGraph line 50
  11. theorem OAI.DFVSGames.Foundations.PCP.PortTables.portGraph_rot line 58
  12. def OAI.DFVSGames.Foundations.PCP.PortTables.baseGraph line 61
  13. theorem OAI.DFVSGames.Foundations.PCP.PortTables.baseGraph_reverse line 68
  14. theorem OAI.DFVSGames.Foundations.PCP.PortTables.baseGraph_tail line 71
  15. theorem OAI.DFVSGames.Foundations.PCP.PortTables.baseGraph_head line 74
  16. theorem OAI.DFVSGames.Foundations.PCP.PortTables.baseGraph_accepts line 77
  17. def OAI.DFVSGames.Foundations.PCP.PortTables.ofPortGraph line 80
  18. theorem OAI.DFVSGames.Foundations.PCP.PortTables.rotation_ofPortGraph line 97
  19. theorem OAI.DFVSGames.Foundations.PCP.PortTables.accepts_ofPortGraph line 104
  20. def OAI.DFVSGames.Foundations.PCP.PortTables.flatRows line 112
  21. theorem OAI.DFVSGames.Foundations.PCP.PortTables.reverseAt_flatRows line 116
  22. theorem OAI.DFVSGames.Foundations.PCP.PortTables.acceptsAt_flatRows line 120
  23. theorem OAI.DFVSGames.Foundations.PCP.PortTables.flatRows_valid line 124
  24. def OAI.DFVSGames.Foundations.PCP.PortTables.graphTable line 131
  25. def OAI.DFVSGames.Foundations.PCP.PortTables.tableWords line 134
  26. def OAI.DFVSGames.Foundations.PCP.PortTables.tableBits line 136
  27. abbrev OAI.DFVSGames.Foundations.PCP.PortTables.Input line 138
  28. def OAI.DFVSGames.Foundations.PCP.PortTables.inputBits line 140
  29. theorem OAI.DFVSGames.Foundations.PCP.PortTables.tableWords_eq line 142
  30. theorem OAI.DFVSGames.Foundations.PCP.PortTables.tableWords_length line 145
  31. theorem OAI.DFVSGames.Foundations.PCP.PortTables.vertices_le_tableBits_length line 149
  32. abbrev OAI.DFVSGames.Foundations.PCP.DegreeReplacement.Cloud line 164
  33. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.cloudIndexEquiv line 166
  34. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.cloudRotation line 176
  35. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.cloudRotation_involutive line 181
  36. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.innerRotation line 188
  37. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.innerRotation_involutive line 192
  38. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.innerRotation_tail line 200
  39. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.replacementStep line 206
  40. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.replacementStep_involutive line 213
  41. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.replacementPortGraph line 225
  42. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.replacementGraph line 234
  43. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.liftLabel line 250
  44. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inl line 253
  45. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inr line 263
  46. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.replacement_complete line 269
  47. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.replacement_satisfiable line 279
  48. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.rejectionCount_eq_sum line 285
  49. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.replacement_rejectionCount line 293
  50. abbrev OAI.DFVSGames.Foundations.PCP.DegreeReplacement.PaddedDart line 304
  51. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.paddedOwner line 307
  52. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.paddedReverse line 312
  53. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.paddedReverse_involutive line 316
  54. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.paddedGraph line 325
  55. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inl line 339
  56. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inr line 344
  57. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.padded_complete line 348
  58. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.padded_satisfiable line 356
  59. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.card_paddedDart line 361
  60. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.padded_rejectionCount line 367
  61. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.paddedReplacementPortGraph line 377
  62. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.paddedReplacementGraph line 382
  63. theorem OAI.DFVSGames.Foundations.PCP.DegreeReplacement.paddedReplacement_rejectionCount line 388
  64. def OAI.DFVSGames.Foundations.PCP.DegreeReplacement.noDummyEquiv line 397
  65. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.truth line 425
  66. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.disagree line 427
  67. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.truth_nonneg line 429
  68. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.disagree_nonneg line 431
  69. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.disagree_eq line 434
  70. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.disagree_xor_le line 438
  71. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.parity line 442
  72. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.bitSign_parity line 445
  73. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.bitSign_injective line 453
  74. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.parity_xor line 457
  75. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.cubeXor_comm line 463
  76. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.cubeXor_right_twice line 468
  77. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.expect_cubeXor line 474
  78. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.distance line 489
  79. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.distance_nonneg line 492
  80. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.distance_parity line 498
  81. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.blrReject line 506
  82. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.blrReject_nonneg line 509
  83. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.blr_correlation line 516
  84. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.blrReject_fourier line 535
  85. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.blr_near_parity line 543
  86. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.selfCorrect line 573
  87. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.parity_selfCorrect line 576
  88. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.selfCorrect_error line 581
  89. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.singleMask line 595
  90. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.flipAt line 597
  91. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.flipAt_twice line 601
  92. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.flipAt_eq_xor line 606
  93. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.expect_flipAt line 610
  94. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.walsh_singleMask line 615
  95. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.parity_singleMask line 625
  96. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.parity_flipAt line 629
  97. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.cubeAnd line 634
  98. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.andLawFailure line 636
  99. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.andLawFailure_flipAt_second line 639
  100. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.four_truth_lower_inline_AssignmentTester line 656
  101. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.parity_and_rejection line 660
  102. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.truth_xor line 689
  103. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.disagree_triangle line 692
  104. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.and_disagree_transfer line 696
  105. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.andReject line 702
  106. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.unitReject line 707
  107. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.inputReject line 712
  108. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.testerReject line 715
  109. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.andReject_nonneg line 718
  110. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.unitReject_nonneg line 731
  111. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.inputReject_nonneg line 737
  112. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.andReject_transfer line 745
  113. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.parity_zero line 769
  114. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.unitReject_zero_parity line 774
  115. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.parity_singleMask_eval line 787
  116. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.inputReject_transfer line 792
  117. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.tester_proximity_soundness line 809
  118. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.selfCorrect_dictator line 857
  119. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.tester_perfect_completeness line 864
  120. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.eventQueries line 876
  121. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.eventAccepts line 892
  122. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.oracleAnswer line 898
  123. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.eventReject line 901
  124. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.truth_not_decide_eq line 906
  125. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.eventReject_blr line 910
  126. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.eventReject_and line 917
  127. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.eventReject_unit line 926
  128. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.eventReject_input line 937
  129. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.event_perfect_completeness line 946
  130. def OAI.DFVSGames.Foundations.PCP.AssignmentTester.explicitTesterReject line 961
  131. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.explicitTesterReject_eq line 965
  132. theorem OAI.DFVSGames.Foundations.PCP.AssignmentTester.explicit_proximity_soundness line 972