IO_MANIFEST.json
Special Functions
IO_MANIFEST.json
This is the original source text. Reading it does not run or verify the program.
1 {
2 "schema": 1,
3 "checkpoint": "SF-LEAN-B17",
4 "base_revision": "200a2798532028f863f923028cb0ead95563975a",
5 "publication_parent": "0eae1fe6a4bf55db27af69ef40b405643aa2e5a9",
6 "input_root": "monographs/special-functions",
7 "inputs": [
8 {
9 "path": "formalization/Block01/declarations.json",
10 "bytes": 3427,
11 "sha256": "cc847de0ea26dd590dd50a7c88b08e9f0e0fb3aab5b8dcd13ca04c28bcf56257"
12 },
13 {
14 "path": "formalization/Block02/declarations.json",
15 "bytes": 2571,
16 "sha256": "2d59af08ac8323f10560ef0c875a56a4d310b299de16c703884669a6763d67d4"
17 },
18 {
19 "path": "formalization/Block03/declarations.json",
20 "bytes": 2303,
21 "sha256": "27d5f24827734959782f77efd7100a12d2b7c074447a0ba1ca79f6ad7a4e058c"
22 },
23 {
24 "path": "formalization/Block04/declarations.json",
25 "bytes": 1975,
26 "sha256": "cef0cfd5ad849e87aa70b145f05181ca12e7592f7c27c9fe0ab8d0757fd31a9d"
27 },
28 {
29 "path": "formalization/Block05/declarations.json",
30 "bytes": 1667,
31 "sha256": "64feee3372696155d70ae5e680af746481f2ce5bb77ddca2e9556f09229745ae"
32 },
33 {
34 "path": "formalization/Block06/declarations.json",
35 "bytes": 2339,
36 "sha256": "0500d0b7c688f76699aa981309d9d41985a67e38efe0b18949c9e8c7e5663259"
37 },
38 {
39 "path": "formalization/Block07/declarations.json",
40 "bytes": 2972,
41 "sha256": "4673180bbe3bab15c16af752c2606bf8aa3c68c1caae544f5e634f9bec07d500"
42 },
43 {
44 "path": "formalization/Block08/declarations.json",
45 "bytes": 2595,
46 "sha256": "ceac534b75b3eeb715c628abe510e41a80463dc69f0ec7b83f76789fafdb8c98"
47 },
48 {
49 "path": "formalization/Block09/declarations.json",
50 "bytes": 1977,
51 "sha256": "e35d0affbd0da4b374718d8ead0334fb997e52e61610d8123df52238b83074b3"
52 },
53 {
54 "path": "formalization/Block10/declarations.json",
55 "bytes": 3965,
56 "sha256": "4aeb09db6f3ced4ff84c4a936e5380e93df1ae88b2357dd5e8cb4636d2ecf7ab"
57 },
58 {
59 "path": "formalization/Block11/declarations.json",
60 "bytes": 2707,
61 "sha256": "d0c40586326778cdd2f9a8f1e3f5bb20f962f8c5b1fc333274cabcf0a61328bb"
62 },
63 {
64 "path": "formalization/Block12/declarations.json",
65 "bytes": 3204,
66 "sha256": "4446f6555cfa77b07e5c72e34c7dafdda6a418d2766d9c1b0fb9e415a50120f9"
67 },
68 {
69 "path": "formalization/Block13/declarations.json",
70 "bytes": 5170,
71 "sha256": "271520a2e68616cddd7733b86459d701d403de468335f0a22838c33180e6e5b0"
72 },
73 {
74 "path": "formalization/Block14/declarations.json",
75 "bytes": 3340,
76 "sha256": "f8fd1801faacdf73c8f3ce709125e23c20eb3dad26a792cda87fbff9df50dd2f"
77 },
78 {
79 "path": "formalization/Block15/declarations.json",
80 "bytes": 4247,
81 "sha256": "32e3483d9270830520a5e2d37cc2343b6d8facc915e87cace73aa46fa45e61f2"
82 },
83 {
84 "path": "formalization/Block16/declarations.json",
85 "bytes": 3593,
86 "sha256": "cdcbb211a9be8b66e8e4ea93716422f71d00249e62c0ac78116eacf5285295a5"
87 },
88 {
89 "path": "formalization/Block17/declarations.json",
90 "bytes": 3531,
91 "sha256": "211335ba76a5f06b419389dbceceac6394a8f76fd629a577c5b7481f7d40b11d"
92 },
93 {
94 "path": "lean/CoupledAnalytic.lean",
95 "bytes": 11864,
96 "sha256": "4317cc45436eb5434b0ddd1418bd4096b3865cf4e9a92e32f2e5b23eeb1a247f"
97 },
98 {
99 "path": "lean/CoupledAnalyticAudit.lean",
100 "bytes": 1659,
101 "sha256": "24327e3a8365da563fb7c654ecf379d9ec14ac5d137c3a5a27a00b883bf12051"
102 },
103 {
104 "path": "lean/CoupledCharacteristic.lean",
105 "bytes": 15542,
106 "sha256": "bba339b502ee9582dda88e226d3544e367cfce8a6153e14345d6c8e86a62eb84"
107 },
108 {
109 "path": "lean/CoupledCharacteristicAudit.lean",
110 "bytes": 2057,
111 "sha256": "c6871063f94b1e70dc1656737863d91eef847dc6f5f39e0a048ccdadaf496cf0"
112 },
113 {
114 "path": "lean/CoupledEntire.lean",
115 "bytes": 13938,
116 "sha256": "48359369ee25322fb301a060d239c2f688f46ac59098394a22fd7a3f6272cb64"
117 },
118 {
119 "path": "lean/CoupledEntireAudit.lean",
120 "bytes": 1523,
121 "sha256": "26d045313a9af0ba5dba699fb3b4a87403824f5cbfb1fc5778009d16fc3233de"
122 },
123 {
124 "path": "lean/CoupledEvaluation.lean",
125 "bytes": 21743,
126 "sha256": "59bf338f4b10672501ebf1a6dd0e2e02c74b86750adef2cc679fabc735dc1cd9"
127 },
128 {
129 "path": "lean/CoupledEvaluationAudit.lean",
130 "bytes": 2894,
131 "sha256": "5eac0617b6c36c875a5da3f43aa8ca9e484aea17d84ea5f15720358ee2f3c972"
132 },
133 {
134 "path": "lean/CoupledFormal.lean",
135 "bytes": 20471,
136 "sha256": "18ca2a8c463d83c9402bab3f2c312fd84e1a63fdb21873d669f6d2d0cc4d6c87"
137 },
138 {
139 "path": "lean/CoupledFormalAudit.lean",
140 "bytes": 2303,
141 "sha256": "f6d92e0dec5458142cbbf0b2b717b5233f2330b59ef58e89c8be10361f24f437"
142 },
143 {
144 "path": "lean/CoupledGermInverse.lean",
145 "bytes": 7481,
146 "sha256": "92a0a2fa8fa33a9f6d602e73d8714c645d57b8bcee4d89205f87ad9dfb56bb2b"
147 },
148 {
149 "path": "lean/CoupledGermInverseAudit.lean",
150 "bytes": 1094,
151 "sha256": "fd14f78ea526cb4eab5e57f4f7a64c95161c14299b145be811b2ccb20e1ca6db"
152 },
153 {
154 "path": "lean/CoupledGrowthTypes.lean",
155 "bytes": 12547,
156 "sha256": "1363c216cfd64706fce14bc8fece963f3313ecc3b4e393a7486c89b09b313c7a"
157 },
158 {
159 "path": "lean/CoupledGrowthTypesAudit.lean",
160 "bytes": 1828,
161 "sha256": "92e54ca0a72c76e6ede67b590a1152f7de3eed5c21f226a1fbe56c942d93e1fe"
162 },
163 {
164 "path": "lean/CoupledGuardedMajorant.lean",
165 "bytes": 15497,
166 "sha256": "349f0d3ae54d93aa5035cee180e26c8d8ba30169c478511136af20cc6d421b0c"
167 },
168 {
169 "path": "lean/CoupledGuardedMajorantAudit.lean",
170 "bytes": 2378,
171 "sha256": "66312a82efcb43fe59998181bd3c872c33956b221fca5a47c61bfa1db980ddf8"
172 },
173 {
174 "path": "lean/CoupledLowerGrowth.lean",
175 "bytes": 12398,
176 "sha256": "17b055c76799ed380374f2834d47cdf461d52ee95fab0babd9151f602e1c540f"
177 },
178 {
179 "path": "lean/CoupledLowerGrowthAudit.lean",
180 "bytes": 1302,
181 "sha256": "76b48f9a4aac1d6e996c1b7deabf17cf77821a72f461046f59e9c4e5e84cd2e7"
182 },
183 {
184 "path": "lean/CoupledNormalization.lean",
185 "bytes": 13312,
186 "sha256": "907fd0fa37a59dff472088a2afa6cc4f9bb22663ce9d153378560cfdeaa549f8"
187 },
188 {
189 "path": "lean/CoupledNormalizationAudit.lean",
190 "bytes": 2443,
191 "sha256": "ae5eb111ac8335a186618a20171734e385322ccef7aa0b71985cc83ed523a3af"
192 },
193 {
194 "path": "lean/CoupledOperator.lean",
195 "bytes": 14441,
196 "sha256": "743c863d39fccb19ea88e09e49671ffddaea40030ad867a8902c4169e9e1a047"
197 },
198 {
199 "path": "lean/CoupledOperatorAudit.lean",
200 "bytes": 2288,
201 "sha256": "6b4cd5578f5ebaceb20d704ac7acc29b90fc5360f53bda5a46ebd1c5d18573f0"
202 },
203 {
204 "path": "lean/CoupledPositiveReal.lean",
205 "bytes": 13569,
206 "sha256": "a1e1b4f42efbffd0dcb0acf1a8b9ab23fe9fd775397219ad2c7961789414a8d7"
207 },
208 {
209 "path": "lean/CoupledPositiveRealAudit.lean",
210 "bytes": 1716,
211 "sha256": "49a920db319b72249aa31058c6f492238dbe239de18644defccc4dad6f25bdbe"
212 },
213 {
214 "path": "lean/CoupledRescaling.lean",
215 "bytes": 14717,
216 "sha256": "83a014bccd72204a121a11b6e558100da0b2accef37be43fcad809be037eea5e"
217 },
218 {
219 "path": "lean/CoupledRescalingAudit.lean",
220 "bytes": 1559,
221 "sha256": "97104bd96fe19af8bb0d2e700940258cb084ae044ca0f47ab86d9264536f8b76"
222 },
223 {
224 "path": "lean/CoupledScalarReduction.lean",
225 "bytes": 20328,
226 "sha256": "4ca29da51d06096d34b8e85d62018d2c8c03329f1378f7e57d69926f62119c00"
227 },
228 {
229 "path": "lean/CoupledScalarReductionAudit.lean",
230 "bytes": 3579,
231 "sha256": "53ed37138bafd35638304c2cb5c644930b5f4b7c403ee5705e3e9f26b6cfc536"
232 },
233 {
234 "path": "lean/CoupledTypeProportions.lean",
235 "bytes": 26412,
236 "sha256": "c6b3d8dfb786730a7b0ed456992dd87af160016841bfd7195596017b42a16194"
237 },
238 {
239 "path": "lean/CoupledTypeProportionsAudit.lean",
240 "bytes": 2188,
241 "sha256": "4532e08e1efa4619f56e134e53a29e6a3b94a6bf7b2d284531f912f0640ebe3f"
242 },
243 {
244 "path": "lean/CoupledUniqueness.lean",
245 "bytes": 12294,
246 "sha256": "40ce00b496300eff1cefd1204918e43661b9487273d90e13c6b8352c305f5e21"
247 },
248 {
249 "path": "lean/CoupledUniquenessAudit.lean",
250 "bytes": 1299,
251 "sha256": "228af41b5b27418b3d4202df64b144c84affb9a4e05cdfbeb7a8d8e438823180"
252 },
253 {
254 "path": "lean/CoupledUpperGrowth.lean",
255 "bytes": 28188,
256 "sha256": "0b899b5d8639a9fe6a957af7ceffc7a3e173557c0bc7f347c92dc92fec344f1d"
257 },
258 {
259 "path": "lean/CoupledUpperGrowthAudit.lean",
260 "bytes": 2676,
261 "sha256": "6ecf165aa171a96f4bd8d7ed1f8bb1e9bd4d81dca3d4711e4946f7005be398be"
262 },
263 {
264 "path": "lean/dependency_pins.json",
265 "bytes": 3574,
266 "sha256": "2ba2018e7b8400a7d83c028a312111c629c07f4c882b03f1d303340c78d6f218"
267 },
268 {
269 "path": "lean/guarded_majorant_controls/GuardedInterfaces.lean",
270 "bytes": 2872,
271 "sha256": "db154df0784b0e0ab4c783bc4715b95e76506d26aa0334eb553f9e65e4a4879c"
272 },
273 {
274 "path": "lean/guarded_majorant_controls/MissingSuccess.lean",
275 "bytes": 487,
276 "sha256": "7fc06fd8c21959132b8f9b57f4b6eeeb8da94edf875873926db88230e4be721d"
277 },
278 {
279 "path": "lean/guarded_majorant_controls/Placeholder.lean",
280 "bytes": 127,
281 "sha256": "2177f3660448e3b75d6cfb0e832c6054df4d104ddd6e4b9defc516a2624b67c3"
282 },
283 {
284 "path": "lean/guarded_majorant_controls/SeedSizeCheck.lean",
285 "bytes": 326,
286 "sha256": "ce8b8866a49191c2960b99adfb4ed6829e0612e7b592d3c210fbbf0d378dd426"
287 },
288 {
289 "path": "lean/guarded_majorant_controls/WrongFoldOrder.lean",
290 "bytes": 208,
291 "sha256": "7b98be33d886e664e29eff84d149a80f6ec9413c94be4ac1cbeb0abb7387fe3e"
292 },
293 {
294 "path": "lean/guarded_majorant_controls/manifest.json",
295 "bytes": 551,
296 "sha256": "58bec4ec119bb3d53af2b967c28288fba90d387161f436ecbcfde4d94a55ef4b"
297 },
298 {
299 "path": "tools/verify_coupled_guarded_majorant.py",
300 "bytes": 10901,
301 "sha256": "ac2926ca7ca6b95669a54b41d4bdbc9767b1e3e5c21be4d06dc6743cc2b5a035"
302 }
303 ],
304 "output_root": "monographs/special-functions/formalization/Block17/evidence",
305 "external_work_root": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001",
306 "outputs": [
307 {
308 "path": "audit-CoupledAnalytic.log",
309 "bytes": 2676,
310 "sha256": "01fbbe555c55df58c021c49fcb259e7cd94613753dcf81407383d541a5a8bd7e"
311 },
312 {
313 "path": "audit-CoupledCharacteristic.log",
314 "bytes": 3223,
315 "sha256": "566806518bf6e6afd18131d4b00ed8299b52a6437e75feaeb7c2cd8de0861436"
316 },
317 {
318 "path": "audit-CoupledEntire.log",
319 "bytes": 2469,
320 "sha256": "62a85ece04c9e5ce9b2bc8e8a16dc8f6e100df943eed0456cb6be4f1a2f698c3"
321 },
322 {
323 "path": "audit-CoupledEvaluation.log",
324 "bytes": 4732,
325 "sha256": "eb10f7700c095ca3a20a377aee1f63e6b8e234e728e17595ffab1945c2dbc25e"
326 },
327 {
328 "path": "audit-CoupledFormal.log",
329 "bytes": 3757,
330 "sha256": "1f4565862ab4148f2d41846713d90e78ec5d7a70a12459bd76cec0541a25258e"
331 },
332 {
333 "path": "audit-CoupledGermInverse.log",
334 "bytes": 1731,
335 "sha256": "29ca11b50404f4ec732608578c31e1615de73ef235fd6a047530e19ebcd240d2"
336 },
337 {
338 "path": "audit-CoupledGrowthTypes.log",
339 "bytes": 2937,
340 "sha256": "4577c67387bb1c5220da0f26b4b66e963e4053b7671ca461a4a9d089e6d26131"
341 },
342 {
343 "path": "audit-CoupledGuardedMajorant.log",
344 "bytes": 3857,
345 "sha256": "50ee73dda82f56e81ba6a3a055f7d6541f49e2cdf45127e3fb8425f1c08ef568"
346 },
347 {
348 "path": "audit-CoupledLowerGrowth.log",
349 "bytes": 2095,
350 "sha256": "089dee8832e638911fda4950309f04afb1f29799f8e650a7e65717c9f2863449"
351 },
352 {
353 "path": "audit-CoupledNormalization.log",
354 "bytes": 3962,
355 "sha256": "431f4010cdbd0e001f2dfcd254982f1f7a49e3ffd8ae79555cc8c68804f8336f"
356 },
357 {
358 "path": "audit-CoupledOperator.log",
359 "bytes": 3668,
360 "sha256": "f7310d3c06690fb47124f01dd94cee0b3ddec019c8877aebd607b2b1dd8f746a"
361 },
362 {
363 "path": "audit-CoupledPositiveReal.log",
364 "bytes": 2804,
365 "sha256": "b2c437fc2b3dd64acdb3ba290babb5e4accedc77b5e52e19639f92b7d0132b5e"
366 },
367 {
368 "path": "audit-CoupledRescaling.log",
369 "bytes": 2510,
370 "sha256": "fa4122625f487f5fa18c8f780bc7e9185a49ca664abadfc528bdcdd7db7f58dd"
371 },
372 {
373 "path": "audit-CoupledScalarReduction.log",
374 "bytes": 5768,
375 "sha256": "9cd1320677ca9f4fbccebb507bf1a6cadc897c66127543ed5a2c4a257181bdb8"
376 },
377 {
378 "path": "audit-CoupledTypeProportions.log",
379 "bytes": 3501,
380 "sha256": "c5640f259db7704f918f93b732637fd20a4155030008465d8e7c0d78ef6e20f4"
381 },
382 {
383 "path": "audit-CoupledUniqueness.log",
384 "bytes": 2101,
385 "sha256": "797bc578bb2b6d8dc1832700a24571df3ab0490de85746454591b722c83129d2"
386 },
387 {
388 "path": "audit-CoupledUpperGrowth.log",
389 "bytes": 4377,
390 "sha256": "9e30f5b39cb8ca1ca3254bb3234cf9fd9dd83a70abe7f5a242a9d5902ea59fbf"
391 },
392 {
393 "path": "compile-CoupledAnalytic.log",
394 "bytes": 0,
395 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
396 },
397 {
398 "path": "compile-CoupledCharacteristic.log",
399 "bytes": 0,
400 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
401 },
402 {
403 "path": "compile-CoupledEntire.log",
404 "bytes": 0,
405 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
406 },
407 {
408 "path": "compile-CoupledEvaluation.log",
409 "bytes": 0,
410 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
411 },
412 {
413 "path": "compile-CoupledFormal.log",
414 "bytes": 0,
415 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
416 },
417 {
418 "path": "compile-CoupledGermInverse.log",
419 "bytes": 0,
420 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
421 },
422 {
423 "path": "compile-CoupledGrowthTypes.log",
424 "bytes": 0,
425 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
426 },
427 {
428 "path": "compile-CoupledGuardedMajorant.log",
429 "bytes": 0,
430 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
431 },
432 {
433 "path": "compile-CoupledLowerGrowth.log",
434 "bytes": 0,
435 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
436 },
437 {
438 "path": "compile-CoupledNormalization.log",
439 "bytes": 0,
440 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
441 },
442 {
443 "path": "compile-CoupledOperator.log",
444 "bytes": 0,
445 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
446 },
447 {
448 "path": "compile-CoupledPositiveReal.log",
449 "bytes": 0,
450 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
451 },
452 {
453 "path": "compile-CoupledRescaling.log",
454 "bytes": 0,
455 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
456 },
457 {
458 "path": "compile-CoupledScalarReduction.log",
459 "bytes": 0,
460 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
461 },
462 {
463 "path": "compile-CoupledTypeProportions.log",
464 "bytes": 0,
465 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
466 },
467 {
468 "path": "compile-CoupledUniqueness.log",
469 "bytes": 0,
470 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
471 },
472 {
473 "path": "compile-CoupledUpperGrowth.log",
474 "bytes": 0,
475 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
476 },
477 {
478 "path": "control-GuardedInterfaces.log",
479 "bytes": 0,
480 "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
481 },
482 {
483 "path": "control-MissingSuccess.log",
484 "bytes": 304,
485 "sha256": "5acb22a2de35e297a4f46645228e772148b58952bd5cdc51f0ef9ce0ad6b2d3e"
486 },
487 {
488 "path": "control-Placeholder.log",
489 "bytes": 63,
490 "sha256": "0682d764d4f78ca960e5b641d4317d1a6a252cedccba3fc52d1d4285bcbcd22c"
491 },
492 {
493 "path": "control-SeedSizeCheck.log",
494 "bytes": 160,
495 "sha256": "71a8a9941a116292d8bc60489d534d35848e5d8015eaf5fc072197e9e2f1a506"
496 },
497 {
498 "path": "control-WrongFoldOrder.log",
499 "bytes": 68,
500 "sha256": "7a0fbc2dc6ec976b7626041ce44dd578b8fac974504f7643073b79759d7f8b78"
501 },
502 {
503 "path": "kernel-CoupledAnalytic.log",
504 "bytes": 27,
505 "sha256": "b34cae702aebfd97f5b6f0072c7c3870a024f5674f894bb43e5095b3abbd3e11"
506 },
507 {
508 "path": "kernel-CoupledCharacteristic.log",
509 "bytes": 33,
510 "sha256": "7ab004782e0bd997d0c6c4da4bd88fa3c59f1a8f67b37c5ab68b8604a1c58720"
511 },
512 {
513 "path": "kernel-CoupledEntire.log",
514 "bytes": 25,
515 "sha256": "c446b7b5cc66373292a4817fb55a2d5fb7529242d2c14618948bda64f5bacacf"
516 },
517 {
518 "path": "kernel-CoupledEvaluation.log",
519 "bytes": 29,
520 "sha256": "d8d1a695efa203aa7bb482e09575bc289672cd0e8d647d73e45c4cee9d63b6c5"
521 },
522 {
523 "path": "kernel-CoupledFormal.log",
524 "bytes": 25,
525 "sha256": "5677a5b892e16d2badc84a00a24d266c83e8722957f0cbe5026cdb1b3fae9d87"
526 },
527 {
528 "path": "kernel-CoupledGermInverse.log",
529 "bytes": 30,
530 "sha256": "41d81afce63beaa32a4e23b443babf8cc0b29822e5976309d25e8c0551b4641e"
531 },
532 {
533 "path": "kernel-CoupledGrowthTypes.log",
534 "bytes": 30,
535 "sha256": "02d0569e20b329c54e5ec1f9fca3b5aa17a079da19621ac8437209d97aae10e0"
536 },
537 {
538 "path": "kernel-CoupledGuardedMajorant.log",
539 "bytes": 34,
540 "sha256": "12f0e0b63cfb0cdd829073472d92ce55691102b9846632725ed583945c4fcfbc"
541 },
542 {
543 "path": "kernel-CoupledLowerGrowth.log",
544 "bytes": 30,
545 "sha256": "902005e34aafb99d0391d38f47733cb3e4e57d95bf17adcfaff4fab9f461b466"
546 },
547 {
548 "path": "kernel-CoupledNormalization.log",
549 "bytes": 32,
550 "sha256": "4917715134963e1596c82a035d4f3229888742709a324179d637300b56e346ee"
551 },
552 {
553 "path": "kernel-CoupledOperator.log",
554 "bytes": 27,
555 "sha256": "edde0347950876fbd42cb758eda027a2024943e8582fa69276685869ae987271"
556 },
557 {
558 "path": "kernel-CoupledPositiveReal.log",
559 "bytes": 31,
560 "sha256": "87614063b2d254266354c370ccfda3eada390bd88fc0726d99e533e502b744fc"
561 },
562 {
563 "path": "kernel-CoupledRescaling.log",
564 "bytes": 28,
565 "sha256": "2be26a71c3207180267b0f38d4a0b1419b0ca2f7f9c3e57b98a8fc822437018a"
566 },
567 {
568 "path": "kernel-CoupledScalarReduction.log",
569 "bytes": 34,
570 "sha256": "07eb9281238890692b04d108486325738b74533d0f639dd082ce915a7cedac39"
571 },
572 {
573 "path": "kernel-CoupledTypeProportions.log",
574 "bytes": 34,
575 "sha256": "615a9b67566d9ab88f5cb1a45e798569c9f7e6b49f4e388f12cd38cafeb6e157"
576 },
577 {
578 "path": "kernel-CoupledUniqueness.log",
579 "bytes": 29,
580 "sha256": "30a98c266a4da85ac60052fc1407dbcc728a60bc360fc50505cbb9836e3d0f76"
581 },
582 {
583 "path": "kernel-CoupledUpperGrowth.log",
584 "bytes": 30,
585 "sha256": "d1db25a7f481c0fbec79d211502c26978ab96ef8f4b76cd14683899310f1d8e5"
586 },
587 {
588 "path": "pin-aesop.log",
589 "bytes": 42,
590 "sha256": "d44104024af2d060f35ec40580c3f3bde96dce8a2439187e6ec69dc516635226"
591 },
592 {
593 "path": "pin-batteries.log",
594 "bytes": 42,
595 "sha256": "e0a3a54a768a0ca7c42bd5ea43945f0764b4576bfee8ee81f27e5ea533c2366d"
596 },
597 {
598 "path": "pin-Cli.log",
599 "bytes": 42,
600 "sha256": "bc44402ba0248c4c20de0520fbe58f81cc93b86368083f4411a92656bc61fc98"
601 },
602 {
603 "path": "pin-importGraph.log",
604 "bytes": 42,
605 "sha256": "26db343c868a270c2f0bbaa414122483e8a33b2ccccd6e4f75fd8d3ae0132bf7"
606 },
607 {
608 "path": "pin-LeanSearchClient.log",
609 "bytes": 42,
610 "sha256": "910b2313febb5044703357be69b8692792ff7b80631cf30506e64656d2f94024"
611 },
612 {
613 "path": "pin-mathlib.log",
614 "bytes": 42,
615 "sha256": "62989ebe8b53589b05c10a31d55d06742e3e0c2ba54bbc69d678aa07dd30f172"
616 },
617 {
618 "path": "pin-plausible.log",
619 "bytes": 42,
620 "sha256": "5a24a15a2a5fa89534035ca17f5dc4d13f0677ab9637067469bb1a4910727293"
621 },
622 {
623 "path": "pin-proofwidgets.log",
624 "bytes": 42,
625 "sha256": "c5137af62109636b0782f96afb8061cd85449a3d0f5944e9480669cd92d656cd"
626 },
627 {
628 "path": "pin-Qq.log",
629 "bytes": 42,
630 "sha256": "2861275b98971639094343db957db7cc9a8fc2d1b0195efb01a8b22ee9f8251f"
631 },
632 {
633 "path": "receipt.json",
634 "bytes": 96332,
635 "sha256": "bf5d67e5128ef3dde45f66277823e30124196829873dd61158d0c9161ba33e1f"
636 },
637 {
638 "path": "version.log",
639 "bytes": 109,
640 "sha256": "87b9d84c24871d31d733f3c474b1372aeba74b55e40dcd54247ecf506523e850"
641 }
642 ],
643 "generated_objects": [
644 {
645 "path": "build/CoupledAnalytic.olean",
646 "sha256": "bad582a3f10184ad4fc46256ce79899bdc3129421bf4a16c5c76656b86ab6648",
647 "packaged": false
648 },
649 {
650 "path": "build/CoupledCharacteristic.olean",
651 "sha256": "62520836deb6d046be8149ffa976ae5a1ad615337ccbed55a00394ffc0576301",
652 "packaged": false
653 },
654 {
655 "path": "build/CoupledEntire.olean",
656 "sha256": "ae0882279dc3832088306a5b75d4181d6e85499ebd119e36c1a6609b079588c0",
657 "packaged": false
658 },
659 {
660 "path": "build/CoupledEvaluation.olean",
661 "sha256": "8ee322c2c650ed21cea63a88ea3b74781f4fefad7bb479373b8a6af06af1694b",
662 "packaged": false
663 },
664 {
665 "path": "build/CoupledFormal.olean",
666 "sha256": "78763668d71b9efdda4e622a176f558255957e7aa73cfa903dddc514e5858e0c",
667 "packaged": false
668 },
669 {
670 "path": "build/CoupledGermInverse.olean",
671 "sha256": "0922c81308d397f5e3ca3553112ffe290c0eac75fc2be773cd18328b51b04f38",
672 "packaged": false
673 },
674 {
675 "path": "build/CoupledGrowthTypes.olean",
676 "sha256": "5daf0eacf4ff861721b98a3e245fe638ef52b1e4fd29d536b1d0ec0ba768f297",
677 "packaged": false
678 },
679 {
680 "path": "build/CoupledGuardedMajorant.olean",
681 "sha256": "54a31c67af2766b1e4b51ca48fd3536b87041492c0c8b4b40352cc3d6b1ded0a",
682 "packaged": false
683 },
684 {
685 "path": "build/CoupledLowerGrowth.olean",
686 "sha256": "7f88b1783d93d146d75d5b6c497091eefb37bdc4906d6be20c0161be859387b8",
687 "packaged": false
688 },
689 {
690 "path": "build/CoupledNormalization.olean",
691 "sha256": "fa44300fa480a07124448db052af35917b91a6cf668bb43300f00016e73dfb44",
692 "packaged": false
693 },
694 {
695 "path": "build/CoupledOperator.olean",
696 "sha256": "7308d5a4f987242791aa8a7df933348da5ad0c609252317d5248a2c26f138952",
697 "packaged": false
698 },
699 {
700 "path": "build/CoupledPositiveReal.olean",
701 "sha256": "00bcb8cf4e423cf198b20d97d7fb0cc3129af56ce5ec4cdb72590126fa157f77",
702 "packaged": false
703 },
704 {
705 "path": "build/CoupledRescaling.olean",
706 "sha256": "c738b2db5b6eb42a6f7b350f24bd8a757043341d3b1ef03e67842d0f601eeb93",
707 "packaged": false
708 },
709 {
710 "path": "build/CoupledScalarReduction.olean",
711 "sha256": "fb517e450df6df0bcbf2bf70ea9ca1377a446c1077c05a9845a4b97d2ba1c067",
712 "packaged": false
713 },
714 {
715 "path": "build/CoupledTypeProportions.olean",
716 "sha256": "340a5ce8f40d2a25c8092d87eb27b89195da7070632e60689b17bdab112c6e2a",
717 "packaged": false
718 },
719 {
720 "path": "build/CoupledUniqueness.olean",
721 "sha256": "9cfb141a050059378fced0b66cd62d4c082eda01f00c6ee7e0b72173a8ac0011",
722 "packaged": false
723 },
724 {
725 "path": "build/CoupledUpperGrowth.olean",
726 "sha256": "94f1d80f535fc508df24328f610dfa1580af397392ae6abb4e44f5f63d1907a4",
727 "packaged": false
728 }
729 ],
730 "staged_input_copies": [
731 {
732 "path": "build/control-GuardedInterfaces.lean",
733 "bytes": 2872,
734 "sha256": "db154df0784b0e0ab4c783bc4715b95e76506d26aa0334eb553f9e65e4a4879c",
735 "packaged": false
736 },
737 {
738 "path": "build/control-MissingSuccess.lean",
739 "bytes": 487,
740 "sha256": "7fc06fd8c21959132b8f9b57f4b6eeeb8da94edf875873926db88230e4be721d",
741 "packaged": false
742 },
743 {
744 "path": "build/control-Placeholder.lean",
745 "bytes": 127,
746 "sha256": "2177f3660448e3b75d6cfb0e832c6054df4d104ddd6e4b9defc516a2624b67c3",
747 "packaged": false
748 },
749 {
750 "path": "build/control-SeedSizeCheck.lean",
751 "bytes": 326,
752 "sha256": "ce8b8866a49191c2960b99adfb4ed6829e0612e7b592d3c210fbbf0d378dd426",
753 "packaged": false
754 },
755 {
756 "path": "build/control-WrongFoldOrder.lean",
757 "bytes": 208,
758 "sha256": "7b98be33d886e664e29eff84d149a80f6ec9413c94be4ac1cbeb0abb7387fe3e",
759 "packaged": false
760 },
761 {
762 "path": "build/CoupledAnalytic.lean",
763 "bytes": 11864,
764 "sha256": "4317cc45436eb5434b0ddd1418bd4096b3865cf4e9a92e32f2e5b23eeb1a247f",
765 "packaged": false
766 },
767 {
768 "path": "build/CoupledAnalyticAudit.lean",
769 "bytes": 1659,
770 "sha256": "24327e3a8365da563fb7c654ecf379d9ec14ac5d137c3a5a27a00b883bf12051",
771 "packaged": false
772 },
773 {
774 "path": "build/CoupledCharacteristic.lean",
775 "bytes": 15542,
776 "sha256": "bba339b502ee9582dda88e226d3544e367cfce8a6153e14345d6c8e86a62eb84",
777 "packaged": false
778 },
779 {
780 "path": "build/CoupledCharacteristicAudit.lean",
781 "bytes": 2057,
782 "sha256": "c6871063f94b1e70dc1656737863d91eef847dc6f5f39e0a048ccdadaf496cf0",
783 "packaged": false
784 },
785 {
786 "path": "build/CoupledEntire.lean",
787 "bytes": 13938,
788 "sha256": "48359369ee25322fb301a060d239c2f688f46ac59098394a22fd7a3f6272cb64",
789 "packaged": false
790 },
791 {
792 "path": "build/CoupledEntireAudit.lean",
793 "bytes": 1523,
794 "sha256": "26d045313a9af0ba5dba699fb3b4a87403824f5cbfb1fc5778009d16fc3233de",
795 "packaged": false
796 },
797 {
798 "path": "build/CoupledEvaluation.lean",
799 "bytes": 21743,
800 "sha256": "59bf338f4b10672501ebf1a6dd0e2e02c74b86750adef2cc679fabc735dc1cd9",
801 "packaged": false
802 },
803 {
804 "path": "build/CoupledEvaluationAudit.lean",
805 "bytes": 2894,
806 "sha256": "5eac0617b6c36c875a5da3f43aa8ca9e484aea17d84ea5f15720358ee2f3c972",
807 "packaged": false
808 },
809 {
810 "path": "build/CoupledFormal.lean",
811 "bytes": 20471,
812 "sha256": "18ca2a8c463d83c9402bab3f2c312fd84e1a63fdb21873d669f6d2d0cc4d6c87",
813 "packaged": false
814 },
815 {
816 "path": "build/CoupledFormalAudit.lean",
817 "bytes": 2303,
818 "sha256": "f6d92e0dec5458142cbbf0b2b717b5233f2330b59ef58e89c8be10361f24f437",
819 "packaged": false
820 },
821 {
822 "path": "build/CoupledGermInverse.lean",
823 "bytes": 7481,
824 "sha256": "92a0a2fa8fa33a9f6d602e73d8714c645d57b8bcee4d89205f87ad9dfb56bb2b",
825 "packaged": false
826 },
827 {
828 "path": "build/CoupledGermInverseAudit.lean",
829 "bytes": 1094,
830 "sha256": "fd14f78ea526cb4eab5e57f4f7a64c95161c14299b145be811b2ccb20e1ca6db",
831 "packaged": false
832 },
833 {
834 "path": "build/CoupledGrowthTypes.lean",
835 "bytes": 12547,
836 "sha256": "1363c216cfd64706fce14bc8fece963f3313ecc3b4e393a7486c89b09b313c7a",
837 "packaged": false
838 },
839 {
840 "path": "build/CoupledGrowthTypesAudit.lean",
841 "bytes": 1828,
842 "sha256": "92e54ca0a72c76e6ede67b590a1152f7de3eed5c21f226a1fbe56c942d93e1fe",
843 "packaged": false
844 },
845 {
846 "path": "build/CoupledGuardedMajorant.lean",
847 "bytes": 15497,
848 "sha256": "349f0d3ae54d93aa5035cee180e26c8d8ba30169c478511136af20cc6d421b0c",
849 "packaged": false
850 },
851 {
852 "path": "build/CoupledGuardedMajorantAudit.lean",
853 "bytes": 2378,
854 "sha256": "66312a82efcb43fe59998181bd3c872c33956b221fca5a47c61bfa1db980ddf8",
855 "packaged": false
856 },
857 {
858 "path": "build/CoupledLowerGrowth.lean",
859 "bytes": 12398,
860 "sha256": "17b055c76799ed380374f2834d47cdf461d52ee95fab0babd9151f602e1c540f",
861 "packaged": false
862 },
863 {
864 "path": "build/CoupledLowerGrowthAudit.lean",
865 "bytes": 1302,
866 "sha256": "76b48f9a4aac1d6e996c1b7deabf17cf77821a72f461046f59e9c4e5e84cd2e7",
867 "packaged": false
868 },
869 {
870 "path": "build/CoupledNormalization.lean",
871 "bytes": 13312,
872 "sha256": "907fd0fa37a59dff472088a2afa6cc4f9bb22663ce9d153378560cfdeaa549f8",
873 "packaged": false
874 },
875 {
876 "path": "build/CoupledNormalizationAudit.lean",
877 "bytes": 2443,
878 "sha256": "ae5eb111ac8335a186618a20171734e385322ccef7aa0b71985cc83ed523a3af",
879 "packaged": false
880 },
881 {
882 "path": "build/CoupledOperator.lean",
883 "bytes": 14441,
884 "sha256": "743c863d39fccb19ea88e09e49671ffddaea40030ad867a8902c4169e9e1a047",
885 "packaged": false
886 },
887 {
888 "path": "build/CoupledOperatorAudit.lean",
889 "bytes": 2288,
890 "sha256": "6b4cd5578f5ebaceb20d704ac7acc29b90fc5360f53bda5a46ebd1c5d18573f0",
891 "packaged": false
892 },
893 {
894 "path": "build/CoupledPositiveReal.lean",
895 "bytes": 13569,
896 "sha256": "a1e1b4f42efbffd0dcb0acf1a8b9ab23fe9fd775397219ad2c7961789414a8d7",
897 "packaged": false
898 },
899 {
900 "path": "build/CoupledPositiveRealAudit.lean",
901 "bytes": 1716,
902 "sha256": "49a920db319b72249aa31058c6f492238dbe239de18644defccc4dad6f25bdbe",
903 "packaged": false
904 },
905 {
906 "path": "build/CoupledRescaling.lean",
907 "bytes": 14717,
908 "sha256": "83a014bccd72204a121a11b6e558100da0b2accef37be43fcad809be037eea5e",
909 "packaged": false
910 },
911 {
912 "path": "build/CoupledRescalingAudit.lean",
913 "bytes": 1559,
914 "sha256": "97104bd96fe19af8bb0d2e700940258cb084ae044ca0f47ab86d9264536f8b76",
915 "packaged": false
916 },
917 {
918 "path": "build/CoupledScalarReduction.lean",
919 "bytes": 20328,
920 "sha256": "4ca29da51d06096d34b8e85d62018d2c8c03329f1378f7e57d69926f62119c00",
921 "packaged": false
922 },
923 {
924 "path": "build/CoupledScalarReductionAudit.lean",
925 "bytes": 3579,
926 "sha256": "53ed37138bafd35638304c2cb5c644930b5f4b7c403ee5705e3e9f26b6cfc536",
927 "packaged": false
928 },
929 {
930 "path": "build/CoupledTypeProportions.lean",
931 "bytes": 26412,
932 "sha256": "c6b3d8dfb786730a7b0ed456992dd87af160016841bfd7195596017b42a16194",
933 "packaged": false
934 },
935 {
936 "path": "build/CoupledTypeProportionsAudit.lean",
937 "bytes": 2188,
938 "sha256": "4532e08e1efa4619f56e134e53a29e6a3b94a6bf7b2d284531f912f0640ebe3f",
939 "packaged": false
940 },
941 {
942 "path": "build/CoupledUniqueness.lean",
943 "bytes": 12294,
944 "sha256": "40ce00b496300eff1cefd1204918e43661b9487273d90e13c6b8352c305f5e21",
945 "packaged": false
946 },
947 {
948 "path": "build/CoupledUniquenessAudit.lean",
949 "bytes": 1299,
950 "sha256": "228af41b5b27418b3d4202df64b144c84affb9a4e05cdfbeb7a8d8e438823180",
951 "packaged": false
952 },
953 {
954 "path": "build/CoupledUpperGrowth.lean",
955 "bytes": 28188,
956 "sha256": "0b899b5d8639a9fe6a957af7ceffc7a3e173557c0bc7f347c92dc92fec344f1d",
957 "packaged": false
958 },
959 {
960 "path": "build/CoupledUpperGrowthAudit.lean",
961 "bytes": 2676,
962 "sha256": "6ecf165aa171a96f4bd8d7ed1f8bb1e9bd4d81dca3d4711e4946f7005be398be",
963 "packaged": false
964 }
965 ],
966 "scope_assessment_inputs": [
967 {
968 "path": "monograph/main.tex",
969 "bytes": 27330,
970 "sha256": "87aed62acfff0d2459d4fd681a275647c39dfdc26390e140e46dc8326faac012"
971 },
972 {
973 "path": "monograph/sections/proof_map.tex",
974 "bytes": 1971,
975 "sha256": "5dd77cbc25ee8e6d8e55b6e38d3643cdf4e2389cccfab227303c169202dc3fd3"
976 },
977 {
978 "path": "monograph/sections/dilation_full.tex",
979 "bytes": 9041,
980 "sha256": "82e6f0d01ba7f74e57c7aa8c5e72b08fdd105740835799b57c9829ad39851bd1"
981 },
982 {
983 "path": "monograph/sections/arithmetic_full.tex",
984 "bytes": 20583,
985 "sha256": "9be2b7608113ddd8c999b354a514260d7d0ad8ed6d82fdcc84f0d341e4cc4077"
986 },
987 {
988 "path": "monograph/sections/sieve_full.tex",
989 "bytes": 18393,
990 "sha256": "6782798e9c965e4e73ca5c819fa0afd44a66324b214cd1d2af8bc86ba08e1478"
991 },
992 {
993 "path": "monograph/sections/spectral_full.tex",
994 "bytes": 18201,
995 "sha256": "b44d7c4d943f4b96aec9f0e60ccacf9013e6ba4e48de7182fcf818056893a827"
996 },
997 {
998 "path": "monograph/sections/sequence_full.tex",
999 "bytes": 17301,
1000 "sha256": "89fd6815d44a5a22a5b53e6bfd42ef8d15e224be6b5d4d7355bcf46086678066"
1001 },
1002 {
1003 "path": "monograph/sections_v11/coupled_growth_full.tex",
1004 "bytes": 15016,
1005 "sha256": "f57be25d0f0995bc917246bfecdd0e3ca096fbdd5d8a04f67d4efa602ac7a55e"
1006 },
1007 {
1008 "path": "monograph/sections_v11/coupled_inverse_full.tex",
1009 "bytes": 6142,
1010 "sha256": "30baa4f5be97ed2e057e239e48172bc4586729a8c338ded226b30cc4acaf5ec6"
1011 },
1012 {
1013 "path": "monograph/sections_v11/coupled_structure_full.tex",
1014 "bytes": 9067,
1015 "sha256": "6fb71b94c4680fc8ef2b22e310bed9220d8820fdce107ddd9a4d1c145538cf21"
1016 },
1017 {
1018 "path": "monograph/sections_v11/resolution_full.tex",
1019 "bytes": 21478,
1020 "sha256": "ae9e2b3182ba293a9fc5fbff799382b1e55d5b1414ecaa687dba46112c5911c0"
1021 },
1022 {
1023 "path": "monograph/sections_v11/coupled_lab_full.tex",
1024 "bytes": 5120,
1025 "sha256": "c8c069de5c5aa4638021c87e2e56a7ce3c77a983a112cec4d95fd5b5aa932ec7"
1026 },
1027 {
1028 "path": "lean/BrowserCoreLocal.lean",
1029 "bytes": 16306,
1030 "sha256": "610dc4b03643dbc69e780cde91f6bc58c3c1050be4c82c3a182f03cae9fbd95c"
1031 },
1032 {
1033 "path": "LEAN_STATUS.md",
1034 "bytes": 2036,
1035 "sha256": "6cfe5b218d17085de87eb520a11021e87e8182677674ac7b5ab707e90c575a58"
1036 },
1037 {
1038 "path": "formalization/Block06/CLAIM_MAP.json",
1039 "bytes": 3615,
1040 "sha256": "7f72d9f31f500e8bd1264477c1ee6ca91910100cf765d878aed5ff765984b538"
1041 },
1042 {
1043 "path": "formalization/Block10/CLAIM_MAP.json",
1044 "bytes": 4378,
1045 "sha256": "0c36fec2f78a02b9a75f8eedb82f7b9367b161951eb994a6265d7d7157b1c7c7"
1046 },
1047 {
1048 "path": "formalization/Block11/REMAINING_WORK.json",
1049 "bytes": 10431,
1050 "sha256": "a14722cadfeb17e1bc03b894a40e49c79f50174df6040c556924d9be517f9218"
1051 },
1052 {
1053 "path": "formalization/Block11/CLAIM_MAP.json",
1054 "bytes": 3428,
1055 "sha256": "4fff7656cc3a51f530d9011f86b5ad63aaa10458a9cfb38b29f75397a5545588"
1056 },
1057 {
1058 "path": "formalization/Block12/CLAIM_MAP.json",
1059 "bytes": 4076,
1060 "sha256": "1dec593631193af2dba2997d35bb4116603324064bcd97941c3623f65856b621"
1061 },
1062 {
1063 "path": "lean/CoupledTypeProportions.lean",
1064 "bytes": 26412,
1065 "sha256": "c6b3d8dfb786730a7b0ed456992dd87af160016841bfd7195596017b42a16194"
1066 },
1067 {
1068 "path": "formalization/Block12/REMAINING_WORK.json",
1069 "bytes": 11196,
1070 "sha256": "faf9829386dab0aa6994ae7f72888e98aed9ec87fb9ef838b83460f47518a686"
1071 },
1072 {
1073 "path": "formalization/Block13/CLAIM_MAP.json",
1074 "bytes": 4765,
1075 "sha256": "b82ea7a8e40707fff1816e972a41f8234f91ff7d2976e2034b0344247430ac65"
1076 },
1077 {
1078 "path": "lean/CoupledScalarReduction.lean",
1079 "bytes": 20328,
1080 "sha256": "4ca29da51d06096d34b8e85d62018d2c8c03329f1378f7e57d69926f62119c00"
1081 },
1082 {
1083 "path": "formalization/Block13/REMAINING_WORK.json",
1084 "bytes": 12170,
1085 "sha256": "b9cf59c6155ebe5dec557d8f725c1d72db60cbb6765d430f3beb6b048608f5b0"
1086 },
1087 {
1088 "path": "formalization/Block14/CLAIM_MAP.json",
1089 "bytes": 3969,
1090 "sha256": "656b3b423b62f92f66a421108c23d12b7c5efa7502e60a9de5e3ea452c2eceba"
1091 },
1092 {
1093 "path": "lean/CoupledOperator.lean",
1094 "bytes": 14441,
1095 "sha256": "743c863d39fccb19ea88e09e49671ffddaea40030ad867a8902c4169e9e1a047"
1096 },
1097 {
1098 "path": "formalization/Block14/REMAINING_WORK.json",
1099 "bytes": 13018,
1100 "sha256": "4f49e7ba97f18f45e0bf5ce8774530ffb1fe12eee99b1a8607bf5ad39007a5ce"
1101 },
1102 {
1103 "path": "formalization/Block15/CLAIM_MAP.json",
1104 "bytes": 4602,
1105 "sha256": "8262f2a54e41fbf651456d40d6280f59fc6877a5541e2b4770f9416037121d00"
1106 },
1107 {
1108 "path": "lean/CoupledEvaluation.lean",
1109 "bytes": 21743,
1110 "sha256": "59bf338f4b10672501ebf1a6dd0e2e02c74b86750adef2cc679fabc735dc1cd9"
1111 },
1112 {
1113 "path": "research/coupled_lab.py",
1114 "bytes": 8988,
1115 "sha256": "dff2a80db6f459e52dda45bc3399e0be45edf287df2efbeb1a56b57d38dfe20a"
1116 },
1117 {
1118 "path": "research/family_lab.py",
1119 "bytes": 10565,
1120 "sha256": "7b546c1cd3159bb59634a3306c116719cd8d8d368c0046af90270c709b08cc8e"
1121 },
1122 {
1123 "path": "formalization/Block15/REMAINING_WORK.json",
1124 "bytes": 14263,
1125 "sha256": "7754fa603cdd48064eb5a1baab0a5f2dd970bfe028ed072e022c8ef5126f24cc"
1126 },
1127 {
1128 "path": "formalization/Block16/CLAIM_MAP.json",
1129 "bytes": 4054,
1130 "sha256": "a6dd555bea82a7d3cb4943000c21ab6d3a77449e8d4cbbd782d806c6a9345ca0"
1131 },
1132 {
1133 "path": "lean/CoupledNormalization.lean",
1134 "bytes": 13312,
1135 "sha256": "907fd0fa37a59dff472088a2afa6cc4f9bb22663ce9d153378560cfdeaa549f8"
1136 },
1137 {
1138 "path": "formalization/Block16/REMAINING_WORK.json",
1139 "bytes": 15177,
1140 "sha256": "be368af32e2826dc21af2a9131ec146014db9612c0a985913e3883484ef26151"
1141 },
1142 {
1143 "path": "formalization/Block17/CLAIM_MAP.json",
1144 "bytes": 3730,
1145 "sha256": "5504b82f528db46e510e4310f0307913afc868124487475efef2ef10de15e057"
1146 },
1147 {
1148 "path": "lean/CoupledGuardedMajorant.lean",
1149 "bytes": 15497,
1150 "sha256": "349f0d3ae54d93aa5035cee180e26c8d8ba30169c478511136af20cc6d421b0c"
1151 }
1152 ],
1153 "scope_assessment_output_root": "monographs/special-functions/formalization/Block17",
1154 "scope_assessment_outputs": [
1155 {
1156 "path": "REMAINING_WORK.json",
1157 "bytes": 16066,
1158 "sha256": "030f09c4814f22de8233c8022cd5e467db9126fade706884b5fb75e2826b51ac"
1159 },
1160 {
1161 "path": "REMAINING_WORK.md",
1162 "bytes": 3730,
1163 "sha256": "ada1120f6e3543097f2b9a48c4d6e871e336f488102647b1732f946285310f0a"
1164 }
1165 ],
1166 "development_diagnostic_outputs": [
1167 {
1168 "path": "development/CoupledGuardedMajorant-development-001.lean",
1169 "bytes": 10360,
1170 "sha256": "fe777bf48df2c23b439b3bd0ef6e5757c703316e10e685e3c06fc21a373245fd",
1171 "accepted_proof_evidence": false,
1172 "source_snapshot_available": true
1173 },
1174 {
1175 "path": "development/CoupledGuardedMajorant-development-001.log",
1176 "bytes": 243,
1177 "sha256": "79a411b8dbf4b11d9618f888fb2794d67d4fdb96c45858784b27b3928739997a",
1178 "accepted_proof_evidence": false,
1179 "source_snapshot_available": true
1180 },
1181 {
1182 "path": "development/CoupledGuardedMajorant-development-002.lean",
1183 "bytes": 10360,
1184 "sha256": "fe777bf48df2c23b439b3bd0ef6e5757c703316e10e685e3c06fc21a373245fd",
1185 "accepted_proof_evidence": false,
1186 "source_snapshot_available": true
1187 },
1188 {
1189 "path": "development/CoupledGuardedMajorant-development-002.log",
1190 "bytes": 1798,
1191 "sha256": "2da15c80a8620ee1ce469d6074d592b3edc7bb12f1b09e6e09f685d21c232302",
1192 "accepted_proof_evidence": false,
1193 "source_snapshot_available": true
1194 },
1195 {
1196 "path": "development/CoupledGuardedMajorant-development-003.lean",
1197 "bytes": 14667,
1198 "sha256": "4dcc5af1e7ae9a6caf4c9ecf8110bb13cb8cd0f1201d7c54f96f22fae0790752",
1199 "accepted_proof_evidence": false,
1200 "source_snapshot_available": true
1201 },
1202 {
1203 "path": "development/CoupledGuardedMajorant-development-003.log",
1204 "bytes": 6205,
1205 "sha256": "b1260b746fc90483fd48bf0bf439883480e92f01ca0764e87bb80ee75d19ca7f",
1206 "accepted_proof_evidence": false,
1207 "source_snapshot_available": true
1208 },
1209 {
1210 "path": "development/guarded-preflight-001.lean",
1211 "bytes": 3782,
1212 "sha256": "1bc09430b17d497a3dd5dd55aa5f958b6eb71a228b643d7055f1e1fe56bc700f",
1213 "accepted_proof_evidence": false,
1214 "source_snapshot_available": true
1215 },
1216 {
1217 "path": "development/guarded-preflight-001.log",
1218 "bytes": 2650,
1219 "sha256": "941fc17786df937f736b10b4ed8e4fa86f5ececee30367395d8e33c3ec17d3f6",
1220 "accepted_proof_evidence": false,
1221 "source_snapshot_available": true
1222 },
1223 {
1224 "path": "development/guarded-preflight-002.lean",
1225 "bytes": 3868,
1226 "sha256": "e2da7bba984868b17e15d6462b6c2b8b051d41d101bf745dfe3e889d5315d0e4",
1227 "accepted_proof_evidence": false,
1228 "source_snapshot_available": true
1229 },
1230 {
1231 "path": "development/guarded-preflight-002.log",
1232 "bytes": 2623,
1233 "sha256": "b695c8608498dee641b56627890e20ac7f31375aa2554e9b31c71c66d5ca9455",
1234 "accepted_proof_evidence": false,
1235 "source_snapshot_available": true
1236 },
1237 {
1238 "path": "development/guarded-preflight-003.lean",
1239 "bytes": 3598,
1240 "sha256": "ed07cf6f37e604e394096b4925f8733f404a7574112bb741c60080abd5b6859b",
1241 "accepted_proof_evidence": false,
1242 "source_snapshot_available": true
1243 },
1244 {
1245 "path": "development/guarded-preflight-003.log",
1246 "bytes": 1310,
1247 "sha256": "a99cd1be3546d4e80d6f91ed58d15c4d76e3aa10363bdaabd8f54d46aabf51c3",
1248 "accepted_proof_evidence": false,
1249 "source_snapshot_available": true
1250 },
1251 {
1252 "path": "development/scratch-guarded-majorant-batch.lean",
1253 "bytes": 4155,
1254 "sha256": "b84ceb1fafdd6041ff8fe943870523759efc296758f82365aeb777f5e1c918a5",
1255 "accepted_proof_evidence": false,
1256 "source_snapshot_available": true
1257 },
1258 {
1259 "path": "development/scratch-guarded-majorant-batch.log",
1260 "bytes": 635,
1261 "sha256": "0629ea69c4b5553a6e3855f13f1c7da1b04272a63bb94ac51462fcb5e22b2acf",
1262 "accepted_proof_evidence": false,
1263 "source_snapshot_available": true
1264 }
1265 ],
1266 "development_diagnostic_boundary": "Development and preflight source/log pairs are diagnostics, not accepted proof evidence.",
1267 "rejected_executions": [],
1268 "toolchain": {
1269 "lean_sha256": "37dfe799f69b990251f3b6bcff8a1c10c1afe2adcdecc5c580cc6726ffb63433",
1270 "leanchecker_sha256": "b7c503a7a984f32f04c1badb79e53e350ddb72aed530da12699e4b06357ce149",
1271 "version": "Lean (version 4.34.0-rc2, x86_64-w64-windows-gnu, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d, Release)"
1272 },
1273 "execution_platform": "Windows-11-10.0.26200-SP0",
1274 "replay_tool": "tools/verify_coupled_guarded_majorant.py",
1275 "contract": "Pinned formal inputs and end-of-run stability; exact logs/objects/staging; separate source assessment and rejected diagnostics. Python files are not trusted proof leaves. No verifier installation or network access.",
1276 "status": "passed",
1277 "passed_steps": 66
1278 }
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: 68a25112c91d33a01f5da3f64cc567fdde4636826ba83678ef152d83887331d4