OAI/Computability/DirectedFeedback/Machines/ContextLoad.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.Tape line 12
2. inductive OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.Label line 19
3. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.place line 28
4. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.fill line 32
5. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.fill_place line 39
6. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.fill_self line 44
7. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.fill_update line 54
8. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.placedLabel line 63
9. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.placedConfiguration line 67
10. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.placedStatement line 73
11. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.placed_stepAux line 85
12. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.nextLabel line 110
13. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.program line 113
14. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.placed_step line 124
15. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.lookupOutput line 141
16. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.placedLookupInTime line 146
17. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.copiedTapes line 162
18. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.coordinateOutput line 165
19. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.cleanup_lookupOutput line 173
20. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_current line 202
21. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_remaining line 207
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_field line 212
23. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_other_field line 219
24. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.suffix_length_le_input line 224
25. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.coordinateInTime line 236
26. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.labelAt line 281
27. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.nextLabel_eq line 284
28. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.stageTapes line 286
29. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.stageTapes_frame line 294
30. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.stageTapes_clean line 307
31. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.stageTapes_field line 319
32. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.prefixInTime line 344
33. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.loadInTime line 387
34. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.clauses_length_le_input line 410
35. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.loadUnaryInTime line 415
36. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.timePolynomial line 438
37. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.timePolynomial_eval line 441
38. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.variableSlot line 447
39. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.polaritySlot line 448
40. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.variableField line 449
41. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.polarityField line 450
42. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.clauseWords_variable line 452
43. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.clauseWords_polarity line 458
44. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.output_variable line 466
45. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.output_polarity line 473
46. def OAI.DFVSGames.Foundations.Hastad.SourceContextLoad.machine line 482
47. abbrev OAI.DFVSGames.Foundations.Hastad.Cube line 503
48. def OAI.DFVSGames.Foundations.Hastad.bitSign line 505
49. theorem OAI.DFVSGames.Foundations.Hastad.bitSign_sq line 507
50. theorem OAI.DFVSGames.Foundations.Hastad.bitSign_xor line 510
51. def OAI.DFVSGames.Foundations.Hastad.cubeXor line 514
52. def OAI.DFVSGames.Foundations.Hastad.walsh line 516
53. theorem OAI.DFVSGames.Foundations.Hastad.walsh_symm line 519
54. theorem OAI.DFVSGames.Foundations.Hastad.walsh_sq line 523
55. theorem OAI.DFVSGames.Foundations.Hastad.walsh_xor line 527
56. theorem OAI.DFVSGames.Foundations.Hastad.coordinate_orthogonality line 535
57. theorem OAI.DFVSGames.Foundations.Hastad.walsh_sum_orthogonality line 540
58. theorem OAI.DFVSGames.Foundations.Hastad.walsh_orthogonality line 557
59. def OAI.DFVSGames.Foundations.Hastad.coefficient line 564
60. theorem OAI.DFVSGames.Foundations.Hastad.walsh_inversion line 567
61. theorem OAI.DFVSGames.Foundations.Hastad.walsh_inner line 584
62. theorem OAI.DFVSGames.Foundations.Hastad.walsh_parseval line 601
63. theorem OAI.DFVSGames.Foundations.Hastad.sign_parseval line 605
64. def OAI.DFVSGames.Foundations.Hastad.support line 623
65. def OAI.DFVSGames.Foundations.Hastad.noiseWeight line 625
66. theorem OAI.DFVSGames.Foundations.Hastad.noiseWeight_nonneg line 629
67. theorem OAI.DFVSGames.Foundations.Hastad.noiseWeight_sum line 635
68. theorem OAI.DFVSGames.Foundations.Hastad.noise_walsh line 640
69. def OAI.DFVSGames.Foundations.Hastad.thirdQuery line 653
70. theorem OAI.DFVSGames.Foundations.Hastad.walsh_autocorrelation line 656
71. def OAI.DFVSGames.Foundations.Hastad.projectedCoefficient line 674
72. def OAI.DFVSGames.Foundations.Hastad.testBias line 677
73. theorem OAI.DFVSGames.Foundations.Hastad.testBias_fourier line 681
74. def OAI.DFVSGames.Foundations.Hastad.testAcceptance line 709
75. theorem OAI.DFVSGames.Foundations.Hastad.threeBit_indicator line 714
76. theorem OAI.DFVSGames.Foundations.Hastad.testAcceptance_eq line 719
77. def OAI.DFVSGames.Foundations.Hastad.cubeFlip line 751
78. theorem OAI.DFVSGames.Foundations.Hastad.cubeFlip_cubeFlip line 754
79. theorem OAI.DFVSGames.Foundations.Hastad.bitSign_not line 758
80. theorem OAI.DFVSGames.Foundations.Hastad.sum_cubeFlip line 761
81. theorem OAI.DFVSGames.Foundations.Hastad.coefficient_zero_of_odd line 773
82. theorem OAI.DFVSGames.Foundations.Hastad.coefficient_sign_zero_of_folded line 782
83. def OAI.DFVSGames.Foundations.Hastad.representative line 789
84. theorem OAI.DFVSGames.Foundations.Hastad.representative_at line 793
85. theorem OAI.DFVSGames.Foundations.Hastad.representative_flip line 798
86. abbrev OAI.DFVSGames.Foundations.Hastad.HalfCube line 802
87. def OAI.DFVSGames.Foundations.Hastad.canonicalInput line 804
88. theorem OAI.DFVSGames.Foundations.Hastad.canonicalInput_flip line 808
89. def OAI.DFVSGames.Foundations.Hastad.foldedAnswer line 813
90. theorem OAI.DFVSGames.Foundations.Hastad.foldedAnswer_flip line 817
91. theorem OAI.DFVSGames.Foundations.Hastad.foldedAnswer_zero_coefficient line 825
92. theorem OAI.DFVSGames.Foundations.Hastad.foldedAnswer_dictator line 830
93. def OAI.DFVSGames.Foundations.Hastad.coordinateMask line 835
94. def OAI.DFVSGames.Foundations.Hastad.cubeToggle line 837
95. theorem OAI.DFVSGames.Foundations.Hastad.cubeToggle_twice line 841
96. theorem OAI.DFVSGames.Foundations.Hastad.walsh_coordinateMask line 847
97. theorem OAI.DFVSGames.Foundations.Hastad.walsh_cubeToggle line 857
98. theorem OAI.DFVSGames.Foundations.Hastad.sum_cubeToggle line 862
99. def OAI.DFVSGames.Foundations.Hastad.restrictQuery line 875
100. theorem OAI.DFVSGames.Foundations.Hastad.restrictQuery_cubeToggle line 879
101. theorem OAI.DFVSGames.Foundations.Hastad.conditioned_coefficient_zero_invalid line 890
102. theorem OAI.DFVSGames.Foundations.Hastad.conditioned_coefficient_support line 900
103. def OAI.DFVSGames.Foundations.Hastad.conditionedFoldedAnswer line 910
104. theorem OAI.DFVSGames.Foundations.Hastad.conditionedFoldedAnswer_flip line 915
105. theorem OAI.DFVSGames.Foundations.Hastad.conditionedFoldedAnswer_zero_coefficient line 922
106. theorem OAI.DFVSGames.Foundations.Hastad.conditionedFoldedAnswer_dictator line 929