OAI/Computability/BinPacking/PCP/PreprocessingRegularSoundness.lean

GitHub source file

159 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.CloudPadding.paddedSize line 16
2. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.paddedSize_zero line 18
3. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.paddedSize_of_pos line 20
4. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.le_paddedSize line 24
5. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.paddedSize_le_mul line 31
6. def OAI.BinPackingGames.Foundations.PCP.CloudPadding.paddedCloudEquiv line 38
7. def OAI.BinPackingGames.Foundations.PCP.CloudPadding.dartCloudEquiv line 61
8. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.sum_card_cloud line 72
9. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.card_padded_cloud line 76
10. abbrev OAI.BinPackingGames.Foundations.PCP.CloudPadding.dummy line 82
11. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.card_cloud line 85
12. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.card_dummy_of_empty line 93
13. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.card_cloud_of_empty line 97
14. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.card_cloud_eq_family line 102
15. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.card_paddedDart_eq_sum line 110
16. theorem OAI.BinPackingGames.Foundations.PCP.CloudPadding.card_paddedDart_le line 122
17. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv line 141
18. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_val line 150
19. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_symm_apply line 154
20. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts line 158
21. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.mem_cloudDarts line 161
22. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_nodup line 165
23. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_sublist line 169
24. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize line 172
25. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_le_darts line 174
26. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect line 178
27. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank line 183
28. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_val line 188
29. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_val line 192
30. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_cloudRank line 196
31. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_cloudSelect line 201
32. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudEquiv line 206
33. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_card_cloud line 213
34. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_eq_nil_iff line 217
35. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_zero_iff line 221
36. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.sum_cloudSize line 225
37. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.oldCloudIndex line 234
38. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_oldCloudIndex line 237
39. abbrev OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.PaddedCloud line 241
40. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedOld line 245
41. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedNew line 249
42. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudEquiv line 253
43. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank line 259
44. def OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect line 263
45. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_rank line 267
46. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_select line 272
47. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old line 277
48. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new line 282
49. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old_val line 287
50. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new_val line 292
51. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_castAdd line 297
52. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_natAdd line 309
53. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingCloudIndex.card_paddedCloud line 315
54. abbrev OAI.BinPackingGames.Foundations.PCP.Regularization.Vertex line 331
55. abbrev OAI.BinPackingGames.Foundations.PCP.Regularization.Port line 332
56. def OAI.BinPackingGames.Foundations.PCP.Regularization.degree line 334
57. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.degree_eq line 336
58. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.degree_positive line 339
59. def OAI.BinPackingGames.Foundations.PCP.Regularization.cloudEquiv line 341
60. def OAI.BinPackingGames.Foundations.PCP.Regularization.cloudGraph line 347
61. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.cloudGraph_of_pos line 358
62. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.cloudGraph_certificate_of_pos line 366
63. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.cloud_expansion line 374
64. def OAI.BinPackingGames.Foundations.PCP.Regularization.portGraph line 389
65. def OAI.BinPackingGames.Foundations.PCP.Regularization.graph line 392
66. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.graph_tail line 397
67. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.graph_reverse line 401
68. def OAI.BinPackingGames.Foundations.PCP.Regularization.degreeEquiv line 404
69. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.fixed_degree line 416
70. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.vertex_count_le line 421
71. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.dart_count line 426
72. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.dart_count_le line 431
73. def OAI.BinPackingGames.Foundations.PCP.Regularization.liftLabel line 441
74. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.lift_rejectionCount line 445
75. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.completeness line 450
76. def OAI.BinPackingGames.Foundations.PCP.Regularization.roundLabels line 455
77. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.soundness line 458
78. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.exists_rounding line 463
79. theorem OAI.BinPackingGames.Foundations.PCP.Regularization.soundness_of_uniform_lower_bound line 467
80. def OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.levelLoop line 478
81. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.levelLoop_level_le line 484
82. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.levelLoop_power line 495
83. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.levelLoop_covers line 506
84. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.levelLoop_le_of_covering_power line 521
85. def OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.searchResult line 538
86. def OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.boundedLevel line 541
87. def OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.paddedSize line 543
88. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.boundedLevel_zero line 545
89. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.paddedSize_zero line 547
90. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_input line 549
91. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.paddedSize_power line 553
92. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.le_paddedSize line 558
93. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.boundedLevel_eq_level line 562
94. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.paddedSize_eq_size line 572
95. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_of_le_power line 576
96. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.paddedSize_positive line 581
97. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.paddedSize_bounds line 585
98. def OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize line 590
99. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_zero line 592
100. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_of_pos line 594
101. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_bounds line 598
102. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.table_vertexCount_eq_paddedSize line 606
103. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLevels.family_row_count_at_size line 617
104. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.paddingList line 633
105. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.paddingList_nodup line 637
106. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.mem_paddingList line 641
107. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.paddingListOrder line 646
108. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.paddingList_length line 651
109. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.paddingOrder line 656
110. abbrev OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.Vertex line 660
111. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.vertexCount line 663
112. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder line 666
113. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_original line 670
114. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_dummy line 674
115. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.unitOrder line 679
116. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.portOrder line 685
117. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.portOrder_internal line 688
118. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.portOrder_inherited line 691
119. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.cloudGraphs line 694
120. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.sourcePortGraph line 702
121. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.sourceGraph line 709
122. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.numberedPortGraph line 717
123. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts line 724
124. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts_transpose line 732
125. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.ofCloudTables line 745
126. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.rotation_ofCloudTables line 752
127. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.accepts_ofCloudTables line 764
128. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.accepts_internal line 775
129. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.accepts_original line 785
130. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.accepts_dummy line 796
131. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.edgeSatisfied_ofCloudTables line 806
132. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_ofCloudTables line 823
133. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.liftedLabel line 839
134. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_liftedLabel line 845
135. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.emptyTable line 857
136. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.resizeTable line 860
137. abbrev OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.BaseTable line 863
138. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.internalDegree line 867
139. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.padding line 869
140. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.cloudSize_add_padding line 873
141. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_sum_cloudPaddedSize line 878
142. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_le line 885
143. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_zero_of_no_darts line 891
144. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.familyCloudTable line 897
145. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.regularize line 910
146. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularTables.regularizeInput line 914
147. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.internalDegree_ge_eight line 924
148. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.baseDegree_ne_zero line 928
149. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.resizeTable_certificate line 934
150. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.familyCloudTable_certificate_of_pos line 941
151. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.cloudGraphs_certificate_of_pos line 952
152. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.cloud_expansion line 961
153. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.roundLabels line 983
154. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.soundness line 990
155. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.exists_rounding line 1001
156. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.lift_rejectionCount line 1010
157. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.completeness line 1016
158. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_lower_bound line 1038
159. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_real_lower_bound line 1047