OAI/Computability/BinPacking/PCP/CloudRounding.lean

GitHub source file

146 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingGames.Foundations.PCP.PoweringWalks.PortGraph line 22
  2. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringWalks.Edge line 26
  3. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringWalks.Walk line 27
  4. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.next line 31
  5. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.rot_rot line 33
  6. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.walkEnd line 36
  7. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.walkEnd_nil line 40
  8. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.walkEnd_cons line 42
  9. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.walkEnd_append line 45
  10. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.splitHead line 51
  11. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.rotateHead line 62
  12. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.rotateHead_vertex line 66
  13. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.rotateHead_zero line 69
  14. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.rotateHead_succ line 72
  15. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.permutePorts line 76
  16. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.wordEnd line 90
  17. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.endpoint line 94
  18. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.natCard_walk line 97
  19. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.headTailEquiv line 101
  20. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.advanceTail line 112
  21. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.edgeAt line 115
  22. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.pivotEquiv line 121
  23. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.pivotEquiv_fst line 131
  24. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.edgeAt_port line 145
  25. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.pivotEquiv_zero_apply line 161
  26. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.pivotEquiv_succ_apply line 165
  27. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.projectedFiberEquiv line 172
  28. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.projectedEventEquiv line 184
  29. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_fiber line 202
  30. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_event line 211
  31. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.leftFromPivot line 221
  32. def OAI.BinPackingGames.Foundations.PCP.PoweringWalks.rightFromPivot line 227
  33. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.leftFromPivot_zero line 234
  34. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.rightFromPivot_zero line 238
  35. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.leftFromPivot_actual line 243
  36. theorem OAI.BinPackingGames.Foundations.PCP.PoweringWalks.rightFromPivot_actual line 262
  37. structure OAI.BinPackingGames.Foundations.PCP.ConstraintGraph line 283
  38. def OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.head line 294
  39. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.head_reverse line 296
  40. def OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.edgeSatisfied line 300
  41. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.edgeSatisfied_reverse line 303
  42. def OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.Satisfiable line 309
  43. def OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.rejectedDarts line 312
  44. def OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.rejectionCount line 315
  45. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.mem_rejectedDarts line 318
  46. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.rejectionCount_le line 323
  47. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.rejected_exists_of_not_satisfiable line 327
  48. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.rejectionCount_positive line 339
  49. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringLabels.PortWords line 356
  50. instance OAI.BinPackingGames.Foundations.PCP.PoweringLabels.finitePortWords line 358
  51. def OAI.BinPackingGames.Foundations.PCP.PoweringLabels.Ball line 362
  52. def OAI.BinPackingGames.Foundations.PCP.PoweringLabels.wordToBall line 365
  53. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLabels.wordToBall_surjective line 368
  54. instance OAI.BinPackingGames.Foundations.PCP.PoweringLabels.finiteBall line 375
  55. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLabels.card_portWords line 379
  56. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLabels.card_ball_le line 383
  57. structure OAI.BinPackingGames.Foundations.PCP.PoweringLabels.AddressSelector line 390
  58. def OAI.BinPackingGames.Foundations.PCP.PoweringLabels.classicalSelector line 394
  59. def OAI.BinPackingGames.Foundations.PCP.PoweringLabels.scanWitness line 399
  60. def OAI.BinPackingGames.Foundations.PCP.PoweringLabels.listSelector line 410
  61. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringLabels.PaddedLabel line 421
  62. def OAI.BinPackingGames.Foundations.PCP.PoweringLabels.encode line 423
  63. def OAI.BinPackingGames.Foundations.PCP.PoweringLabels.decode line 426
  64. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLabels.decode_encode line 429
  65. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLabels.decode_surjective line 436
  66. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLabels.encode_injective line 440
  67. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLabels.decoded_word_collision line 447
  68. theorem OAI.BinPackingGames.Foundations.PCP.PoweringLabels.card_paddedLabel line 453
  69. abbrev OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.Cloud line 470
  70. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.cloudIndexEquiv line 472
  71. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.cloudRotation line 482
  72. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.cloudRotation_involutive line 487
  73. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.innerRotation line 494
  74. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.innerRotation_involutive line 498
  75. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.innerRotation_tail line 506
  76. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.replacementStep line 512
  77. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.replacementStep_involutive line 519
  78. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.replacementPortGraph line 531
  79. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.replacementGraph line 540
  80. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.liftLabel line 556
  81. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inl line 559
  82. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inr line 569
  83. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.replacement_complete line 575
  84. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.replacement_satisfiable line 585
  85. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.rejectionCount_eq_sum line 591
  86. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.replacement_rejectionCount line 599
  87. abbrev OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.PaddedDart line 612
  88. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.paddedOwner line 615
  89. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.paddedReverse line 620
  90. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.paddedReverse_involutive line 624
  91. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.paddedGraph line 633
  92. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inl line 647
  93. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inr line 652
  94. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.padded_complete line 656
  95. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.padded_satisfiable line 664
  96. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.card_paddedDart line 669
  97. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.padded_rejectionCount line 675
  98. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.paddedReplacementPortGraph line 687
  99. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.paddedReplacementGraph line 692
  100. theorem OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.paddedReplacement_rejectionCount line 698
  101. def OAI.BinPackingGames.Foundations.PCP.DegreeReplacement.noDummyEquiv line 707
  102. def OAI.BinPackingGames.Foundations.PCP.PoweringAddresses.allWords line 731
  103. theorem OAI.BinPackingGames.Foundations.PCP.PoweringAddresses.mem_allWords line 736
  104. def OAI.BinPackingGames.Foundations.PCP.PoweringAddresses.allAddresses line 752
  105. theorem OAI.BinPackingGames.Foundations.PCP.PoweringAddresses.mem_allAddresses line 756
  106. theorem OAI.BinPackingGames.Foundations.PCP.PoweringAddresses.length_allWords line 764
  107. theorem OAI.BinPackingGames.Foundations.PCP.PoweringAddresses.length_allAddresses line 774
  108. def OAI.BinPackingGames.Foundations.PCP.PoweringAddresses.finitePortSelector line 780
  109. def OAI.BinPackingGames.Foundations.PCP.PoweringDecoding.mass line 792
  110. theorem OAI.BinPackingGames.Foundations.PCP.PoweringDecoding.mass_sum line 797
  111. theorem OAI.BinPackingGames.Foundations.PCP.PoweringDecoding.exists_mode line 812
  112. def OAI.BinPackingGames.Foundations.PCP.PoweringDecoding.mode line 818
  113. theorem OAI.BinPackingGames.Foundations.PCP.PoweringDecoding.mode_max line 821
  114. theorem OAI.BinPackingGames.Foundations.PCP.PoweringDecoding.mode_mass_lower line 825
  115. theorem OAI.BinPackingGames.Foundations.PCP.PoweringDecoding.exists_letter_mass_lower line 836
  116. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.dart_rejection_count_le line 846
  117. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.colorSet line 895
  118. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.minoritySet line 898
  119. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.directedCut line 901
  120. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.disagreementSet line 904
  121. abbrev OAI.BinPackingGames.Foundations.PCP.CloudRounding.Nonmajor line 907
  122. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.exists_max_color line 910
  123. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.majority line 917
  124. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.majority_maximal line 921
  125. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.nonchosen_color_twice_le line 926
  126. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.minorityEquiv line 945
  127. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.minority_card_eq_sum line 962
  128. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.minorityCutEmbedding line 967
  129. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.minority_cut_sum_le line 993
  130. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.minority_expansion_bound line 1000
  131. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.mismatchSet line 1030
  132. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.copiedRejectionCount line 1034
  133. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.innerDisagreementSet line 1037
  134. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.roundLabels line 1041
  135. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.mismatchFiberEquiv line 1045
  136. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.mismatch_card_eq_sum line 1063
  137. def OAI.BinPackingGames.Foundations.PCP.CloudRounding.disagreementFiberEquiv line 1070
  138. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.disagreement_card_eq_sum line 1092
  139. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.rounded_mismatch_expansion line 1100
  140. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.rounded_endpoint_bound line 1117
  141. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.copied_satisfied_inl line 1124
  142. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.copied_satisfied_inr line 1130
  143. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.replacement_rejection_split line 1136
  144. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.replacement_soundness line 1148
  145. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.padded_replacement_soundness line 1164
  146. theorem OAI.BinPackingGames.Foundations.PCP.CloudRounding.combine_counts line 1179