OAI/Geometry/HarmonicGrowth/Counting.lean

GitHub source file

336 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.Certificate.binomRat line 11

   Source documentation

   The binomial polynomial, evaluated in exact rational arithmetic.

   def binomRat (x : ℚ) : ℕ → ℚ
     | 0 => 1
     | k+1 => binomRat x k * (x-k)/(k+1)

2. lemma OAI.HarmonicCounterexample.Certificate.binomRat_eq_pochhammer line 15
3. lemma OAI.HarmonicCounterexample.Certificate.binomRat_nat line 25
4. lemma OAI.HarmonicCounterexample.Certificate.binomRat_step line 28
5. lemma OAI.HarmonicCounterexample.Certificate.binomRat_difference line 40
6. def OAI.HarmonicCounterexample.Certificate.prefixCoefficient line 45

   Source documentation

   Coefficients in the exact degree-six reflected Vandermonde expansion.

   def prefixCoefficient (l : ℚ) (j : ℕ) : ℚ :=
   …

7. def OAI.HarmonicCounterexample.Certificate.countPrefix line 49

   Source documentation

   An exact antiderivative of the harmonic multiplicity kernel for s=8.

   def countPrefix (l x : ℚ) : ℚ :=
   …

8. lemma OAI.HarmonicCounterexample.Certificate.binomRat_product_six line 52
9. lemma OAI.HarmonicCounterexample.Certificate.reflected_binomial_six line 57
10. lemma OAI.HarmonicCounterexample.Certificate.reflected_vandermonde_six line 64
11. lemma OAI.HarmonicCounterexample.Certificate.countPrefix_difference line 74
12. lemma OAI.HarmonicCounterexample.Certificate.countPrefix_neg_one line 85
13. lemma OAI.HarmonicCounterexample.Certificate.binomRat_mul_succ line 106
14. lemma OAI.HarmonicCounterexample.Certificate.shifted_binom_difference line 112
15. def OAI.HarmonicCounterexample.Certificate.chargePrimitive line 117
16. lemma OAI.HarmonicCounterexample.Certificate.chargePrimitive_difference line 122
17. def OAI.HarmonicCounterexample.Certificate.chargePrefix line 148
18. lemma OAI.HarmonicCounterexample.Certificate.chargePrefix_difference line 151
19. lemma OAI.HarmonicCounterexample.Certificate.chargePrefix_neg_one line 160
20. lemma OAI.HarmonicCounterexample.Certificate.countPrefix_sum line 173

    Source documentation

    Exact finite prefix sum, with no asymptotic approximation.

    lemma countPrefix_sum (l : ℚ) (b : ℕ) :
        countPrefix l b = ∑ i ∈ Finset.range (b+1),binomRat (i+6) 6*binomRat (l-i+6) 6 := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.Certificate.countPrefix, OAI.HarmonicCounterexample.Certificate.binomRat

21. lemma OAI.HarmonicCounterexample.Certificate.chargePrefix_sum line 185
22. structure OAI.HarmonicCounterexample.Certificate.GroupCertificate line 209

    Source documentation

    Exact data for a paired, nonmiddle Hopf-charge prefix at n=16,k=50000.

    structure GroupCertificate where
    …

23. def OAI.HarmonicCounterexample.Certificate.group49964 line 223
24. def OAI.HarmonicCounterexample.Certificate.group49965 line 238
25. def OAI.HarmonicCounterexample.Certificate.group49966 line 253
26. def OAI.HarmonicCounterexample.Certificate.group49967 line 268
27. def OAI.HarmonicCounterexample.Certificate.group49968 line 283
28. def OAI.HarmonicCounterexample.Certificate.group49969 line 298
29. def OAI.HarmonicCounterexample.Certificate.group49970 line 313
30. def OAI.HarmonicCounterexample.Certificate.group49971 line 328
31. def OAI.HarmonicCounterexample.Certificate.group49972 line 343
32. def OAI.HarmonicCounterexample.Certificate.group49973 line 358
33. def OAI.HarmonicCounterexample.Certificate.group49974 line 373
34. def OAI.HarmonicCounterexample.Certificate.group49975 line 388
35. def OAI.HarmonicCounterexample.Certificate.group49976 line 403
36. def OAI.HarmonicCounterexample.Certificate.group49977 line 418
37. def OAI.HarmonicCounterexample.Certificate.group49978 line 433
38. def OAI.HarmonicCounterexample.Certificate.group49979 line 448
39. def OAI.HarmonicCounterexample.Certificate.group49980 line 463
40. def OAI.HarmonicCounterexample.Certificate.group49981 line 478
41. def OAI.HarmonicCounterexample.Certificate.group49982 line 493
42. def OAI.HarmonicCounterexample.Certificate.group49983 line 508
43. def OAI.HarmonicCounterexample.Certificate.group49984 line 523
44. def OAI.HarmonicCounterexample.Certificate.group49985 line 538
45. def OAI.HarmonicCounterexample.Certificate.group49986 line 553
46. def OAI.HarmonicCounterexample.Certificate.group49987 line 568
47. def OAI.HarmonicCounterexample.Certificate.group49988 line 583
48. def OAI.HarmonicCounterexample.Certificate.group49989 line 598
49. def OAI.HarmonicCounterexample.Certificate.group49990 line 613
50. def OAI.HarmonicCounterexample.Certificate.group49991 line 628
51. def OAI.HarmonicCounterexample.Certificate.group49992 line 643
52. def OAI.HarmonicCounterexample.Certificate.group49993 line 658
53. def OAI.HarmonicCounterexample.Certificate.group49994 line 673
54. def OAI.HarmonicCounterexample.Certificate.group49995 line 688
55. def OAI.HarmonicCounterexample.Certificate.group49996 line 703
56. def OAI.HarmonicCounterexample.Certificate.group49997 line 718
57. def OAI.HarmonicCounterexample.Certificate.group49998 line 733
58. def OAI.HarmonicCounterexample.Certificate.group49999 line 748
59. def OAI.HarmonicCounterexample.Certificate.group50000 line 763
60. def OAI.HarmonicCounterexample.Certificate.group50001 line 778
61. def OAI.HarmonicCounterexample.Certificate.group50002 line 793
62. def OAI.HarmonicCounterexample.Certificate.group50003 line 808
63. def OAI.HarmonicCounterexample.Certificate.group50004 line 823
64. def OAI.HarmonicCounterexample.Certificate.group50005 line 838
65. def OAI.HarmonicCounterexample.Certificate.group50006 line 853
66. def OAI.HarmonicCounterexample.Certificate.group50007 line 868
67. def OAI.HarmonicCounterexample.Certificate.group50008 line 883
68. def OAI.HarmonicCounterexample.Certificate.group50009 line 898
69. def OAI.HarmonicCounterexample.Certificate.group50010 line 913
70. def OAI.HarmonicCounterexample.Certificate.group50011 line 928
71. def OAI.HarmonicCounterexample.Certificate.group50012 line 943
72. def OAI.HarmonicCounterexample.Certificate.group50013 line 958
73. def OAI.HarmonicCounterexample.Certificate.group50014 line 973
74. def OAI.HarmonicCounterexample.Certificate.group50015 line 988
75. def OAI.HarmonicCounterexample.Certificate.group50016 line 1003
76. def OAI.HarmonicCounterexample.Certificate.group50017 line 1018
77. def OAI.HarmonicCounterexample.Certificate.group50018 line 1033
78. def OAI.HarmonicCounterexample.Certificate.group50019 line 1048
79. def OAI.HarmonicCounterexample.Certificate.group50020 line 1063
80. def OAI.HarmonicCounterexample.Certificate.group50021 line 1078
81. def OAI.HarmonicCounterexample.Certificate.group50022 line 1093
82. def OAI.HarmonicCounterexample.Certificate.group50023 line 1108
83. def OAI.HarmonicCounterexample.Certificate.group50024 line 1123
84. def OAI.HarmonicCounterexample.Certificate.group50025 line 1138
85. def OAI.HarmonicCounterexample.Certificate.group50026 line 1153
86. def OAI.HarmonicCounterexample.Certificate.group50027 line 1168
87. def OAI.HarmonicCounterexample.Certificate.group50028 line 1183
88. def OAI.HarmonicCounterexample.Certificate.group50029 line 1198
89. def OAI.HarmonicCounterexample.Certificate.group50030 line 1213
90. def OAI.HarmonicCounterexample.Certificate.group50031 line 1228
91. def OAI.HarmonicCounterexample.Certificate.group50032 line 1243
92. def OAI.HarmonicCounterexample.Certificate.group50033 line 1258
93. def OAI.HarmonicCounterexample.Certificate.group50034 line 1273
94. def OAI.HarmonicCounterexample.Certificate.group50035 line 1288
95. def OAI.HarmonicCounterexample.Certificate.group50036 line 1303
96. def OAI.HarmonicCounterexample.Certificate.group50037 line 1318
97. def OAI.HarmonicCounterexample.Certificate.group50038 line 1333
98. def OAI.HarmonicCounterexample.Certificate.group50039 line 1348
99. def OAI.HarmonicCounterexample.Certificate.group50040 line 1363
100. def OAI.HarmonicCounterexample.Certificate.group50041 line 1378
101. def OAI.HarmonicCounterexample.Certificate.group50042 line 1393
102. def OAI.HarmonicCounterexample.Certificate.group50043 line 1408
103. def OAI.HarmonicCounterexample.Certificate.group50044 line 1423
104. def OAI.HarmonicCounterexample.Certificate.group50045 line 1438
105. def OAI.HarmonicCounterexample.Certificate.group50046 line 1453
106. def OAI.HarmonicCounterexample.Certificate.group50047 line 1468
107. def OAI.HarmonicCounterexample.Certificate.group50048 line 1483
108. def OAI.HarmonicCounterexample.Certificate.group50049 line 1498
109. def OAI.HarmonicCounterexample.Certificate.group50050 line 1513
110. def OAI.HarmonicCounterexample.Certificate.group50051 line 1528
111. def OAI.HarmonicCounterexample.Certificate.group50052 line 1543
112. def OAI.HarmonicCounterexample.Certificate.group50053 line 1558
113. def OAI.HarmonicCounterexample.Certificate.group50054 line 1573
114. def OAI.HarmonicCounterexample.Certificate.group50055 line 1588
115. def OAI.HarmonicCounterexample.Certificate.group50056 line 1603
116. def OAI.HarmonicCounterexample.Certificate.group50057 line 1618
117. def OAI.HarmonicCounterexample.Certificate.group50058 line 1633
118. def OAI.HarmonicCounterexample.Certificate.group50059 line 1648
119. def OAI.HarmonicCounterexample.Certificate.group50060 line 1663
120. def OAI.HarmonicCounterexample.Certificate.group50061 line 1678
121. def OAI.HarmonicCounterexample.Certificate.group50062 line 1693
122. def OAI.HarmonicCounterexample.Certificate.group50063 line 1708
123. def OAI.HarmonicCounterexample.Certificate.group50064 line 1723
124. def OAI.HarmonicCounterexample.Certificate.group50065 line 1738
125. def OAI.HarmonicCounterexample.Certificate.group50066 line 1753
126. def OAI.HarmonicCounterexample.Certificate.group50067 line 1768
127. def OAI.HarmonicCounterexample.Certificate.group50068 line 1783
128. def OAI.HarmonicCounterexample.Certificate.group50069 line 1798
129. def OAI.HarmonicCounterexample.Certificate.group50070 line 1813
130. def OAI.HarmonicCounterexample.Certificate.group50071 line 1828
131. def OAI.HarmonicCounterexample.Certificate.group50072 line 1843
132. def OAI.HarmonicCounterexample.Certificate.group50073 line 1858
133. def OAI.HarmonicCounterexample.Certificate.group50074 line 1873
134. def OAI.HarmonicCounterexample.Certificate.group50075 line 1888
135. def OAI.HarmonicCounterexample.Certificate.group50076 line 1903
136. def OAI.HarmonicCounterexample.Certificate.group50077 line 1918
137. def OAI.HarmonicCounterexample.Certificate.group50078 line 1933
138. def OAI.HarmonicCounterexample.Certificate.group50079 line 1948
139. def OAI.HarmonicCounterexample.Certificate.group50080 line 1963
140. def OAI.HarmonicCounterexample.Certificate.group50081 line 1978
141. def OAI.HarmonicCounterexample.Certificate.group50082 line 1993
142. def OAI.HarmonicCounterexample.Certificate.group50083 line 2008
143. def OAI.HarmonicCounterexample.Certificate.group50084 line 2023
144. def OAI.HarmonicCounterexample.Certificate.group50085 line 2038
145. def OAI.HarmonicCounterexample.Certificate.group50086 line 2053
146. def OAI.HarmonicCounterexample.Certificate.group50087 line 2068
147. def OAI.HarmonicCounterexample.Certificate.group50088 line 2083
148. def OAI.HarmonicCounterexample.Certificate.group50089 line 2098
149. def OAI.HarmonicCounterexample.Certificate.group50090 line 2113
150. def OAI.HarmonicCounterexample.Certificate.group50091 line 2128
151. def OAI.HarmonicCounterexample.Certificate.group50092 line 2143
152. def OAI.HarmonicCounterexample.Certificate.group50093 line 2158
153. def OAI.HarmonicCounterexample.Certificate.group50094 line 2173
154. def OAI.HarmonicCounterexample.Certificate.group50095 line 2188
155. def OAI.HarmonicCounterexample.Certificate.group50096 line 2203
156. def OAI.HarmonicCounterexample.Certificate.group50097 line 2218
157. def OAI.HarmonicCounterexample.Certificate.group50098 line 2233
158. def OAI.HarmonicCounterexample.Certificate.group50099 line 2248
159. def OAI.HarmonicCounterexample.Certificate.group50100 line 2263
160. def OAI.HarmonicCounterexample.Certificate.group50101 line 2278
161. def OAI.HarmonicCounterexample.Certificate.group50102 line 2293
162. def OAI.HarmonicCounterexample.Certificate.group50103 line 2308
163. def OAI.HarmonicCounterexample.Certificate.group50104 line 2323
164. def OAI.HarmonicCounterexample.Certificate.group50105 line 2338
165. def OAI.HarmonicCounterexample.Certificate.group50106 line 2353
166. def OAI.HarmonicCounterexample.Certificate.group50107 line 2368
167. def OAI.HarmonicCounterexample.Certificate.group50108 line 2383
168. def OAI.HarmonicCounterexample.Certificate.group50109 line 2398
169. def OAI.HarmonicCounterexample.Certificate.group50110 line 2413
170. def OAI.HarmonicCounterexample.Certificate.group50111 line 2428
171. def OAI.HarmonicCounterexample.Certificate.group50112 line 2443
172. def OAI.HarmonicCounterexample.Certificate.group50113 line 2458
173. def OAI.HarmonicCounterexample.Certificate.group50114 line 2473
174. def OAI.HarmonicCounterexample.Certificate.group50115 line 2488
175. def OAI.HarmonicCounterexample.Certificate.group50116 line 2503
176. def OAI.HarmonicCounterexample.Certificate.group50117 line 2518
177. def OAI.HarmonicCounterexample.Certificate.group50118 line 2533
178. def OAI.HarmonicCounterexample.Certificate.group50119 line 2548
179. def OAI.HarmonicCounterexample.Certificate.group50120 line 2563
180. def OAI.HarmonicCounterexample.Certificate.group50121 line 2578
181. def OAI.HarmonicCounterexample.Certificate.group50122 line 2593
182. def OAI.HarmonicCounterexample.Certificate.group50123 line 2608
183. def OAI.HarmonicCounterexample.Certificate.group50124 line 2623
184. def OAI.HarmonicCounterexample.Certificate.group50125 line 2638
185. def OAI.HarmonicCounterexample.Certificate.group50126 line 2653
186. def OAI.HarmonicCounterexample.Certificate.group50127 line 2668
187. def OAI.HarmonicCounterexample.Certificate.group50128 line 2683
188. def OAI.HarmonicCounterexample.Certificate.group50129 line 2698
189. def OAI.HarmonicCounterexample.Certificate.group50130 line 2713
190. def OAI.HarmonicCounterexample.Certificate.group50131 line 2728
191. def OAI.HarmonicCounterexample.Certificate.group50132 line 2743
192. def OAI.HarmonicCounterexample.Certificate.group50133 line 2758
193. def OAI.HarmonicCounterexample.Certificate.group50134 line 2773
194. def OAI.HarmonicCounterexample.Certificate.group50135 line 2788
195. def OAI.HarmonicCounterexample.Certificate.group50136 line 2803
196. def OAI.HarmonicCounterexample.Certificate.group50137 line 2818
197. def OAI.HarmonicCounterexample.Certificate.group50138 line 2833
198. def OAI.HarmonicCounterexample.Certificate.group50139 line 2848
199. def OAI.HarmonicCounterexample.Certificate.group50140 line 2863
200. def OAI.HarmonicCounterexample.Certificate.group50141 line 2878
201. def OAI.HarmonicCounterexample.Certificate.group50142 line 2893
202. def OAI.HarmonicCounterexample.Certificate.group50143 line 2908
203. def OAI.HarmonicCounterexample.Certificate.group50144 line 2923
204. def OAI.HarmonicCounterexample.Certificate.group50145 line 2938
205. def OAI.HarmonicCounterexample.Certificate.group50146 line 2953
206. def OAI.HarmonicCounterexample.Certificate.group50147 line 2968
207. def OAI.HarmonicCounterexample.Certificate.group50148 line 2983
208. def OAI.HarmonicCounterexample.Certificate.group50149 line 2998
209. def OAI.HarmonicCounterexample.Certificate.group50150 line 3013
210. def OAI.HarmonicCounterexample.Certificate.group50151 line 3028
211. def OAI.HarmonicCounterexample.Certificate.group50152 line 3043
212. def OAI.HarmonicCounterexample.Certificate.group50153 line 3058
213. def OAI.HarmonicCounterexample.Certificate.group50154 line 3073
214. def OAI.HarmonicCounterexample.Certificate.group50155 line 3088
215. def OAI.HarmonicCounterexample.Certificate.group50156 line 3103
216. def OAI.HarmonicCounterexample.Certificate.group50157 line 3118
217. def OAI.HarmonicCounterexample.Certificate.group50158 line 3133
218. def OAI.HarmonicCounterexample.Certificate.group50159 line 3148
219. def OAI.HarmonicCounterexample.Certificate.group50160 line 3163
220. def OAI.HarmonicCounterexample.Certificate.group50161 line 3178
221. def OAI.HarmonicCounterexample.Certificate.group50162 line 3193
222. def OAI.HarmonicCounterexample.Certificate.group50163 line 3208
223. def OAI.HarmonicCounterexample.Certificate.group50164 line 3223
224. def OAI.HarmonicCounterexample.Certificate.group50165 line 3238
225. def OAI.HarmonicCounterexample.Certificate.group50166 line 3253
226. def OAI.HarmonicCounterexample.Certificate.group50167 line 3268
227. def OAI.HarmonicCounterexample.Certificate.group50168 line 3283
228. def OAI.HarmonicCounterexample.Certificate.group50169 line 3298
229. def OAI.HarmonicCounterexample.Certificate.group50170 line 3313
230. def OAI.HarmonicCounterexample.Certificate.group50171 line 3328
231. def OAI.HarmonicCounterexample.Certificate.group50172 line 3343
232. def OAI.HarmonicCounterexample.Certificate.group50173 line 3358
233. def OAI.HarmonicCounterexample.Certificate.group50174 line 3373
234. def OAI.HarmonicCounterexample.Certificate.group50175 line 3388
235. def OAI.HarmonicCounterexample.Certificate.group50176 line 3403
236. def OAI.HarmonicCounterexample.Certificate.group50177 line 3418
237. def OAI.HarmonicCounterexample.Certificate.group50178 line 3433
238. def OAI.HarmonicCounterexample.Certificate.group50179 line 3448
239. def OAI.HarmonicCounterexample.Certificate.group50180 line 3463
240. def OAI.HarmonicCounterexample.Certificate.group50181 line 3478
241. def OAI.HarmonicCounterexample.Certificate.group50182 line 3493
242. def OAI.HarmonicCounterexample.Certificate.group50183 line 3508
243. def OAI.HarmonicCounterexample.Certificate.group50184 line 3523
244. def OAI.HarmonicCounterexample.Certificate.group50185 line 3538
245. def OAI.HarmonicCounterexample.Certificate.group50186 line 3553
246. def OAI.HarmonicCounterexample.Certificate.group50187 line 3568
247. def OAI.HarmonicCounterexample.Certificate.group50188 line 3583
248. def OAI.HarmonicCounterexample.Certificate.group50189 line 3598
249. def OAI.HarmonicCounterexample.Certificate.group50190 line 3613
250. def OAI.HarmonicCounterexample.Certificate.group50191 line 3628
251. def OAI.HarmonicCounterexample.Certificate.group50192 line 3643
252. def OAI.HarmonicCounterexample.Certificate.group50193 line 3658
253. def OAI.HarmonicCounterexample.Certificate.group50194 line 3673
254. def OAI.HarmonicCounterexample.Certificate.group50195 line 3688
255. def OAI.HarmonicCounterexample.Certificate.group50196 line 3703
256. def OAI.HarmonicCounterexample.Certificate.group50197 line 3718
257. def OAI.HarmonicCounterexample.Certificate.group50198 line 3733
258. def OAI.HarmonicCounterexample.Certificate.group50199 line 3748
259. def OAI.HarmonicCounterexample.Certificate.group50200 line 3763
260. def OAI.HarmonicCounterexample.Certificate.group50201 line 3778
261. def OAI.HarmonicCounterexample.Certificate.group50202 line 3793
262. def OAI.HarmonicCounterexample.Certificate.group50203 line 3808
263. def OAI.HarmonicCounterexample.Certificate.group50204 line 3823
264. def OAI.HarmonicCounterexample.Certificate.group50205 line 3838
265. def OAI.HarmonicCounterexample.Certificate.group50206 line 3853
266. def OAI.HarmonicCounterexample.Certificate.group50207 line 3868
267. def OAI.HarmonicCounterexample.Certificate.group50208 line 3883
268. def OAI.HarmonicCounterexample.Certificate.group50209 line 3898
269. def OAI.HarmonicCounterexample.Certificate.group50210 line 3913
270. def OAI.HarmonicCounterexample.Certificate.group50211 line 3928
271. def OAI.HarmonicCounterexample.Certificate.group50212 line 3943
272. def OAI.HarmonicCounterexample.Certificate.block0 line 3958
273. lemma OAI.HarmonicCounterexample.Certificate.block0_count line 3960
274. def OAI.HarmonicCounterexample.Certificate.block1 line 3963
275. lemma OAI.HarmonicCounterexample.Certificate.block1_count line 3965
276. def OAI.HarmonicCounterexample.Certificate.block2 line 3968
277. lemma OAI.HarmonicCounterexample.Certificate.block2_count line 3970
278. def OAI.HarmonicCounterexample.Certificate.block3 line 3973
279. lemma OAI.HarmonicCounterexample.Certificate.block3_count line 3975
280. def OAI.HarmonicCounterexample.Certificate.block4 line 3978
281. lemma OAI.HarmonicCounterexample.Certificate.block4_count line 3980
282. def OAI.HarmonicCounterexample.Certificate.block5 line 3983
283. lemma OAI.HarmonicCounterexample.Certificate.block5_count line 3985
284. def OAI.HarmonicCounterexample.Certificate.block6 line 3988
285. lemma OAI.HarmonicCounterexample.Certificate.block6_count line 3990
286. def OAI.HarmonicCounterexample.Certificate.block7 line 3993
287. lemma OAI.HarmonicCounterexample.Certificate.block7_count line 3995
288. def OAI.HarmonicCounterexample.Certificate.block8 line 3998
289. lemma OAI.HarmonicCounterexample.Certificate.block8_count line 4000
290. def OAI.HarmonicCounterexample.Certificate.block9 line 4003
291. lemma OAI.HarmonicCounterexample.Certificate.block9_count line 4005
292. def OAI.HarmonicCounterexample.Certificate.block10 line 4008
293. lemma OAI.HarmonicCounterexample.Certificate.block10_count line 4010
294. def OAI.HarmonicCounterexample.Certificate.block11 line 4013
295. lemma OAI.HarmonicCounterexample.Certificate.block11_count line 4015
296. def OAI.HarmonicCounterexample.Certificate.block12 line 4018
297. lemma OAI.HarmonicCounterexample.Certificate.block12_count line 4020
298. def OAI.HarmonicCounterexample.Certificate.block13 line 4023
299. lemma OAI.HarmonicCounterexample.Certificate.block13_count line 4025
300. def OAI.HarmonicCounterexample.Certificate.block14 line 4028
301. lemma OAI.HarmonicCounterexample.Certificate.block14_count line 4030
302. def OAI.HarmonicCounterexample.Certificate.block15 line 4033
303. lemma OAI.HarmonicCounterexample.Certificate.block15_count line 4035
304. def OAI.HarmonicCounterexample.Certificate.block16 line 4038
305. lemma OAI.HarmonicCounterexample.Certificate.block16_count line 4040
306. def OAI.HarmonicCounterexample.Certificate.block17 line 4043
307. lemma OAI.HarmonicCounterexample.Certificate.block17_count line 4045
308. def OAI.HarmonicCounterexample.Certificate.block18 line 4048
309. lemma OAI.HarmonicCounterexample.Certificate.block18_count line 4050
310. def OAI.HarmonicCounterexample.Certificate.block19 line 4053
311. lemma OAI.HarmonicCounterexample.Certificate.block19_count line 4055
312. def OAI.HarmonicCounterexample.Certificate.block20 line 4058
313. lemma OAI.HarmonicCounterexample.Certificate.block20_count line 4060
314. def OAI.HarmonicCounterexample.Certificate.block21 line 4063
315. lemma OAI.HarmonicCounterexample.Certificate.block21_count line 4065
316. def OAI.HarmonicCounterexample.Certificate.block22 line 4068
317. lemma OAI.HarmonicCounterexample.Certificate.block22_count line 4070
318. def OAI.HarmonicCounterexample.Certificate.block23 line 4073
319. lemma OAI.HarmonicCounterexample.Certificate.block23_count line 4075
320. def OAI.HarmonicCounterexample.Certificate.block24 line 4078
321. lemma OAI.HarmonicCounterexample.Certificate.block24_count line 4080
322. def OAI.HarmonicCounterexample.Certificate.superblock0 line 4083
323. lemma OAI.HarmonicCounterexample.Certificate.superblock0_count line 4085
324. def OAI.HarmonicCounterexample.Certificate.superblock1 line 4089
325. lemma OAI.HarmonicCounterexample.Certificate.superblock1_count line 4091
326. def OAI.HarmonicCounterexample.Certificate.superblock2 line 4095
327. lemma OAI.HarmonicCounterexample.Certificate.superblock2_count line 4097
328. def OAI.HarmonicCounterexample.Certificate.superblock3 line 4101
329. lemma OAI.HarmonicCounterexample.Certificate.superblock3_count line 4103
330. def OAI.HarmonicCounterexample.Certificate.superblock4 line 4107
331. lemma OAI.HarmonicCounterexample.Certificate.superblock4_count line 4109
332. def OAI.HarmonicCounterexample.Certificate.selectedGroups line 4113
333. lemma OAI.HarmonicCounterexample.Certificate.selectedGroups_count line 4115
334. lemma OAI.HarmonicCounterexample.Certificate.low_full_count line 4119
335. lemma OAI.HarmonicCounterexample.Certificate.euclidean_count line 4122
336. lemma OAI.HarmonicCounterexample.Certificate.strict_surplus line 4125