OAI/Analysis/Laughlin/FiniteFlux/GramData21.lean

GitHub source file

244 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Laughlin.Certificate.source_error_21_1_1 line 85
2. theorem OAI.Laughlin.Certificate.source_error_21_1_3 line 96
3. theorem OAI.Laughlin.Certificate.source_error_21_1_5 line 107
4. theorem OAI.Laughlin.Certificate.source_error_21_1_7 line 118
5. theorem OAI.Laughlin.Certificate.source_error_21_1_9 line 129
6. theorem OAI.Laughlin.Certificate.source_error_21_1_11 line 140
7. theorem OAI.Laughlin.Certificate.source_error_21_1_13 line 151
8. theorem OAI.Laughlin.Certificate.source_error_21_1_15 line 162
9. theorem OAI.Laughlin.Certificate.source_error_21_1_17 line 173
10. theorem OAI.Laughlin.Certificate.source_error_21_1_19 line 184
11. theorem OAI.Laughlin.Certificate.source_error_21_1_21 line 195
12. theorem OAI.Laughlin.Certificate.source_error_21_3_3 line 206
13. theorem OAI.Laughlin.Certificate.source_error_21_3_5 line 217
14. theorem OAI.Laughlin.Certificate.source_error_21_3_7 line 228
15. theorem OAI.Laughlin.Certificate.source_error_21_3_9 line 239
16. theorem OAI.Laughlin.Certificate.source_error_21_3_11 line 250
17. theorem OAI.Laughlin.Certificate.source_error_21_3_13 line 261
18. theorem OAI.Laughlin.Certificate.source_error_21_3_15 line 272
19. theorem OAI.Laughlin.Certificate.source_error_21_3_17 line 283
20. theorem OAI.Laughlin.Certificate.source_error_21_3_19 line 294
21. theorem OAI.Laughlin.Certificate.source_error_21_3_21 line 305
22. theorem OAI.Laughlin.Certificate.source_error_21_5_5 line 316
23. theorem OAI.Laughlin.Certificate.source_error_21_5_7 line 327
24. theorem OAI.Laughlin.Certificate.source_error_21_5_9 line 338
25. theorem OAI.Laughlin.Certificate.source_error_21_5_11 line 349
26. theorem OAI.Laughlin.Certificate.source_error_21_5_13 line 360
27. theorem OAI.Laughlin.Certificate.source_error_21_5_15 line 371
28. theorem OAI.Laughlin.Certificate.source_error_21_5_17 line 382
29. theorem OAI.Laughlin.Certificate.source_error_21_5_19 line 393
30. theorem OAI.Laughlin.Certificate.source_error_21_5_21 line 404
31. theorem OAI.Laughlin.Certificate.source_error_21_7_7 line 415
32. theorem OAI.Laughlin.Certificate.source_error_21_7_9 line 426
33. theorem OAI.Laughlin.Certificate.source_error_21_7_11 line 437
34. theorem OAI.Laughlin.Certificate.source_error_21_7_13 line 448
35. theorem OAI.Laughlin.Certificate.source_error_21_7_15 line 459
36. theorem OAI.Laughlin.Certificate.source_error_21_7_17 line 470
37. theorem OAI.Laughlin.Certificate.source_error_21_7_19 line 481
38. theorem OAI.Laughlin.Certificate.source_error_21_7_21 line 492
39. theorem OAI.Laughlin.Certificate.source_error_21_9_9 line 503
40. theorem OAI.Laughlin.Certificate.source_error_21_9_11 line 514
41. theorem OAI.Laughlin.Certificate.source_error_21_9_13 line 525
42. theorem OAI.Laughlin.Certificate.source_error_21_9_15 line 536
43. theorem OAI.Laughlin.Certificate.source_error_21_9_17 line 547
44. theorem OAI.Laughlin.Certificate.source_error_21_9_19 line 558
45. theorem OAI.Laughlin.Certificate.source_error_21_9_21 line 569
46. theorem OAI.Laughlin.Certificate.source_error_21_11_11 line 580
47. theorem OAI.Laughlin.Certificate.source_error_21_11_13 line 591
48. theorem OAI.Laughlin.Certificate.source_error_21_11_15 line 602
49. theorem OAI.Laughlin.Certificate.source_error_21_11_17 line 613
50. theorem OAI.Laughlin.Certificate.source_error_21_11_19 line 624
51. theorem OAI.Laughlin.Certificate.source_error_21_11_21 line 635
52. theorem OAI.Laughlin.Certificate.source_error_21_13_13 line 646
53. theorem OAI.Laughlin.Certificate.source_error_21_13_15 line 657
54. theorem OAI.Laughlin.Certificate.source_error_21_13_17 line 668
55. theorem OAI.Laughlin.Certificate.source_error_21_13_19 line 679
56. theorem OAI.Laughlin.Certificate.source_error_21_13_21 line 690
57. theorem OAI.Laughlin.Certificate.source_error_21_15_15 line 701
58. theorem OAI.Laughlin.Certificate.source_error_21_15_17 line 712
59. theorem OAI.Laughlin.Certificate.source_error_21_15_19 line 723
60. theorem OAI.Laughlin.Certificate.source_error_21_15_21 line 734
61. theorem OAI.Laughlin.Certificate.source_error_21_17_17 line 745
62. theorem OAI.Laughlin.Certificate.source_error_21_17_19 line 756
63. theorem OAI.Laughlin.Certificate.source_error_21_17_21 line 767
64. theorem OAI.Laughlin.Certificate.source_error_21_19_19 line 778
65. theorem OAI.Laughlin.Certificate.source_error_21_19_21 line 789
66. theorem OAI.Laughlin.Certificate.source_error_21_21_21 line 800
67. theorem OAI.Laughlin.Certificate.source_gram_21_1_1 line 811
68. theorem OAI.Laughlin.Certificate.source_gram_21_1_3 line 815
69. theorem OAI.Laughlin.Certificate.source_gram_21_1_5 line 819
70. theorem OAI.Laughlin.Certificate.source_gram_21_1_7 line 823
71. theorem OAI.Laughlin.Certificate.source_gram_21_1_9 line 827
72. theorem OAI.Laughlin.Certificate.source_gram_21_1_11 line 831
73. theorem OAI.Laughlin.Certificate.source_gram_21_1_13 line 835
74. theorem OAI.Laughlin.Certificate.source_gram_21_1_15 line 839
75. theorem OAI.Laughlin.Certificate.source_gram_21_1_17 line 843
76. theorem OAI.Laughlin.Certificate.source_gram_21_1_19 line 847
77. theorem OAI.Laughlin.Certificate.source_gram_21_1_21 line 851
78. theorem OAI.Laughlin.Certificate.source_gram_21_3_3 line 855
79. theorem OAI.Laughlin.Certificate.source_gram_21_3_5 line 859
80. theorem OAI.Laughlin.Certificate.source_gram_21_3_7 line 863
81. theorem OAI.Laughlin.Certificate.source_gram_21_3_9 line 867
82. theorem OAI.Laughlin.Certificate.source_gram_21_3_11 line 871
83. theorem OAI.Laughlin.Certificate.source_gram_21_3_13 line 875
84. theorem OAI.Laughlin.Certificate.source_gram_21_3_15 line 879
85. theorem OAI.Laughlin.Certificate.source_gram_21_3_17 line 883
86. theorem OAI.Laughlin.Certificate.source_gram_21_3_19 line 887
87. theorem OAI.Laughlin.Certificate.source_gram_21_3_21 line 891
88. theorem OAI.Laughlin.Certificate.source_gram_21_5_5 line 895
89. theorem OAI.Laughlin.Certificate.source_gram_21_5_7 line 899
90. theorem OAI.Laughlin.Certificate.source_gram_21_5_9 line 903
91. theorem OAI.Laughlin.Certificate.source_gram_21_5_11 line 907
92. theorem OAI.Laughlin.Certificate.source_gram_21_5_13 line 911
93. theorem OAI.Laughlin.Certificate.source_gram_21_5_15 line 915
94. theorem OAI.Laughlin.Certificate.source_gram_21_5_17 line 919
95. theorem OAI.Laughlin.Certificate.source_gram_21_5_19 line 923
96. theorem OAI.Laughlin.Certificate.source_gram_21_5_21 line 927
97. theorem OAI.Laughlin.Certificate.source_gram_21_7_7 line 931
98. theorem OAI.Laughlin.Certificate.source_gram_21_7_9 line 935
99. theorem OAI.Laughlin.Certificate.source_gram_21_7_11 line 939
100. theorem OAI.Laughlin.Certificate.source_gram_21_7_13 line 943
101. theorem OAI.Laughlin.Certificate.source_gram_21_7_15 line 947
102. theorem OAI.Laughlin.Certificate.source_gram_21_7_17 line 951
103. theorem OAI.Laughlin.Certificate.source_gram_21_7_19 line 955
104. theorem OAI.Laughlin.Certificate.source_gram_21_7_21 line 959
105. theorem OAI.Laughlin.Certificate.source_gram_21_9_9 line 963
106. theorem OAI.Laughlin.Certificate.source_gram_21_9_11 line 967
107. theorem OAI.Laughlin.Certificate.source_gram_21_9_13 line 971
108. theorem OAI.Laughlin.Certificate.source_gram_21_9_15 line 975
109. theorem OAI.Laughlin.Certificate.source_gram_21_9_17 line 979
110. theorem OAI.Laughlin.Certificate.source_gram_21_9_19 line 983
111. theorem OAI.Laughlin.Certificate.source_gram_21_9_21 line 987
112. theorem OAI.Laughlin.Certificate.source_gram_21_11_11 line 991
113. theorem OAI.Laughlin.Certificate.source_gram_21_11_13 line 995
114. theorem OAI.Laughlin.Certificate.source_gram_21_11_15 line 999
115. theorem OAI.Laughlin.Certificate.source_gram_21_11_17 line 1003
116. theorem OAI.Laughlin.Certificate.source_gram_21_11_19 line 1007
117. theorem OAI.Laughlin.Certificate.source_gram_21_11_21 line 1011
118. theorem OAI.Laughlin.Certificate.source_gram_21_13_13 line 1015
119. theorem OAI.Laughlin.Certificate.source_gram_21_13_15 line 1019
120. theorem OAI.Laughlin.Certificate.source_gram_21_13_17 line 1023
121. theorem OAI.Laughlin.Certificate.source_gram_21_13_19 line 1027
122. theorem OAI.Laughlin.Certificate.source_gram_21_13_21 line 1031
123. theorem OAI.Laughlin.Certificate.source_gram_21_15_15 line 1035
124. theorem OAI.Laughlin.Certificate.source_gram_21_15_17 line 1039
125. theorem OAI.Laughlin.Certificate.source_gram_21_15_19 line 1043
126. theorem OAI.Laughlin.Certificate.source_gram_21_15_21 line 1047
127. theorem OAI.Laughlin.Certificate.source_gram_21_17_17 line 1051
128. theorem OAI.Laughlin.Certificate.source_gram_21_17_19 line 1055
129. theorem OAI.Laughlin.Certificate.source_gram_21_17_21 line 1059
130. theorem OAI.Laughlin.Certificate.source_gram_21_19_19 line 1063
131. theorem OAI.Laughlin.Certificate.source_gram_21_19_21 line 1067
132. theorem OAI.Laughlin.Certificate.source_gram_21_21_21 line 1071
133. theorem OAI.Laughlin.Certificate.source_error_21_3_1 line 1075
134. theorem OAI.Laughlin.Certificate.source_gram_21_3_1 line 1079
135. theorem OAI.Laughlin.Certificate.source_error_21_5_1 line 1083
136. theorem OAI.Laughlin.Certificate.source_gram_21_5_1 line 1087
137. theorem OAI.Laughlin.Certificate.source_error_21_5_3 line 1091
138. theorem OAI.Laughlin.Certificate.source_gram_21_5_3 line 1095
139. theorem OAI.Laughlin.Certificate.source_error_21_7_1 line 1099
140. theorem OAI.Laughlin.Certificate.source_gram_21_7_1 line 1103
141. theorem OAI.Laughlin.Certificate.source_error_21_7_3 line 1107
142. theorem OAI.Laughlin.Certificate.source_gram_21_7_3 line 1111
143. theorem OAI.Laughlin.Certificate.source_error_21_7_5 line 1115
144. theorem OAI.Laughlin.Certificate.source_gram_21_7_5 line 1119
145. theorem OAI.Laughlin.Certificate.source_error_21_9_1 line 1123
146. theorem OAI.Laughlin.Certificate.source_gram_21_9_1 line 1127
147. theorem OAI.Laughlin.Certificate.source_error_21_9_3 line 1131
148. theorem OAI.Laughlin.Certificate.source_gram_21_9_3 line 1135
149. theorem OAI.Laughlin.Certificate.source_error_21_9_5 line 1139
150. theorem OAI.Laughlin.Certificate.source_gram_21_9_5 line 1143
151. theorem OAI.Laughlin.Certificate.source_error_21_9_7 line 1147
152. theorem OAI.Laughlin.Certificate.source_gram_21_9_7 line 1151
153. theorem OAI.Laughlin.Certificate.source_error_21_11_1 line 1155
154. theorem OAI.Laughlin.Certificate.source_gram_21_11_1 line 1159
155. theorem OAI.Laughlin.Certificate.source_error_21_11_3 line 1163
156. theorem OAI.Laughlin.Certificate.source_gram_21_11_3 line 1167
157. theorem OAI.Laughlin.Certificate.source_error_21_11_5 line 1171
158. theorem OAI.Laughlin.Certificate.source_gram_21_11_5 line 1175
159. theorem OAI.Laughlin.Certificate.source_error_21_11_7 line 1179
160. theorem OAI.Laughlin.Certificate.source_gram_21_11_7 line 1183
161. theorem OAI.Laughlin.Certificate.source_error_21_11_9 line 1187
162. theorem OAI.Laughlin.Certificate.source_gram_21_11_9 line 1191
163. theorem OAI.Laughlin.Certificate.source_error_21_13_1 line 1195
164. theorem OAI.Laughlin.Certificate.source_gram_21_13_1 line 1199
165. theorem OAI.Laughlin.Certificate.source_error_21_13_3 line 1203
166. theorem OAI.Laughlin.Certificate.source_gram_21_13_3 line 1207
167. theorem OAI.Laughlin.Certificate.source_error_21_13_5 line 1211
168. theorem OAI.Laughlin.Certificate.source_gram_21_13_5 line 1215
169. theorem OAI.Laughlin.Certificate.source_error_21_13_7 line 1219
170. theorem OAI.Laughlin.Certificate.source_gram_21_13_7 line 1223
171. theorem OAI.Laughlin.Certificate.source_error_21_13_9 line 1227
172. theorem OAI.Laughlin.Certificate.source_gram_21_13_9 line 1231
173. theorem OAI.Laughlin.Certificate.source_error_21_13_11 line 1235
174. theorem OAI.Laughlin.Certificate.source_gram_21_13_11 line 1239
175. theorem OAI.Laughlin.Certificate.source_error_21_15_1 line 1243
176. theorem OAI.Laughlin.Certificate.source_gram_21_15_1 line 1247
177. theorem OAI.Laughlin.Certificate.source_error_21_15_3 line 1251
178. theorem OAI.Laughlin.Certificate.source_gram_21_15_3 line 1255
179. theorem OAI.Laughlin.Certificate.source_error_21_15_5 line 1259
180. theorem OAI.Laughlin.Certificate.source_gram_21_15_5 line 1263
181. theorem OAI.Laughlin.Certificate.source_error_21_15_7 line 1267
182. theorem OAI.Laughlin.Certificate.source_gram_21_15_7 line 1271
183. theorem OAI.Laughlin.Certificate.source_error_21_15_9 line 1275
184. theorem OAI.Laughlin.Certificate.source_gram_21_15_9 line 1279
185. theorem OAI.Laughlin.Certificate.source_error_21_15_11 line 1283
186. theorem OAI.Laughlin.Certificate.source_gram_21_15_11 line 1287
187. theorem OAI.Laughlin.Certificate.source_error_21_15_13 line 1291
188. theorem OAI.Laughlin.Certificate.source_gram_21_15_13 line 1295
189. theorem OAI.Laughlin.Certificate.source_error_21_17_1 line 1299
190. theorem OAI.Laughlin.Certificate.source_gram_21_17_1 line 1303
191. theorem OAI.Laughlin.Certificate.source_error_21_17_3 line 1307
192. theorem OAI.Laughlin.Certificate.source_gram_21_17_3 line 1311
193. theorem OAI.Laughlin.Certificate.source_error_21_17_5 line 1315
194. theorem OAI.Laughlin.Certificate.source_gram_21_17_5 line 1319
195. theorem OAI.Laughlin.Certificate.source_error_21_17_7 line 1323
196. theorem OAI.Laughlin.Certificate.source_gram_21_17_7 line 1327
197. theorem OAI.Laughlin.Certificate.source_error_21_17_9 line 1331
198. theorem OAI.Laughlin.Certificate.source_gram_21_17_9 line 1335
199. theorem OAI.Laughlin.Certificate.source_error_21_17_11 line 1339
200. theorem OAI.Laughlin.Certificate.source_gram_21_17_11 line 1343
201. theorem OAI.Laughlin.Certificate.source_error_21_17_13 line 1347
202. theorem OAI.Laughlin.Certificate.source_gram_21_17_13 line 1351
203. theorem OAI.Laughlin.Certificate.source_error_21_17_15 line 1355
204. theorem OAI.Laughlin.Certificate.source_gram_21_17_15 line 1359
205. theorem OAI.Laughlin.Certificate.source_error_21_19_1 line 1363
206. theorem OAI.Laughlin.Certificate.source_gram_21_19_1 line 1367
207. theorem OAI.Laughlin.Certificate.source_error_21_19_3 line 1371
208. theorem OAI.Laughlin.Certificate.source_gram_21_19_3 line 1375
209. theorem OAI.Laughlin.Certificate.source_error_21_19_5 line 1379
210. theorem OAI.Laughlin.Certificate.source_gram_21_19_5 line 1383
211. theorem OAI.Laughlin.Certificate.source_error_21_19_7 line 1387
212. theorem OAI.Laughlin.Certificate.source_gram_21_19_7 line 1391
213. theorem OAI.Laughlin.Certificate.source_error_21_19_9 line 1395
214. theorem OAI.Laughlin.Certificate.source_gram_21_19_9 line 1399
215. theorem OAI.Laughlin.Certificate.source_error_21_19_11 line 1403
216. theorem OAI.Laughlin.Certificate.source_gram_21_19_11 line 1407
217. theorem OAI.Laughlin.Certificate.source_error_21_19_13 line 1411
218. theorem OAI.Laughlin.Certificate.source_gram_21_19_13 line 1415
219. theorem OAI.Laughlin.Certificate.source_error_21_19_15 line 1419
220. theorem OAI.Laughlin.Certificate.source_gram_21_19_15 line 1423
221. theorem OAI.Laughlin.Certificate.source_error_21_19_17 line 1427
222. theorem OAI.Laughlin.Certificate.source_gram_21_19_17 line 1431
223. theorem OAI.Laughlin.Certificate.source_error_21_21_1 line 1435
224. theorem OAI.Laughlin.Certificate.source_gram_21_21_1 line 1439
225. theorem OAI.Laughlin.Certificate.source_error_21_21_3 line 1443
226. theorem OAI.Laughlin.Certificate.source_gram_21_21_3 line 1447
227. theorem OAI.Laughlin.Certificate.source_error_21_21_5 line 1451
228. theorem OAI.Laughlin.Certificate.source_gram_21_21_5 line 1455
229. theorem OAI.Laughlin.Certificate.source_error_21_21_7 line 1459
230. theorem OAI.Laughlin.Certificate.source_gram_21_21_7 line 1463
231. theorem OAI.Laughlin.Certificate.source_error_21_21_9 line 1467
232. theorem OAI.Laughlin.Certificate.source_gram_21_21_9 line 1471
233. theorem OAI.Laughlin.Certificate.source_error_21_21_11 line 1475
234. theorem OAI.Laughlin.Certificate.source_gram_21_21_11 line 1479
235. theorem OAI.Laughlin.Certificate.source_error_21_21_13 line 1483
236. theorem OAI.Laughlin.Certificate.source_gram_21_21_13 line 1487
237. theorem OAI.Laughlin.Certificate.source_error_21_21_15 line 1491
238. theorem OAI.Laughlin.Certificate.source_gram_21_21_15 line 1495
239. theorem OAI.Laughlin.Certificate.source_error_21_21_17 line 1499
240. theorem OAI.Laughlin.Certificate.source_gram_21_21_17 line 1503
241. theorem OAI.Laughlin.Certificate.source_error_21_21_19 line 1507
242. theorem OAI.Laughlin.Certificate.source_gram_21_21_19 line 1511
243. theorem OAI.Laughlin.Certificate.error_21 line 1515
244. theorem OAI.Laughlin.Certificate.gram_21 line 1640