OAI/Computability/BinPacking/PCP/PoweringTableSemantics.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.PoweringReach.ReachLE line 13
2. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReach.reach_refl line 16
3. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReach.reach_mono line 19
4. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReach.reach_prepend line 24
5. def OAI.BinPackingGames.Foundations.PCP.PoweringReach.reversePorts line 31
6. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReach.reversePorts_length line 35
7. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReach.walkEnd_reversePorts line 41
8. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReach.wordEnd_eq_walkEnd_ofFn line 52
9. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReach.reach_reverse line 62
10. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReach.tail_reach line 74
11. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReach.head_reach_endpoint line 88
12. def OAI.BinPackingGames.Foundations.PCP.PoweringReach.tailFromStart line 102
13. def OAI.BinPackingGames.Foundations.PCP.PoweringReach.headFromEnd line 106
14. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReach.tailFromStart_val line 110
15. theorem OAI.BinPackingGames.Foundations.PCP.PoweringReach.headFromEnd_val line 114
16. def OAI.BinPackingGames.Foundations.PCP.PoweringOpinions.opinionAt line 129
17. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinions.opinionAt_eq_decode line 136
18. def OAI.BinPackingGames.Foundations.PCP.PoweringOpinions.honestLabels line 144
19. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinions.opinionAt_honest line 147
20. def OAI.BinPackingGames.Foundations.PCP.PoweringOpinions.sampleOpinion line 157
21. def OAI.BinPackingGames.Foundations.PCP.PoweringOpinions.decoded line 162
22. def OAI.BinPackingGames.Foundations.PCP.PoweringOpinions.matchFn line 167
23. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinions.matchFn_mem_Icc line 173
24. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinions.decoded_modal_baseline line 183
25. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinions.decoded_modal_near line 193
26. def OAI.BinPackingGames.Foundations.PCP.PoweringTest.baseGraph line 220
27. def OAI.BinPackingGames.Foundations.PCP.PoweringTest.pathAccepts line 229
28. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.pathAccepts_eq_true_iff line 237
29. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringTest.Dart line 248
30. def OAI.BinPackingGames.Foundations.PCP.PoweringTest.reverseDart line 250
31. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.reverseDart_involutive line 260
32. def OAI.BinPackingGames.Foundations.PCP.PoweringTest.poweredGraph line 265
33. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.poweredGraph_tail_false line 277
34. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.poweredGraph_tail_true line 282
35. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.poweredGraph_edgeSatisfied line 287
36. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.rejection_mean_eq_path_mean line 296
37. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.pathAccepts_honest line 307
38. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.perfect_completeness line 321
39. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.preserves_satisfiability line 332
40. def OAI.BinPackingGames.Foundations.PCP.PoweringTest.decodedBad line 344
41. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.decodedBad_eq_true_iff line 348
42. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.decodedBad_rot line 354
43. def OAI.BinPackingGames.Foundations.PCP.PoweringTest.witness line 363
44. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.witness_bad line 375
45. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.witness_implies_path_rejection line 383
46. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTest.witness_implies_rejection line 410
47. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.match_in_tail line 430
48. def OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.firstIndex line 437
49. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.get_firstIndex line 444
50. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.firstIndex_matches line 457
51. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.firstIndex_is_first line 462
52. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.AddressIndex line 478
53. def OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.addressIndex line 482
54. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.addressIndex_get line 489
55. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.addressIndex_matches line 498
56. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.addressIndex_is_first line 504
57. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.addressIndex_lt line 510
58. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.LabelTable line 516
59. def OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.labelTable line 518
60. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.labelTable_get line 521
61. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.labelTable_addressIndex line 526
62. structure OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.WalkOpinionRow line 533
63. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.WalkRows line 538
64. def OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.walkRows line 540
65. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.walkRows_edge line 547
66. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.walkRows_tail_value line 552
67. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.walkRows_head_value line 560
68. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.walkRows_length line 568
69. def OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.rowsAccepts line 573
70. theorem OAI.BinPackingGames.Foundations.PCP.PoweringOpinionTables.rowsAccepts_walkRows line 578
71. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.constraint_rejection_mean_eq_count line 597
72. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.constraint_rejection_lower_iff line 612
73. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.edgeDensity_eq_bit_mean line 621
74. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.base_edgeDensity_eq_rejection_count line 635
75. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.base_count_lower_to_density line 653
76. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.powered_rejection_mean_eq_count line 663
77. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.path_rejection_mean_eq_count line 673
78. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.powered_density_lower_to_count line 684
79. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.natCard_dart line 696
80. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.fintypeCard_dart line 700
81. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.natCard_poweredAlphabet line 705
82. theorem OAI.BinPackingGames.Foundations.PCP.PoweringCounting.natCard_finitePortAlphabet line 710
83. def OAI.BinPackingGames.Foundations.PCP.PoweringTables.labelCount line 722
84. def OAI.BinPackingGames.Foundations.PCP.PoweringTables.dartCount line 724
85. def OAI.BinPackingGames.Foundations.PCP.PoweringTables.mathematicalGraph line 726
86. def OAI.BinPackingGames.Foundations.PCP.PoweringTables.rowAccepts line 732
87. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTables.rowAccepts_eq line 741
88. def OAI.BinPackingGames.Foundations.PCP.PoweringTables.table line 751
89. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTables.table_vertices line 756
90. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTables.table_darts line 759
91. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTables.semantics_table line 762
92. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTables.table_accepts line 768
93. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTables.table_reverse line 776
94. def OAI.BinPackingGames.Foundations.PCP.PoweringTables.outputBits line 788
95. def OAI.BinPackingGames.Foundations.PCP.PoweringTables.transform line 791
96. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.RawLabeling line 800
97. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling line 803
98. def OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling line 806
99. def OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling line 810
100. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling_encodeLabeling line 814
101. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling_decodeLabeling line 820
102. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_encoded line 826
103. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_decoded line 838
104. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_eq_path line 847
105. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_encoded line 862
106. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_decoded line 872
107. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.card_darts_eq_table line 880
108. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.satisfiable_iff line 887
109. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.preserves_satisfiability line 904
110. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.path_rejection_mean_eq_table_fraction line 912
111. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap_iff line 927
112. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap line 946