Block17 source publication inventory
Special Functions
SOURCE_MANIFEST.json
This is the original source text. Reading it does not run or verify the program.
1 {
2 "schema": 1,
3 "block": "SF-LEAN-B17",
4 "base_revision": "200a2798532028f863f923028cb0ead95563975a",
5 "publication_parent": "0eae1fe6a4bf55db27af69ef40b405643aa2e5a9",
6 "scope": "Immutable mathematical records, raw evidence, labeled diagnostics, formal/assessment inputs, dated guide and live hub snapshot; excludes this manifest and mutable current/ guidance/catalogue state. Earlier snapshots remain intact.",
7 "files": [
8 {
9 "path": "docs/SPECIAL_FUNCTIONS.md",
10 "bytes": 10100,
11 "sha256": "7c4a877e0ad0e8252b90d93d0038990587a47f03040d7a43eae2a494d1e4bb10"
12 },
13 {
14 "path": "docs/SPECIAL_FUNCTIONS_GUARDED_MAJORANT_BLOCK17.md",
15 "bytes": 2727,
16 "sha256": "6786b34937787ea5400e2d735f0ba5ea4cf48d3e9b1cc19524e2cedf149343ff"
17 },
18 {
19 "path": "monographs/special-functions/formalization/Block01/declarations.json",
20 "bytes": 3427,
21 "sha256": "cc847de0ea26dd590dd50a7c88b08e9f0e0fb3aab5b8dcd13ca04c28bcf56257"
22 },
23 {
24 "path": "monographs/special-functions/formalization/Block02/declarations.json",
25 "bytes": 2571,
26 "sha256": "2d59af08ac8323f10560ef0c875a56a4d310b299de16c703884669a6763d67d4"
27 },
28 {
29 "path": "monographs/special-functions/formalization/Block03/declarations.json",
30 "bytes": 2303,
31 "sha256": "27d5f24827734959782f77efd7100a12d2b7c074447a0ba1ca79f6ad7a4e058c"
32 },
33 {
34 "path": "monographs/special-functions/formalization/Block04/declarations.json",
35 "bytes": 1975,
36 "sha256": "cef0cfd5ad849e87aa70b145f05181ca12e7592f7c27c9fe0ab8d0757fd31a9d"
37 },
38 {
39 "path": "monographs/special-functions/formalization/Block05/declarations.json",
40 "bytes": 1667,
41 "sha256": "64feee3372696155d70ae5e680af746481f2ce5bb77ddca2e9556f09229745ae"
42 },
43 {
44 "path": "monographs/special-functions/formalization/Block06/CLAIM_MAP.json",
45 "bytes": 3615,
46 "sha256": "7f72d9f31f500e8bd1264477c1ee6ca91910100cf765d878aed5ff765984b538"
47 },
48 {
49 "path": "monographs/special-functions/formalization/Block06/declarations.json",
50 "bytes": 2339,
51 "sha256": "0500d0b7c688f76699aa981309d9d41985a67e38efe0b18949c9e8c7e5663259"
52 },
53 {
54 "path": "monographs/special-functions/formalization/Block07/declarations.json",
55 "bytes": 2972,
56 "sha256": "4673180bbe3bab15c16af752c2606bf8aa3c68c1caae544f5e634f9bec07d500"
57 },
58 {
59 "path": "monographs/special-functions/formalization/Block08/declarations.json",
60 "bytes": 2595,
61 "sha256": "ceac534b75b3eeb715c628abe510e41a80463dc69f0ec7b83f76789fafdb8c98"
62 },
63 {
64 "path": "monographs/special-functions/formalization/Block09/declarations.json",
65 "bytes": 1977,
66 "sha256": "e35d0affbd0da4b374718d8ead0334fb997e52e61610d8123df52238b83074b3"
67 },
68 {
69 "path": "monographs/special-functions/formalization/Block10/CLAIM_MAP.json",
70 "bytes": 4378,
71 "sha256": "0c36fec2f78a02b9a75f8eedb82f7b9367b161951eb994a6265d7d7157b1c7c7"
72 },
73 {
74 "path": "monographs/special-functions/formalization/Block10/declarations.json",
75 "bytes": 3965,
76 "sha256": "4aeb09db6f3ced4ff84c4a936e5380e93df1ae88b2357dd5e8cb4636d2ecf7ab"
77 },
78 {
79 "path": "monographs/special-functions/formalization/Block11/CLAIM_MAP.json",
80 "bytes": 3428,
81 "sha256": "4fff7656cc3a51f530d9011f86b5ad63aaa10458a9cfb38b29f75397a5545588"
82 },
83 {
84 "path": "monographs/special-functions/formalization/Block11/declarations.json",
85 "bytes": 2707,
86 "sha256": "d0c40586326778cdd2f9a8f1e3f5bb20f962f8c5b1fc333274cabcf0a61328bb"
87 },
88 {
89 "path": "monographs/special-functions/formalization/Block11/REMAINING_WORK.json",
90 "bytes": 10431,
91 "sha256": "a14722cadfeb17e1bc03b894a40e49c79f50174df6040c556924d9be517f9218"
92 },
93 {
94 "path": "monographs/special-functions/formalization/Block12/CLAIM_MAP.json",
95 "bytes": 4076,
96 "sha256": "1dec593631193af2dba2997d35bb4116603324064bcd97941c3623f65856b621"
97 },
98 {
99 "path": "monographs/special-functions/formalization/Block12/declarations.json",
100 "bytes": 3204,
101 "sha256": "4446f6555cfa77b07e5c72e34c7dafdda6a418d2766d9c1b0fb9e415a50120f9"
102 },
103 {
104 "path": "monographs/special-functions/formalization/Block12/REMAINING_WORK.json",
105 "bytes": 11196,
106 "sha256": "faf9829386dab0aa6994ae7f72888e98aed9ec87fb9ef838b83460f47518a686"
107 },
108 {
109 "path": "monographs/special-functions/formalization/Block13/CLAIM_MAP.json",
110 "bytes": 4765,
111 "sha256": "b82ea7a8e40707fff1816e972a41f8234f91ff7d2976e2034b0344247430ac65"
112 },
113 {
114 "path": "monographs/special-functions/formalization/Block13/declarations.json",
115 "bytes": 5170,
116 "sha256": "271520a2e68616cddd7733b86459d701d403de468335f0a22838c33180e6e5b0"
117 },
118 {
119 "path": "monographs/special-functions/formalization/Block13/REMAINING_WORK.json",
120 "bytes": 12170,
121 "sha256": "b9cf59c6155ebe5dec557d8f725c1d72db60cbb6765d430f3beb6b048608f5b0"
122 },
123 {
124 "path": "monographs/special-functions/formalization/Block14/CLAIM_MAP.json",
125 "bytes": 3969,
126 "sha256": "656b3b423b62f92f66a421108c23d12b7c5efa7502e60a9de5e3ea452c2eceba"
127 },
128 {
129 "path": "monographs/special-functions/formalization/Block14/declarations.json",
130 "bytes": 3340,
131 "sha256": "f8fd1801faacdf73c8f3ce709125e23c20eb3dad26a792cda87fbff9df50dd2f"
132 },
133 {
134 "path": "monographs/special-functions/formalization/Block14/REMAINING_WORK.json",
135 "bytes": 13018,
136 "sha256": "4f49e7ba97f18f45e0bf5ce8774530ffb1fe12eee99b1a8607bf5ad39007a5ce"
137 },
138 {
139 "path": "monographs/special-functions/formalization/Block15/CLAIM_MAP.json",
140 "bytes": 4602,
141 "sha256": "8262f2a54e41fbf651456d40d6280f59fc6877a5541e2b4770f9416037121d00"
142 },
143 {
144 "path": "monographs/special-functions/formalization/Block15/declarations.json",
145 "bytes": 4247,
146 "sha256": "32e3483d9270830520a5e2d37cc2343b6d8facc915e87cace73aa46fa45e61f2"
147 },
148 {
149 "path": "monographs/special-functions/formalization/Block15/REMAINING_WORK.json",
150 "bytes": 14263,
151 "sha256": "7754fa603cdd48064eb5a1baab0a5f2dd970bfe028ed072e022c8ef5126f24cc"
152 },
153 {
154 "path": "monographs/special-functions/formalization/Block16/CLAIM_MAP.json",
155 "bytes": 4054,
156 "sha256": "a6dd555bea82a7d3cb4943000c21ab6d3a77449e8d4cbbd782d806c6a9345ca0"
157 },
158 {
159 "path": "monographs/special-functions/formalization/Block16/declarations.json",
160 "bytes": 3593,
161 "sha256": "cdcbb211a9be8b66e8e4ea93716422f71d00249e62c0ac78116eacf5285295a5"
162 },
163 {
164 "path": "monographs/special-functions/formalization/Block16/REMAINING_WORK.json",
165 "bytes": 15177,
166 "sha256": "be368af32e2826dc21af2a9131ec146014db9612c0a985913e3883484ef26151"
167 },
168 {
169 "path": "monographs/special-functions/formalization/Block17/ATTEMPTS_AND_CORRECTIONS.md",
170 "bytes": 1935,
171 "sha256": "02b318f03fde5d1ac409c183608318344b86ac44fb726a274a118d42c0c83592"
172 },
173 {
174 "path": "monographs/special-functions/formalization/Block17/CLAIM_MAP.json",
175 "bytes": 3730,
176 "sha256": "5504b82f528db46e510e4310f0307913afc868124487475efef2ef10de15e057"
177 },
178 {
179 "path": "monographs/special-functions/formalization/Block17/CLOSEOUT.md",
180 "bytes": 1617,
181 "sha256": "2248b98b4821b2eeeb222f74078dedac6eb170b3d735af3d05f2fa1159ac0dca"
182 },
183 {
184 "path": "monographs/special-functions/formalization/Block17/declarations.json",
185 "bytes": 3531,
186 "sha256": "211335ba76a5f06b419389dbceceac6394a8f76fd629a577c5b7481f7d40b11d"
187 },
188 {
189 "path": "monographs/special-functions/formalization/Block17/development/CoupledGuardedMajorant-development-001.lean",
190 "bytes": 10360,
191 "sha256": "fe777bf48df2c23b439b3bd0ef6e5757c703316e10e685e3c06fc21a373245fd"
192 },
193 {
194 "path": "monographs/special-functions/formalization/Block17/development/CoupledGuardedMajorant-development-001.log",
195 "bytes": 243,
196 "sha256": "79a411b8dbf4b11d9618f888fb2794d67d4fdb96c45858784b27b3928739997a"
197 },
198 {
199 "path": "monographs/special-functions/formalization/Block17/development/CoupledGuardedMajorant-development-002.lean",
200 "bytes": 10360,
201 "sha256": "fe777bf48df2c23b439b3bd0ef6e5757c703316e10e685e3c06fc21a373245fd"
202 },
203 {
204 "path": "monographs/special-functions/formalization/Block17/development/CoupledGuardedMajorant-development-002.log",
205 "bytes": 1798,
206 "sha256": "2da15c80a8620ee1ce469d6074d592b3edc7bb12f1b09e6e09f685d21c232302"
207 },
208 {
209 "path": "monographs/special-functions/formalization/Block17/development/CoupledGuardedMajorant-development-003.lean",
210 "bytes": 14667,
211 "sha256": "4dcc5af1e7ae9a6caf4c9ecf8110bb13cb8cd0f1201d7c54f96f22fae0790752"
212 },
213 {
214 "path": "monographs/special-functions/formalization/Block17/development/CoupledGuardedMajorant-development-003.log",
215 "bytes": 6205,
216 "sha256": "b1260b746fc90483fd48bf0bf439883480e92f01ca0764e87bb80ee75d19ca7f"
217 },
218 {
219 "path": "monographs/special-functions/formalization/Block17/development/guarded-preflight-001.lean",
220 "bytes": 3782,
221 "sha256": "1bc09430b17d497a3dd5dd55aa5f958b6eb71a228b643d7055f1e1fe56bc700f"
222 },
223 {
224 "path": "monographs/special-functions/formalization/Block17/development/guarded-preflight-001.log",
225 "bytes": 2650,
226 "sha256": "941fc17786df937f736b10b4ed8e4fa86f5ececee30367395d8e33c3ec17d3f6"
227 },
228 {
229 "path": "monographs/special-functions/formalization/Block17/development/guarded-preflight-002.lean",
230 "bytes": 3868,
231 "sha256": "e2da7bba984868b17e15d6462b6c2b8b051d41d101bf745dfe3e889d5315d0e4"
232 },
233 {
234 "path": "monographs/special-functions/formalization/Block17/development/guarded-preflight-002.log",
235 "bytes": 2623,
236 "sha256": "b695c8608498dee641b56627890e20ac7f31375aa2554e9b31c71c66d5ca9455"
237 },
238 {
239 "path": "monographs/special-functions/formalization/Block17/development/guarded-preflight-003.lean",
240 "bytes": 3598,
241 "sha256": "ed07cf6f37e604e394096b4925f8733f404a7574112bb741c60080abd5b6859b"
242 },
243 {
244 "path": "monographs/special-functions/formalization/Block17/development/guarded-preflight-003.log",
245 "bytes": 1310,
246 "sha256": "a99cd1be3546d4e80d6f91ed58d15c4d76e3aa10363bdaabd8f54d46aabf51c3"
247 },
248 {
249 "path": "monographs/special-functions/formalization/Block17/development/scratch-guarded-majorant-batch.lean",
250 "bytes": 4155,
251 "sha256": "b84ceb1fafdd6041ff8fe943870523759efc296758f82365aeb777f5e1c918a5"
252 },
253 {
254 "path": "monographs/special-functions/formalization/Block17/development/scratch-guarded-majorant-batch.log",
255 "bytes": 635,
256 "sha256": "0629ea69c4b5553a6e3855f13f1c7da1b04272a63bb94ac51462fcb5e22b2acf"
257 },
258 {
259 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledAnalytic.log",
260 "bytes": 2676,
261 "sha256": "01fbbe555c55df58c021c49fcb259e7cd94613753dcf81407383d541a5a8bd7e"
262 },
263 {
264 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledCharacteristic.log",
265 "bytes": 3223,
266 "sha256": "566806518bf6e6afd18131d4b00ed8299b52a6437e75feaeb7c2cd8de0861436"
267 },
268 {
269 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledEntire.log",
270 "bytes": 2469,
271 "sha256": "62a85ece04c9e5ce9b2bc8e8a16dc8f6e100df943eed0456cb6be4f1a2f698c3"
272 },
273 {
274 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledEvaluation.log",
275 "bytes": 4732,
276 "sha256": "eb10f7700c095ca3a20a377aee1f63e6b8e234e728e17595ffab1945c2dbc25e"
277 },
278 {
279 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledFormal.log",
280 "bytes": 3757,
281 "sha256": "1f4565862ab4148f2d41846713d90e78ec5d7a70a12459bd76cec0541a25258e"
282 },
283 {
284 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledGermInverse.log",
285 "bytes": 1731,
286 "sha256": "29ca11b50404f4ec732608578c31e1615de73ef235fd6a047530e19ebcd240d2"
287 },
288 {
289 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledGrowthTypes.log",
290 "bytes": 2937,
291 "sha256": "4577c67387bb1c5220da0f26b4b66e963e4053b7671ca461a4a9d089e6d26131"
292 },
293 {
294 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledGuardedMajorant.log",
295 "bytes": 3857,
296 "sha256": "50ee73dda82f56e81ba6a3a055f7d6541f49e2cdf45127e3fb8425f1c08ef568"
297 },
298 {
299 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledLowerGrowth.log",
300 "bytes": 2095,
301 "sha256": "089dee8832e638911fda4950309f04afb1f29799f8e650a7e65717c9f2863449"
302 },
303 {
304 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledNormalization.log",
305 "bytes": 3962,
306 "sha256": "431f4010cdbd0e001f2dfcd254982f1f7a49e3ffd8ae79555cc8c68804f8336f"
307 },
308 {
309 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledOperator.log",
310 "bytes": 3668,
311 "sha256": "f7310d3c06690fb47124f01dd94cee0b3ddec019c8877aebd607b2b1dd8f746a"
312 },
313 {
314 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledPositiveReal.log",
315 "bytes": 2804,
316 "sha256": "b2c437fc2b3dd64acdb3ba290babb5e4accedc77b5e52e19639f92b7d0132b5e"
317 },
318 {
319 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledRescaling.log",
320 "bytes": 2510,
321 "sha256": "fa4122625f487f5fa18c8f780bc7e9185a49ca664abadfc528bdcdd7db7f58dd"
322 },
323 {
324 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledScalarReduction.log",
325 "bytes": 5768,
326 "sha256": "9cd1320677ca9f4fbccebb507bf1a6cadc897c66127543ed5a2c4a257181bdb8"
327 },
328 {
329 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledTypeProportions.log",
330 "bytes": 3501,
331 "sha256": "c5640f259db7704f918f93b732637fd20a4155030008465d8e7c0d78ef6e20f4"
332 },
333 {
334 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledUniqueness.log",
335 "bytes": 2101,
336 "sha256": "797bc578bb2b6d8dc1832700a24571df3ab0490de85746454591b722c83129d2"
337 },
338 {
339 "path": "monographs/special-functions/formalization/Block17/evidence/audit-CoupledUpperGrowth.log",
340 "bytes": 4377,
341 "sha256": "9e30f5b39cb8ca1ca3254bb3234cf9fd9dd83a70abe7f5a242a9d5902ea59fbf"
342 },
343 {
344 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledAnalytic.log",
345 "bytes": 0,
346 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
347 },
348 {
349 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledCharacteristic.log",
350 "bytes": 0,
351 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
352 },
353 {
354 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledEntire.log",
355 "bytes": 0,
356 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
357 },
358 {
359 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledEvaluation.log",
360 "bytes": 0,
361 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
362 },
363 {
364 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledFormal.log",
365 "bytes": 0,
366 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
367 },
368 {
369 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledGermInverse.log",
370 "bytes": 0,
371 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
372 },
373 {
374 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledGrowthTypes.log",
375 "bytes": 0,
376 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
377 },
378 {
379 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledGuardedMajorant.log",
380 "bytes": 0,
381 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
382 },
383 {
384 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledLowerGrowth.log",
385 "bytes": 0,
386 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
387 },
388 {
389 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledNormalization.log",
390 "bytes": 0,
391 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
392 },
393 {
394 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledOperator.log",
395 "bytes": 0,
396 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
397 },
398 {
399 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledPositiveReal.log",
400 "bytes": 0,
401 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
402 },
403 {
404 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledRescaling.log",
405 "bytes": 0,
406 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
407 },
408 {
409 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledScalarReduction.log",
410 "bytes": 0,
411 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
412 },
413 {
414 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledTypeProportions.log",
415 "bytes": 0,
416 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
417 },
418 {
419 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledUniqueness.log",
420 "bytes": 0,
421 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
422 },
423 {
424 "path": "monographs/special-functions/formalization/Block17/evidence/compile-CoupledUpperGrowth.log",
425 "bytes": 0,
426 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
427 },
428 {
429 "path": "monographs/special-functions/formalization/Block17/evidence/control-GuardedInterfaces.log",
430 "bytes": 0,
431 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
432 },
433 {
434 "path": "monographs/special-functions/formalization/Block17/evidence/control-MissingSuccess.log",
435 "bytes": 304,
436 "sha256": "5acb22a2de35e297a4f46645228e772148b58952bd5cdc51f0ef9ce0ad6b2d3e"
437 },
438 {
439 "path": "monographs/special-functions/formalization/Block17/evidence/control-Placeholder.log",
440 "bytes": 63,
441 "sha256": "0682d764d4f78ca960e5b641d4317d1a6a252cedccba3fc52d1d4285bcbcd22c"
442 },
443 {
444 "path": "monographs/special-functions/formalization/Block17/evidence/control-SeedSizeCheck.log",
445 "bytes": 160,
446 "sha256": "71a8a9941a116292d8bc60489d534d35848e5d8015eaf5fc072197e9e2f1a506"
447 },
448 {
449 "path": "monographs/special-functions/formalization/Block17/evidence/control-WrongFoldOrder.log",
450 "bytes": 68,
451 "sha256": "7a0fbc2dc6ec976b7626041ce44dd578b8fac974504f7643073b79759d7f8b78"
452 },
453 {
454 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledAnalytic.log",
455 "bytes": 27,
456 "sha256": "b34cae702aebfd97f5b6f0072c7c3870a024f5674f894bb43e5095b3abbd3e11"
457 },
458 {
459 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledCharacteristic.log",
460 "bytes": 33,
461 "sha256": "7ab004782e0bd997d0c6c4da4bd88fa3c59f1a8f67b37c5ab68b8604a1c58720"
462 },
463 {
464 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledEntire.log",
465 "bytes": 25,
466 "sha256": "c446b7b5cc66373292a4817fb55a2d5fb7529242d2c14618948bda64f5bacacf"
467 },
468 {
469 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledEvaluation.log",
470 "bytes": 29,
471 "sha256": "d8d1a695efa203aa7bb482e09575bc289672cd0e8d647d73e45c4cee9d63b6c5"
472 },
473 {
474 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledFormal.log",
475 "bytes": 25,
476 "sha256": "5677a5b892e16d2badc84a00a24d266c83e8722957f0cbe5026cdb1b3fae9d87"
477 },
478 {
479 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledGermInverse.log",
480 "bytes": 30,
481 "sha256": "41d81afce63beaa32a4e23b443babf8cc0b29822e5976309d25e8c0551b4641e"
482 },
483 {
484 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledGrowthTypes.log",
485 "bytes": 30,
486 "sha256": "02d0569e20b329c54e5ec1f9fca3b5aa17a079da19621ac8437209d97aae10e0"
487 },
488 {
489 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledGuardedMajorant.log",
490 "bytes": 34,
491 "sha256": "12f0e0b63cfb0cdd829073472d92ce55691102b9846632725ed583945c4fcfbc"
492 },
493 {
494 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledLowerGrowth.log",
495 "bytes": 30,
496 "sha256": "902005e34aafb99d0391d38f47733cb3e4e57d95bf17adcfaff4fab9f461b466"
497 },
498 {
499 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledNormalization.log",
500 "bytes": 32,
501 "sha256": "4917715134963e1596c82a035d4f3229888742709a324179d637300b56e346ee"
502 },
503 {
504 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledOperator.log",
505 "bytes": 27,
506 "sha256": "edde0347950876fbd42cb758eda027a2024943e8582fa69276685869ae987271"
507 },
508 {
509 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledPositiveReal.log",
510 "bytes": 31,
511 "sha256": "87614063b2d254266354c370ccfda3eada390bd88fc0726d99e533e502b744fc"
512 },
513 {
514 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledRescaling.log",
515 "bytes": 28,
516 "sha256": "2be26a71c3207180267b0f38d4a0b1419b0ca2f7f9c3e57b98a8fc822437018a"
517 },
518 {
519 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledScalarReduction.log",
520 "bytes": 34,
521 "sha256": "07eb9281238890692b04d108486325738b74533d0f639dd082ce915a7cedac39"
522 },
523 {
524 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledTypeProportions.log",
525 "bytes": 34,
526 "sha256": "615a9b67566d9ab88f5cb1a45e798569c9f7e6b49f4e388f12cd38cafeb6e157"
527 },
528 {
529 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledUniqueness.log",
530 "bytes": 29,
531 "sha256": "30a98c266a4da85ac60052fc1407dbcc728a60bc360fc50505cbb9836e3d0f76"
532 },
533 {
534 "path": "monographs/special-functions/formalization/Block17/evidence/kernel-CoupledUpperGrowth.log",
535 "bytes": 30,
536 "sha256": "d1db25a7f481c0fbec79d211502c26978ab96ef8f4b76cd14683899310f1d8e5"
537 },
538 {
539 "path": "monographs/special-functions/formalization/Block17/evidence/pin-aesop.log",
540 "bytes": 42,
541 "sha256": "d44104024af2d060f35ec40580c3f3bde96dce8a2439187e6ec69dc516635226"
542 },
543 {
544 "path": "monographs/special-functions/formalization/Block17/evidence/pin-batteries.log",
545 "bytes": 42,
546 "sha256": "e0a3a54a768a0ca7c42bd5ea43945f0764b4576bfee8ee81f27e5ea533c2366d"
547 },
548 {
549 "path": "monographs/special-functions/formalization/Block17/evidence/pin-Cli.log",
550 "bytes": 42,
551 "sha256": "bc44402ba0248c4c20de0520fbe58f81cc93b86368083f4411a92656bc61fc98"
552 },
553 {
554 "path": "monographs/special-functions/formalization/Block17/evidence/pin-importGraph.log",
555 "bytes": 42,
556 "sha256": "26db343c868a270c2f0bbaa414122483e8a33b2ccccd6e4f75fd8d3ae0132bf7"
557 },
558 {
559 "path": "monographs/special-functions/formalization/Block17/evidence/pin-LeanSearchClient.log",
560 "bytes": 42,
561 "sha256": "910b2313febb5044703357be69b8692792ff7b80631cf30506e64656d2f94024"
562 },
563 {
564 "path": "monographs/special-functions/formalization/Block17/evidence/pin-mathlib.log",
565 "bytes": 42,
566 "sha256": "62989ebe8b53589b05c10a31d55d06742e3e0c2ba54bbc69d678aa07dd30f172"
567 },
568 {
569 "path": "monographs/special-functions/formalization/Block17/evidence/pin-plausible.log",
570 "bytes": 42,
571 "sha256": "5a24a15a2a5fa89534035ca17f5dc4d13f0677ab9637067469bb1a4910727293"
572 },
573 {
574 "path": "monographs/special-functions/formalization/Block17/evidence/pin-proofwidgets.log",
575 "bytes": 42,
576 "sha256": "c5137af62109636b0782f96afb8061cd85449a3d0f5944e9480669cd92d656cd"
577 },
578 {
579 "path": "monographs/special-functions/formalization/Block17/evidence/pin-Qq.log",
580 "bytes": 42,
581 "sha256": "2861275b98971639094343db957db7cc9a8fc2d1b0195efb01a8b22ee9f8251f"
582 },
583 {
584 "path": "monographs/special-functions/formalization/Block17/evidence/receipt.json",
585 "bytes": 96332,
586 "sha256": "bf5d67e5128ef3dde45f66277823e30124196829873dd61158d0c9161ba33e1f"
587 },
588 {
589 "path": "monographs/special-functions/formalization/Block17/evidence/version.log",
590 "bytes": 109,
591 "sha256": "87b9d84c24871d31d733f3c474b1372aeba74b55e40dcd54247ecf506523e850"
592 },
593 {
594 "path": "monographs/special-functions/formalization/Block17/IO_MANIFEST.json",
595 "bytes": 43004,
596 "sha256": "68a25112c91d33a01f5da3f64cc567fdde4636826ba83678ef152d83887331d4"
597 },
598 {
599 "path": "monographs/special-functions/formalization/Block17/PROGRESS_v0.17.0.json",
600 "bytes": 1552,
601 "sha256": "0399c3c3e3b50e4fff57628300ff8938ea944ab02b2eeac59e33e8445d6eec8d"
602 },
603 {
604 "path": "monographs/special-functions/formalization/Block17/PROOFREADING.md",
605 "bytes": 735,
606 "sha256": "6af106f563a210618420ce15df00906a8cdee782216e7ed5d21bc7488877dbfa"
607 },
608 {
609 "path": "monographs/special-functions/formalization/Block17/REMAINING_WORK.json",
610 "bytes": 16066,
611 "sha256": "030f09c4814f22de8233c8022cd5e467db9126fade706884b5fb75e2826b51ac"
612 },
613 {
614 "path": "monographs/special-functions/formalization/Block17/REMAINING_WORK.md",
615 "bytes": 3730,
616 "sha256": "ada1120f6e3543097f2b9a48c4d6e871e336f488102647b1732f946285310f0a"
617 },
618 {
619 "path": "monographs/special-functions/formalization/Block17/REPORT.md",
620 "bytes": 3712,
621 "sha256": "525d93c14032a84acb2c02fd70b0847d2551a7cbad4d0fdd9f704e8eafc0bcb8"
622 },
623 {
624 "path": "monographs/special-functions/formalization/Block17/SELF_REVIEW.md",
625 "bytes": 3285,
626 "sha256": "7c1bc89fb13b3e1d2c69b6cb31aff5726396b3f6f84ec388db8092fcda07fdea"
627 },
628 {
629 "path": "monographs/special-functions/formalization/Block17/TARGET.md",
630 "bytes": 2998,
631 "sha256": "5738e1114dc58abf239b001f956ee2cf20ee2f1480eaba9e2778b92b422e4abb"
632 },
633 {
634 "path": "monographs/special-functions/lean/BrowserCoreLocal.lean",
635 "bytes": 16306,
636 "sha256": "610dc4b03643dbc69e780cde91f6bc58c3c1050be4c82c3a182f03cae9fbd95c"
637 },
638 {
639 "path": "monographs/special-functions/lean/CoupledAnalytic.lean",
640 "bytes": 11864,
641 "sha256": "4317cc45436eb5434b0ddd1418bd4096b3865cf4e9a92e32f2e5b23eeb1a247f"
642 },
643 {
644 "path": "monographs/special-functions/lean/CoupledAnalyticAudit.lean",
645 "bytes": 1659,
646 "sha256": "24327e3a8365da563fb7c654ecf379d9ec14ac5d137c3a5a27a00b883bf12051"
647 },
648 {
649 "path": "monographs/special-functions/lean/CoupledCharacteristic.lean",
650 "bytes": 15542,
651 "sha256": "bba339b502ee9582dda88e226d3544e367cfce8a6153e14345d6c8e86a62eb84"
652 },
653 {
654 "path": "monographs/special-functions/lean/CoupledCharacteristicAudit.lean",
655 "bytes": 2057,
656 "sha256": "c6871063f94b1e70dc1656737863d91eef847dc6f5f39e0a048ccdadaf496cf0"
657 },
658 {
659 "path": "monographs/special-functions/lean/CoupledEntire.lean",
660 "bytes": 13938,
661 "sha256": "48359369ee25322fb301a060d239c2f688f46ac59098394a22fd7a3f6272cb64"
662 },
663 {
664 "path": "monographs/special-functions/lean/CoupledEntireAudit.lean",
665 "bytes": 1523,
666 "sha256": "26d045313a9af0ba5dba699fb3b4a87403824f5cbfb1fc5778009d16fc3233de"
667 },
668 {
669 "path": "monographs/special-functions/lean/CoupledEvaluation.lean",
670 "bytes": 21743,
671 "sha256": "59bf338f4b10672501ebf1a6dd0e2e02c74b86750adef2cc679fabc735dc1cd9"
672 },
673 {
674 "path": "monographs/special-functions/lean/CoupledEvaluationAudit.lean",
675 "bytes": 2894,
676 "sha256": "5eac0617b6c36c875a5da3f43aa8ca9e484aea17d84ea5f15720358ee2f3c972"
677 },
678 {
679 "path": "monographs/special-functions/lean/CoupledFormal.lean",
680 "bytes": 20471,
681 "sha256": "18ca2a8c463d83c9402bab3f2c312fd84e1a63fdb21873d669f6d2d0cc4d6c87"
682 },
683 {
684 "path": "monographs/special-functions/lean/CoupledFormalAudit.lean",
685 "bytes": 2303,
686 "sha256": "f6d92e0dec5458142cbbf0b2b717b5233f2330b59ef58e89c8be10361f24f437"
687 },
688 {
689 "path": "monographs/special-functions/lean/CoupledGermInverse.lean",
690 "bytes": 7481,
691 "sha256": "92a0a2fa8fa33a9f6d602e73d8714c645d57b8bcee4d89205f87ad9dfb56bb2b"
692 },
693 {
694 "path": "monographs/special-functions/lean/CoupledGermInverseAudit.lean",
695 "bytes": 1094,
696 "sha256": "fd14f78ea526cb4eab5e57f4f7a64c95161c14299b145be811b2ccb20e1ca6db"
697 },
698 {
699 "path": "monographs/special-functions/lean/CoupledGrowthTypes.lean",
700 "bytes": 12547,
701 "sha256": "1363c216cfd64706fce14bc8fece963f3313ecc3b4e393a7486c89b09b313c7a"
702 },
703 {
704 "path": "monographs/special-functions/lean/CoupledGrowthTypesAudit.lean",
705 "bytes": 1828,
706 "sha256": "92e54ca0a72c76e6ede67b590a1152f7de3eed5c21f226a1fbe56c942d93e1fe"
707 },
708 {
709 "path": "monographs/special-functions/lean/CoupledGuardedMajorant.lean",
710 "bytes": 15497,
711 "sha256": "349f0d3ae54d93aa5035cee180e26c8d8ba30169c478511136af20cc6d421b0c"
712 },
713 {
714 "path": "monographs/special-functions/lean/CoupledGuardedMajorantAudit.lean",
715 "bytes": 2378,
716 "sha256": "66312a82efcb43fe59998181bd3c872c33956b221fca5a47c61bfa1db980ddf8"
717 },
718 {
719 "path": "monographs/special-functions/lean/CoupledLowerGrowth.lean",
720 "bytes": 12398,
721 "sha256": "17b055c76799ed380374f2834d47cdf461d52ee95fab0babd9151f602e1c540f"
722 },
723 {
724 "path": "monographs/special-functions/lean/CoupledLowerGrowthAudit.lean",
725 "bytes": 1302,
726 "sha256": "76b48f9a4aac1d6e996c1b7deabf17cf77821a72f461046f59e9c4e5e84cd2e7"
727 },
728 {
729 "path": "monographs/special-functions/lean/CoupledNormalization.lean",
730 "bytes": 13312,
731 "sha256": "907fd0fa37a59dff472088a2afa6cc4f9bb22663ce9d153378560cfdeaa549f8"
732 },
733 {
734 "path": "monographs/special-functions/lean/CoupledNormalizationAudit.lean",
735 "bytes": 2443,
736 "sha256": "ae5eb111ac8335a186618a20171734e385322ccef7aa0b71985cc83ed523a3af"
737 },
738 {
739 "path": "monographs/special-functions/lean/CoupledOperator.lean",
740 "bytes": 14441,
741 "sha256": "743c863d39fccb19ea88e09e49671ffddaea40030ad867a8902c4169e9e1a047"
742 },
743 {
744 "path": "monographs/special-functions/lean/CoupledOperatorAudit.lean",
745 "bytes": 2288,
746 "sha256": "6b4cd5578f5ebaceb20d704ac7acc29b90fc5360f53bda5a46ebd1c5d18573f0"
747 },
748 {
749 "path": "monographs/special-functions/lean/CoupledPositiveReal.lean",
750 "bytes": 13569,
751 "sha256": "a1e1b4f42efbffd0dcb0acf1a8b9ab23fe9fd775397219ad2c7961789414a8d7"
752 },
753 {
754 "path": "monographs/special-functions/lean/CoupledPositiveRealAudit.lean",
755 "bytes": 1716,
756 "sha256": "49a920db319b72249aa31058c6f492238dbe239de18644defccc4dad6f25bdbe"
757 },
758 {
759 "path": "monographs/special-functions/lean/CoupledRescaling.lean",
760 "bytes": 14717,
761 "sha256": "83a014bccd72204a121a11b6e558100da0b2accef37be43fcad809be037eea5e"
762 },
763 {
764 "path": "monographs/special-functions/lean/CoupledRescalingAudit.lean",
765 "bytes": 1559,
766 "sha256": "97104bd96fe19af8bb0d2e700940258cb084ae044ca0f47ab86d9264536f8b76"
767 },
768 {
769 "path": "monographs/special-functions/lean/CoupledScalarReduction.lean",
770 "bytes": 20328,
771 "sha256": "4ca29da51d06096d34b8e85d62018d2c8c03329f1378f7e57d69926f62119c00"
772 },
773 {
774 "path": "monographs/special-functions/lean/CoupledScalarReductionAudit.lean",
775 "bytes": 3579,
776 "sha256": "53ed37138bafd35638304c2cb5c644930b5f4b7c403ee5705e3e9f26b6cfc536"
777 },
778 {
779 "path": "monographs/special-functions/lean/CoupledTypeProportions.lean",
780 "bytes": 26412,
781 "sha256": "c6b3d8dfb786730a7b0ed456992dd87af160016841bfd7195596017b42a16194"
782 },
783 {
784 "path": "monographs/special-functions/lean/CoupledTypeProportionsAudit.lean",
785 "bytes": 2188,
786 "sha256": "4532e08e1efa4619f56e134e53a29e6a3b94a6bf7b2d284531f912f0640ebe3f"
787 },
788 {
789 "path": "monographs/special-functions/lean/CoupledUniqueness.lean",
790 "bytes": 12294,
791 "sha256": "40ce00b496300eff1cefd1204918e43661b9487273d90e13c6b8352c305f5e21"
792 },
793 {
794 "path": "monographs/special-functions/lean/CoupledUniquenessAudit.lean",
795 "bytes": 1299,
796 "sha256": "228af41b5b27418b3d4202df64b144c84affb9a4e05cdfbeb7a8d8e438823180"
797 },
798 {
799 "path": "monographs/special-functions/lean/CoupledUpperGrowth.lean",
800 "bytes": 28188,
801 "sha256": "0b899b5d8639a9fe6a957af7ceffc7a3e173557c0bc7f347c92dc92fec344f1d"
802 },
803 {
804 "path": "monographs/special-functions/lean/CoupledUpperGrowthAudit.lean",
805 "bytes": 2676,
806 "sha256": "6ecf165aa171a96f4bd8d7ed1f8bb1e9bd4d81dca3d4711e4946f7005be398be"
807 },
808 {
809 "path": "monographs/special-functions/lean/dependency_pins.json",
810 "bytes": 3574,
811 "sha256": "2ba2018e7b8400a7d83c028a312111c629c07f4c882b03f1d303340c78d6f218"
812 },
813 {
814 "path": "monographs/special-functions/lean/guarded_majorant_controls/GuardedInterfaces.lean",
815 "bytes": 2872,
816 "sha256": "db154df0784b0e0ab4c783bc4715b95e76506d26aa0334eb553f9e65e4a4879c"
817 },
818 {
819 "path": "monographs/special-functions/lean/guarded_majorant_controls/manifest.json",
820 "bytes": 551,
821 "sha256": "58bec4ec119bb3d53af2b967c28288fba90d387161f436ecbcfde4d94a55ef4b"
822 },
823 {
824 "path": "monographs/special-functions/lean/guarded_majorant_controls/MissingSuccess.lean",
825 "bytes": 487,
826 "sha256": "7fc06fd8c21959132b8f9b57f4b6eeeb8da94edf875873926db88230e4be721d"
827 },
828 {
829 "path": "monographs/special-functions/lean/guarded_majorant_controls/Placeholder.lean",
830 "bytes": 127,
831 "sha256": "2177f3660448e3b75d6cfb0e832c6054df4d104ddd6e4b9defc516a2624b67c3"
832 },
833 {
834 "path": "monographs/special-functions/lean/guarded_majorant_controls/SeedSizeCheck.lean",
835 "bytes": 326,
836 "sha256": "ce8b8866a49191c2960b99adfb4ed6829e0612e7b592d3c210fbbf0d378dd426"
837 },
838 {
839 "path": "monographs/special-functions/lean/guarded_majorant_controls/WrongFoldOrder.lean",
840 "bytes": 208,
841 "sha256": "7b98be33d886e664e29eff84d149a80f6ec9413c94be4ac1cbeb0abb7387fe3e"
842 },
843 {
844 "path": "monographs/special-functions/LEAN_STATUS.md",
845 "bytes": 2036,
846 "sha256": "6cfe5b218d17085de87eb520a11021e87e8182677674ac7b5ab707e90c575a58"
847 },
848 {
849 "path": "monographs/special-functions/monograph/main.tex",
850 "bytes": 27330,
851 "sha256": "87aed62acfff0d2459d4fd681a275647c39dfdc26390e140e46dc8326faac012"
852 },
853 {
854 "path": "monographs/special-functions/monograph/sections/arithmetic_full.tex",
855 "bytes": 20583,
856 "sha256": "9be2b7608113ddd8c999b354a514260d7d0ad8ed6d82fdcc84f0d341e4cc4077"
857 },
858 {
859 "path": "monographs/special-functions/monograph/sections/dilation_full.tex",
860 "bytes": 9041,
861 "sha256": "82e6f0d01ba7f74e57c7aa8c5e72b08fdd105740835799b57c9829ad39851bd1"
862 },
863 {
864 "path": "monographs/special-functions/monograph/sections/proof_map.tex",
865 "bytes": 1971,
866 "sha256": "5dd77cbc25ee8e6d8e55b6e38d3643cdf4e2389cccfab227303c169202dc3fd3"
867 },
868 {
869 "path": "monographs/special-functions/monograph/sections/sequence_full.tex",
870 "bytes": 17301,
871 "sha256": "89fd6815d44a5a22a5b53e6bfd42ef8d15e224be6b5d4d7355bcf46086678066"
872 },
873 {
874 "path": "monographs/special-functions/monograph/sections/sieve_full.tex",
875 "bytes": 18393,
876 "sha256": "6782798e9c965e4e73ca5c819fa0afd44a66324b214cd1d2af8bc86ba08e1478"
877 },
878 {
879 "path": "monographs/special-functions/monograph/sections/spectral_full.tex",
880 "bytes": 18201,
881 "sha256": "b44d7c4d943f4b96aec9f0e60ccacf9013e6ba4e48de7182fcf818056893a827"
882 },
883 {
884 "path": "monographs/special-functions/monograph/sections_v11/coupled_growth_full.tex",
885 "bytes": 15016,
886 "sha256": "f57be25d0f0995bc917246bfecdd0e3ca096fbdd5d8a04f67d4efa602ac7a55e"
887 },
888 {
889 "path": "monographs/special-functions/monograph/sections_v11/coupled_inverse_full.tex",
890 "bytes": 6142,
891 "sha256": "30baa4f5be97ed2e057e239e48172bc4586729a8c338ded226b30cc4acaf5ec6"
892 },
893 {
894 "path": "monographs/special-functions/monograph/sections_v11/coupled_lab_full.tex",
895 "bytes": 5120,
896 "sha256": "c8c069de5c5aa4638021c87e2e56a7ce3c77a983a112cec4d95fd5b5aa932ec7"
897 },
898 {
899 "path": "monographs/special-functions/monograph/sections_v11/coupled_structure_full.tex",
900 "bytes": 9067,
901 "sha256": "6fb71b94c4680fc8ef2b22e310bed9220d8820fdce107ddd9a4d1c145538cf21"
902 },
903 {
904 "path": "monographs/special-functions/monograph/sections_v11/resolution_full.tex",
905 "bytes": 21478,
906 "sha256": "ae9e2b3182ba293a9fc5fbff799382b1e55d5b1414ecaa687dba46112c5911c0"
907 },
908 {
909 "path": "monographs/special-functions/research/coupled_lab.py",
910 "bytes": 8988,
911 "sha256": "dff2a80db6f459e52dda45bc3399e0be45edf287df2efbeb1a56b57d38dfe20a"
912 },
913 {
914 "path": "monographs/special-functions/research/family_lab.py",
915 "bytes": 10565,
916 "sha256": "7b546c1cd3159bb59634a3306c116719cd8d8d368c0046af90270c709b08cc8e"
917 },
918 {
919 "path": "monographs/special-functions/tools/verify_coupled_guarded_majorant.py",
920 "bytes": 10901,
921 "sha256": "ac2926ca7ca6b95669a54b41d4bdbc9767b1e3e5c21be4d06dc6743cc2b5a035"
922 }
923 ]
924 }
Other PDFs for this work
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: 28397265a8c046fe96808490ad63d0d6f36237de1d611a360897f7505faf566a