OAI/Analysis/Laughlin/FiniteFlux/GramData20.lean

GitHub source file

202 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Certificate.source_error_20_1_1 line 73
  2. theorem OAI.Laughlin.Certificate.source_error_20_1_3 line 84
  3. theorem OAI.Laughlin.Certificate.source_error_20_1_5 line 95
  4. theorem OAI.Laughlin.Certificate.source_error_20_1_7 line 106
  5. theorem OAI.Laughlin.Certificate.source_error_20_1_9 line 117
  6. theorem OAI.Laughlin.Certificate.source_error_20_1_11 line 128
  7. theorem OAI.Laughlin.Certificate.source_error_20_1_13 line 139
  8. theorem OAI.Laughlin.Certificate.source_error_20_1_15 line 150
  9. theorem OAI.Laughlin.Certificate.source_error_20_1_17 line 161
  10. theorem OAI.Laughlin.Certificate.source_error_20_1_19 line 172
  11. theorem OAI.Laughlin.Certificate.source_error_20_3_3 line 183
  12. theorem OAI.Laughlin.Certificate.source_error_20_3_5 line 194
  13. theorem OAI.Laughlin.Certificate.source_error_20_3_7 line 205
  14. theorem OAI.Laughlin.Certificate.source_error_20_3_9 line 216
  15. theorem OAI.Laughlin.Certificate.source_error_20_3_11 line 227
  16. theorem OAI.Laughlin.Certificate.source_error_20_3_13 line 238
  17. theorem OAI.Laughlin.Certificate.source_error_20_3_15 line 249
  18. theorem OAI.Laughlin.Certificate.source_error_20_3_17 line 260
  19. theorem OAI.Laughlin.Certificate.source_error_20_3_19 line 271
  20. theorem OAI.Laughlin.Certificate.source_error_20_5_5 line 282
  21. theorem OAI.Laughlin.Certificate.source_error_20_5_7 line 293
  22. theorem OAI.Laughlin.Certificate.source_error_20_5_9 line 304
  23. theorem OAI.Laughlin.Certificate.source_error_20_5_11 line 315
  24. theorem OAI.Laughlin.Certificate.source_error_20_5_13 line 326
  25. theorem OAI.Laughlin.Certificate.source_error_20_5_15 line 337
  26. theorem OAI.Laughlin.Certificate.source_error_20_5_17 line 348
  27. theorem OAI.Laughlin.Certificate.source_error_20_5_19 line 359
  28. theorem OAI.Laughlin.Certificate.source_error_20_7_7 line 370
  29. theorem OAI.Laughlin.Certificate.source_error_20_7_9 line 381
  30. theorem OAI.Laughlin.Certificate.source_error_20_7_11 line 392
  31. theorem OAI.Laughlin.Certificate.source_error_20_7_13 line 403
  32. theorem OAI.Laughlin.Certificate.source_error_20_7_15 line 414
  33. theorem OAI.Laughlin.Certificate.source_error_20_7_17 line 425
  34. theorem OAI.Laughlin.Certificate.source_error_20_7_19 line 436
  35. theorem OAI.Laughlin.Certificate.source_error_20_9_9 line 447
  36. theorem OAI.Laughlin.Certificate.source_error_20_9_11 line 458
  37. theorem OAI.Laughlin.Certificate.source_error_20_9_13 line 469
  38. theorem OAI.Laughlin.Certificate.source_error_20_9_15 line 480
  39. theorem OAI.Laughlin.Certificate.source_error_20_9_17 line 491
  40. theorem OAI.Laughlin.Certificate.source_error_20_9_19 line 502
  41. theorem OAI.Laughlin.Certificate.source_error_20_11_11 line 513
  42. theorem OAI.Laughlin.Certificate.source_error_20_11_13 line 524
  43. theorem OAI.Laughlin.Certificate.source_error_20_11_15 line 535
  44. theorem OAI.Laughlin.Certificate.source_error_20_11_17 line 546
  45. theorem OAI.Laughlin.Certificate.source_error_20_11_19 line 557
  46. theorem OAI.Laughlin.Certificate.source_error_20_13_13 line 568
  47. theorem OAI.Laughlin.Certificate.source_error_20_13_15 line 579
  48. theorem OAI.Laughlin.Certificate.source_error_20_13_17 line 590
  49. theorem OAI.Laughlin.Certificate.source_error_20_13_19 line 601
  50. theorem OAI.Laughlin.Certificate.source_error_20_15_15 line 612
  51. theorem OAI.Laughlin.Certificate.source_error_20_15_17 line 623
  52. theorem OAI.Laughlin.Certificate.source_error_20_15_19 line 634
  53. theorem OAI.Laughlin.Certificate.source_error_20_17_17 line 645
  54. theorem OAI.Laughlin.Certificate.source_error_20_17_19 line 656
  55. theorem OAI.Laughlin.Certificate.source_error_20_19_19 line 667
  56. theorem OAI.Laughlin.Certificate.source_gram_20_1_1 line 678
  57. theorem OAI.Laughlin.Certificate.source_gram_20_1_3 line 682
  58. theorem OAI.Laughlin.Certificate.source_gram_20_1_5 line 686
  59. theorem OAI.Laughlin.Certificate.source_gram_20_1_7 line 690
  60. theorem OAI.Laughlin.Certificate.source_gram_20_1_9 line 694
  61. theorem OAI.Laughlin.Certificate.source_gram_20_1_11 line 698
  62. theorem OAI.Laughlin.Certificate.source_gram_20_1_13 line 702
  63. theorem OAI.Laughlin.Certificate.source_gram_20_1_15 line 706
  64. theorem OAI.Laughlin.Certificate.source_gram_20_1_17 line 710
  65. theorem OAI.Laughlin.Certificate.source_gram_20_1_19 line 714
  66. theorem OAI.Laughlin.Certificate.source_gram_20_3_3 line 718
  67. theorem OAI.Laughlin.Certificate.source_gram_20_3_5 line 722
  68. theorem OAI.Laughlin.Certificate.source_gram_20_3_7 line 726
  69. theorem OAI.Laughlin.Certificate.source_gram_20_3_9 line 730
  70. theorem OAI.Laughlin.Certificate.source_gram_20_3_11 line 734
  71. theorem OAI.Laughlin.Certificate.source_gram_20_3_13 line 738
  72. theorem OAI.Laughlin.Certificate.source_gram_20_3_15 line 742
  73. theorem OAI.Laughlin.Certificate.source_gram_20_3_17 line 746
  74. theorem OAI.Laughlin.Certificate.source_gram_20_3_19 line 750
  75. theorem OAI.Laughlin.Certificate.source_gram_20_5_5 line 754
  76. theorem OAI.Laughlin.Certificate.source_gram_20_5_7 line 758
  77. theorem OAI.Laughlin.Certificate.source_gram_20_5_9 line 762
  78. theorem OAI.Laughlin.Certificate.source_gram_20_5_11 line 766
  79. theorem OAI.Laughlin.Certificate.source_gram_20_5_13 line 770
  80. theorem OAI.Laughlin.Certificate.source_gram_20_5_15 line 774
  81. theorem OAI.Laughlin.Certificate.source_gram_20_5_17 line 778
  82. theorem OAI.Laughlin.Certificate.source_gram_20_5_19 line 782
  83. theorem OAI.Laughlin.Certificate.source_gram_20_7_7 line 786
  84. theorem OAI.Laughlin.Certificate.source_gram_20_7_9 line 790
  85. theorem OAI.Laughlin.Certificate.source_gram_20_7_11 line 794
  86. theorem OAI.Laughlin.Certificate.source_gram_20_7_13 line 798
  87. theorem OAI.Laughlin.Certificate.source_gram_20_7_15 line 802
  88. theorem OAI.Laughlin.Certificate.source_gram_20_7_17 line 806
  89. theorem OAI.Laughlin.Certificate.source_gram_20_7_19 line 810
  90. theorem OAI.Laughlin.Certificate.source_gram_20_9_9 line 814
  91. theorem OAI.Laughlin.Certificate.source_gram_20_9_11 line 818
  92. theorem OAI.Laughlin.Certificate.source_gram_20_9_13 line 822
  93. theorem OAI.Laughlin.Certificate.source_gram_20_9_15 line 826
  94. theorem OAI.Laughlin.Certificate.source_gram_20_9_17 line 830
  95. theorem OAI.Laughlin.Certificate.source_gram_20_9_19 line 834
  96. theorem OAI.Laughlin.Certificate.source_gram_20_11_11 line 838
  97. theorem OAI.Laughlin.Certificate.source_gram_20_11_13 line 842
  98. theorem OAI.Laughlin.Certificate.source_gram_20_11_15 line 846
  99. theorem OAI.Laughlin.Certificate.source_gram_20_11_17 line 850
  100. theorem OAI.Laughlin.Certificate.source_gram_20_11_19 line 854
  101. theorem OAI.Laughlin.Certificate.source_gram_20_13_13 line 858
  102. theorem OAI.Laughlin.Certificate.source_gram_20_13_15 line 862
  103. theorem OAI.Laughlin.Certificate.source_gram_20_13_17 line 866
  104. theorem OAI.Laughlin.Certificate.source_gram_20_13_19 line 870
  105. theorem OAI.Laughlin.Certificate.source_gram_20_15_15 line 874
  106. theorem OAI.Laughlin.Certificate.source_gram_20_15_17 line 878
  107. theorem OAI.Laughlin.Certificate.source_gram_20_15_19 line 882
  108. theorem OAI.Laughlin.Certificate.source_gram_20_17_17 line 886
  109. theorem OAI.Laughlin.Certificate.source_gram_20_17_19 line 890
  110. theorem OAI.Laughlin.Certificate.source_gram_20_19_19 line 894
  111. theorem OAI.Laughlin.Certificate.source_error_20_3_1 line 898
  112. theorem OAI.Laughlin.Certificate.source_gram_20_3_1 line 902
  113. theorem OAI.Laughlin.Certificate.source_error_20_5_1 line 906
  114. theorem OAI.Laughlin.Certificate.source_gram_20_5_1 line 910
  115. theorem OAI.Laughlin.Certificate.source_error_20_5_3 line 914
  116. theorem OAI.Laughlin.Certificate.source_gram_20_5_3 line 918
  117. theorem OAI.Laughlin.Certificate.source_error_20_7_1 line 922
  118. theorem OAI.Laughlin.Certificate.source_gram_20_7_1 line 926
  119. theorem OAI.Laughlin.Certificate.source_error_20_7_3 line 930
  120. theorem OAI.Laughlin.Certificate.source_gram_20_7_3 line 934
  121. theorem OAI.Laughlin.Certificate.source_error_20_7_5 line 938
  122. theorem OAI.Laughlin.Certificate.source_gram_20_7_5 line 942
  123. theorem OAI.Laughlin.Certificate.source_error_20_9_1 line 946
  124. theorem OAI.Laughlin.Certificate.source_gram_20_9_1 line 950
  125. theorem OAI.Laughlin.Certificate.source_error_20_9_3 line 954
  126. theorem OAI.Laughlin.Certificate.source_gram_20_9_3 line 958
  127. theorem OAI.Laughlin.Certificate.source_error_20_9_5 line 962
  128. theorem OAI.Laughlin.Certificate.source_gram_20_9_5 line 966
  129. theorem OAI.Laughlin.Certificate.source_error_20_9_7 line 970
  130. theorem OAI.Laughlin.Certificate.source_gram_20_9_7 line 974
  131. theorem OAI.Laughlin.Certificate.source_error_20_11_1 line 978
  132. theorem OAI.Laughlin.Certificate.source_gram_20_11_1 line 982
  133. theorem OAI.Laughlin.Certificate.source_error_20_11_3 line 986
  134. theorem OAI.Laughlin.Certificate.source_gram_20_11_3 line 990
  135. theorem OAI.Laughlin.Certificate.source_error_20_11_5 line 994
  136. theorem OAI.Laughlin.Certificate.source_gram_20_11_5 line 998
  137. theorem OAI.Laughlin.Certificate.source_error_20_11_7 line 1002
  138. theorem OAI.Laughlin.Certificate.source_gram_20_11_7 line 1006
  139. theorem OAI.Laughlin.Certificate.source_error_20_11_9 line 1010
  140. theorem OAI.Laughlin.Certificate.source_gram_20_11_9 line 1014
  141. theorem OAI.Laughlin.Certificate.source_error_20_13_1 line 1018
  142. theorem OAI.Laughlin.Certificate.source_gram_20_13_1 line 1022
  143. theorem OAI.Laughlin.Certificate.source_error_20_13_3 line 1026
  144. theorem OAI.Laughlin.Certificate.source_gram_20_13_3 line 1030
  145. theorem OAI.Laughlin.Certificate.source_error_20_13_5 line 1034
  146. theorem OAI.Laughlin.Certificate.source_gram_20_13_5 line 1038
  147. theorem OAI.Laughlin.Certificate.source_error_20_13_7 line 1042
  148. theorem OAI.Laughlin.Certificate.source_gram_20_13_7 line 1046
  149. theorem OAI.Laughlin.Certificate.source_error_20_13_9 line 1050
  150. theorem OAI.Laughlin.Certificate.source_gram_20_13_9 line 1054
  151. theorem OAI.Laughlin.Certificate.source_error_20_13_11 line 1058
  152. theorem OAI.Laughlin.Certificate.source_gram_20_13_11 line 1062
  153. theorem OAI.Laughlin.Certificate.source_error_20_15_1 line 1066
  154. theorem OAI.Laughlin.Certificate.source_gram_20_15_1 line 1070
  155. theorem OAI.Laughlin.Certificate.source_error_20_15_3 line 1074
  156. theorem OAI.Laughlin.Certificate.source_gram_20_15_3 line 1078
  157. theorem OAI.Laughlin.Certificate.source_error_20_15_5 line 1082
  158. theorem OAI.Laughlin.Certificate.source_gram_20_15_5 line 1086
  159. theorem OAI.Laughlin.Certificate.source_error_20_15_7 line 1090
  160. theorem OAI.Laughlin.Certificate.source_gram_20_15_7 line 1094
  161. theorem OAI.Laughlin.Certificate.source_error_20_15_9 line 1098
  162. theorem OAI.Laughlin.Certificate.source_gram_20_15_9 line 1102
  163. theorem OAI.Laughlin.Certificate.source_error_20_15_11 line 1106
  164. theorem OAI.Laughlin.Certificate.source_gram_20_15_11 line 1110
  165. theorem OAI.Laughlin.Certificate.source_error_20_15_13 line 1114
  166. theorem OAI.Laughlin.Certificate.source_gram_20_15_13 line 1118
  167. theorem OAI.Laughlin.Certificate.source_error_20_17_1 line 1122
  168. theorem OAI.Laughlin.Certificate.source_gram_20_17_1 line 1126
  169. theorem OAI.Laughlin.Certificate.source_error_20_17_3 line 1130
  170. theorem OAI.Laughlin.Certificate.source_gram_20_17_3 line 1134
  171. theorem OAI.Laughlin.Certificate.source_error_20_17_5 line 1138
  172. theorem OAI.Laughlin.Certificate.source_gram_20_17_5 line 1142
  173. theorem OAI.Laughlin.Certificate.source_error_20_17_7 line 1146
  174. theorem OAI.Laughlin.Certificate.source_gram_20_17_7 line 1150
  175. theorem OAI.Laughlin.Certificate.source_error_20_17_9 line 1154
  176. theorem OAI.Laughlin.Certificate.source_gram_20_17_9 line 1158
  177. theorem OAI.Laughlin.Certificate.source_error_20_17_11 line 1162
  178. theorem OAI.Laughlin.Certificate.source_gram_20_17_11 line 1166
  179. theorem OAI.Laughlin.Certificate.source_error_20_17_13 line 1170
  180. theorem OAI.Laughlin.Certificate.source_gram_20_17_13 line 1174
  181. theorem OAI.Laughlin.Certificate.source_error_20_17_15 line 1178
  182. theorem OAI.Laughlin.Certificate.source_gram_20_17_15 line 1182
  183. theorem OAI.Laughlin.Certificate.source_error_20_19_1 line 1186
  184. theorem OAI.Laughlin.Certificate.source_gram_20_19_1 line 1190
  185. theorem OAI.Laughlin.Certificate.source_error_20_19_3 line 1194
  186. theorem OAI.Laughlin.Certificate.source_gram_20_19_3 line 1198
  187. theorem OAI.Laughlin.Certificate.source_error_20_19_5 line 1202
  188. theorem OAI.Laughlin.Certificate.source_gram_20_19_5 line 1206
  189. theorem OAI.Laughlin.Certificate.source_error_20_19_7 line 1210
  190. theorem OAI.Laughlin.Certificate.source_gram_20_19_7 line 1214
  191. theorem OAI.Laughlin.Certificate.source_error_20_19_9 line 1218
  192. theorem OAI.Laughlin.Certificate.source_gram_20_19_9 line 1222
  193. theorem OAI.Laughlin.Certificate.source_error_20_19_11 line 1226
  194. theorem OAI.Laughlin.Certificate.source_gram_20_19_11 line 1230
  195. theorem OAI.Laughlin.Certificate.source_error_20_19_13 line 1234
  196. theorem OAI.Laughlin.Certificate.source_gram_20_19_13 line 1238
  197. theorem OAI.Laughlin.Certificate.source_error_20_19_15 line 1242
  198. theorem OAI.Laughlin.Certificate.source_gram_20_19_15 line 1246
  199. theorem OAI.Laughlin.Certificate.source_error_20_19_17 line 1250
  200. theorem OAI.Laughlin.Certificate.source_gram_20_19_17 line 1254
  201. theorem OAI.Laughlin.Certificate.error_20 line 1258
  202. theorem OAI.Laughlin.Certificate.gram_20 line 1362