Special Functions

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 {
2   "schema": 1,
3   "block": "SF-LEAN-B17",
4   "status": "passed",
5   "started_utc": "2026-11-03T16:08:10Z",
6   "platform": "Windows-11-10.0.26200-SP0",
7   "python": "3.12.14 (main, Aug 25 2026, 14:01:42) [MSC v.1944 64 bit (AMD64)]",
8   "scope": "Appendix J exact rational bounded first-small ladder and guarded reverse-fold specification, explicit step/size errors, binary-width guard and abstract input-validation order; successful results certify actual complex bounds and real endpoints. Actual Python interpreter/Fraction/stdlib/type-classification/dictionary refinement, other J claims, I and A-E remain open.",
9   "kernel_scope": "Same-kernel replay of CoupledFormal, CoupledAnalytic, CoupledEntire, CoupledUniqueness, CoupledGermInverse, CoupledRescaling, CoupledCharacteristic, CoupledPositiveReal, CoupledLowerGrowth, CoupledUpperGrowth, CoupledGrowthTypes, CoupledTypeProportions, CoupledScalarReduction, CoupledOperator, CoupledEvaluation, CoupledNormalization and CoupledGuardedMajorant against cached imports; imported Mathlib is not freshly replayed.",
10   "steps": [
11     {
12       "name": "version",
13       "argv": [
14         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
15         "--version"
16       ],
17       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
18       "exit_code": 0,
19       "expected_exit_code": 0,
20       "required_diagnostic": "4.34.0-rc2",
21       "timed_out": false,
22       "seconds": 0.188,
23       "passed": true,
24       "log": "version.log",
25       "log_sha256": "87b9d84c24871d31d733f3c474b1372aeba74b55e40dcd54247ecf506523e850"
26     },
27     {
28       "name": "pin-mathlib",
29       "argv": [
30         "C:/Users/victor/.cache/codex-runtimes/codex-primary-runtime/dependencies/native/git/cmd/git.exe",
31         "rev-parse",
32         "HEAD"
33       ],
34       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\mathlib",
35       "exit_code": 0,
36       "expected_exit_code": 0,
37       "required_diagnostic": null,
38       "timed_out": false,
39       "seconds": 0.078,
40       "passed": true,
41       "log": "pin-mathlib.log",
42       "log_sha256": "62989ebe8b53589b05c10a31d55d06742e3e0c2ba54bbc69d678aa07dd30f172"
43     },
44     {
45       "name": "pin-plausible",
46       "argv": [
47         "C:/Users/victor/.cache/codex-runtimes/codex-primary-runtime/dependencies/native/git/cmd/git.exe",
48         "rev-parse",
49         "HEAD"
50       ],
51       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\mathlib\\.lake\\packages\\plausible",
52       "exit_code": 0,
53       "expected_exit_code": 0,
54       "required_diagnostic": null,
55       "timed_out": false,
56       "seconds": 0.078,
57       "passed": true,
58       "log": "pin-plausible.log",
59       "log_sha256": "5a24a15a2a5fa89534035ca17f5dc4d13f0677ab9637067469bb1a4910727293"
60     },
61     {
62       "name": "pin-LeanSearchClient",
63       "argv": [
64         "C:/Users/victor/.cache/codex-runtimes/codex-primary-runtime/dependencies/native/git/cmd/git.exe",
65         "rev-parse",
66         "HEAD"
67       ],
68       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\mathlib\\.lake\\packages\\LeanSearchClient",
69       "exit_code": 0,
70       "expected_exit_code": 0,
71       "required_diagnostic": null,
72       "timed_out": false,
73       "seconds": 0.094,
74       "passed": true,
75       "log": "pin-LeanSearchClient.log",
76       "log_sha256": "910b2313febb5044703357be69b8692792ff7b80631cf30506e64656d2f94024"
77     },
78     {
79       "name": "pin-importGraph",
80       "argv": [
81         "C:/Users/victor/.cache/codex-runtimes/codex-primary-runtime/dependencies/native/git/cmd/git.exe",
82         "rev-parse",
83         "HEAD"
84       ],
85       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\mathlib\\.lake\\packages\\importGraph",
86       "exit_code": 0,
87       "expected_exit_code": 0,
88       "required_diagnostic": null,
89       "timed_out": false,
90       "seconds": 0.094,
91       "passed": true,
92       "log": "pin-importGraph.log",
93       "log_sha256": "26db343c868a270c2f0bbaa414122483e8a33b2ccccd6e4f75fd8d3ae0132bf7"
94     },
95     {
96       "name": "pin-proofwidgets",
97       "argv": [
98         "C:/Users/victor/.cache/codex-runtimes/codex-primary-runtime/dependencies/native/git/cmd/git.exe",
99         "rev-parse",
100         "HEAD"
101       ],
102       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\mathlib\\.lake\\packages\\proofwidgets",
103       "exit_code": 0,
104       "expected_exit_code": 0,
105       "required_diagnostic": null,
106       "timed_out": false,
107       "seconds": 0.078,
108       "passed": true,
109       "log": "pin-proofwidgets.log",
110       "log_sha256": "c5137af62109636b0782f96afb8061cd85449a3d0f5944e9480669cd92d656cd"
111     },
112     {
113       "name": "pin-aesop",
114       "argv": [
115         "C:/Users/victor/.cache/codex-runtimes/codex-primary-runtime/dependencies/native/git/cmd/git.exe",
116         "rev-parse",
117         "HEAD"
118       ],
119       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\mathlib\\.lake\\packages\\aesop",
120       "exit_code": 0,
121       "expected_exit_code": 0,
122       "required_diagnostic": null,
123       "timed_out": false,
124       "seconds": 0.078,
125       "passed": true,
126       "log": "pin-aesop.log",
127       "log_sha256": "d44104024af2d060f35ec40580c3f3bde96dce8a2439187e6ec69dc516635226"
128     },
129     {
130       "name": "pin-Qq",
131       "argv": [
132         "C:/Users/victor/.cache/codex-runtimes/codex-primary-runtime/dependencies/native/git/cmd/git.exe",
133         "rev-parse",
134         "HEAD"
135       ],
136       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\mathlib\\.lake\\packages\\Qq",
137       "exit_code": 0,
138       "expected_exit_code": 0,
139       "required_diagnostic": null,
140       "timed_out": false,
141       "seconds": 0.094,
142       "passed": true,
143       "log": "pin-Qq.log",
144       "log_sha256": "2861275b98971639094343db957db7cc9a8fc2d1b0195efb01a8b22ee9f8251f"
145     },
146     {
147       "name": "pin-batteries",
148       "argv": [
149         "C:/Users/victor/.cache/codex-runtimes/codex-primary-runtime/dependencies/native/git/cmd/git.exe",
150         "rev-parse",
151         "HEAD"
152       ],
153       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\mathlib\\.lake\\packages\\batteries",
154       "exit_code": 0,
155       "expected_exit_code": 0,
156       "required_diagnostic": null,
157       "timed_out": false,
158       "seconds": 0.078,
159       "passed": true,
160       "log": "pin-batteries.log",
161       "log_sha256": "e0a3a54a768a0ca7c42bd5ea43945f0764b4576bfee8ee81f27e5ea533c2366d"
162     },
163     {
164       "name": "pin-Cli",
165       "argv": [
166         "C:/Users/victor/.cache/codex-runtimes/codex-primary-runtime/dependencies/native/git/cmd/git.exe",
167         "rev-parse",
168         "HEAD"
169       ],
170       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\mathlib\\.lake\\packages\\Cli",
171       "exit_code": 0,
172       "expected_exit_code": 0,
173       "required_diagnostic": null,
174       "timed_out": false,
175       "seconds": 0.063,
176       "passed": true,
177       "log": "pin-Cli.log",
178       "log_sha256": "bc44402ba0248c4c20de0520fbe58f81cc93b86368083f4411a92656bc61fc98"
179     },
180     {
181       "name": "compile-CoupledFormal",
182       "argv": [
183         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
184         "-j1",
185         "-DwarningAsError=true",
186         "-o",
187         "CoupledFormal.olean",
188         "CoupledFormal.lean"
189       ],
190       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
191       "exit_code": 0,
192       "expected_exit_code": 0,
193       "required_diagnostic": null,
194       "timed_out": false,
195       "seconds": 41.281,
196       "passed": true,
197       "log": "compile-CoupledFormal.log",
198       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
199     },
200     {
201       "name": "audit-CoupledFormal",
202       "argv": [
203         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
204         "-j1",
205         "-DwarningAsError=true",
206         "CoupledFormalAudit.lean"
207       ],
208       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
209       "exit_code": 0,
210       "expected_exit_code": 0,
211       "required_diagnostic": null,
212       "timed_out": false,
213       "seconds": 19.047,
214       "passed": true,
215       "log": "audit-CoupledFormal.log",
216       "log_sha256": "1f4565862ab4148f2d41846713d90e78ec5d7a70a12459bd76cec0541a25258e"
217     },
218     {
219       "name": "compile-CoupledAnalytic",
220       "argv": [
221         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
222         "-j1",
223         "-DwarningAsError=true",
224         "-o",
225         "CoupledAnalytic.olean",
226         "CoupledAnalytic.lean"
227       ],
228       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
229       "exit_code": 0,
230       "expected_exit_code": 0,
231       "required_diagnostic": null,
232       "timed_out": false,
233       "seconds": 43.172,
234       "passed": true,
235       "log": "compile-CoupledAnalytic.log",
236       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
237     },
238     {
239       "name": "audit-CoupledAnalytic",
240       "argv": [
241         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
242         "-j1",
243         "-DwarningAsError=true",
244         "CoupledAnalyticAudit.lean"
245       ],
246       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
247       "exit_code": 0,
248       "expected_exit_code": 0,
249       "required_diagnostic": null,
250       "timed_out": false,
251       "seconds": 21.219,
252       "passed": true,
253       "log": "audit-CoupledAnalytic.log",
254       "log_sha256": "01fbbe555c55df58c021c49fcb259e7cd94613753dcf81407383d541a5a8bd7e"
255     },
256     {
257       "name": "compile-CoupledEntire",
258       "argv": [
259         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
260         "-j1",
261         "-DwarningAsError=true",
262         "-o",
263         "CoupledEntire.olean",
264         "CoupledEntire.lean"
265       ],
266       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
267       "exit_code": 0,
268       "expected_exit_code": 0,
269       "required_diagnostic": null,
270       "timed_out": false,
271       "seconds": 24.281,
272       "passed": true,
273       "log": "compile-CoupledEntire.log",
274       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
275     },
276     {
277       "name": "audit-CoupledEntire",
278       "argv": [
279         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
280         "-j1",
281         "-DwarningAsError=true",
282         "CoupledEntireAudit.lean"
283       ],
284       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
285       "exit_code": 0,
286       "expected_exit_code": 0,
287       "required_diagnostic": null,
288       "timed_out": false,
289       "seconds": 21.953,
290       "passed": true,
291       "log": "audit-CoupledEntire.log",
292       "log_sha256": "62a85ece04c9e5ce9b2bc8e8a16dc8f6e100df943eed0456cb6be4f1a2f698c3"
293     },
294     {
295       "name": "compile-CoupledUniqueness",
296       "argv": [
297         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
298         "-j1",
299         "-DwarningAsError=true",
300         "-o",
301         "CoupledUniqueness.olean",
302         "CoupledUniqueness.lean"
303       ],
304       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
305       "exit_code": 0,
306       "expected_exit_code": 0,
307       "required_diagnostic": null,
308       "timed_out": false,
309       "seconds": 22.437,
310       "passed": true,
311       "log": "compile-CoupledUniqueness.log",
312       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
313     },
314     {
315       "name": "audit-CoupledUniqueness",
316       "argv": [
317         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
318         "-j1",
319         "-DwarningAsError=true",
320         "CoupledUniquenessAudit.lean"
321       ],
322       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
323       "exit_code": 0,
324       "expected_exit_code": 0,
325       "required_diagnostic": null,
326       "timed_out": false,
327       "seconds": 22.0,
328       "passed": true,
329       "log": "audit-CoupledUniqueness.log",
330       "log_sha256": "797bc578bb2b6d8dc1832700a24571df3ab0490de85746454591b722c83129d2"
331     },
332     {
333       "name": "compile-CoupledGermInverse",
334       "argv": [
335         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
336         "-j1",
337         "-DwarningAsError=true",
338         "-o",
339         "CoupledGermInverse.olean",
340         "CoupledGermInverse.lean"
341       ],
342       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
343       "exit_code": 0,
344       "expected_exit_code": 0,
345       "required_diagnostic": null,
346       "timed_out": false,
347       "seconds": 22.968,
348       "passed": true,
349       "log": "compile-CoupledGermInverse.log",
350       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
351     },
352     {
353       "name": "audit-CoupledGermInverse",
354       "argv": [
355         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
356         "-j1",
357         "-DwarningAsError=true",
358         "CoupledGermInverseAudit.lean"
359       ],
360       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
361       "exit_code": 0,
362       "expected_exit_code": 0,
363       "required_diagnostic": null,
364       "timed_out": false,
365       "seconds": 20.969,
366       "passed": true,
367       "log": "audit-CoupledGermInverse.log",
368       "log_sha256": "29ca11b50404f4ec732608578c31e1615de73ef235fd6a047530e19ebcd240d2"
369     },
370     {
371       "name": "compile-CoupledRescaling",
372       "argv": [
373         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
374         "-j1",
375         "-DwarningAsError=true",
376         "-o",
377         "CoupledRescaling.olean",
378         "CoupledRescaling.lean"
379       ],
380       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
381       "exit_code": 0,
382       "expected_exit_code": 0,
383       "required_diagnostic": null,
384       "timed_out": false,
385       "seconds": 24.656,
386       "passed": true,
387       "log": "compile-CoupledRescaling.log",
388       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
389     },
390     {
391       "name": "audit-CoupledRescaling",
392       "argv": [
393         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
394         "-j1",
395         "-DwarningAsError=true",
396         "CoupledRescalingAudit.lean"
397       ],
398       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
399       "exit_code": 0,
400       "expected_exit_code": 0,
401       "required_diagnostic": null,
402       "timed_out": false,
403       "seconds": 21.047,
404       "passed": true,
405       "log": "audit-CoupledRescaling.log",
406       "log_sha256": "fa4122625f487f5fa18c8f780bc7e9185a49ca664abadfc528bdcdd7db7f58dd"
407     },
408     {
409       "name": "compile-CoupledCharacteristic",
410       "argv": [
411         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
412         "-j1",
413         "-DwarningAsError=true",
414         "-o",
415         "CoupledCharacteristic.olean",
416         "CoupledCharacteristic.lean"
417       ],
418       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
419       "exit_code": 0,
420       "expected_exit_code": 0,
421       "required_diagnostic": null,
422       "timed_out": false,
423       "seconds": 31.906,
424       "passed": true,
425       "log": "compile-CoupledCharacteristic.log",
426       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
427     },
428     {
429       "name": "audit-CoupledCharacteristic",
430       "argv": [
431         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
432         "-j1",
433         "-DwarningAsError=true",
434         "CoupledCharacteristicAudit.lean"
435       ],
436       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
437       "exit_code": 0,
438       "expected_exit_code": 0,
439       "required_diagnostic": null,
440       "timed_out": false,
441       "seconds": 22.203,
442       "passed": true,
443       "log": "audit-CoupledCharacteristic.log",
444       "log_sha256": "566806518bf6e6afd18131d4b00ed8299b52a6437e75feaeb7c2cd8de0861436"
445     },
446     {
447       "name": "compile-CoupledPositiveReal",
448       "argv": [
449         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
450         "-j1",
451         "-DwarningAsError=true",
452         "-o",
453         "CoupledPositiveReal.olean",
454         "CoupledPositiveReal.lean"
455       ],
456       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
457       "exit_code": 0,
458       "expected_exit_code": 0,
459       "required_diagnostic": null,
460       "timed_out": false,
461       "seconds": 24.078,
462       "passed": true,
463       "log": "compile-CoupledPositiveReal.log",
464       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
465     },
466     {
467       "name": "audit-CoupledPositiveReal",
468       "argv": [
469         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
470         "-j1",
471         "-DwarningAsError=true",
472         "CoupledPositiveRealAudit.lean"
473       ],
474       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
475       "exit_code": 0,
476       "expected_exit_code": 0,
477       "required_diagnostic": null,
478       "timed_out": false,
479       "seconds": 20.703,
480       "passed": true,
481       "log": "audit-CoupledPositiveReal.log",
482       "log_sha256": "b2c437fc2b3dd64acdb3ba290babb5e4accedc77b5e52e19639f92b7d0132b5e"
483     },
484     {
485       "name": "compile-CoupledLowerGrowth",
486       "argv": [
487         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
488         "-j1",
489         "-DwarningAsError=true",
490         "-o",
491         "CoupledLowerGrowth.olean",
492         "CoupledLowerGrowth.lean"
493       ],
494       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
495       "exit_code": 0,
496       "expected_exit_code": 0,
497       "required_diagnostic": null,
498       "timed_out": false,
499       "seconds": 24.547,
500       "passed": true,
501       "log": "compile-CoupledLowerGrowth.log",
502       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
503     },
504     {
505       "name": "audit-CoupledLowerGrowth",
506       "argv": [
507         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
508         "-j1",
509         "-DwarningAsError=true",
510         "CoupledLowerGrowthAudit.lean"
511       ],
512       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
513       "exit_code": 0,
514       "expected_exit_code": 0,
515       "required_diagnostic": null,
516       "timed_out": false,
517       "seconds": 21.578,
518       "passed": true,
519       "log": "audit-CoupledLowerGrowth.log",
520       "log_sha256": "089dee8832e638911fda4950309f04afb1f29799f8e650a7e65717c9f2863449"
521     },
522     {
523       "name": "compile-CoupledUpperGrowth",
524       "argv": [
525         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
526         "-j1",
527         "-DwarningAsError=true",
528         "-o",
529         "CoupledUpperGrowth.olean",
530         "CoupledUpperGrowth.lean"
531       ],
532       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
533       "exit_code": 0,
534       "expected_exit_code": 0,
535       "required_diagnostic": null,
536       "timed_out": false,
537       "seconds": 27.718,
538       "passed": true,
539       "log": "compile-CoupledUpperGrowth.log",
540       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
541     },
542     {
543       "name": "audit-CoupledUpperGrowth",
544       "argv": [
545         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
546         "-j1",
547         "-DwarningAsError=true",
548         "CoupledUpperGrowthAudit.lean"
549       ],
550       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
551       "exit_code": 0,
552       "expected_exit_code": 0,
553       "required_diagnostic": null,
554       "timed_out": false,
555       "seconds": 21.532,
556       "passed": true,
557       "log": "audit-CoupledUpperGrowth.log",
558       "log_sha256": "9e30f5b39cb8ca1ca3254bb3234cf9fd9dd83a70abe7f5a242a9d5902ea59fbf"
559     },
560     {
561       "name": "compile-CoupledGrowthTypes",
562       "argv": [
563         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
564         "-j1",
565         "-DwarningAsError=true",
566         "-o",
567         "CoupledGrowthTypes.olean",
568         "CoupledGrowthTypes.lean"
569       ],
570       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
571       "exit_code": 0,
572       "expected_exit_code": 0,
573       "required_diagnostic": null,
574       "timed_out": false,
575       "seconds": 22.828,
576       "passed": true,
577       "log": "compile-CoupledGrowthTypes.log",
578       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
579     },
580     {
581       "name": "audit-CoupledGrowthTypes",
582       "argv": [
583         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
584         "-j1",
585         "-DwarningAsError=true",
586         "CoupledGrowthTypesAudit.lean"
587       ],
588       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
589       "exit_code": 0,
590       "expected_exit_code": 0,
591       "required_diagnostic": null,
592       "timed_out": false,
593       "seconds": 21.375,
594       "passed": true,
595       "log": "audit-CoupledGrowthTypes.log",
596       "log_sha256": "4577c67387bb1c5220da0f26b4b66e963e4053b7671ca461a4a9d089e6d26131"
597     },
598     {
599       "name": "compile-CoupledTypeProportions",
600       "argv": [
601         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
602         "-j1",
603         "-DwarningAsError=true",
604         "-o",
605         "CoupledTypeProportions.olean",
606         "CoupledTypeProportions.lean"
607       ],
608       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
609       "exit_code": 0,
610       "expected_exit_code": 0,
611       "required_diagnostic": null,
612       "timed_out": false,
613       "seconds": 26.906,
614       "passed": true,
615       "log": "compile-CoupledTypeProportions.log",
616       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
617     },
618     {
619       "name": "audit-CoupledTypeProportions",
620       "argv": [
621         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
622         "-j1",
623         "-DwarningAsError=true",
624         "CoupledTypeProportionsAudit.lean"
625       ],
626       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
627       "exit_code": 0,
628       "expected_exit_code": 0,
629       "required_diagnostic": null,
630       "timed_out": false,
631       "seconds": 22.0,
632       "passed": true,
633       "log": "audit-CoupledTypeProportions.log",
634       "log_sha256": "c5640f259db7704f918f93b732637fd20a4155030008465d8e7c0d78ef6e20f4"
635     },
636     {
637       "name": "compile-CoupledScalarReduction",
638       "argv": [
639         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
640         "-j1",
641         "-DwarningAsError=true",
642         "-o",
643         "CoupledScalarReduction.olean",
644         "CoupledScalarReduction.lean"
645       ],
646       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
647       "exit_code": 0,
648       "expected_exit_code": 0,
649       "required_diagnostic": null,
650       "timed_out": false,
651       "seconds": 30.406,
652       "passed": true,
653       "log": "compile-CoupledScalarReduction.log",
654       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
655     },
656     {
657       "name": "audit-CoupledScalarReduction",
658       "argv": [
659         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
660         "-j1",
661         "-DwarningAsError=true",
662         "CoupledScalarReductionAudit.lean"
663       ],
664       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
665       "exit_code": 0,
666       "expected_exit_code": 0,
667       "required_diagnostic": null,
668       "timed_out": false,
669       "seconds": 31.906,
670       "passed": true,
671       "log": "audit-CoupledScalarReduction.log",
672       "log_sha256": "9cd1320677ca9f4fbccebb507bf1a6cadc897c66127543ed5a2c4a257181bdb8"
673     },
674     {
675       "name": "compile-CoupledOperator",
676       "argv": [
677         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
678         "-j1",
679         "-DwarningAsError=true",
680         "-o",
681         "CoupledOperator.olean",
682         "CoupledOperator.lean"
683       ],
684       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
685       "exit_code": 0,
686       "expected_exit_code": 0,
687       "required_diagnostic": null,
688       "timed_out": false,
689       "seconds": 30.718,
690       "passed": true,
691       "log": "compile-CoupledOperator.log",
692       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
693     },
694     {
695       "name": "audit-CoupledOperator",
696       "argv": [
697         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
698         "-j1",
699         "-DwarningAsError=true",
700         "CoupledOperatorAudit.lean"
701       ],
702       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
703       "exit_code": 0,
704       "expected_exit_code": 0,
705       "required_diagnostic": null,
706       "timed_out": false,
707       "seconds": 25.829,
708       "passed": true,
709       "log": "audit-CoupledOperator.log",
710       "log_sha256": "f7310d3c06690fb47124f01dd94cee0b3ddec019c8877aebd607b2b1dd8f746a"
711     },
712     {
713       "name": "compile-CoupledEvaluation",
714       "argv": [
715         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
716         "-j1",
717         "-DwarningAsError=true",
718         "-o",
719         "CoupledEvaluation.olean",
720         "CoupledEvaluation.lean"
721       ],
722       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
723       "exit_code": 0,
724       "expected_exit_code": 0,
725       "required_diagnostic": null,
726       "timed_out": false,
727       "seconds": 84.828,
728       "passed": true,
729       "log": "compile-CoupledEvaluation.log",
730       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
731     },
732     {
733       "name": "audit-CoupledEvaluation",
734       "argv": [
735         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
736         "-j1",
737         "-DwarningAsError=true",
738         "CoupledEvaluationAudit.lean"
739       ],
740       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
741       "exit_code": 0,
742       "expected_exit_code": 0,
743       "required_diagnostic": null,
744       "timed_out": false,
745       "seconds": 21.594,
746       "passed": true,
747       "log": "audit-CoupledEvaluation.log",
748       "log_sha256": "eb10f7700c095ca3a20a377aee1f63e6b8e234e728e17595ffab1945c2dbc25e"
749     },
750     {
751       "name": "compile-CoupledNormalization",
752       "argv": [
753         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
754         "-j1",
755         "-DwarningAsError=true",
756         "-o",
757         "CoupledNormalization.olean",
758         "CoupledNormalization.lean"
759       ],
760       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
761       "exit_code": 0,
762       "expected_exit_code": 0,
763       "required_diagnostic": null,
764       "timed_out": false,
765       "seconds": 24.36,
766       "passed": true,
767       "log": "compile-CoupledNormalization.log",
768       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
769     },
770     {
771       "name": "audit-CoupledNormalization",
772       "argv": [
773         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
774         "-j1",
775         "-DwarningAsError=true",
776         "CoupledNormalizationAudit.lean"
777       ],
778       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
779       "exit_code": 0,
780       "expected_exit_code": 0,
781       "required_diagnostic": null,
782       "timed_out": false,
783       "seconds": 22.312,
784       "passed": true,
785       "log": "audit-CoupledNormalization.log",
786       "log_sha256": "431f4010cdbd0e001f2dfcd254982f1f7a49e3ffd8ae79555cc8c68804f8336f"
787     },
788     {
789       "name": "compile-CoupledGuardedMajorant",
790       "argv": [
791         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
792         "-j1",
793         "-DwarningAsError=true",
794         "-o",
795         "CoupledGuardedMajorant.olean",
796         "CoupledGuardedMajorant.lean"
797       ],
798       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
799       "exit_code": 0,
800       "expected_exit_code": 0,
801       "required_diagnostic": null,
802       "timed_out": false,
803       "seconds": 23.594,
804       "passed": true,
805       "log": "compile-CoupledGuardedMajorant.log",
806       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
807     },
808     {
809       "name": "audit-CoupledGuardedMajorant",
810       "argv": [
811         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
812         "-j1",
813         "-DwarningAsError=true",
814         "CoupledGuardedMajorantAudit.lean"
815       ],
816       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
817       "exit_code": 0,
818       "expected_exit_code": 0,
819       "required_diagnostic": null,
820       "timed_out": false,
821       "seconds": 41.578,
822       "passed": true,
823       "log": "audit-CoupledGuardedMajorant.log",
824       "log_sha256": "50ee73dda82f56e81ba6a3a055f7d6541f49e2cdf45127e3fb8425f1c08ef568"
825     },
826     {
827       "name": "kernel-CoupledFormal",
828       "argv": [
829         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
830         "--verbose",
831         "CoupledFormal"
832       ],
833       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
834       "exit_code": 0,
835       "expected_exit_code": 0,
836       "required_diagnostic": "replaying CoupledFormal",
837       "timed_out": false,
838       "seconds": 27.453,
839       "passed": true,
840       "log": "kernel-CoupledFormal.log",
841       "log_sha256": "5677a5b892e16d2badc84a00a24d266c83e8722957f0cbe5026cdb1b3fae9d87"
842     },
843     {
844       "name": "kernel-CoupledAnalytic",
845       "argv": [
846         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
847         "--verbose",
848         "CoupledAnalytic"
849       ],
850       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
851       "exit_code": 0,
852       "expected_exit_code": 0,
853       "required_diagnostic": "replaying CoupledAnalytic",
854       "timed_out": false,
855       "seconds": 23.86,
856       "passed": true,
857       "log": "kernel-CoupledAnalytic.log",
858       "log_sha256": "b34cae702aebfd97f5b6f0072c7c3870a024f5674f894bb43e5095b3abbd3e11"
859     },
860     {
861       "name": "kernel-CoupledEntire",
862       "argv": [
863         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
864         "--verbose",
865         "CoupledEntire"
866       ],
867       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
868       "exit_code": 0,
869       "expected_exit_code": 0,
870       "required_diagnostic": "replaying CoupledEntire",
871       "timed_out": false,
872       "seconds": 22.125,
873       "passed": true,
874       "log": "kernel-CoupledEntire.log",
875       "log_sha256": "c446b7b5cc66373292a4817fb55a2d5fb7529242d2c14618948bda64f5bacacf"
876     },
877     {
878       "name": "kernel-CoupledUniqueness",
879       "argv": [
880         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
881         "--verbose",
882         "CoupledUniqueness"
883       ],
884       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
885       "exit_code": 0,
886       "expected_exit_code": 0,
887       "required_diagnostic": "replaying CoupledUniqueness",
888       "timed_out": false,
889       "seconds": 24.078,
890       "passed": true,
891       "log": "kernel-CoupledUniqueness.log",
892       "log_sha256": "30a98c266a4da85ac60052fc1407dbcc728a60bc360fc50505cbb9836e3d0f76"
893     },
894     {
895       "name": "kernel-CoupledGermInverse",
896       "argv": [
897         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
898         "--verbose",
899         "CoupledGermInverse"
900       ],
901       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
902       "exit_code": 0,
903       "expected_exit_code": 0,
904       "required_diagnostic": "replaying CoupledGermInverse",
905       "timed_out": false,
906       "seconds": 24.25,
907       "passed": true,
908       "log": "kernel-CoupledGermInverse.log",
909       "log_sha256": "41d81afce63beaa32a4e23b443babf8cc0b29822e5976309d25e8c0551b4641e"
910     },
911     {
912       "name": "kernel-CoupledRescaling",
913       "argv": [
914         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
915         "--verbose",
916         "CoupledRescaling"
917       ],
918       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
919       "exit_code": 0,
920       "expected_exit_code": 0,
921       "required_diagnostic": "replaying CoupledRescaling",
922       "timed_out": false,
923       "seconds": 24.422,
924       "passed": true,
925       "log": "kernel-CoupledRescaling.log",
926       "log_sha256": "2be26a71c3207180267b0f38d4a0b1419b0ca2f7f9c3e57b98a8fc822437018a"
927     },
928     {
929       "name": "kernel-CoupledCharacteristic",
930       "argv": [
931         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
932         "--verbose",
933         "CoupledCharacteristic"
934       ],
935       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
936       "exit_code": 0,
937       "expected_exit_code": 0,
938       "required_diagnostic": "replaying CoupledCharacteristic",
939       "timed_out": false,
940       "seconds": 24.531,
941       "passed": true,
942       "log": "kernel-CoupledCharacteristic.log",
943       "log_sha256": "7ab004782e0bd997d0c6c4da4bd88fa3c59f1a8f67b37c5ab68b8604a1c58720"
944     },
945     {
946       "name": "kernel-CoupledPositiveReal",
947       "argv": [
948         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
949         "--verbose",
950         "CoupledPositiveReal"
951       ],
952       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
953       "exit_code": 0,
954       "expected_exit_code": 0,
955       "required_diagnostic": "replaying CoupledPositiveReal",
956       "timed_out": false,
957       "seconds": 23.469,
958       "passed": true,
959       "log": "kernel-CoupledPositiveReal.log",
960       "log_sha256": "87614063b2d254266354c370ccfda3eada390bd88fc0726d99e533e502b744fc"
961     },
962     {
963       "name": "kernel-CoupledLowerGrowth",
964       "argv": [
965         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
966         "--verbose",
967         "CoupledLowerGrowth"
968       ],
969       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
970       "exit_code": 0,
971       "expected_exit_code": 0,
972       "required_diagnostic": "replaying CoupledLowerGrowth",
973       "timed_out": false,
974       "seconds": 23.453,
975       "passed": true,
976       "log": "kernel-CoupledLowerGrowth.log",
977       "log_sha256": "902005e34aafb99d0391d38f47733cb3e4e57d95bf17adcfaff4fab9f461b466"
978     },
979     {
980       "name": "kernel-CoupledUpperGrowth",
981       "argv": [
982         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
983         "--verbose",
984         "CoupledUpperGrowth"
985       ],
986       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
987       "exit_code": 0,
988       "expected_exit_code": 0,
989       "required_diagnostic": "replaying CoupledUpperGrowth",
990       "timed_out": false,
991       "seconds": 23.016,
992       "passed": true,
993       "log": "kernel-CoupledUpperGrowth.log",
994       "log_sha256": "d1db25a7f481c0fbec79d211502c26978ab96ef8f4b76cd14683899310f1d8e5"
995     },
996     {
997       "name": "kernel-CoupledGrowthTypes",
998       "argv": [
999         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
1000         "--verbose",
1001         "CoupledGrowthTypes"
1002       ],
1003       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1004       "exit_code": 0,
1005       "expected_exit_code": 0,
1006       "required_diagnostic": "replaying CoupledGrowthTypes",
1007       "timed_out": false,
1008       "seconds": 23.859,
1009       "passed": true,
1010       "log": "kernel-CoupledGrowthTypes.log",
1011       "log_sha256": "02d0569e20b329c54e5ec1f9fca3b5aa17a079da19621ac8437209d97aae10e0"
1012     },
1013     {
1014       "name": "kernel-CoupledTypeProportions",
1015       "argv": [
1016         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
1017         "--verbose",
1018         "CoupledTypeProportions"
1019       ],
1020       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1021       "exit_code": 0,
1022       "expected_exit_code": 0,
1023       "required_diagnostic": "replaying CoupledTypeProportions",
1024       "timed_out": false,
1025       "seconds": 23.328,
1026       "passed": true,
1027       "log": "kernel-CoupledTypeProportions.log",
1028       "log_sha256": "615a9b67566d9ab88f5cb1a45e798569c9f7e6b49f4e388f12cd38cafeb6e157"
1029     },
1030     {
1031       "name": "kernel-CoupledScalarReduction",
1032       "argv": [
1033         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
1034         "--verbose",
1035         "CoupledScalarReduction"
1036       ],
1037       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1038       "exit_code": 0,
1039       "expected_exit_code": 0,
1040       "required_diagnostic": "replaying CoupledScalarReduction",
1041       "timed_out": false,
1042       "seconds": 22.859,
1043       "passed": true,
1044       "log": "kernel-CoupledScalarReduction.log",
1045       "log_sha256": "07eb9281238890692b04d108486325738b74533d0f639dd082ce915a7cedac39"
1046     },
1047     {
1048       "name": "kernel-CoupledOperator",
1049       "argv": [
1050         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
1051         "--verbose",
1052         "CoupledOperator"
1053       ],
1054       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1055       "exit_code": 0,
1056       "expected_exit_code": 0,
1057       "required_diagnostic": "replaying CoupledOperator",
1058       "timed_out": false,
1059       "seconds": 22.781,
1060       "passed": true,
1061       "log": "kernel-CoupledOperator.log",
1062       "log_sha256": "edde0347950876fbd42cb758eda027a2024943e8582fa69276685869ae987271"
1063     },
1064     {
1065       "name": "kernel-CoupledEvaluation",
1066       "argv": [
1067         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
1068         "--verbose",
1069         "CoupledEvaluation"
1070       ],
1071       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1072       "exit_code": 0,
1073       "expected_exit_code": 0,
1074       "required_diagnostic": "replaying CoupledEvaluation",
1075       "timed_out": false,
1076       "seconds": 23.562,
1077       "passed": true,
1078       "log": "kernel-CoupledEvaluation.log",
1079       "log_sha256": "d8d1a695efa203aa7bb482e09575bc289672cd0e8d647d73e45c4cee9d63b6c5"
1080     },
1081     {
1082       "name": "kernel-CoupledNormalization",
1083       "argv": [
1084         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
1085         "--verbose",
1086         "CoupledNormalization"
1087       ],
1088       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1089       "exit_code": 0,
1090       "expected_exit_code": 0,
1091       "required_diagnostic": "replaying CoupledNormalization",
1092       "timed_out": false,
1093       "seconds": 23.25,
1094       "passed": true,
1095       "log": "kernel-CoupledNormalization.log",
1096       "log_sha256": "4917715134963e1596c82a035d4f3229888742709a324179d637300b56e346ee"
1097     },
1098     {
1099       "name": "kernel-CoupledGuardedMajorant",
1100       "argv": [
1101         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\leanchecker.exe",
1102         "--verbose",
1103         "CoupledGuardedMajorant"
1104       ],
1105       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1106       "exit_code": 0,
1107       "expected_exit_code": 0,
1108       "required_diagnostic": "replaying CoupledGuardedMajorant",
1109       "timed_out": false,
1110       "seconds": 23.438,
1111       "passed": true,
1112       "log": "kernel-CoupledGuardedMajorant.log",
1113       "log_sha256": "12f0e0b63cfb0cdd829073472d92ce55691102b9846632725ed583945c4fcfbc"
1114     },
1115     {
1116       "name": "control-MissingSuccess",
1117       "argv": [
1118         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
1119         "-j1",
1120         "-DwarningAsError=true",
1121         "control-MissingSuccess.lean"
1122       ],
1123       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1124       "exit_code": 1,
1125       "expected_exit_code": 1,
1126       "required_diagnostic": "Application type mismatch",
1127       "timed_out": false,
1128       "seconds": 26.266,
1129       "passed": true,
1130       "log": "control-MissingSuccess.log",
1131       "log_sha256": "5acb22a2de35e297a4f46645228e772148b58952bd5cdc51f0ef9ce0ad6b2d3e"
1132     },
1133     {
1134       "name": "control-WrongFoldOrder",
1135       "argv": [
1136         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
1137         "-j1",
1138         "-DwarningAsError=true",
1139         "control-WrongFoldOrder.lean"
1140       ],
1141       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1142       "exit_code": 1,
1143       "expected_exit_code": 1,
1144       "required_diagnostic": "unsolved goals",
1145       "timed_out": false,
1146       "seconds": 22.047,
1147       "passed": true,
1148       "log": "control-WrongFoldOrder.log",
1149       "log_sha256": "7a0fbc2dc6ec976b7626041ce44dd578b8fac974504f7643073b79759d7f8b78"
1150     },
1151     {
1152       "name": "control-SeedSizeCheck",
1153       "argv": [
1154         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
1155         "-j1",
1156         "-DwarningAsError=true",
1157         "control-SeedSizeCheck.lean"
1158       ],
1159       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1160       "exit_code": 1,
1161       "expected_exit_code": 1,
1162       "required_diagnostic": "unsolved goals",
1163       "timed_out": false,
1164       "seconds": 21.578,
1165       "passed": true,
1166       "log": "control-SeedSizeCheck.log",
1167       "log_sha256": "71a8a9941a116292d8bc60489d534d35848e5d8015eaf5fc072197e9e2f1a506"
1168     },
1169     {
1170       "name": "control-Placeholder",
1171       "argv": [
1172         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
1173         "-j1",
1174         "-DwarningAsError=true",
1175         "control-Placeholder.lean"
1176       ],
1177       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1178       "exit_code": 1,
1179       "expected_exit_code": 1,
1180       "required_diagnostic": "declaration uses `sorry`",
1181       "timed_out": false,
1182       "seconds": 21.047,
1183       "passed": true,
1184       "log": "control-Placeholder.log",
1185       "log_sha256": "0682d764d4f78ca960e5b641d4317d1a6a252cedccba3fc52d1d4285bcbcd22c"
1186     },
1187     {
1188       "name": "control-GuardedInterfaces",
1189       "argv": [
1190         "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\.tools\\lean-4.34.0-rc2-windows\\bin\\lean.exe",
1191         "-j1",
1192         "-DwarningAsError=true",
1193         "control-GuardedInterfaces.lean"
1194       ],
1195       "cwd": "C:\\Users\\victor\\Documents\\Codex\\2026-11-02\\machine-societies-has-the-clearest-unfinished\\guarded-majorant-replay-001\\build",
1196       "exit_code": 0,
1197       "expected_exit_code": 0,
1198       "required_diagnostic": null,
1199       "timed_out": false,
1200       "seconds": 22.109,
1201       "passed": true,
1202       "log": "control-GuardedInterfaces.log",
1203       "log_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
1204     }
1205   ],
1206   "inputs": {
1207     "tools/verify_coupled_guarded_majorant.py": "ac2926ca7ca6b95669a54b41d4bdbc9767b1e3e5c21be4d06dc6743cc2b5a035",
1208     "lean/dependency_pins.json": "2ba2018e7b8400a7d83c028a312111c629c07f4c882b03f1d303340c78d6f218",
1209     "formalization/Block01/declarations.json": "cc847de0ea26dd590dd50a7c88b08e9f0e0fb3aab5b8dcd13ca04c28bcf56257",
1210     "formalization/Block02/declarations.json": "2d59af08ac8323f10560ef0c875a56a4d310b299de16c703884669a6763d67d4",
1211     "formalization/Block03/declarations.json": "27d5f24827734959782f77efd7100a12d2b7c074447a0ba1ca79f6ad7a4e058c",
1212     "formalization/Block04/declarations.json": "cef0cfd5ad849e87aa70b145f05181ca12e7592f7c27c9fe0ab8d0757fd31a9d",
1213     "formalization/Block05/declarations.json": "64feee3372696155d70ae5e680af746481f2ce5bb77ddca2e9556f09229745ae",
1214     "formalization/Block06/declarations.json": "0500d0b7c688f76699aa981309d9d41985a67e38efe0b18949c9e8c7e5663259",
1215     "formalization/Block07/declarations.json": "4673180bbe3bab15c16af752c2606bf8aa3c68c1caae544f5e634f9bec07d500",
1216     "formalization/Block08/declarations.json": "ceac534b75b3eeb715c628abe510e41a80463dc69f0ec7b83f76789fafdb8c98",
1217     "formalization/Block09/declarations.json": "e35d0affbd0da4b374718d8ead0334fb997e52e61610d8123df52238b83074b3",
1218     "formalization/Block10/declarations.json": "4aeb09db6f3ced4ff84c4a936e5380e93df1ae88b2357dd5e8cb4636d2ecf7ab",
1219     "formalization/Block11/declarations.json": "d0c40586326778cdd2f9a8f1e3f5bb20f962f8c5b1fc333274cabcf0a61328bb",
1220     "formalization/Block12/declarations.json": "4446f6555cfa77b07e5c72e34c7dafdda6a418d2766d9c1b0fb9e415a50120f9",
1221     "formalization/Block13/declarations.json": "271520a2e68616cddd7733b86459d701d403de468335f0a22838c33180e6e5b0",
1222     "formalization/Block14/declarations.json": "f8fd1801faacdf73c8f3ce709125e23c20eb3dad26a792cda87fbff9df50dd2f",
1223     "formalization/Block15/declarations.json": "32e3483d9270830520a5e2d37cc2343b6d8facc915e87cace73aa46fa45e61f2",
1224     "formalization/Block16/declarations.json": "cdcbb211a9be8b66e8e4ea93716422f71d00249e62c0ac78116eacf5285295a5",
1225     "formalization/Block17/declarations.json": "211335ba76a5f06b419389dbceceac6394a8f76fd629a577c5b7481f7d40b11d",
1226     "lean/guarded_majorant_controls/manifest.json": "58bec4ec119bb3d53af2b967c28288fba90d387161f436ecbcfde4d94a55ef4b",
1227     "lean/CoupledFormal.lean": "18ca2a8c463d83c9402bab3f2c312fd84e1a63fdb21873d669f6d2d0cc4d6c87",
1228     "lean/CoupledFormalAudit.lean": "f6d92e0dec5458142cbbf0b2b717b5233f2330b59ef58e89c8be10361f24f437",
1229     "lean/CoupledAnalytic.lean": "4317cc45436eb5434b0ddd1418bd4096b3865cf4e9a92e32f2e5b23eeb1a247f",
1230     "lean/CoupledAnalyticAudit.lean": "24327e3a8365da563fb7c654ecf379d9ec14ac5d137c3a5a27a00b883bf12051",
1231     "lean/CoupledEntire.lean": "48359369ee25322fb301a060d239c2f688f46ac59098394a22fd7a3f6272cb64",
1232     "lean/CoupledEntireAudit.lean": "26d045313a9af0ba5dba699fb3b4a87403824f5cbfb1fc5778009d16fc3233de",
1233     "lean/CoupledUniqueness.lean": "40ce00b496300eff1cefd1204918e43661b9487273d90e13c6b8352c305f5e21",
1234     "lean/CoupledUniquenessAudit.lean": "228af41b5b27418b3d4202df64b144c84affb9a4e05cdfbeb7a8d8e438823180",
1235     "lean/CoupledGermInverse.lean": "92a0a2fa8fa33a9f6d602e73d8714c645d57b8bcee4d89205f87ad9dfb56bb2b",
1236     "lean/CoupledGermInverseAudit.lean": "fd14f78ea526cb4eab5e57f4f7a64c95161c14299b145be811b2ccb20e1ca6db",
1237     "lean/CoupledRescaling.lean": "83a014bccd72204a121a11b6e558100da0b2accef37be43fcad809be037eea5e",
1238     "lean/CoupledRescalingAudit.lean": "97104bd96fe19af8bb0d2e700940258cb084ae044ca0f47ab86d9264536f8b76",
1239     "lean/CoupledCharacteristic.lean": "bba339b502ee9582dda88e226d3544e367cfce8a6153e14345d6c8e86a62eb84",
1240     "lean/CoupledCharacteristicAudit.lean": "c6871063f94b1e70dc1656737863d91eef847dc6f5f39e0a048ccdadaf496cf0",
1241     "lean/CoupledPositiveReal.lean": "a1e1b4f42efbffd0dcb0acf1a8b9ab23fe9fd775397219ad2c7961789414a8d7",
1242     "lean/CoupledPositiveRealAudit.lean": "49a920db319b72249aa31058c6f492238dbe239de18644defccc4dad6f25bdbe",
1243     "lean/CoupledLowerGrowth.lean": "17b055c76799ed380374f2834d47cdf461d52ee95fab0babd9151f602e1c540f",
1244     "lean/CoupledLowerGrowthAudit.lean": "76b48f9a4aac1d6e996c1b7deabf17cf77821a72f461046f59e9c4e5e84cd2e7",
1245     "lean/CoupledUpperGrowth.lean": "0b899b5d8639a9fe6a957af7ceffc7a3e173557c0bc7f347c92dc92fec344f1d",
1246     "lean/CoupledUpperGrowthAudit.lean": "6ecf165aa171a96f4bd8d7ed1f8bb1e9bd4d81dca3d4711e4946f7005be398be",
1247     "lean/CoupledGrowthTypes.lean": "1363c216cfd64706fce14bc8fece963f3313ecc3b4e393a7486c89b09b313c7a",
1248     "lean/CoupledGrowthTypesAudit.lean": "92e54ca0a72c76e6ede67b590a1152f7de3eed5c21f226a1fbe56c942d93e1fe",
1249     "lean/CoupledTypeProportions.lean": "c6b3d8dfb786730a7b0ed456992dd87af160016841bfd7195596017b42a16194",
1250     "lean/CoupledTypeProportionsAudit.lean": "4532e08e1efa4619f56e134e53a29e6a3b94a6bf7b2d284531f912f0640ebe3f",
1251     "lean/CoupledScalarReduction.lean": "4ca29da51d06096d34b8e85d62018d2c8c03329f1378f7e57d69926f62119c00",
1252     "lean/CoupledScalarReductionAudit.lean": "53ed37138bafd35638304c2cb5c644930b5f4b7c403ee5705e3e9f26b6cfc536",
1253     "lean/CoupledOperator.lean": "743c863d39fccb19ea88e09e49671ffddaea40030ad867a8902c4169e9e1a047",
1254     "lean/CoupledOperatorAudit.lean": "6b4cd5578f5ebaceb20d704ac7acc29b90fc5360f53bda5a46ebd1c5d18573f0",
1255     "lean/CoupledEvaluation.lean": "59bf338f4b10672501ebf1a6dd0e2e02c74b86750adef2cc679fabc735dc1cd9",
1256     "lean/CoupledEvaluationAudit.lean": "5eac0617b6c36c875a5da3f43aa8ca9e484aea17d84ea5f15720358ee2f3c972",
1257     "lean/CoupledNormalization.lean": "907fd0fa37a59dff472088a2afa6cc4f9bb22663ce9d153378560cfdeaa549f8",
1258     "lean/CoupledNormalizationAudit.lean": "ae5eb111ac8335a186618a20171734e385322ccef7aa0b71985cc83ed523a3af",
1259     "lean/CoupledGuardedMajorant.lean": "349f0d3ae54d93aa5035cee180e26c8d8ba30169c478511136af20cc6d421b0c",
1260     "lean/CoupledGuardedMajorantAudit.lean": "66312a82efcb43fe59998181bd3c872c33956b221fca5a47c61bfa1db980ddf8",
1261     "lean/guarded_majorant_controls/MissingSuccess.lean": "7fc06fd8c21959132b8f9b57f4b6eeeb8da94edf875873926db88230e4be721d",
1262     "lean/guarded_majorant_controls/WrongFoldOrder.lean": "7b98be33d886e664e29eff84d149a80f6ec9413c94be4ac1cbeb0abb7387fe3e",
1263     "lean/guarded_majorant_controls/SeedSizeCheck.lean": "ce8b8866a49191c2960b99adfb4ed6829e0612e7b592d3c210fbbf0d378dd426",
1264     "lean/guarded_majorant_controls/Placeholder.lean": "2177f3660448e3b75d6cfb0e832c6054df4d104ddd6e4b9defc516a2624b67c3",
1265     "lean/guarded_majorant_controls/GuardedInterfaces.lean": "db154df0784b0e0ab4c783bc4715b95e76506d26aa0334eb553f9e65e4a4879c"
1266   },
1267   "toolchain": {
1268     "lean_sha256": "37dfe799f69b990251f3b6bcff8a1c10c1afe2adcdecc5c580cc6726ffb63433",
1269     "leanchecker_sha256": "b7c503a7a984f32f04c1badb79e53e350ddb72aed530da12699e4b06357ce149",
1270     "version": "Lean (version 4.34.0-rc2, x86_64-w64-windows-gnu, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d, Release)"
1271   },
1272   "CoupledFormal_audit": {
1273     "names": [
1274       "Komorebi.SpecialFunctions.Coupled.positive_pair_recovery",
1275       "Komorebi.SpecialFunctions.Coupled.Scales.defect_factor",
1276       "Komorebi.SpecialFunctions.Coupled.Scales.defect_eq_zero_iff",
1277       "Komorebi.SpecialFunctions.Coupled.Scales.positive_square_injective",
1278       "Komorebi.SpecialFunctions.Coupled.Scales.seven_jet_injective",
1279       "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_solution",
1280       "Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_congr",
1281       "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_solution_unique",
1282       "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_solution_exists_unique",
1283       "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_zero",
1284       "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_one",
1285       "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_two",
1286       "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_three",
1287       "Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_positive",
1288       "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_positive",
1289       "Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_le_geometric",
1290       "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_le_geometric",
1291       "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_norm_bound",
1292       "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_norm_summable",
1293       "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_summable",
1294       "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_absolutely_convergent",
1295       "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_tail_bound",
1296       "Komorebi.SpecialFunctions.Coupled.Scales.sameJet_of_coefficients_eq",
1297       "Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_jet_through_degree_seven",
1298       "Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_formal_pair_eq",
1299       "Komorebi.SpecialFunctions.Coupled.Scales.workedScales_positive",
1300       "Komorebi.SpecialFunctions.Coupled.Scales.workedScales_defect",
1301       "Komorebi.SpecialFunctions.Coupled.Scales.workedScales_recoverable",
1302       "Komorebi.SpecialFunctions.Coupled.Scales.boundary_collision"
1303     ],
1304     "count": 29,
1305     "axioms": [
1306       "Classical.choice",
1307       "Quot.sound",
1308       "propext"
1309     ]
1310   },
1311   "objects": {
1312     "CoupledFormal.olean": "78763668d71b9efdda4e622a176f558255957e7aa73cfa903dddc514e5858e0c",
1313     "CoupledAnalytic.olean": "bad582a3f10184ad4fc46256ce79899bdc3129421bf4a16c5c76656b86ab6648",
1314     "CoupledEntire.olean": "ae0882279dc3832088306a5b75d4181d6e85499ebd119e36c1a6609b079588c0",
1315     "CoupledUniqueness.olean": "9cfb141a050059378fced0b66cd62d4c082eda01f00c6ee7e0b72173a8ac0011",
1316     "CoupledGermInverse.olean": "0922c81308d397f5e3ca3553112ffe290c0eac75fc2be773cd18328b51b04f38",
1317     "CoupledRescaling.olean": "c738b2db5b6eb42a6f7b350f24bd8a757043341d3b1ef03e67842d0f601eeb93",
1318     "CoupledCharacteristic.olean": "62520836deb6d046be8149ffa976ae5a1ad615337ccbed55a00394ffc0576301",
1319     "CoupledPositiveReal.olean": "00bcb8cf4e423cf198b20d97d7fb0cc3129af56ce5ec4cdb72590126fa157f77",
1320     "CoupledLowerGrowth.olean": "7f88b1783d93d146d75d5b6c497091eefb37bdc4906d6be20c0161be859387b8",
1321     "CoupledUpperGrowth.olean": "94f1d80f535fc508df24328f610dfa1580af397392ae6abb4e44f5f63d1907a4",
1322     "CoupledGrowthTypes.olean": "5daf0eacf4ff861721b98a3e245fe638ef52b1e4fd29d536b1d0ec0ba768f297",
1323     "CoupledTypeProportions.olean": "340a5ce8f40d2a25c8092d87eb27b89195da7070632e60689b17bdab112c6e2a",
1324     "CoupledScalarReduction.olean": "fb517e450df6df0bcbf2bf70ea9ca1377a446c1077c05a9845a4b97d2ba1c067",
1325     "CoupledOperator.olean": "7308d5a4f987242791aa8a7df933348da5ad0c609252317d5248a2c26f138952",
1326     "CoupledEvaluation.olean": "8ee322c2c650ed21cea63a88ea3b74781f4fefad7bb479373b8a6af06af1694b",
1327     "CoupledNormalization.olean": "fa44300fa480a07124448db052af35917b91a6cf668bb43300f00016e73dfb44",
1328     "CoupledGuardedMajorant.olean": "54a31c67af2766b1e4b51ca48fd3536b87041492c0c8b4b40352cc3d6b1ded0a"
1329   },
1330   "CoupledAnalytic_audit": {
1331     "names": [
1332       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_zero",
1333       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_neg",
1334       "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_uniform_bound",
1335       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableOn_ball",
1336       "Komorebi.SpecialFunctions.Coupled.Scales.exists_local_radius",
1337       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableAt",
1338       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableOn",
1339       "Komorebi.SpecialFunctions.Coupled.Scales.oddTerm_hasDerivAt",
1340       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasSum_deriv",
1341       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasDerivAt",
1342       "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_bounds_left",
1343       "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_bounds_right",
1344       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_differentiableOn",
1345       "Komorebi.SpecialFunctions.Coupled.Scales.mul_mem_localDisk",
1346       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_mul_eq",
1347       "Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_mul_denominator",
1348       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_deriv_eq_of_recurrence",
1349       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_local_equations",
1350       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_local_solution",
1351       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_initial_derivatives",
1352       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_odd"
1353     ],
1354     "count": 21,
1355     "axioms": [
1356       "Classical.choice",
1357       "Quot.sound",
1358       "propext"
1359     ]
1360   },
1361   "CoupledEntire_audit": {
1362     "names": [
1363       "Komorebi.SpecialFunctions.Coupled.Scales.oddConvolution_eq",
1364       "Komorebi.SpecialFunctions.Coupled.Scales.next_term_mul_denominator",
1365       "Komorebi.SpecialFunctions.Coupled.Scales.next_term_norm_le",
1366       "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_bootstrap",
1367       "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_bootstrap",
1368       "Komorebi.SpecialFunctions.Coupled.Scales.maxScale_bounds",
1369       "Komorebi.SpecialFunctions.Coupled.Scales.maxScale_lt_one",
1370       "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_on_ladder",
1371       "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_entire",
1372       "Komorebi.SpecialFunctions.Coupled.Scales.odd_term_norm_le_radius",
1373       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableOn_of_radius",
1374       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasSum_deriv_of_radius",
1375       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_entire_of_norm_summable",
1376       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire",
1377       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasSum_deriv_entire",
1378       "Komorebi.SpecialFunctions.Coupled.Scales.next_derivative_term_eq",
1379       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_entire_equation",
1380       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire_equations",
1381       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire_solution"
1382     ],
1383     "count": 19,
1384     "axioms": [
1385       "Classical.choice",
1386       "Quot.sound",
1387       "propext"
1388     ]
1389   },
1390   "CoupledUniqueness_audit": {
1391     "names": [
1392       "Komorebi.SpecialFunctions.Coupled.Scales.analytic_scale_at_zero",
1393       "Komorebi.SpecialFunctions.Coupled.Scales.analytic_order_scale_ge",
1394       "Komorebi.SpecialFunctions.Coupled.Scales.analytic_order_mul_ge_left",
1395       "Komorebi.SpecialFunctions.Coupled.Scales.analytic_order_mul_ge_right",
1396       "Komorebi.SpecialFunctions.Coupled.Scales.analytic_row_order_ge",
1397       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_difference_germ",
1398       "Komorebi.SpecialFunctions.Coupled.Scales.analytic_pair_germ_unique",
1399       "Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_differentiable",
1400       "Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_unique",
1401       "Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_eq",
1402       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire_exists_unique",
1403       "Komorebi.SpecialFunctions.Coupled.Scales.analytic_solution_germ_eq",
1404       "Komorebi.SpecialFunctions.Coupled.Scales.analytic_solution_hasSum",
1405       "Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_hasSum",
1406       "Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_odd",
1407       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_F1_contract"
1408     ],
1409     "count": 16,
1410     "axioms": [
1411       "Classical.choice",
1412       "Quot.sound",
1413       "propext"
1414     ]
1415   },
1416   "CoupledGermInverse_audit": {
1417     "names": [
1418       "Komorebi.SpecialFunctions.Coupled.Scales.denseOdd_odd",
1419       "Komorebi.SpecialFunctions.Coupled.Scales.denseOdd_even",
1420       "Komorebi.SpecialFunctions.Coupled.Scales.odd_hasSum_dense",
1421       "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_hasFPowerSeriesAt",
1422       "Komorebi.SpecialFunctions.Coupled.Scales.odd_coefficients_eq_of_germ_eq",
1423       "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_Taylor_coefficients",
1424       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_hasFPowerSeriesAt",
1425       "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_eq_of_analytic_germs",
1426       "Komorebi.SpecialFunctions.Coupled.Scales.sameJet_of_analytic_germs",
1427       "Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_analytic_germs",
1428       "Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_entire_pair_eq",
1429       "Komorebi.SpecialFunctions.Coupled.Scales.analytic_solution_Taylor_coefficients",
1430       "Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_shared_solution_germ"
1431     ],
1432     "count": 13,
1433     "axioms": [
1434       "Classical.choice",
1435       "Quot.sound",
1436       "propext"
1437     ]
1438   },
1439   "CoupledRescaling_audit": {
1440     "names": [
1441       "Komorebi.SpecialFunctions.Coupled.Scales.denseOddComplex_odd",
1442       "Komorebi.SpecialFunctions.Coupled.Scales.complex_odd_series_hasFPowerSeriesAt",
1443       "Komorebi.SpecialFunctions.Coupled.Scales.complex_odd_coefficients_eq",
1444       "Komorebi.SpecialFunctions.Coupled.Scales.rescaling_coefficient_identity",
1445       "Komorebi.SpecialFunctions.Coupled.Scales.rescaling_forces_defect_zero",
1446       "Komorebi.SpecialFunctions.Coupled.Scales.scalar_components_equal",
1447       "Komorebi.SpecialFunctions.Coupled.Scales.scalarT_solution",
1448       "Komorebi.SpecialFunctions.Coupled.Scales.reductionScale_positive_sq",
1449       "Komorebi.SpecialFunctions.Coupled.Scales.reductionScale_surface",
1450       "Komorebi.SpecialFunctions.Coupled.Scales.effective_scalar_scales",
1451       "Komorebi.SpecialFunctions.Coupled.Scales.scalar_rescaled_solution",
1452       "Komorebi.SpecialFunctions.Coupled.Scales.reductionRoot_positive_sq",
1453       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_scalar_representation",
1454       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_component_rescaling",
1455       "Komorebi.SpecialFunctions.Coupled.Scales.component_rescaling_iff_defect",
1456       "Komorebi.SpecialFunctions.Coupled.Scales.component_rescaling_iff_surfaces",
1457       "Komorebi.SpecialFunctions.Coupled.Scales.scalarT_unique",
1458       "Komorebi.SpecialFunctions.Coupled.Scales.scalarT_symm",
1459       "Komorebi.SpecialFunctions.Coupled.Scales.boundary_entire_collision"
1460     ],
1461     "count": 19,
1462     "axioms": [
1463       "Classical.choice",
1464       "Quot.sound",
1465       "propext"
1466     ]
1467   },
1468   "CoupledCharacteristic_audit": {
1469     "names": [
1470       "Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_zero",
1471       "Komorebi.SpecialFunctions.Coupled.Scales.rpow_contraction_bounds",
1472       "Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_continuous",
1473       "Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_strictMono",
1474       "Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_tendsto",
1475       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_exponent_exists_unique",
1476       "Komorebi.SpecialFunctions.Coupled.Scales.characteristicExponent_spec",
1477       "Komorebi.SpecialFunctions.Coupled.Scales.characteristicVector_positive",
1478       "Komorebi.SpecialFunctions.Coupled.Scales.characteristicLeftVector_positive",
1479       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_right_eigenvector",
1480       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_left_eigenvector",
1481       "Komorebi.SpecialFunctions.Coupled.Scales.characteristicNormalizer_positive",
1482       "Komorebi.SpecialFunctions.Coupled.Scales.normalizedCharacteristicVector_positive",
1483       "Komorebi.SpecialFunctions.Coupled.Scales.normalizedCharacteristicVector_max",
1484       "Komorebi.SpecialFunctions.Coupled.Scales.normalized_characteristic_eigenvector",
1485       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_second_eigenvalue_bound",
1486       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectrum",
1487       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectralRadius",
1488       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_mem_spectrum_iff",
1489       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectrum_real",
1490       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectrum_norm_attained",
1491       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectralRadius_iff",
1492       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectral_exponent_exists_unique"
1493     ],
1494     "count": 23,
1495     "axioms": [
1496       "Classical.choice",
1497       "Quot.sound",
1498       "propext"
1499     ]
1500   },
1501   "CoupledPositiveReal_audit": {
1502     "names": [
1503       "Komorebi.SpecialFunctions.Coupled.Scales.real_series_hasSum",
1504       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_identification",
1505       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_zero",
1506       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_nonneg",
1507       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_lower_linear",
1508       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_hasDerivAt",
1509       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_differentiable",
1510       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_deriv_ge_one",
1511       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_strictMono",
1512       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_positive",
1513       "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_norm_le_real_sum",
1514       "Komorebi.SpecialFunctions.Coupled.Scales.complex_norm_le_real_axis",
1515       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_norm",
1516       "Komorebi.SpecialFunctions.Coupled.Scales.sphere_norm_isGreatest",
1517       "Komorebi.SpecialFunctions.Coupled.Scales.maximum_modulus_real_axis",
1518       "Komorebi.SpecialFunctions.Coupled.Scales.unit_shift_lower_from_deriv",
1519       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_unit_lower",
1520       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_unit_lower",
1521       "Komorebi.SpecialFunctions.Coupled.Scales.minScale_bounds",
1522       "Komorebi.SpecialFunctions.Coupled.Scales.minScale_positive",
1523       "Komorebi.SpecialFunctions.Coupled.Scales.lowerThreshold_gt_one",
1524       "Komorebi.SpecialFunctions.Coupled.Scales.lower_child_radii"
1525     ],
1526     "count": 22,
1527     "axioms": [
1528       "Classical.choice",
1529       "Quot.sound",
1530       "propext"
1531     ]
1532   },
1533   "CoupledLowerGrowth_audit": {
1534     "names": [
1535       "Komorebi.SpecialFunctions.Coupled.Scales.maxScale_positive",
1536       "Komorebi.SpecialFunctions.Coupled.Scales.lowerShift_positive",
1537       "Komorebi.SpecialFunctions.Coupled.Scales.lowerDescent_positive",
1538       "Komorebi.SpecialFunctions.Coupled.Scales.lowerPowerConstant_positive",
1539       "Komorebi.SpecialFunctions.Coupled.Scales.shifted_child_radius",
1540       "Komorebi.SpecialFunctions.Coupled.Scales.child_radius_descent",
1541       "Komorebi.SpecialFunctions.Coupled.Scales.real_radius_descent_induction",
1542       "Komorebi.SpecialFunctions.Coupled.Scales.lower_power_seed",
1543       "Komorebi.SpecialFunctions.Coupled.Scales.lower_power_step",
1544       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_lower_log_power",
1545       "Komorebi.SpecialFunctions.Coupled.Scales.normalizedCharacteristicVector_le_one",
1546       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_lower_log_power",
1547       "Komorebi.SpecialFunctions.Coupled.Scales.lower_log_power_ratio",
1548       "Komorebi.SpecialFunctions.Coupled.Scales.canonicalLowerCoefficient_positive",
1549       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_lower_growth_ratio",
1550       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_lower_norm_power"
1551     ],
1552     "count": 16,
1553     "axioms": [
1554       "Classical.choice",
1555       "Quot.sound",
1556       "propext"
1557     ]
1558   },
1559   "CoupledUpperGrowth_audit": {
1560     "names": [
1561       "Komorebi.SpecialFunctions.Coupled.Scales.full_radius_upper_from_deriv",
1562       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_full_upper",
1563       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_at_one_le_two",
1564       "Komorebi.SpecialFunctions.Coupled.Scales.upperRadius_ge_one",
1565       "Komorebi.SpecialFunctions.Coupled.Scales.upperRadius_child",
1566       "Komorebi.SpecialFunctions.Coupled.Scales.upperSeed_ge_one",
1567       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_upper_ladder",
1568       "Komorebi.SpecialFunctions.Coupled.Scales.upperLogSeed_recurrence",
1569       "Komorebi.SpecialFunctions.Coupled.Scales.upperSeed_log_le",
1570       "Komorebi.SpecialFunctions.Coupled.Scales.scaleDelay_positive",
1571       "Komorebi.SpecialFunctions.Coupled.Scales.scaleDelay_bounds",
1572       "Komorebi.SpecialFunctions.Coupled.Scales.upperCorrection_positive",
1573       "Komorebi.SpecialFunctions.Coupled.Scales.upperCorrection_rows",
1574       "Komorebi.SpecialFunctions.Coupled.Scales.exp_one_lt_three",
1575       "Komorebi.SpecialFunctions.Coupled.Scales.exists_upper_seed_index",
1576       "Komorebi.SpecialFunctions.Coupled.Scales.upper_seed_exp_radius",
1577       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_upper_log_seed",
1578       "Komorebi.SpecialFunctions.Coupled.Scales.log_upper_from_full",
1579       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_full_upper",
1580       "Komorebi.SpecialFunctions.Coupled.Scales.upperSeedBudget_positive",
1581       "Komorebi.SpecialFunctions.Coupled.Scales.upperPowerConstant_positive",
1582       "Komorebi.SpecialFunctions.Coupled.Scales.upper_power_seed",
1583       "Komorebi.SpecialFunctions.Coupled.Scales.exp_sub_scaleDelay",
1584       "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_delayed_upper",
1585       "Komorebi.SpecialFunctions.Coupled.Scales.exp_weight_shift",
1586       "Komorebi.SpecialFunctions.Coupled.Scales.real_log_delay_induction",
1587       "Komorebi.SpecialFunctions.Coupled.Scales.upper_power_step",
1588       "Komorebi.SpecialFunctions.Coupled.Scales.coupled_upper_log_power",
1589       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_log_power",
1590       "Komorebi.SpecialFunctions.Coupled.Scales.upperSeedIndex_spec",
1591       "Komorebi.SpecialFunctions.Coupled.Scales.canonicalUpperCoefficient_positive",
1592       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_growth_ratio",
1593       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_two_sided_growth_ratio",
1594       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_norm_power"
1595     ],
1596     "count": 34,
1597     "axioms": [
1598       "Classical.choice",
1599       "Quot.sound",
1600       "propext"
1601     ]
1602   },
1603   "CoupledGrowthTypes_audit": {
1604     "names": [
1605       "Komorebi.SpecialFunctions.Coupled.Scales.realComponent_positive",
1606       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_growth_ratio_bounds",
1607       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_growth_ratio_eventually",
1608       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_growth_ratio_bounded",
1609       "Komorebi.SpecialFunctions.Coupled.Scales.real_type_sandwich",
1610       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_bounds",
1611       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_types_positive",
1612       "Komorebi.SpecialFunctions.Coupled.Scales.loglog_ratio_sandwich",
1613       "Komorebi.SpecialFunctions.Coupled.Scales.tendsto_loglog_of_ratio_bounds",
1614       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_radial_exponent_limit",
1615       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_radial_order",
1616       "Komorebi.SpecialFunctions.Coupled.Scales.component_spherical_maximum",
1617       "Komorebi.SpecialFunctions.Coupled.Scales.component_real_norm",
1618       "Komorebi.SpecialFunctions.Coupled.Scales.norm_growth_ratio_eventually_eq",
1619       "Komorebi.SpecialFunctions.Coupled.Scales.norm_type_identification",
1620       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_norm_radial_limit",
1621       "Komorebi.SpecialFunctions.Coupled.Scales.maximumModulus_eq",
1622       "Komorebi.SpecialFunctions.Coupled.Scales.maximum_growth_ratio_eventually_eq",
1623       "Komorebi.SpecialFunctions.Coupled.Scales.maximum_type_identification",
1624       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_type_bounds",
1625       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_radial_limit",
1626       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_order"
1627     ],
1628     "count": 22,
1629     "axioms": [
1630       "Classical.choice",
1631       "Quot.sound",
1632       "propext"
1633     ]
1634   },
1635   "CoupledTypeProportions_audit": {
1636     "names": [
1637       "Komorebi.SpecialFunctions.Coupled.Scales.affine_scale_tendsto",
1638       "Komorebi.SpecialFunctions.Coupled.Scales.affine_power_ratio_tendsto",
1639       "Komorebi.SpecialFunctions.Coupled.Scales.lower_comparison_of_tendsto",
1640       "Komorebi.SpecialFunctions.Coupled.Scales.upper_comparison_of_tendsto",
1641       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_envelopes",
1642       "Komorebi.SpecialFunctions.Coupled.Scales.scaled_log_factorization",
1643       "Komorebi.SpecialFunctions.Coupled.Scales.scaled_type_envelopes",
1644       "Komorebi.SpecialFunctions.Coupled.Scales.log_power_correction_tendsto",
1645       "Komorebi.SpecialFunctions.Coupled.Scales.lower_type_row",
1646       "Komorebi.SpecialFunctions.Coupled.Scales.upper_type_row",
1647       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_lower_type_superinvariant",
1648       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_type_subinvariant",
1649       "Komorebi.SpecialFunctions.Coupled.Scales.positive_dot_rigidity",
1650       "Komorebi.SpecialFunctions.Coupled.Scales.left_eigenvector_preserves_dot",
1651       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_fixed_vectors",
1652       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_fixed_proportion",
1653       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_proportions",
1654       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_positive_type_proportions",
1655       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_fixed_ratios",
1656       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_ratios",
1657       "Komorebi.SpecialFunctions.Coupled.Scales.ordinary_type_limit_iff",
1658       "Komorebi.SpecialFunctions.Coupled.Scales.type_equality_iff_scalar_equality",
1659       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_limit_equivalence",
1660       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_limit_vector",
1661       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_type_proportions",
1662       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_type_limit_equivalence"
1663     ],
1664     "count": 26,
1665     "axioms": [
1666       "Classical.choice",
1667       "Quot.sound",
1668       "propext"
1669     ]
1670   },
1671   "CoupledScalarReduction_audit": {
1672     "names": [
1673       "Komorebi.SpecialFunctions.Coupled.Scales.positive_pair_from_product_and_square_sum",
1674       "Komorebi.SpecialFunctions.Coupled.Scales.equal_components_coefficients",
1675       "Komorebi.SpecialFunctions.Coupled.Scales.equal_components_product",
1676       "Komorebi.SpecialFunctions.Coupled.Scales.equal_components_square_sum",
1677       "Komorebi.SpecialFunctions.Coupled.Scales.equal_components_unordered_rows",
1678       "Komorebi.SpecialFunctions.Coupled.Scales.scalar_pair_solution",
1679       "Komorebi.SpecialFunctions.Coupled.Scales.unordered_rows_scalar_representation",
1680       "Komorebi.SpecialFunctions.Coupled.Scales.components_equal_iff_unordered_rows",
1681       "Komorebi.SpecialFunctions.Coupled.Scales.components_equal_iff_scale_pair_set",
1682       "Komorebi.SpecialFunctions.Coupled.Scales.characteristicExponent_eq_of_balance",
1683       "Komorebi.SpecialFunctions.Coupled.Scales.scalar_characteristic_balance_iff",
1684       "Komorebi.SpecialFunctions.Coupled.Scales.scalar_characteristic_order",
1685       "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_order_invariant",
1686       "Komorebi.SpecialFunctions.Coupled.Scales.complex_sinh_hasDerivAt",
1687       "Komorebi.SpecialFunctions.Coupled.Scales.sinh_half_derivative_identity",
1688       "Komorebi.SpecialFunctions.Coupled.Scales.scaled_sinh_half_equation",
1689       "Komorebi.SpecialFunctions.Coupled.Scales.halfScales_positive",
1690       "Komorebi.SpecialFunctions.Coupled.Scales.halfScales_strict",
1691       "Komorebi.SpecialFunctions.Coupled.Scales.scaled_sinh_half_solution",
1692       "Komorebi.SpecialFunctions.Coupled.Scales.sqrt_two_complex_square",
1693       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_half_sinh",
1694       "Komorebi.SpecialFunctions.Coupled.Scales.half_characteristic_order",
1695       "Komorebi.SpecialFunctions.Coupled.Scales.half_radial_order",
1696       "Komorebi.SpecialFunctions.Coupled.Scales.unequalScales_positive",
1697       "Komorebi.SpecialFunctions.Coupled.Scales.unequalScales_strict",
1698       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_characteristic_order",
1699       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_radial_order",
1700       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_normalized_vector",
1701       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_type_proportions",
1702       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_components_different",
1703       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_coefficients_through_seven",
1704       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_row_sums",
1705       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_lower_constants",
1706       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_explicit_lower_growth",
1707       "Komorebi.SpecialFunctions.Coupled.Scales.surface_cross_scale_contract",
1708       "Komorebi.SpecialFunctions.Coupled.Scales.order_surface_realization",
1709       "Komorebi.SpecialFunctions.Coupled.Scales.component_oddSum",
1710       "Komorebi.SpecialFunctions.Coupled.Scales.component_coefficient_majorant",
1711       "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_truncation_eq_tail",
1712       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_complex_truncation_bound",
1713       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_four_term_remainder",
1714       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_degree_seven_polynomials",
1715       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_degree_seven_error"
1716     ],
1717     "count": 43,
1718     "axioms": [
1719       "Classical.choice",
1720       "Quot.sound",
1721       "propext"
1722     ]
1723   },
1724   "CoupledOperator_audit": {
1725     "names": [
1726       "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_iff_scalar_functional",
1727       "Komorebi.SpecialFunctions.Coupled.Scales.nodePolynomial_differentiable",
1728       "Komorebi.SpecialFunctions.Coupled.Scales.nodePolynomial_zero",
1729       "Komorebi.SpecialFunctions.Coupled.Scales.nodePolynomial_values",
1730       "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_scalar_fibers",
1731       "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_row_sum_zero",
1732       "Komorebi.SpecialFunctions.Coupled.Scales.nonzero_row_first_ne_zero",
1733       "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_scale_products",
1734       "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_ordered_rows",
1735       "Komorebi.SpecialFunctions.Coupled.Scales.ordered_rows_field_zero",
1736       "Komorebi.SpecialFunctions.Coupled.Scales.ordered_rows_autonomous",
1737       "Komorebi.SpecialFunctions.Coupled.Scales.zero_row_autonomous",
1738       "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_iff_zero_or_ordered",
1739       "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_nonzero_classification",
1740       "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_projected_field_zero",
1741       "Komorebi.SpecialFunctions.Coupled.Scales.no_nonzero_autonomous_if_rows_differ",
1742       "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_matrix_det_zero",
1743       "Komorebi.SpecialFunctions.Coupled.Scales.no_invertible_constant_decoupling",
1744       "Komorebi.SpecialFunctions.Coupled.Scales.local_projection_analytic",
1745       "Komorebi.SpecialFunctions.Coupled.Scales.local_field_analytic",
1746       "Komorebi.SpecialFunctions.Coupled.Scales.local_field_respects_component_germs",
1747       "Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_iff_scalar_functional",
1748       "Komorebi.SpecialFunctions.Coupled.Scales.entire_field_differentiable",
1749       "Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_implies_entire",
1750       "Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_iff_entire",
1751       "Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_nonzero_classification",
1752       "Komorebi.SpecialFunctions.Coupled.Scales.no_invertible_constant_germ_decoupling"
1753     ],
1754     "count": 27,
1755     "axioms": [
1756       "Classical.choice",
1757       "Quot.sound",
1758       "propext"
1759     ]
1760   },
1761   "CoupledEvaluation_audit": {
1762     "names": [
1763       "Komorebi.SpecialFunctions.Coupled.Scales.component_real_hasSum",
1764       "Komorebi.SpecialFunctions.Coupled.Scales.component_norm_summable",
1765       "Komorebi.SpecialFunctions.Coupled.Scales.component_real_nonneg",
1766       "Komorebi.SpecialFunctions.Coupled.Scales.component_real_mono",
1767       "Komorebi.SpecialFunctions.Coupled.Scales.component_at_real",
1768       "Komorebi.SpecialFunctions.Coupled.Scales.component_le_pairMax",
1769       "Komorebi.SpecialFunctions.Coupled.Scales.realPairMax_nonneg",
1770       "Komorebi.SpecialFunctions.Coupled.Scales.realPairMax_recurrence",
1771       "Komorebi.SpecialFunctions.Coupled.Scales.component_coefficient_le_one",
1772       "Komorebi.SpecialFunctions.Coupled.Scales.component_small_disk_bound",
1773       "Komorebi.SpecialFunctions.Coupled.Scales.pair_small_disk_bound",
1774       "Komorebi.SpecialFunctions.Coupled.Scales.diskMajorant_of_small",
1775       "Komorebi.SpecialFunctions.Coupled.Scales.pair_le_diskMajorant",
1776       "Komorebi.SpecialFunctions.Coupled.Scales.exists_diskMajorant_fuel",
1777       "Komorebi.SpecialFunctions.Coupled.Scales.component_disk_majorant",
1778       "Komorebi.SpecialFunctions.Coupled.Scales.disk_majorant_exists",
1779       "Komorebi.SpecialFunctions.Coupled.Scales.outer_power_comparison",
1780       "Komorebi.SpecialFunctions.Coupled.Scales.positive_odd_outer_remainder",
1781       "Komorebi.SpecialFunctions.Coupled.Scales.oddPolynomial_at_real",
1782       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_outer_remainder",
1783       "Komorebi.SpecialFunctions.Coupled.Scales.canonical_ladder_remainder",
1784       "Komorebi.SpecialFunctions.Coupled.Scales.real_polynomial_le_component",
1785       "Komorebi.SpecialFunctions.Coupled.Scales.real_evaluation_enclosure",
1786       "Komorebi.SpecialFunctions.Coupled.Scales.real_ladder_enclosure",
1787       "Komorebi.SpecialFunctions.Coupled.Scales.rationalDiskMajorant_cast",
1788       "Komorebi.SpecialFunctions.Coupled.Scales.rational_disk_majorant_sound",
1789       "Komorebi.SpecialFunctions.Coupled.Scales.rational_outer_remainder",
1790       "Komorebi.SpecialFunctions.Coupled.Scales.rational_real_enclosure",
1791       "Komorebi.SpecialFunctions.Coupled.Scales.rational_coefficients_cast",
1792       "Komorebi.SpecialFunctions.Coupled.Scales.rational_component_coefficient_cast",
1793       "Komorebi.SpecialFunctions.Coupled.Scales.rational_polynomial_cast",
1794       "Komorebi.SpecialFunctions.Coupled.Scales.rational_maxScale_cast",
1795       "Komorebi.SpecialFunctions.Coupled.Scales.rational_fuel_exists",
1796       "Komorebi.SpecialFunctions.Coupled.Scales.rational_endpoint_enclosure",
1797       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_last_thirty_tail_rational",
1798       "Komorebi.SpecialFunctions.Coupled.Scales.unequal_last_thirty_error"
1799     ],
1800     "count": 36,
1801     "axioms": [
1802       "Classical.choice",
1803       "Quot.sound",
1804       "propext"
1805     ]
1806   },
1807   "CoupledNormalization_audit": {
1808     "names": [
1809       "Komorebi.SpecialFunctions.Coupled.Scales.oddFactorial_ne_zero",
1810       "Komorebi.SpecialFunctions.Coupled.Scales.oddFactorial_zero",
1811       "Komorebi.SpecialFunctions.Coupled.Scales.oddFactorial_succ",
1812       "Komorebi.SpecialFunctions.Coupled.Scales.binomial_factorial_product",
1813       "Komorebi.SpecialFunctions.Coupled.Scales.binomial_factorial_quotient",
1814       "Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_zero",
1815       "Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_succ",
1816       "Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_solution",
1817       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_solution_unique",
1818       "Komorebi.SpecialFunctions.Coupled.Scales.derivativeRow_factorialScale",
1819       "Komorebi.SpecialFunctions.Coupled.Scales.factorial_scaled_coefficients_solution",
1820       "Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_factorial",
1821       "Komorebi.SpecialFunctions.Coupled.Scales.derivativeNext_congr",
1822       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_array_eq",
1823       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_array_length",
1824       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_array_entry",
1825       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_component_factorial",
1826       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_component_normalized",
1827       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_normalized_cast",
1828       "Komorebi.SpecialFunctions.Coupled.Scales.ordinary_array_eq",
1829       "Komorebi.SpecialFunctions.Coupled.Scales.ordinary_array_length",
1830       "Komorebi.SpecialFunctions.Coupled.Scales.ordinary_array_entry",
1831       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_polynomial_eq",
1832       "Komorebi.SpecialFunctions.Coupled.Scales.array_polynomial_eq",
1833       "Komorebi.SpecialFunctions.Coupled.Scales.array_polynomial_cast",
1834       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_polynomial_cast",
1835       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_endpoint_enclosure",
1836       "Komorebi.SpecialFunctions.Coupled.Scales.array_endpoint_enclosure",
1837       "Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_one",
1838       "Komorebi.SpecialFunctions.Coupled.Scales.derivative_normalization_first"
1839     ],
1840     "count": 30,
1841     "axioms": [
1842       "Classical.choice",
1843       "Quot.sound",
1844       "propext"
1845     ]
1846   },
1847   "CoupledGuardedMajorant_audit": {
1848     "names": [
1849       "Komorebi.SpecialFunctions.Coupled.Scales.ladder_terminal",
1850       "Komorebi.SpecialFunctions.Coupled.Scales.ladder_terminal_small",
1851       "Komorebi.SpecialFunctions.Coupled.Scales.ladder_adequate",
1852       "Komorebi.SpecialFunctions.Coupled.Scales.ladder_fold_eq",
1853       "Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_ok",
1854       "Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_of_trace",
1855       "Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_ok_iff",
1856       "Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_not_bits",
1857       "Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_exists_of_adequate",
1858       "Komorebi.SpecialFunctions.Coupled.Scales.guarded_fold_not_steps",
1859       "Komorebi.SpecialFunctions.Coupled.Scales.guarded_fold_ok_iff",
1860       "Komorebi.SpecialFunctions.Coupled.Scales.guarded_fold_bits_iff",
1861       "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_success",
1862       "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_small",
1863       "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_zero",
1864       "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_no_steps",
1865       "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_disk_bound",
1866       "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_endpoint_enclosure",
1867       "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_step_failure",
1868       "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_bit_failure",
1869       "Komorebi.SpecialFunctions.Coupled.Scales.size_fits_iff",
1870       "Komorebi.SpecialFunctions.Coupled.Scales.checked_invalid_scales",
1871       "Komorebi.SpecialFunctions.Coupled.Scales.checked_negative_radius",
1872       "Komorebi.SpecialFunctions.Coupled.Scales.checked_zero_before_resources",
1873       "Komorebi.SpecialFunctions.Coupled.Scales.checked_invalid_steps",
1874       "Komorebi.SpecialFunctions.Coupled.Scales.checked_invalid_bits",
1875       "Komorebi.SpecialFunctions.Coupled.Scales.checked_valid_inputs",
1876       "Komorebi.SpecialFunctions.Coupled.Scales.checked_small_seed_unchecked",
1877       "Komorebi.SpecialFunctions.Coupled.Scales.checked_success_core",
1878       "Komorebi.SpecialFunctions.Coupled.Scales.checked_endpoint_enclosure"
1879     ],
1880     "count": 30,
1881     "axioms": [
1882       "Classical.choice",
1883       "Quot.sound",
1884       "propext"
1885     ]
1886   }
1887 }

Back to source controls

Back to Special Functions