OAI/Analysis/Laughlin/FiniteFlux/GramData23.lean

GitHub source file

290 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Laughlin.Certificate.source_error_23_1_1 line 98
2. theorem OAI.Laughlin.Certificate.source_error_23_1_3 line 109
3. theorem OAI.Laughlin.Certificate.source_error_23_1_5 line 120
4. theorem OAI.Laughlin.Certificate.source_error_23_1_7 line 131
5. theorem OAI.Laughlin.Certificate.source_error_23_1_9 line 142
6. theorem OAI.Laughlin.Certificate.source_error_23_1_11 line 153
7. theorem OAI.Laughlin.Certificate.source_error_23_1_13 line 164
8. theorem OAI.Laughlin.Certificate.source_error_23_1_15 line 175
9. theorem OAI.Laughlin.Certificate.source_error_23_1_17 line 186
10. theorem OAI.Laughlin.Certificate.source_error_23_1_19 line 197
11. theorem OAI.Laughlin.Certificate.source_error_23_1_21 line 208
12. theorem OAI.Laughlin.Certificate.source_error_23_1_23 line 219
13. theorem OAI.Laughlin.Certificate.source_error_23_3_3 line 230
14. theorem OAI.Laughlin.Certificate.source_error_23_3_5 line 241
15. theorem OAI.Laughlin.Certificate.source_error_23_3_7 line 252
16. theorem OAI.Laughlin.Certificate.source_error_23_3_9 line 263
17. theorem OAI.Laughlin.Certificate.source_error_23_3_11 line 274
18. theorem OAI.Laughlin.Certificate.source_error_23_3_13 line 285
19. theorem OAI.Laughlin.Certificate.source_error_23_3_15 line 296
20. theorem OAI.Laughlin.Certificate.source_error_23_3_17 line 307
21. theorem OAI.Laughlin.Certificate.source_error_23_3_19 line 318
22. theorem OAI.Laughlin.Certificate.source_error_23_3_21 line 329
23. theorem OAI.Laughlin.Certificate.source_error_23_3_23 line 340
24. theorem OAI.Laughlin.Certificate.source_error_23_5_5 line 351
25. theorem OAI.Laughlin.Certificate.source_error_23_5_7 line 362
26. theorem OAI.Laughlin.Certificate.source_error_23_5_9 line 373
27. theorem OAI.Laughlin.Certificate.source_error_23_5_11 line 384
28. theorem OAI.Laughlin.Certificate.source_error_23_5_13 line 395
29. theorem OAI.Laughlin.Certificate.source_error_23_5_15 line 406
30. theorem OAI.Laughlin.Certificate.source_error_23_5_17 line 417
31. theorem OAI.Laughlin.Certificate.source_error_23_5_19 line 428
32. theorem OAI.Laughlin.Certificate.source_error_23_5_21 line 439
33. theorem OAI.Laughlin.Certificate.source_error_23_5_23 line 450
34. theorem OAI.Laughlin.Certificate.source_error_23_7_7 line 461
35. theorem OAI.Laughlin.Certificate.source_error_23_7_9 line 472
36. theorem OAI.Laughlin.Certificate.source_error_23_7_11 line 483
37. theorem OAI.Laughlin.Certificate.source_error_23_7_13 line 494
38. theorem OAI.Laughlin.Certificate.source_error_23_7_15 line 505
39. theorem OAI.Laughlin.Certificate.source_error_23_7_17 line 516
40. theorem OAI.Laughlin.Certificate.source_error_23_7_19 line 527
41. theorem OAI.Laughlin.Certificate.source_error_23_7_21 line 538
42. theorem OAI.Laughlin.Certificate.source_error_23_7_23 line 549
43. theorem OAI.Laughlin.Certificate.source_error_23_9_9 line 560
44. theorem OAI.Laughlin.Certificate.source_error_23_9_11 line 571
45. theorem OAI.Laughlin.Certificate.source_error_23_9_13 line 582
46. theorem OAI.Laughlin.Certificate.source_error_23_9_15 line 593
47. theorem OAI.Laughlin.Certificate.source_error_23_9_17 line 604
48. theorem OAI.Laughlin.Certificate.source_error_23_9_19 line 615
49. theorem OAI.Laughlin.Certificate.source_error_23_9_21 line 626
50. theorem OAI.Laughlin.Certificate.source_error_23_9_23 line 637
51. theorem OAI.Laughlin.Certificate.source_error_23_11_11 line 648
52. theorem OAI.Laughlin.Certificate.source_error_23_11_13 line 659
53. theorem OAI.Laughlin.Certificate.source_error_23_11_15 line 670
54. theorem OAI.Laughlin.Certificate.source_error_23_11_17 line 681
55. theorem OAI.Laughlin.Certificate.source_error_23_11_19 line 692
56. theorem OAI.Laughlin.Certificate.source_error_23_11_21 line 703
57. theorem OAI.Laughlin.Certificate.source_error_23_11_23 line 714
58. theorem OAI.Laughlin.Certificate.source_error_23_13_13 line 725
59. theorem OAI.Laughlin.Certificate.source_error_23_13_15 line 736
60. theorem OAI.Laughlin.Certificate.source_error_23_13_17 line 747
61. theorem OAI.Laughlin.Certificate.source_error_23_13_19 line 758
62. theorem OAI.Laughlin.Certificate.source_error_23_13_21 line 769
63. theorem OAI.Laughlin.Certificate.source_error_23_13_23 line 780
64. theorem OAI.Laughlin.Certificate.source_error_23_15_15 line 791
65. theorem OAI.Laughlin.Certificate.source_error_23_15_17 line 802
66. theorem OAI.Laughlin.Certificate.source_error_23_15_19 line 813
67. theorem OAI.Laughlin.Certificate.source_error_23_15_21 line 824
68. theorem OAI.Laughlin.Certificate.source_error_23_15_23 line 835
69. theorem OAI.Laughlin.Certificate.source_error_23_17_17 line 846
70. theorem OAI.Laughlin.Certificate.source_error_23_17_19 line 857
71. theorem OAI.Laughlin.Certificate.source_error_23_17_21 line 868
72. theorem OAI.Laughlin.Certificate.source_error_23_17_23 line 879
73. theorem OAI.Laughlin.Certificate.source_error_23_19_19 line 890
74. theorem OAI.Laughlin.Certificate.source_error_23_19_21 line 901
75. theorem OAI.Laughlin.Certificate.source_error_23_19_23 line 912
76. theorem OAI.Laughlin.Certificate.source_error_23_21_21 line 923
77. theorem OAI.Laughlin.Certificate.source_error_23_21_23 line 934
78. theorem OAI.Laughlin.Certificate.source_error_23_23_23 line 945
79. theorem OAI.Laughlin.Certificate.source_gram_23_1_1 line 956
80. theorem OAI.Laughlin.Certificate.source_gram_23_1_3 line 960
81. theorem OAI.Laughlin.Certificate.source_gram_23_1_5 line 964
82. theorem OAI.Laughlin.Certificate.source_gram_23_1_7 line 968
83. theorem OAI.Laughlin.Certificate.source_gram_23_1_9 line 972
84. theorem OAI.Laughlin.Certificate.source_gram_23_1_11 line 976
85. theorem OAI.Laughlin.Certificate.source_gram_23_1_13 line 980
86. theorem OAI.Laughlin.Certificate.source_gram_23_1_15 line 984
87. theorem OAI.Laughlin.Certificate.source_gram_23_1_17 line 988
88. theorem OAI.Laughlin.Certificate.source_gram_23_1_19 line 992
89. theorem OAI.Laughlin.Certificate.source_gram_23_1_21 line 996
90. theorem OAI.Laughlin.Certificate.source_gram_23_1_23 line 1000
91. theorem OAI.Laughlin.Certificate.source_gram_23_3_3 line 1004
92. theorem OAI.Laughlin.Certificate.source_gram_23_3_5 line 1008
93. theorem OAI.Laughlin.Certificate.source_gram_23_3_7 line 1012
94. theorem OAI.Laughlin.Certificate.source_gram_23_3_9 line 1016
95. theorem OAI.Laughlin.Certificate.source_gram_23_3_11 line 1020
96. theorem OAI.Laughlin.Certificate.source_gram_23_3_13 line 1024
97. theorem OAI.Laughlin.Certificate.source_gram_23_3_15 line 1028
98. theorem OAI.Laughlin.Certificate.source_gram_23_3_17 line 1032
99. theorem OAI.Laughlin.Certificate.source_gram_23_3_19 line 1036
100. theorem OAI.Laughlin.Certificate.source_gram_23_3_21 line 1040
101. theorem OAI.Laughlin.Certificate.source_gram_23_3_23 line 1044
102. theorem OAI.Laughlin.Certificate.source_gram_23_5_5 line 1048
103. theorem OAI.Laughlin.Certificate.source_gram_23_5_7 line 1052
104. theorem OAI.Laughlin.Certificate.source_gram_23_5_9 line 1056
105. theorem OAI.Laughlin.Certificate.source_gram_23_5_11 line 1060
106. theorem OAI.Laughlin.Certificate.source_gram_23_5_13 line 1064
107. theorem OAI.Laughlin.Certificate.source_gram_23_5_15 line 1068
108. theorem OAI.Laughlin.Certificate.source_gram_23_5_17 line 1072
109. theorem OAI.Laughlin.Certificate.source_gram_23_5_19 line 1076
110. theorem OAI.Laughlin.Certificate.source_gram_23_5_21 line 1080
111. theorem OAI.Laughlin.Certificate.source_gram_23_5_23 line 1084
112. theorem OAI.Laughlin.Certificate.source_gram_23_7_7 line 1088
113. theorem OAI.Laughlin.Certificate.source_gram_23_7_9 line 1092
114. theorem OAI.Laughlin.Certificate.source_gram_23_7_11 line 1096
115. theorem OAI.Laughlin.Certificate.source_gram_23_7_13 line 1100
116. theorem OAI.Laughlin.Certificate.source_gram_23_7_15 line 1104
117. theorem OAI.Laughlin.Certificate.source_gram_23_7_17 line 1108
118. theorem OAI.Laughlin.Certificate.source_gram_23_7_19 line 1112
119. theorem OAI.Laughlin.Certificate.source_gram_23_7_21 line 1116
120. theorem OAI.Laughlin.Certificate.source_gram_23_7_23 line 1120
121. theorem OAI.Laughlin.Certificate.source_gram_23_9_9 line 1124
122. theorem OAI.Laughlin.Certificate.source_gram_23_9_11 line 1128
123. theorem OAI.Laughlin.Certificate.source_gram_23_9_13 line 1132
124. theorem OAI.Laughlin.Certificate.source_gram_23_9_15 line 1136
125. theorem OAI.Laughlin.Certificate.source_gram_23_9_17 line 1140
126. theorem OAI.Laughlin.Certificate.source_gram_23_9_19 line 1144
127. theorem OAI.Laughlin.Certificate.source_gram_23_9_21 line 1148
128. theorem OAI.Laughlin.Certificate.source_gram_23_9_23 line 1152
129. theorem OAI.Laughlin.Certificate.source_gram_23_11_11 line 1156
130. theorem OAI.Laughlin.Certificate.source_gram_23_11_13 line 1160
131. theorem OAI.Laughlin.Certificate.source_gram_23_11_15 line 1164
132. theorem OAI.Laughlin.Certificate.source_gram_23_11_17 line 1168
133. theorem OAI.Laughlin.Certificate.source_gram_23_11_19 line 1172
134. theorem OAI.Laughlin.Certificate.source_gram_23_11_21 line 1176
135. theorem OAI.Laughlin.Certificate.source_gram_23_11_23 line 1180
136. theorem OAI.Laughlin.Certificate.source_gram_23_13_13 line 1184
137. theorem OAI.Laughlin.Certificate.source_gram_23_13_15 line 1188
138. theorem OAI.Laughlin.Certificate.source_gram_23_13_17 line 1192
139. theorem OAI.Laughlin.Certificate.source_gram_23_13_19 line 1196
140. theorem OAI.Laughlin.Certificate.source_gram_23_13_21 line 1200
141. theorem OAI.Laughlin.Certificate.source_gram_23_13_23 line 1204
142. theorem OAI.Laughlin.Certificate.source_gram_23_15_15 line 1208
143. theorem OAI.Laughlin.Certificate.source_gram_23_15_17 line 1212
144. theorem OAI.Laughlin.Certificate.source_gram_23_15_19 line 1216
145. theorem OAI.Laughlin.Certificate.source_gram_23_15_21 line 1220
146. theorem OAI.Laughlin.Certificate.source_gram_23_15_23 line 1224
147. theorem OAI.Laughlin.Certificate.source_gram_23_17_17 line 1228
148. theorem OAI.Laughlin.Certificate.source_gram_23_17_19 line 1232
149. theorem OAI.Laughlin.Certificate.source_gram_23_17_21 line 1236
150. theorem OAI.Laughlin.Certificate.source_gram_23_17_23 line 1240
151. theorem OAI.Laughlin.Certificate.source_gram_23_19_19 line 1244
152. theorem OAI.Laughlin.Certificate.source_gram_23_19_21 line 1248
153. theorem OAI.Laughlin.Certificate.source_gram_23_19_23 line 1252
154. theorem OAI.Laughlin.Certificate.source_gram_23_21_21 line 1256
155. theorem OAI.Laughlin.Certificate.source_gram_23_21_23 line 1260
156. theorem OAI.Laughlin.Certificate.source_gram_23_23_23 line 1264
157. theorem OAI.Laughlin.Certificate.source_error_23_3_1 line 1268
158. theorem OAI.Laughlin.Certificate.source_gram_23_3_1 line 1272
159. theorem OAI.Laughlin.Certificate.source_error_23_5_1 line 1276
160. theorem OAI.Laughlin.Certificate.source_gram_23_5_1 line 1280
161. theorem OAI.Laughlin.Certificate.source_error_23_5_3 line 1284
162. theorem OAI.Laughlin.Certificate.source_gram_23_5_3 line 1288
163. theorem OAI.Laughlin.Certificate.source_error_23_7_1 line 1292
164. theorem OAI.Laughlin.Certificate.source_gram_23_7_1 line 1296
165. theorem OAI.Laughlin.Certificate.source_error_23_7_3 line 1300
166. theorem OAI.Laughlin.Certificate.source_gram_23_7_3 line 1304
167. theorem OAI.Laughlin.Certificate.source_error_23_7_5 line 1308
168. theorem OAI.Laughlin.Certificate.source_gram_23_7_5 line 1312
169. theorem OAI.Laughlin.Certificate.source_error_23_9_1 line 1316
170. theorem OAI.Laughlin.Certificate.source_gram_23_9_1 line 1320
171. theorem OAI.Laughlin.Certificate.source_error_23_9_3 line 1324
172. theorem OAI.Laughlin.Certificate.source_gram_23_9_3 line 1328
173. theorem OAI.Laughlin.Certificate.source_error_23_9_5 line 1332
174. theorem OAI.Laughlin.Certificate.source_gram_23_9_5 line 1336
175. theorem OAI.Laughlin.Certificate.source_error_23_9_7 line 1340
176. theorem OAI.Laughlin.Certificate.source_gram_23_9_7 line 1344
177. theorem OAI.Laughlin.Certificate.source_error_23_11_1 line 1348
178. theorem OAI.Laughlin.Certificate.source_gram_23_11_1 line 1352
179. theorem OAI.Laughlin.Certificate.source_error_23_11_3 line 1356
180. theorem OAI.Laughlin.Certificate.source_gram_23_11_3 line 1360
181. theorem OAI.Laughlin.Certificate.source_error_23_11_5 line 1364
182. theorem OAI.Laughlin.Certificate.source_gram_23_11_5 line 1368
183. theorem OAI.Laughlin.Certificate.source_error_23_11_7 line 1372
184. theorem OAI.Laughlin.Certificate.source_gram_23_11_7 line 1376
185. theorem OAI.Laughlin.Certificate.source_error_23_11_9 line 1380
186. theorem OAI.Laughlin.Certificate.source_gram_23_11_9 line 1384
187. theorem OAI.Laughlin.Certificate.source_error_23_13_1 line 1388
188. theorem OAI.Laughlin.Certificate.source_gram_23_13_1 line 1392
189. theorem OAI.Laughlin.Certificate.source_error_23_13_3 line 1396
190. theorem OAI.Laughlin.Certificate.source_gram_23_13_3 line 1400
191. theorem OAI.Laughlin.Certificate.source_error_23_13_5 line 1404
192. theorem OAI.Laughlin.Certificate.source_gram_23_13_5 line 1408
193. theorem OAI.Laughlin.Certificate.source_error_23_13_7 line 1412
194. theorem OAI.Laughlin.Certificate.source_gram_23_13_7 line 1416
195. theorem OAI.Laughlin.Certificate.source_error_23_13_9 line 1420
196. theorem OAI.Laughlin.Certificate.source_gram_23_13_9 line 1424
197. theorem OAI.Laughlin.Certificate.source_error_23_13_11 line 1428
198. theorem OAI.Laughlin.Certificate.source_gram_23_13_11 line 1432
199. theorem OAI.Laughlin.Certificate.source_error_23_15_1 line 1436
200. theorem OAI.Laughlin.Certificate.source_gram_23_15_1 line 1440
201. theorem OAI.Laughlin.Certificate.source_error_23_15_3 line 1444
202. theorem OAI.Laughlin.Certificate.source_gram_23_15_3 line 1448
203. theorem OAI.Laughlin.Certificate.source_error_23_15_5 line 1452
204. theorem OAI.Laughlin.Certificate.source_gram_23_15_5 line 1456
205. theorem OAI.Laughlin.Certificate.source_error_23_15_7 line 1460
206. theorem OAI.Laughlin.Certificate.source_gram_23_15_7 line 1464
207. theorem OAI.Laughlin.Certificate.source_error_23_15_9 line 1468
208. theorem OAI.Laughlin.Certificate.source_gram_23_15_9 line 1472
209. theorem OAI.Laughlin.Certificate.source_error_23_15_11 line 1476
210. theorem OAI.Laughlin.Certificate.source_gram_23_15_11 line 1480
211. theorem OAI.Laughlin.Certificate.source_error_23_15_13 line 1484
212. theorem OAI.Laughlin.Certificate.source_gram_23_15_13 line 1488
213. theorem OAI.Laughlin.Certificate.source_error_23_17_1 line 1492
214. theorem OAI.Laughlin.Certificate.source_gram_23_17_1 line 1496
215. theorem OAI.Laughlin.Certificate.source_error_23_17_3 line 1500
216. theorem OAI.Laughlin.Certificate.source_gram_23_17_3 line 1504
217. theorem OAI.Laughlin.Certificate.source_error_23_17_5 line 1508
218. theorem OAI.Laughlin.Certificate.source_gram_23_17_5 line 1512
219. theorem OAI.Laughlin.Certificate.source_error_23_17_7 line 1516
220. theorem OAI.Laughlin.Certificate.source_gram_23_17_7 line 1520
221. theorem OAI.Laughlin.Certificate.source_error_23_17_9 line 1524
222. theorem OAI.Laughlin.Certificate.source_gram_23_17_9 line 1528
223. theorem OAI.Laughlin.Certificate.source_error_23_17_11 line 1532
224. theorem OAI.Laughlin.Certificate.source_gram_23_17_11 line 1536
225. theorem OAI.Laughlin.Certificate.source_error_23_17_13 line 1540
226. theorem OAI.Laughlin.Certificate.source_gram_23_17_13 line 1544
227. theorem OAI.Laughlin.Certificate.source_error_23_17_15 line 1548
228. theorem OAI.Laughlin.Certificate.source_gram_23_17_15 line 1552
229. theorem OAI.Laughlin.Certificate.source_error_23_19_1 line 1556
230. theorem OAI.Laughlin.Certificate.source_gram_23_19_1 line 1560
231. theorem OAI.Laughlin.Certificate.source_error_23_19_3 line 1564
232. theorem OAI.Laughlin.Certificate.source_gram_23_19_3 line 1568
233. theorem OAI.Laughlin.Certificate.source_error_23_19_5 line 1572
234. theorem OAI.Laughlin.Certificate.source_gram_23_19_5 line 1576
235. theorem OAI.Laughlin.Certificate.source_error_23_19_7 line 1580
236. theorem OAI.Laughlin.Certificate.source_gram_23_19_7 line 1584
237. theorem OAI.Laughlin.Certificate.source_error_23_19_9 line 1588
238. theorem OAI.Laughlin.Certificate.source_gram_23_19_9 line 1592
239. theorem OAI.Laughlin.Certificate.source_error_23_19_11 line 1596
240. theorem OAI.Laughlin.Certificate.source_gram_23_19_11 line 1600
241. theorem OAI.Laughlin.Certificate.source_error_23_19_13 line 1604
242. theorem OAI.Laughlin.Certificate.source_gram_23_19_13 line 1608
243. theorem OAI.Laughlin.Certificate.source_error_23_19_15 line 1612
244. theorem OAI.Laughlin.Certificate.source_gram_23_19_15 line 1616
245. theorem OAI.Laughlin.Certificate.source_error_23_19_17 line 1620
246. theorem OAI.Laughlin.Certificate.source_gram_23_19_17 line 1624
247. theorem OAI.Laughlin.Certificate.source_error_23_21_1 line 1628
248. theorem OAI.Laughlin.Certificate.source_gram_23_21_1 line 1632
249. theorem OAI.Laughlin.Certificate.source_error_23_21_3 line 1636
250. theorem OAI.Laughlin.Certificate.source_gram_23_21_3 line 1640
251. theorem OAI.Laughlin.Certificate.source_error_23_21_5 line 1644
252. theorem OAI.Laughlin.Certificate.source_gram_23_21_5 line 1648
253. theorem OAI.Laughlin.Certificate.source_error_23_21_7 line 1652
254. theorem OAI.Laughlin.Certificate.source_gram_23_21_7 line 1656
255. theorem OAI.Laughlin.Certificate.source_error_23_21_9 line 1660
256. theorem OAI.Laughlin.Certificate.source_gram_23_21_9 line 1664
257. theorem OAI.Laughlin.Certificate.source_error_23_21_11 line 1668
258. theorem OAI.Laughlin.Certificate.source_gram_23_21_11 line 1672
259. theorem OAI.Laughlin.Certificate.source_error_23_21_13 line 1676
260. theorem OAI.Laughlin.Certificate.source_gram_23_21_13 line 1680
261. theorem OAI.Laughlin.Certificate.source_error_23_21_15 line 1684
262. theorem OAI.Laughlin.Certificate.source_gram_23_21_15 line 1688
263. theorem OAI.Laughlin.Certificate.source_error_23_21_17 line 1692
264. theorem OAI.Laughlin.Certificate.source_gram_23_21_17 line 1696
265. theorem OAI.Laughlin.Certificate.source_error_23_21_19 line 1700
266. theorem OAI.Laughlin.Certificate.source_gram_23_21_19 line 1704
267. theorem OAI.Laughlin.Certificate.source_error_23_23_1 line 1708
268. theorem OAI.Laughlin.Certificate.source_gram_23_23_1 line 1712
269. theorem OAI.Laughlin.Certificate.source_error_23_23_3 line 1716
270. theorem OAI.Laughlin.Certificate.source_gram_23_23_3 line 1720
271. theorem OAI.Laughlin.Certificate.source_error_23_23_5 line 1724
272. theorem OAI.Laughlin.Certificate.source_gram_23_23_5 line 1728
273. theorem OAI.Laughlin.Certificate.source_error_23_23_7 line 1732
274. theorem OAI.Laughlin.Certificate.source_gram_23_23_7 line 1736
275. theorem OAI.Laughlin.Certificate.source_error_23_23_9 line 1740
276. theorem OAI.Laughlin.Certificate.source_gram_23_23_9 line 1744
277. theorem OAI.Laughlin.Certificate.source_error_23_23_11 line 1748
278. theorem OAI.Laughlin.Certificate.source_gram_23_23_11 line 1752
279. theorem OAI.Laughlin.Certificate.source_error_23_23_13 line 1756
280. theorem OAI.Laughlin.Certificate.source_gram_23_23_13 line 1760
281. theorem OAI.Laughlin.Certificate.source_error_23_23_15 line 1764
282. theorem OAI.Laughlin.Certificate.source_gram_23_23_15 line 1768
283. theorem OAI.Laughlin.Certificate.source_error_23_23_17 line 1772
284. theorem OAI.Laughlin.Certificate.source_gram_23_23_17 line 1776
285. theorem OAI.Laughlin.Certificate.source_error_23_23_19 line 1780
286. theorem OAI.Laughlin.Certificate.source_gram_23_23_19 line 1784
287. theorem OAI.Laughlin.Certificate.source_error_23_23_21 line 1788
288. theorem OAI.Laughlin.Certificate.source_gram_23_23_21 line 1792
289. theorem OAI.Laughlin.Certificate.error_23 line 1796
290. theorem OAI.Laughlin.Certificate.gram_23 line 1944