Run 1247

git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1679-source

Cloning into '/var/lib/apodeixis/repos/job-1679-source'...
error: unable to read askpass response from '/usr/bin/false'
fatal: could not read Username for 'https://github.com': terminal prompts disabled

git clone (github installation auth fallback)

Cloning into '/var/lib/apodeixis/repos/job-1679-source'...

git checkout 15230b9e01eb3b110a0f15575dd89641c4b895cc

Note: switching to '15230b9e01eb3b110a0f15575dd89641c4b895cc'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at 15230b9 E19.3: construct the explicit tame Kummer local field (#891)

lake exe cache get

Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)

✔ [8/25] Built Cache.Lean (1.2s)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (1.4s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (138ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (183ms)
✔ [13/25] Built Cache.Lean:c.o (141ms)
✔ [15/25] Built Cache.Init (291ms)
✔ [16/25] Built Cache.IO (2.6s)
✔ [17/25] Built Cache.Init:c.o (98ms)
✔ [18/25] Built Cache.IO:c.o (1.2s)
✔ [19/25] Built Cache.Hashing (1.1s)
✔ [20/25] Built Cache.Hashing:c.o (409ms)
✔ [21/25] Built Cache.Requests (2.5s)
✔ [22/25] Built Cache.Requests:c.o (1.0s)
✔ [23/25] Built Cache.Main (1.4s)
✔ [24/25] Built Cache.Main:c.o (1.7s)
✔ [25/25] Built cache:exe (5.4s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 1 KB/s], Decompressed: 14
Downloaded: 36 file(s) [attempted 36/8459 = 0%, 27 KB/s], Decompressed: 30
Downloaded: 66 file(s) [attempted 66/8459 = 0%, 46 KB/s], Decompressed: 45
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 245 KB/s], Decompressed: 61
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 397 KB/s], Decompressed: 93
Downloaded: 155 file(s) [attempted 155/8459 = 1%, 727 KB/s], Decompressed: 121
Downloaded: 189 file(s) [attempted 189/8459 = 2%, 240 KB/s], Decompressed: 148
Downloaded: 223 file(s) [attempted 223/8459 = 2%, 89 KB/s], Decompressed: 186
Downloaded: 258 file(s) [attempted 258/8459 = 3%, 324 KB/s], Decompressed: 223
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 171 KB/s], Decompressed: 258
Downloaded: 343 file(s) [attempted 343/8459 = 4%, 37 KB/s], Decompressed: 258
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 139 KB/s], Decompressed: 302
Downloaded: 429 file(s) [attempted 429/8459 = 5%, 54 KB/s], Decompressed: 354
Downloaded: 467 file(s) [attempted 467/8459 = 5%, 163 KB/s], Decompressed: 354
Downloaded: 501 file(s) [attempted 501/8459 = 5%, 866 KB/s], Decompressed: 412
Downloaded: 539 file(s) [attempted 539/8459 = 6%, 319 KB/s], Decompressed: 412
Downloaded: 583 file(s) [attempted 583/8459 = 6%, 32 KB/s], Decompressed: 484
Downloaded: 625 file(s) [attempted 625/8459 = 7%, 156 KB/s], Decompressed: 484
Downloaded: 662 file(s) [attempted 662/8459 = 7%, 144 KB/s], Decompressed: 484
Downloaded: 703 file(s) [attempted 703/8459 = 8%, 238 KB/s], Decompressed: 563
Downloaded: 748 file(s) [attempted 748/8459 = 8%, 88 KB/s], Decompressed: 563
Downloaded: 789 file(s) [attempted 789/8459 = 9%, 1657 KB/s], Decompressed: 666
Downloaded: 827 file(s) [attempted 827/8459 = 9%, 131 KB/s], Decompressed: 666
Downloaded: 868 file(s) [attempted 868/8459 = 10%, 39 KB/s], Decompressed: 666
Downloaded: 909 file(s) [attempted 909/8459 = 10%, 492 KB/s], Decompressed: 666
Downloaded: 954 file(s) [attempted 954/8459 = 11%, 163 KB/s], Decompressed: 788
Downloaded: 998 file(s) [attempted 998/8459 = 11%, 280 KB/s], Decompressed: 788
Downloaded: 1036 file(s) [attempted 1036/8459 = 12%, 957 KB/s], Decompressed: 788
Downloaded: 1070 file(s) [attempted 1070/8459 = 12%, 234 KB/s], Decompressed: 919
Downloaded: 1111 file(s) [attempted 1111/8459 = 13%, 356 KB/s], Decompressed: 919
Downloaded: 1156 file(s) [attempted 1156/8459 = 13%, 154 KB/s], Decompressed: 919
Downloaded: 1204 file(s) [attempted 1204/8459 = 14%, 342 KB/s], Decompressed: 919
Downloaded: 1245 file(s) [attempted 1245/8459 = 14%, 207 KB/s], Decompressed: 1060
Downloaded: 1283 file(s) [attempted 1283/8459 = 15%, 1648 KB/s], Decompressed: 1060
Downloaded: 1324 file(s) [attempted 1324/8459 = 15%, 1119 KB/s], Decompressed: 1060
Downloaded: 1361 file(s) [attempted 1361/8459 = 16%, 65 KB/s], Decompressed: 1060
Downloaded: 1406 file(s) [attempted 1406/8459 = 16%, 383 KB/s], Decompressed: 1207
Downloaded: 1447 file(s) [attempted 1447/8459 = 17%, 1082 KB/s], Decompressed: 1207
Downloaded: 1485 file(s) [attempted 1485/8459 = 17%, 425 KB/s], Decompressed: 1207
Downloaded: 1526 file(s) [attempted 1526/8459 = 18%, 220 KB/s], Decompressed: 1207
Downloaded: 1570 file(s) [attempted 1570/8459 = 18%, 212 KB/s], Decompressed: 1365
Downloaded: 1611 file(s) [attempted 1611/8459 = 19%, 92 KB/s], Decompressed: 1365
Downloaded: 1652 file(s) [attempted 1652/8459 = 19%, 127 KB/s], Decompressed: 1365
Downloaded: 1690 file(s) [attempted 1690/8459 = 19%, 298 KB/s], Decompressed: 1365
Downloaded: 1735 file(s) [attempted 1735/8459 = 20%, 452 KB/s], Decompressed: 1529
Downloaded: 1776 file(s) [attempted 1776/8459 = 20%, 146 KB/s], Decompressed: 1529
Downloaded: 1813 file(s) [attempted 1813/8459 = 21%, 60 KB/s], Decompressed: 1529
Downloaded: 1858 file(s) [attempted 1858/8459 = 21%, 124 KB/s], Decompressed: 1529
Downloaded: 1896 file(s) [attempted 1896/8459 = 22%, 774 KB/s], Decompressed: 1529
Downloaded: 1937 file(s) [attempted 1937/8459 = 22%, 334 KB/s], Decompressed: 1694
Downloaded: 1978 file(s) [attempted 1978/8459 = 23%, 486 KB/s], Decompressed: 1694
Downloaded: 2016 file(s) [attempted 2016/8459 = 23%, 1622 KB/s], Decompressed: 1694
Downloaded: 2053 file(s) [attempted 2053/8459 = 24%, 45 KB/s], Decompressed: 1694
Downloaded: 2094 file(s) [attempted 2094/8459 = 24%, 253 KB/s], Decompressed: 1694
Downloaded: 2139 file(s) [attempted 2139/8459 = 25%, 130 KB/s], Decompressed: 1913
Downloaded: 2180 file(s) [attempted 2180/8459 = 25%, 113 KB/s], Decompressed: 1913
Downloaded: 2224 file(s) [attempted 2224/8459 = 26%, 124 KB/s], Decompressed: 1913
Downloaded: 2266 file(s) [attempted 2266/8459 = 26%, 337 KB/s], Decompressed: 1913
Downloaded: 2306 file(s) [attempted 2306/8459 = 27%, 178 KB/s], Decompressed: 1913
Downloaded: 2344 file(s) [attempted 2344/8459 = 27%, 238 KB/s], Decompressed: 1913
Downloaded: 2358 file(s) [attempted 2358/8459 = 27%, 350 KB/s], Decompressed: 2129
Downloaded: 2399 file(s) [attempted 2399/8459 = 28%, 464 KB/s], Decompressed: 2129
Downloaded: 2447 file(s) [attempted 2447/8459 = 28%, 264 KB/s], Decompressed: 2129
Downloaded: 2498 file(s) [attempted 2498/8459 = 29%, 62 KB/s], Decompressed: 2129
Downloaded: 2550 file(s) [attempted 2550/8459 = 30%, 69 KB/s], Decompressed: 2129
Downloaded: 2598 file(s) [attempted 2598/8459 = 30%, 1863 KB/s], Decompressed: 2351
Downloaded: 2649 file(s) [attempted 2649/8459 = 31%, 50 KB/s], Decompressed: 2351
Downloaded: 2697 file(s) [attempted 2697/8459 = 31%, 58 KB/s], Decompressed: 2351
Downloaded: 2745 file(s) [attempted 2745/8459 = 32%, 42 KB/s], Decompressed: 2351
Downloaded: 2790 file(s) [attempted 2790/8459 = 32%, 1762 KB/s], Decompressed: 2351
Downloaded: 2827 file(s) [attempted 2827/8459 = 33%, 33 KB/s], Decompressed: 2351
Downloaded: 2868 file(s) [attempted 2868/8459 = 33%, 207 KB/s], Decompressed: 2351
Downloaded: 2906 file(s) [attempted 2906/8459 = 34%, 263 KB/s], Decompressed: 2598
Downloaded: 2951 file(s) [attempted 2951/8459 = 34%, 680 KB/s], Decompressed: 2598
Downloaded: 2992 file(s) [attempted 2992/8459 = 35%, 193 KB/s], Decompressed: 2598
Downloaded: 3029 file(s) [attempted 3029/8459 = 35%, 871 KB/s], Decompressed: 2598
Downloaded: 3074 file(s) [attempted 3074/8459 = 36%, 200 KB/s], Decompressed: 2598
Downloaded: 3118 file(s) [attempted 3118/8459 = 36%, 168 KB/s], Decompressed: 2598
Downloaded: 3156 file(s) [attempted 3156/8459 = 37%, 119 KB/s], Decompressed: 2872
Downloaded: 3197 file(s) [attempted 3197/8459 = 37%, 72 KB/s], Decompressed: 2872
Downloaded: 3238 file(s) [attempted 3238/8459 = 38%, 611 KB/s], Decompressed: 2872
Downloaded: 3279 file(s) [attempted 3279/8459 = 38%, 325 KB/s], Decompressed: 2872
Downloaded: 3327 file(s) [attempted 3327/8459 = 39%, 105 KB/s], Decompressed: 2872
Downloaded: 3368 file(s) [attempted 3368/8459 = 39%, 182 KB/s], Decompressed: 2872
Downloaded: 3410 file(s) [attempted 3410/8459 = 40%, 575 KB/s], Decompressed: 3142
Downloaded: 3447 file(s) [attempted 3447/8459 = 40%, 315 KB/s], Decompressed: 3142
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 256 KB/s], Decompressed: 3142
Downloaded: 3529 file(s) [attempted 3529/8459 = 41%, 253 KB/s], Decompressed: 3142
Downloaded: 3571 file(s) [attempted 3571/8459 = 42%, 496 KB/s], Decompressed: 3142
Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 178 KB/s], Decompressed: 3142
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 1459 KB/s], Decompressed: 3142
Downloaded: 3690 file(s) [attempted 3690/8459 = 43%, 199 KB/s], Decompressed: 3142
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 285 KB/s], Decompressed: 3410
Downloaded: 3776 file(s) [attempted 3776/8459 = 44%, 1590 KB/s], Decompressed: 3410
Downloaded: 3817 file(s) [attempted 3817/8459 = 45%, 382 KB/s], Decompressed: 3410
Downloaded: 3858 file(s) [attempted 3858/8459 = 45%, 780 KB/s], Decompressed: 3410
Downloaded: 3899 file(s) [attempted 3899/8459 = 46%, 205 KB/s], Decompressed: 3410
Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 917 KB/s], Decompressed: 3410
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 167 KB/s], Decompressed: 3410
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 1468 KB/s], Decompressed: 3410
Downloaded: 4067 file(s) [attempted 4067/8459 = 48%, 293 KB/s], Decompressed: 3410
Downloaded: 4112 file(s) [attempted 4112/8459 = 48%, 174 KB/s], Decompressed: 3714
Downloaded: 4153 file(s) [attempted 4153/8459 = 49%, 367 KB/s], Decompressed: 3714
Downloaded: 4191 file(s) [attempted 4191/8459 = 49%, 344 KB/s], Decompressed: 3714
Downloaded: 4232 file(s) [attempted 4232/8459 = 50%, 535 KB/s], Decompressed: 3714
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 371 KB/s], Decompressed: 3714
Downloaded: 4314 file(s) [attempted 4314/8459 = 50%, 256 KB/s], Decompressed: 3714
Downloaded: 4355 file(s) [attempted 4355/8459 = 51%, 81 KB/s], Decompressed: 3714
Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 1024 KB/s], Decompressed: 3714
Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 153 KB/s], Decompressed: 3714
Downloaded: 4489 file(s) [attempted 4489/8459 = 53%, 93 KB/s], Decompressed: 4088
Downloaded: 4526 file(s) [attempted 4526/8459 = 53%, 171 KB/s], Decompressed: 4088
Downloaded: 4560 file(s) [attempted 4560/8459 = 53%, 995 KB/s], Decompressed: 4088
Downloaded: 4602 file(s) [attempted 4602/8459 = 54%, 705 KB/s], Decompressed: 4088
Downloaded: 4646 file(s) [attempted 4646/8459 = 54%, 611 KB/s], Decompressed: 4088
Downloaded: 4691 file(s) [attempted 4691/8459 = 55%, 144 KB/s], Decompressed: 4088
Downloaded: 4735 file(s) [attempted 4735/8459 = 55%, 167 KB/s], Decompressed: 4088
Downloaded: 4780 file(s) [attempted 4780/8459 = 56%, 539 KB/s], Decompressed: 4088
Downloaded: 4811 file(s) [attempted 4811/8459 = 56%, 205 KB/s], Decompressed: 4088
Downloaded: 4848 file(s) [attempted 4848/8459 = 57%, 83 KB/s], Decompressed: 4088
Downloaded: 4889 file(s) [attempted 4889/8459 = 57%, 496 KB/s], Decompressed: 4471
Downloaded: 4934 file(s) [attempted 4934/8459 = 58%, 170 KB/s], Decompressed: 4471
Downloaded: 4982 file(s) [attempted 4982/8459 = 58%, 114 KB/s], Decompressed: 4471
Downloaded: 5019 file(s) [attempted 5019/8459 = 59%, 207 KB/s], Decompressed: 4471
Downloaded: 5057 file(s) [attempted 5057/8459 = 59%, 215 KB/s], Decompressed: 4471
Downloaded: 5095 file(s) [attempted 5095/8459 = 60%, 538 KB/s], Decompressed: 4471
Downloaded: 5136 file(s) [attempted 5136/8459 = 60%, 38 KB/s], Decompressed: 4471
Downloaded: 5180 file(s) [attempted 5180/8459 = 61%, 1339 KB/s], Decompressed: 4471
Downloaded: 5225 file(s) [attempted 5225/8459 = 61%, 59 KB/s], Decompressed: 4471
Downloaded: 5263 file(s) [attempted 5263/8459 = 62%, 575 KB/s], Decompressed: 4850
Downloaded: 5307 file(s) [attempted 5307/8459 = 62%, 163 KB/s], Decompressed: 4850
Downloaded: 5348 file(s) [attempted 5348/8459 = 63%, 151 KB/s], Decompressed: 4850
Downloaded: 5389 file(s) [attempted 5389/8459 = 63%, 78 KB/s], Decompressed: 4850
Downloaded: 5430 file(s) [attempted 5430/8459 = 64%, 251 KB/s], Decompressed: 4850
Downloaded: 5472 file(s) [attempted 5472/8459 = 64%, 23 KB/s], Decompressed: 4850
Downloaded: 5513 file(s) [attempted 5513/8459 = 65%, 101 KB/s], Decompressed: 4850
Downloaded: 5555 file(s) [attempted 5555/8459 = 65%, 268 KB/s], Decompressed: 4850
Downloaded: 5598 file(s) [attempted 5598/8459 = 66%, 88 KB/s], Decompressed: 5232
Downloaded: 5639 file(s) [attempted 5639/8459 = 66%, 122 KB/s], Decompressed: 5232
Downloaded: 5677 file(s) [attempted 5677/8459 = 67%, 67 KB/s], Decompressed: 5232
Downloaded: 5718 file(s) [attempted 5718/8459 = 67%, 54 KB/s], Decompressed: 5232
Downloaded: 5763 file(s) [attempted 5763/8459 = 68%, 211 KB/s], Decompressed: 5232
Downloaded: 5804 file(s) [attempted 5804/8459 = 68%, 201 KB/s], Decompressed: 5232
Downloaded: 5848 file(s) [attempted 5848/8459 = 69%, 1051 KB/s], Decompressed: 5232
Downloaded: 5889 file(s) [attempted 5889/8459 = 69%, 87 KB/s], Decompressed: 5232
Downloaded: 5934 file(s) [attempted 5934/8459 = 70%, 34 KB/s], Decompressed: 5232
Downloaded: 5975 file(s) [attempted 5975/8459 = 70%, 281 KB/s], Decompressed: 5232
Downloaded: 6013 file(s) [attempted 6013/8459 = 71%, 52 KB/s], Decompressed: 5232
Downloaded: 6054 file(s) [attempted 6054/8459 = 71%, 597 KB/s], Decompressed: 5232
Downloaded: 6092 file(s) [attempted 6092/8459 = 72%, 767 KB/s], Decompressed: 5571
Downloaded: 6136 file(s) [attempted 6136/8459 = 72%, 841 KB/s], Decompressed: 5571
Downloaded: 6177 file(s) [attempted 6177/8459 = 73%, 149 KB/s], Decompressed: 5571
Downloaded: 6218 file(s) [attempted 6218/8459 = 73%, 303 KB/s], Decompressed: 5571
Downloaded: 6249 file(s) [attempted 6249/8459 = 73%, 69 KB/s], Decompressed: 5571
Downloaded: 6294 file(s) [attempted 6294/8459 = 74%, 247 KB/s], Decompressed: 5571
Downloaded: 6331 file(s) [attempted 6331/8459 = 74%, 579 KB/s], Decompressed: 5571
Downloaded: 6376 file(s) [attempted 6376/8459 = 75%, 516 KB/s], Decompressed: 5571
Downloaded: 6414 file(s) [attempted 6414/8459 = 75%, 85 KB/s], Decompressed: 5571
Downloaded: 6458 file(s) [attempted 6458/8459 = 76%, 192 KB/s], Decompressed: 5571
Downloaded: 6499 file(s) [attempted 6499/8459 = 76%, 956 KB/s], Decompressed: 6061
Downloaded: 6540 file(s) [attempted 6540/8459 = 77%, 522 KB/s], Decompressed: 6061
Downloaded: 6581 file(s) [attempted 6581/8459 = 77%, 368 KB/s], Decompressed: 6061
Downloaded: 6622 file(s) [attempted 6622/8459 = 78%, 53 KB/s], Decompressed: 6061
Downloaded: 6660 file(s) [attempted 6660/8459 = 78%, 189 KB/s], Decompressed: 6061
Downloaded: 6688 file(s) [attempted 6688/8459 = 79%, 2525 KB/s], Decompressed: 6061
Downloaded: 6735 file(s) [attempted 6735/8459 = 79%, 197 KB/s], Decompressed: 6061
Downloaded: 6783 file(s) [attempted 6783/8459 = 80%, 24 KB/s], Decompressed: 6061
Downloaded: 6831 file(s) [attempted 6831/8459 = 80%, 40 KB/s], Decompressed: 6061
Downloaded: 6872 file(s) [attempted 6872/8459 = 81%, 937 KB/s], Decompressed: 6061
Downloaded: 6920 file(s) [attempted 6920/8459 = 81%, 400 KB/s], Decompressed: 6061
Downloaded: 6962 file(s) [attempted 6962/8459 = 82%, 92 KB/s], Decompressed: 6061
Downloaded: 6999 file(s) [attempted 6999/8459 = 82%, 35 KB/s], Decompressed: 6492
Downloaded: 7037 file(s) [attempted 7037/8459 = 83%, 889 KB/s], Decompressed: 6492
Downloaded: 7081 file(s) [attempted 7081/8459 = 83%, 467 KB/s], Decompressed: 6492
Downloaded: 7123 file(s) [attempted 7123/8459 = 84%, 503 KB/s], Decompressed: 6492
Downloaded: 7164 file(s) [attempted 7164/8459 = 84%, 82 KB/s], Decompressed: 6492
Downloaded: 7205 file(s) [attempted 7205/8459 = 85%, 80 KB/s], Decompressed: 6492
Downloaded: 7242 file(s) [attempted 7242/8459 = 85%, 469 KB/s], Decompressed: 6492
Downloaded: 7283 file(s) [attempted 7283/8459 = 86%, 192 KB/s], Decompressed: 6492
Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 238 KB/s], Decompressed: 6492
Downloaded: 7375 file(s) [attempted 7375/8459 = 87%, 97 KB/s], Decompressed: 6492
Downloaded: 7410 file(s) [attempted 7410/8459 = 87%, 133 KB/s], Decompressed: 6492
Downloaded: 7451 file(s) [attempted 7451/8459 = 88%, 111 KB/s], Decompressed: 6968
Downloaded: 7492 file(s) [attempted 7492/8459 = 88%, 1229 KB/s], Decompressed: 6968
Downloaded: 7530 file(s) [attempted 7530/8459 = 89%, 1222 KB/s], Decompressed: 6968
Downloaded: 7578 file(s) [attempted 7578/8459 = 89%, 69 KB/s], Decompressed: 6968
Downloaded: 7623 file(s) [attempted 7623/8459 = 90%, 1283 KB/s], Decompressed: 6968
Downloaded: 7664 file(s) [attempted 7664/8459 = 90%, 127 KB/s], Decompressed: 6968
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 581 KB/s], Decompressed: 6968
Downloaded: 7739 file(s) [attempted 7739/8459 = 91%, 1596 KB/s], Decompressed: 6968
Downloaded: 7787 file(s) [attempted 7787/8459 = 92%, 131 KB/s], Decompressed: 6968
Downloaded: 7835 file(s) [attempted 7835/8459 = 92%, 308 KB/s], Decompressed: 6968
Downloaded: 7886 file(s) [attempted 7886/8459 = 93%, 827 KB/s], Decompressed: 6968
Downloaded: 7934 file(s) [attempted 7934/8459 = 93%, 329 KB/s], Decompressed: 6968
Downloaded: 7979 file(s) [attempted 7979/8459 = 94%, 153 KB/s], Decompressed: 7417
Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 661 KB/s], Decompressed: 7417
Downloaded: 8058 file(s) [attempted 8058/8459 = 95%, 165 KB/s], Decompressed: 7417
Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 510 KB/s], Decompressed: 7417
Downloaded: 8143 file(s) [attempted 8143/8459 = 96%, 75 KB/s], Decompressed: 7417
Downloaded: 8188 file(s) [attempted 8188/8459 = 96%, 508 KB/s], Decompressed: 7417
Downloaded: 8232 file(s) [attempted 8232/8459 = 97%, 369 KB/s], Decompressed: 7417
Downloaded: 8273 file(s) [attempted 8273/8459 = 97%, 156 KB/s], Decompressed: 7417
Downloaded: 8311 file(s) [attempted 8311/8459 = 98%, 187 KB/s], Decompressed: 7417
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 564 KB/s], Decompressed: 7417
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 85 KB/s], Decompressed: 7417
Downloaded: 8434 file(s) [attempted 8434/8459 = 99%, 409 KB/s], Decompressed: 7417
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 135 KB/s], Decompressed: 7938
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 135 KB/s], Decompressed: 7938

apx-runtime-resource-v1	apx-verifier-job-1679-runtime-lake_cache-3083124-1787103768086256480-0	3698688	3952640	21474836480	0	0	0	0	0	0	622821376	1724448768	21474836480	0	0	0	0	0	0

lake build

or readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: Iut/Foundations/SourceBadPlaceIntegralLogShell.lean:291:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4665/4888] Built Iut.Foundations.LindemannWeierstrassAlgebraicPart (4.5s)
⚠ [4667/4888] Built Iut.Foundations.SourceIUTIIIStepXIPositiveInd3NoEscapeClassification (3.7s)
warning: Iut/Foundations/SourceIUTIIIStepXIPositiveInd3NoEscapeClassification.lean:126:6: unused variable `baseCompact`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [4668/4888] Built Iut.Foundations.SourceIUTIIIStepXICanonicalQPilotRecognitionBoundary (4.6s)
⚠ [4670/4923] Built Iut.Foundations.SourceGlobalLogShellSemantics (7.3s)
warning: Iut/Foundations/SourceGlobalLogShellSemantics.lean:263:4: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: Iut/Foundations/SourceGlobalLogShellSemantics.lean:272:4: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: Iut/Foundations/SourceGlobalLogShellSemantics.lean:326:4: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: Iut/Foundations/SourceGlobalLogShellSemantics.lean:365:2: Try this: intro preimageCompact x hx v label
⚠ [4672/4923] Built Iut.Foundations.SourceIUTIIIStepXICommonIntegralPacketCompactnessConstructor (5.8s)
warning: Iut/Foundations/SourceIUTIIIStepXICommonIntegralPacketCompactnessConstructor.lean:320:64: remove line break in the source

This part of the code
  'label
   '
should be written as
  'label).CanonicalPacketHullIsCompact'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
✔ [4673/4923] Built Iut.Foundations.SourceIUTIIIStepXIAlienCopiesLabelwisePacketHull (76s)
⚠ [4674/4923] Built Iut.Foundations.SourceStepXIDIdentification (4.4s)
warning: Iut/Foundations/SourceStepXIDIdentification.lean:89:0: automatically included section variable(s) unused in theorem `Iut.SourceCorollary312APTStepXIInput.badPlaceLocalQLogDegree_pos`:
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceStepXIDIdentification.lean:98:0: automatically included section variable(s) unused in theorem `Iut.SourceCorollary312APTStepXIInput.badPlaceRawLabelLogVolume_one`:
  [SourceSelectedPlaceFiberFiniteness theta]
  [SourceSelectedBadPlaceFiniteness theta]
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceSelectedPlaceFiberFiniteness
  theta] [SourceSelectedBadPlaceFiniteness theta] [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceStepXIDIdentification.lean:148:0: automatically included section variable(s) unused in theorem `Iut.SourceCorollary312APTStepXIInput.labelTensorIndexOne_tensorIndex`:
  [SourceSelectedPlaceFiberFiniteness theta]
  [SourceSelectedBadPlaceFiniteness theta]
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceSelectedPlaceFiberFiniteness
  theta] [SourceSelectedBadPlaceFiniteness theta] [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
✔ [4676/4923] Built Iut.Foundations.LindemannWeierstrassSymmetricEval (2.3s)
⚠ [4677/4923] Built Iut.Foundations.SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance (27s)
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:273:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:358:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:368:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:380:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:389:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:397:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:406:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:414:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:426:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:435:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:443:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:452:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:472:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:479:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:489:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:496:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:548:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3ThetaHullInvariance.lean:563:64: remove line break in the source

This part of the code
  'label
   '
should be written as
  'label).CanonicalPacketHullIsCompact'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
⚠ [4678/4923] Built Iut.Foundations.SourceIUTIIIStepXIClosureStageSupportClassification (46s)
warning: Iut/Foundations/SourceIUTIIIStepXIClosureStageSupportClassification.lean:146:6: unused variable `baseCompact`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [4679/4923] Built Iut.Foundations.SourceIUTIIIStepXIPaperNativeArithmeticVectorBundleLocalization (8.1s)
✔ [4680/4923] Built Iut.Foundations.SourceIUTIIIStepXIQPilotRegionalCandidateInventory (5.1s)
✔ [4681/4923] Built Iut.Foundations.SourceIUTIIIStepXIAlienCopiesDistortionMargin (6.9s)
✔ [4682/4923] Built Iut.Foundations.SourceStepXIHullRawVolumeMeasure (5.2s)
✔ [4684/4923] Built Iut.Foundations.SourceIUTIIIStepXIAlienCopiesFiniteSupportClassification (4.5s)
✔ [4685/4923] Built Iut.Foundations.SourceIUTIIIStepXIIndPacketCompactFactorizationClassification (6.7s)
✔ [4686/4923] Built Iut.Foundations.SourceIUTIIIStepXIQPilotLocalRegionalRealization (4.5s)
✔ [4687/4923] Built Iut.Foundations.SourceIUTIIIStepXIPositiveLabelRawUpperControlClassification (3.0s)
✔ [4688/4923] Built Iut.Foundations.SourceIUTIIIStepXIIndependentTerminalVerdict (7.8s)
✔ [4689/4923] Built Iut.Foundations.SourceStepXIOrbitRadiusProbe (4.4s)
✔ [4690/4923] Built Iut.Foundations.LindemannWeierstrassLog (6.0s)
⚠ [4691/4923] Built Iut.Foundations.SourceIUTIIIStepXIAdjacentInd3MeasuredStageFactorization (126s)
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3MeasuredStageFactorization.lean:140:2: Try this: intro preimageCompact rationalPlace label
✔ [4692/4923] Built Iut.Foundations.SourceIUTIIIStepXIAmbientIndObjectLogVolumeClassification (134s)
✔ [4693/4923] Built Iut.Foundations.SourceIUTIIIStepXIQPilotBadSupportRegionalMap (7.6s)
✔ [4694/4923] Built Iut.Foundations.SourceIUTIIIStepXIQPilotFiniteSupportGlobalAssembly (4.5s)
✔ [4695/4923] Built Iut.Foundations.SourceIUTIIIStepXIHullLiftEffectiveScaleClassification (3.0s)
✔ [4696/4927] Built Iut.Foundations.SourceStepXIShellFrameProbe (5.3s)
✔ [4697/4927] Built Iut.Foundations.SourcePadicLogarithmLocalVolume (4.0s)
✔ [4698/4927] Built Iut.Foundations.SourceIUTIIIStepXIAdjacentInd3PrincipalRadiusClassification (7.0s)
✔ [4699/4927] Built Iut.Foundations.SourceIUTIIIStepXICrossStageNormalizedValueConstructor (6.0s)
⚠ [4700/4927] Built Iut.Foundations.SourceIUTIIIStepXIAlienCopiesGoodPlaceHullIdentification (95s)
warning: Iut/Foundations/SourceIUTIIIStepXIAlienCopiesGoodPlaceHullIdentification.lean:1338:0: Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in
```
set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...
```

Note: This linter can be disabled with `set_option linter.style.setOption false`
warning: Iut/Foundations/SourceIUTIIIStepXIAlienCopiesGoodPlaceHullIdentification.lean:1590:0: Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in
```
set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...
```

Note: This linter can be disabled with `set_option linter.style.setOption false`
warning: Iut/Foundations/SourceIUTIIIStepXIAlienCopiesGoodPlaceHullIdentification.lean:1988:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [4701/4927] Built Iut.Foundations.SourceIUTIIIStepXIQPilotBadSupportLocalValueFormula (4.0s)
✔ [4702/4927] Built Iut.Foundations.SourceIUTIIIStepXICompleteOutputSlackClassification (3.0s)
✔ [4703/4927] Built Iut.Foundations.SourceStepXIDifferentIdentity (7.3s)
✔ [4705/4931] Built Iut.SourceTrace.PadicLogarithmLocalVolumeSourceMatrix (3.2s)
⚠ [4706/4933] Built Iut.Foundations.SourceFiniteExtensionPadicLogarithm (11s)
info: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:780:2: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:939:5: unused variable `first`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:940:5: unused variable `second`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:1794:61: remove line break in the source

This part of the code
  'index))
   '
should be written as
  'index))).toLogShellDefinition.invariantLocalUnits)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:1815:61: remove line break in the source

This part of the code
  'index))
   '
should be written as
  'index))).toLogShellDefinition.invariantLocalUnits)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:1887:58: remove line break in the source

This part of the code
  'index)
   '
should be written as
  'index)).toLogShellDefinition.invariantLocalUnits)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:1901:58: remove line break in the source

This part of the code
  'index)
   '
should be written as
  'index)).toLogShellDefinition.invariantLocalUnits)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:1919:64: remove line break in the source

This part of the code
  'index)))
   '
should be written as
  'index)))).toLogShellDefinition.invariantLocalUnits)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:1934:58: remove line break in the source

This part of the code
  'index)
   '
should be written as
  'index)).toLogShellDefinition.invariantLocalUnits)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:1953:58: remove line break in the source

This part of the code
  'index)
   '
should be written as
  'index)).toLogShellDefinition.invariantLocalUnits)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:1976:64: remove line break in the source

This part of the code
  'index)))
   '
should be written as
  'index)))).toLogShellDefinition.invariantLocalUnits)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:2001:100: This line exceeds the 100 character limit, please shorten it!
You can use "string gaps" to format long strings: within a string quotation, using a '\' at the end of a line allows you to continue the string on the following line, removing all intervening whitespace.

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:2038:7: unused variable `factor`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:2038:30: unused variable `place`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceFiniteExtensionPadicLogarithm.lean:2120:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
⚠ [4707/4933] Built Iut.Foundations.SourceIUTIIIStepXIAdjacentInd3SecondLogCompatibilityRepair (15s)
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentInd3SecondLogCompatibilityRepair.lean:270:64: remove line break in the source

This part of the code
  'label
   '
should be written as
  'label).CanonicalPacketHullIsCompact'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
✔ [4708/4933] Built Iut.Foundations.SourceIUTIIIStepXIOperationalAmbientOverregionConstructor (4.6s)
✔ [4709/4933] Built Iut.Foundations.SourceIUTIIIStepXIQPilotRegionalHullContainmentClassification (6.4s)
✔ [4710/4933] Built Iut.Foundations.SourceIUTIIIStepXICommonStageUnramifiedIntegralComparison (79s)
✔ [4711/4933] Built Iut.Foundations.SourceIUTIIIStepXITieredTerminalReintegration (11s)
✔ [4712/4933] Built Iut.Foundations.SourceInitialTheta11a1DifferentEquation (8.5s)
⚠ [4715/4944] Built Iut.Foundations.SourceGenuineTensorLogShell (4.5s)
warning: Iut/Foundations/SourceGenuineTensorLogShell.lean:112:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceGenuineTensorLogShell.lean:49:0: `tprod_mem_span_of_mem_spans` does not use the following hypothesis in its type:
  • [DecidableEq index] (#3)

Consider removing this hypothesis and using `classical` in the proof instead. For terms, consider using `open scoped Classical in` at the term level (not the command level).

Note: This linter can be disabled with `set_option linter.unusedDecidableInType false`
warning: Iut/Foundations/SourceGenuineTensorLogShell.lean:49:0: `tprod_mem_span_of_mem_spans` does not use the following hypothesis in its type:
  • [Fintype index] (#2)

Consider replacing this hypothesis with the corresponding instance of `Finite` and using `Fintype.ofFinite` in the proof, or removing it entirely.

Note: This linter can be disabled with `set_option linter.unusedFintypeInType false`
warning: Iut/Foundations/SourceGenuineTensorLogShell.lean:240:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceGenuineTensorLogShell.lean:355:8: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceGenuineTensorLogShell.lean:361:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [4716/5055] Built Iut.Foundations.SourceIUTIIIStepXIAdjacentSecondLogRepairClassification (6.0s)
warning: Iut/Foundations/SourceIUTIIIStepXIAdjacentSecondLogRepairClassification.lean:338:64: remove line break in the source

This part of the code
  'label
   '
should be written as
  'label).CanonicalPacketHullIsCompact'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
⚠ [4717/5055] Built Iut.Foundations.SourceIUTIIIStepXIThetaHullPacketClosedness (5.3s)
warning: Iut/Foundations/SourceIUTIIIStepXIThetaHullPacketClosedness.lean:154:6: Try `simp at this` instead of `simpa using this`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [4718/5055] Built Iut.Foundations.SourceIUTIIIStepXIQPilotBadSupportHullComparison (5.3s)
✔ [4719/5055] Built Iut.Foundations.SourceIUTIIIStepXIQPilotResidualExceptionalContainment (5.9s)
✔ [4720/5055] Built Iut.Foundations.SourceIUTIIIStepXIPaperNativeGoodPlaceHullIdentification (37s)
✔ [4721/5055] Built Iut.Foundations.SourceIUTIIIStepXICanonicalSourceLogShellRebaseRecognition (4.4s)
✔ [4722/5055] Built Iut.Foundations.SourceIUTIIIStepXIFourFrontHypothesisLaboratory (7.4s)
✔ [4723/5055] Built Iut.Foundations.SourceIUTIIIStepXIPackGTopologyAmbientMeasurementEvidence (3.8s)
✔ [4726/5055] Built Iut.Foundations.SourceIUTIVLogShellHullVolumeBounds (6.3s)
✔ [4728/5056] Built Iut.SourceTrace.FiniteExtensionPadicLogarithmSourceMatrix (3.3s)
✔ [4729/5056] Built Iut.Foundations.SourceIUTIIIStepXIHullRestrictedAdjacentSecondLogFixedMaximizerBound (9.4s)
✔ [4730/5056] Built Iut.Foundations.SourceIUTIIIStepXIHullRestrictedAdjacentSecondLogStageLanding (10s)
✔ [4732/5056] Built Iut.SourceTrace.GenuineTensorLogShellSourceMatrix (3.4s)
✔ [4733/5056] Built Iut.SourceTrace.InitialTheta11a1CertifiedSourceAudit (3.1s)
✔ [4734/5056] Built Iut.Foundations.SourceIUTIIIStepXIValueInd3OrbitDiameter (3.5s)
⚠ [4735/5056] Built Iut.Foundations.SourceCyclotomicRigidityZhatAmbiguity (3.1s)
warning: Iut/Foundations/SourceCyclotomicRigidityZhatAmbiguity.lean:179:4: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: Iut/Foundations/SourceCyclotomicRigidityZhatAmbiguity.lean:187:4: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4736/5056] Built Iut.Foundations.SourceScholzeStixHodgeBelyiReduction (5.8s)
✔ [4737/5056] Built Iut.Foundations.SourceScholzeStixLogKummerReduction (3.8s)
✔ [4738/5056] Built Iut.Foundations.SourceScholzeStixRealifiedFrobenioidReduction (5.2s)
✔ [4739/5056] Built Iut.Foundations.SourceIUTIIICorollary312GlobalFrobenioidControl (4.7s)
ℹ [4740/5056] Built Iut.SourceTrace.Corollary312PaperPossibleImageFamilyAudit (3.1s)
info: Iut/SourceTrace/Corollary312PaperPossibleImageFamilyAudit.lean:45:0: 'Iut.sourcePaperPossibleImageFamilyAuditStatus_eq_bounded' does not depend on any axioms
info: Iut/SourceTrace/Corollary312PaperPossibleImageFamilyAudit.lean:46:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalClausewisePossibleImageFamilyAt_subset_canonicalOutputFamilyAt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperPossibleImageFamilyAudit.lean:47:0: 'Iut.SourceCorollary312APTStepXIInput.SourcePaperPossibleImageFamily.ind12_subset' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperPossibleImageFamilyAudit.lean:48:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalPaperPossibleImageCompactnessBoundary_implies_operational' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperPossibleImageFamilyAudit.lean:49:0: 'Iut.SourcePaperPossibleImageFamilySeparationTest.clausewiseFamily_ssubset_operationalFamily' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [4741/5056] Built Iut.SourceTrace.Corollary312PositiveInd3NoEscapeAudit (3.1s)
info: Iut/SourceTrace/Corollary312PositiveInd3NoEscapeAudit.lean:49:0: 'Iut.sourcePositiveInd3NoEscapeAuditStatus_eq_unresolved' does not depend on any axioms
info: Iut/SourceTrace/Corollary312PositiveInd3NoEscapeAudit.lean:50:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalPaperPossibleImageCompactnessBoundary_iff_operational' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PositiveInd3NoEscapeAudit.lean:51:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalCommonIntegralPacketsAreCompact_implies_paperBoundary' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PositiveInd3NoEscapeAudit.lean:52:0: 'Iut.SourceClosedInvariantCarrierNoEscapeTest.escapingProfile_operationalFamily_not_relativelyCompact' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [4742/5056] Built Iut.SourceTrace.Corollary312CommonIntegralPacketCompactnessConstructorAudit (3.0s)
info: Iut/SourceTrace/Corollary312CommonIntegralPacketCompactnessConstructorAudit.lean:55:0: 'Iut.sourceForwardRelation_mem_of_adjacent' does not depend on any axioms
info: Iut/SourceTrace/Corollary312CommonIntegralPacketCompactnessConstructorAudit.lean:56:0: 'Iut.SourceTheorem311Ind3System.reachableCommonRegionFrom_subset_of_adjacentInvariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonIntegralPacketCompactnessConstructorAudit.lean:57:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalThetaHullAdjacentInvariant_implies_uniformCarrier' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonIntegralPacketCompactnessConstructorAudit.lean:58:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalPositiveInd3CompactCarrierConstructor_implies_paperBoundary' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [4743/5056] Built Iut.SourceTrace.Corollary312CrossStageNormalizedValueConstructorAudit (3.2s)
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:124:0: 'Iut.SourcePacketCofinalLogVolume.stageEmbedding_rawMeasuredTransitionMap' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:125:0: 'Iut.SourcePacketCofinalLogVolume.rawMeasuredTransitionMap_apply_eq_rawBlockMap' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:126:0: 'Iut.SourcePacketPresentedMonoAnalyticStage.FiniteEtaleTransition.hasIncreasingFieldDegree_or_hasComponentSplitting_of_rawBlockMap_not_surjective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:127:0: 'Iut.SourcePacketPresentedMonoAnalyticStage.FiniteEtaleTransition.rawBlockMap_not_surjective_of_hasComponentSplitting' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:128:0: 'Iut.SourcePacketCofinalLogVolume.increasingDegree_or_componentSplitting_of_nonSurjectiveRawBlock' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:129:0: 'Iut.SourcePacketCofinalLogVolume.increasingDegree_or_componentSplitting_of_increasingRawBlockDimension' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:130:0: 'Iut.productMeasure_eq_zero_of_closed_subsingleton_fibers' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:131:0: 'Iut.SourcePacketCofinalLogVolume.hasNullRawBlockRangeTransition_of_componentSplitting' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:132:0: 'Iut.SourcePacketCofinalLogVolume.not_rawTransitionsPreserveNormalizedValue_of_componentSplitting' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:133:0: 'Iut.haarMeasure_addSubgroup_eq_zero_of_not_isOpen' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:134:0: 'Iut.SourcePacketCofinalLogVolume.not_rawTransitionsPreserveNormalizedValue_of_measurableNonOpenNonarchimedean' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:135:0: 'Iut.SourcePacketCofinalLogVolume.not_rawTransitionsPreserveNormalizedValue_of_nonSurjectiveNonarchimedean' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:136:0: 'Iut.SourcePacketCofinalLogVolume.not_rawTransitionsPreserveNormalizedValue_of_increasingNonarchimedeanFieldDegree' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:137:0: 'Iut.SourceFiniteLocalFieldStages.exists_root_minpoly_natDegree_gt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:138:0: 'Iut.SourceFiniteLocalFieldStages.exists_stage_finrank_gt' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:139:0: 'Iut.SourceSelectedLocalLogFieldRealization.exists_stage_finrank_gt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:140:0: 'Iut.SourceMonoAnalyticLogShellAlgorithm.exists_fieldPresentationAbove_stage_finrank_gt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:141:0: 'Iut.SourcePacketCofinalLogVolume.hasIncreasingRawBlockDimensionTransition_of_unbounded' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:142:0: 'Iut.SourcePacketCofinalLogVolume.not_rawTransitionsPreserveNormalizedValue_of_increasingRawBlockDimension' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:143:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalCommonMeasuredStageSystemAt_hasIncreasingRawBlockDimensionTransition' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:144:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalCommonMeasuredStageSystemAt_not_rawTransitionsPreserveNormalizedValue' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:145:0: 'Iut.SourceCorollary312APTStepXIInput.not_canonicalCommonMeasuredRawTransitionsPreserveNormalizedValue' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:146:0: 'Iut.SourcePacketCofinalLogVolume.not_rawTransitionsPreserveNormalizedValue_of_hasSingularRawTransition' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:147:0: 'Iut.SourcePacketCofinalLogVolume.rawTransitionsPreserveNormalizedValue_iff_imageAdmissible_and_rawLog' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:148:0: 'Iut.SourcePacketCofinalLogVolume.rawTransitionsPreserveNormalizedValue_of_kummerAgreement' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:149:0: 'Iut.SourcePacketCofinalLogVolume.valuesRespectAmbientInclusion_of_rawTransitionsPreserveNormalizedValue' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CrossStageNormalizedValueConstructorAudit.lean:150:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalCommonMeasuredRawTransitionValueCompatibility_implies_ambientOrder' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [4744/5056] Built Iut.SourceTrace.Corollary312OperationalAmbientOverregionConstructorAudit (3.1s)
info: Iut/SourceTrace/Corollary312OperationalAmbientOverregionConstructorAudit.lean:51:0: 'Iut.SourceCorollary312APTStepXIInput.CanonicalThetaHullPacketImagesAreCompact' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312OperationalAmbientOverregionConstructorAudit.lean:52:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalThetaHullOperationalAmbientOverregion' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312OperationalAmbientOverregionConstructorAudit.lean:53:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalThetaHullAdjacentInvariant_and_closedImages_imply_operationalAmbientOverregions' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312OperationalAmbientOverregionConstructorAudit.lean:54:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalPackGConstructors_imply_generatedOutputAmbientUpperBound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [4745/5056] Built Iut.SourceTrace.Corollary312AdjacentSecondLogRepairClassificationAudit (3.1s)
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:79:0: 'Iut.sourceCirclePrincipalLog_sourceSecondLogUnit_eq_target' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:80:0: 'Iut.sourceCirclePrincipalLog_norm_lt_secondLog_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:81:0: 'Iut.not_all_sourceCircle_secondLogs_nonexpanding' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:82:0: 'Iut.not_all_sourceCircle_secondLogs_normalizedNonexpanding' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:83:0: 'Iut.SourceArchimedeanLogShellDefinition.principalLog_sourceSecondLogUnit_realizes_target' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:85:0: 'Iut.SourceArchimedeanLogShellDefinition.principalLog_sourceSecondLogUnit_seminorm_lt_secondLog' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:87:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalAdjacentSecondLogEndpointRegionsAreCommonIntegral' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:89:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalAdjacentSecondLogEndpointRegionsHavePointwiseMeasuredStageSupport' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:91:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalAdjacentSecondLogFiniteStageFunctional_eq' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:93:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalHullRestrictedAdjacentSecondLogMaps_iff_thetaHullInvariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:95:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalHullRestrictedAdjacentSecondLogMaps_imply_consumers' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:97:0: 'Iut.sourceAdjacentSecondLogRepairResultClass_exact' does not depend on any axioms
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:98:0: 'Iut.sourceAdjacentSecondLogRepairMissingDeclarationNames_exact' does not depend on any axioms
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:99:0: 'Iut.sourceAdjacentSecondLogRepairFollowupIssueIds_exact' does not depend on any axioms
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:100:0: 'Iut.sourceAdjacentSecondLogRepairIUTIVPremiseDeclarationNames_eq_empty' does not depend on any axioms
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:102:0: 'Iut.SourceTrace.adjacentSecondLogRepairClassificationDeclarationNames_count' does not depend on any axioms
info: Iut/SourceTrace/Corollary312AdjacentSecondLogRepairClassificationAudit.lean:104:0: 'Iut.SourceTrace.adjacentSecondLogRepairClassificationIUTIVPremiseIds_eq_empty' does not depend on any axioms
ℹ [4746/5056] Built Iut.SourceTrace.Corollary312QPilotBadSupportRegionalMapAudit (2.0s)
info: Iut/SourceTrace/Corollary312QPilotBadSupportRegionalMapAudit.lean:63:0: 'Iut.SourceCorollary312APTStepXIInput.qPilotBadPlacesOver_nonempty_of_mem_support' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotBadSupportRegionalMapAudit.lean:65:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalLocalizedQPilotObjectAt_eq_globalRestriction' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotBadSupportRegionalMapAudit.lean:67:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalQPilotBadSupportRegionalCarrierLift_of_projection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotBadSupportRegionalMapAudit.lean:69:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalQPilotBadSupportRegionalMapStatus_exact' does not depend on any axioms
ℹ [4747/5056] Built Iut.SourceTrace.Corollary312QPilotBadSupportLocalValueFormulaAudit (2.0s)
info: Iut/SourceTrace/Corollary312QPilotBadSupportLocalValueFormulaAudit.lean:55:0: 'Iut.SourceCorollary312APTStepXIInput.qPilotBadPlacesOverSignedLogVolume_eq_localDegree' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotBadSupportLocalValueFormulaAudit.lean:57:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalBadSupportProjectedQPilotCandidate_regionAt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotBadSupportLocalValueFormulaAudit.lean:59:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalQPilotBadSupportProjectionLocalValueFormula_iff_compatible' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotBadSupportLocalValueFormulaAudit.lean:61:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalQPilotBadSupportLocalRegionalRealization_of_projection_valueFormula' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotBadSupportLocalValueFormulaAudit.lean:63:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalCarrierOnlyIntegralBadSupportProjection_not_valueFormula' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotBadSupportLocalValueFormulaAudit.lean:65:0: 'Iut.SourceCorollary312APTStepXIInput.qPilotBadSupportLocalValueStatus_exact' does not depend on any axioms
ℹ [4748/5056] Built Iut.SourceTrace.Corollary312CommonStageUnramifiedIntegralComparisonAudit (3.0s)
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:84:0: 'Iut.SourceAlienCopiesExceptionalProvenance.unramifiedAbove_of_not_mem' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:86:0: 'Iut.SourceMonoAnalyticLogShellAlgorithm.actualLogShell_lattice_eq_valuationRing_of_goodPlace' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:88:0: 'Iut.SourceNonarchimedeanLocalFieldIntegers.rationalPrimeScaledAddSubgroup_ne_integerAddSubgroup' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:90:0: 'Iut.SourcePacketFiniteStageAnalyticConstruction.sourceLatticePreimage_cannot_recognize_both_rebases' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:92:0: 'Iut.SourcePacketFiniteStageAnalyticConstruction.rationalPrimeCoordinateTwist_moves_packetIntegralRegion' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:94:0: 'Iut.SourcePacketFiniteStageAnalyticConstruction.sourceLatticeReflection_not_preserved_by_primeTwist' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:96:0: 'Iut.SourcePacketMonoAnalyticStage.holomorphicIntegral_eq_monoAnalyticIntegral' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:98:0: 'Iut.SourcePacketMonoAnalyticStage.holomorphicIntegral_eq_monoAnalyticIntegral_iff_of_compatible' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:100:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalCommonStageUnramifiedLogShellRealization_implies_additiveCarrier' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:102:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalCommonHolomorphicIntegralAgreesWithMonoAnalyticOutside_of_factorwise' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:104:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalCommonHolomorphicIntegralAgreesWithMonoAnalyticOutside' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:106:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalSelectedHolomorphicIntegralAgrees_iff_commonOutside' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312CommonStageUnramifiedIntegralComparisonAudit.lean:108:0: 'Iut.sourceCommonStageUnramifiedIntegralComparisonStatus_exact' does not depend on any axioms
✔ [4749/5056] Built Iut.SourceTrace.InitialTheta11a1DifferentEquationSourceAudit (8.6s)
ℹ [4750/5056] Built Iut.SourceTrace.InitialTheta11a1ExactTateParameterAudit (3.9s)
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:43:0: Iut.SourceInitialTheta11a1TateInversionTarget.targetInverseJ_padicValuation_eq_five :
  (Iut.SourceInitialTheta11a1.rationalCompletionPadicRingEquiv
        Iut.SourceInitialTheta11a1TateInversionTarget.targetInverseJ).valuation =
    5
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:44:0: Iut.TateCurve.exists_qExpansionSum_formalReciprocalJ_eq_and_norm {target : ℚ_[11]} (ht : ‖target‖ < 1)
  (ht0 : target ≠ 0) : ∃ q, Iut.TateCurve.qExpansionSum Iut.TateCurve.formalReciprocalJ q = target ∧ ‖q‖ = ‖target‖
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:45:0: Iut.SourceInitialTheta11a1ExactTateParameter.padicTateParameter_reciprocalJ :
  Iut.TateCurve.reciprocalJ ℚ_[11] Iut.SourceInitialTheta11a1ExactTateParameter.padicTateParameter =
    Iut.SourceInitialTheta11a1ExactTateParameter.padicTarget
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:46:0: Iut.SourceInitialTheta11a1ExactTateParameter.padicTateParameter_valuation_eq_five :
  Iut.SourceInitialTheta11a1ExactTateParameter.padicTateParameter.valuation = 5
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:47:0: Iut.SourceInitialTheta11a1ExactTateParameter.padicTateParameter_canonicalIsElliptic :
  (Iut.TateCurve.weierstrassCurve ℚ_[11] Iut.SourceInitialTheta11a1ExactTateParameter.padicTateParameter).IsElliptic
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:48:0: Iut.SourceInitialTheta11a1ExactTateParameter.padicTateParameter_canonicalJ_eq_padicFixedCurve :
  (Iut.TateCurve.weierstrassCurve ℚ_[11] Iut.SourceInitialTheta11a1ExactTateParameter.padicTateParameter).j =
    Iut.SourceInitialTheta11a1ExactTateParameter.padicFixedCurve.j
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:49:0: Iut.SourceInitialTheta11a1ExactTateParameter.exists_padicVariableChange :
  ∃ C,
    C • Iut.TateCurve.weierstrassCurve ℚ_[11] Iut.SourceInitialTheta11a1ExactTateParameter.padicTateParameter =
      Iut.SourceInitialTheta11a1ExactTateParameter.padicFixedCurve
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:50:0: Iut.SourceInitialTheta11a1.rationalCompletionPadicContinuousAlgEquiv :
  Iut.SourceInitialTheta11a1.RationalCompletion ≃A[ℚ] ℚ_[11]
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:52:0: 'Iut.TateCurve.exists_qExpansionSum_formalReciprocalJ_eq_and_norm' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:53:0: 'Iut.SourceInitialTheta11a1ExactTateParameter.padicTateParameter_valuation_eq_five' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:54:0: 'Iut.SourceInitialTheta11a1ExactTateParameter.exists_padicVariableChange' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/InitialTheta11a1ExactTateParameterAudit.lean:55:0: 'Iut.SourceTrace.initialTheta11a1ExactTateParameterDeclarations_nodup' does not depend on any axioms
✔ [4751/5056] Built Iut.Foundations.SourceTateCurveTorsionKummerModule (5.5s)
✔ [4752/5056] Built Iut.Foundations.SourceInitialTheta11a1TateParameterFifthRoot (3.7s)
✔ [4754/5090] Built Iut.Foundations.SourceIUTIIIStepXIPackJThetaHullTopologyEvidence (3.8s)
⚠ [4755/5090] Built Iut.Foundations.SourceIUTIIIStepXIThetaHullPacketTopologyNoGo (17s)
warning: Iut/Foundations/SourceIUTIIIStepXIThetaHullPacketTopologyNoGo.lean:52:2: Try `simp at hx` instead of `simpa using hx`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceIUTIIIStepXIThetaHullPacketTopologyNoGo.lean:72:59: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Iut/Foundations/SourceIUTIIIStepXIThetaHullPacketTopologyNoGo.lean:73:15: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Iut/Foundations/SourceIUTIIIStepXIThetaHullPacketTopologyNoGo.lean:80:2: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
warning: Iut/Foundations/SourceIUTIIIStepXIThetaHullPacketTopologyNoGo.lean:154:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceIUTIIIStepXIThetaHullPacketTopologyNoGo.lean:212:70: remove line break in the source

This part of the code
  'factor)
   '
should be written as
  'factor)).field.carrier)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
ℹ [4756/5090] Built Iut.SourceTrace.Corollary312QPilotBadSupportHullComparisonAudit (3.0s)
info: Iut/SourceTrace/Corollary312QPilotBadSupportHullComparisonAudit.lean:63:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalProjectedQPilotBadSupportCandidate_compatible' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotBadSupportHullComparisonAudit.lean:65:0: 'Iut.SourceCorollary312APTStepXIInput.qPilotBadSupportHullComparisonRoutes_count' does not depend on any axioms
info: Iut/SourceTrace/Corollary312QPilotBadSupportHullComparisonAudit.lean:67:0: 'Iut.SourceCorollary312APTStepXIInput.qPilotBadSupportPaperNativeMissingOperations_count' does not depend on any axioms
info: Iut/SourceTrace/Corollary312QPilotBadSupportHullComparisonAudit.lean:69:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalQPilotPaperNativeHullComparison_pointwiseEndpoint' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotBadSupportHullComparisonAudit.lean:71:0: 'Iut.SourceCorollary312APTStepXIInput.qPilotBadSupportHullComparisonStatus_exact' does not depend on any axioms
✔ [4757/5090] Built Iut.Foundations.SourceIUTIIIStepXICompleteFiberOnePlaceQPilotSlices (9.1s)
ℹ [4758/5090] Built Iut.SourceTrace.Corollary312QPilotResidualExceptionalContainmentAudit (3.1s)
info: Iut/SourceTrace/Corollary312QPilotResidualExceptionalContainmentAudit.lean:66:0: 'Iut.SourceCorollary312APTStepXIInput.qPilotRationalSupport_eq_badRationalSupport' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotResidualExceptionalContainmentAudit.lean:67:0: 'Iut.SourceCorollary312APTStepXIInput.qPilotResidualExceptionalSupport_has_source_cause' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotResidualExceptionalContainmentAudit.lean:68:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalCommonHolomorphicStructureSheaf_holomorphicValue_eq_zero' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotResidualExceptionalContainmentAudit.lean:69:0: 'Iut.SourceCorollary312APTStepXIInput.residualExceptional_monoAnalyticIntegralValue_eq_zero' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312QPilotResidualExceptionalContainmentAudit.lean:70:0: 'Iut.SourceCorollary312APTStepXIInput.qPilotResidualExceptionalMissingOperations_count' does not depend on any axioms
info: Iut/SourceTrace/Corollary312QPilotResidualExceptionalContainmentAudit.lean:71:0: 'Iut.SourceCorollary312APTStepXIInput.qPilotResidualExceptionalContainmentStatus_exact' does not depend on any axioms
info: Iut/SourceTrace/Corollary312QPilotResidualExceptionalContainmentAudit.lean:72:0: 'Iut.SourceResidualExceptionalCarrierSeparation.normalizedZero_does_not_force_residualCarrierContainment' depends on axioms: [propext,
 Quot.sound]
ℹ [4759/5090] Built Iut.SourceTrace.Corollary312PaperNativeGoodPlaceHullIdentificationAudit (2.0s)
info: Iut/SourceTrace/Corollary312PaperNativeGoodPlaceHullIdentificationAudit.lean:102:0: 'Iut.SourceCorollary312APTStepXIInput.paperNativePortions_iff_canonicalFullOutputMeasuredPreimageIntegral' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperNativeGoodPlaceHullIdentificationAudit.lean:104:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalAlienCopiesSelectedFullFamilyHolomorphicRegion_subset_packetIntegralRegion' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperNativeGoodPlaceHullIdentificationAudit.lean:106:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalSelectedHolomorphicIntegral_eq_monoAnalytic_of_commonLogShellGate' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperNativeGoodPlaceHullIdentificationAudit.lean:108:0: 'Iut.SourceCorollary312APTStepXIInput.paperNativePortions_iff_canonicalOutputFamilyMeasuredPreimageIntegral' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperNativeGoodPlaceHullIdentificationAudit.lean:110:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalInd12OutputFamilyMeasuredPreimageIntegralOutside_of_repair' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperNativeGoodPlaceHullIdentificationAudit.lean:112:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalPositiveInd3OutputFamilyMeasuredPreimageIntegralOutside_of_reflection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperNativeGoodPlaceHullIdentificationAudit.lean:114:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalAlienCopiesCommonFullFamilyHull_subset_integral_of_paperNativeGate' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperNativeGoodPlaceHullIdentificationAudit.lean:116:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalPaperNativeAlienCopiesGoodPlaceHullIntegralIdentification' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperNativeGoodPlaceHullIdentificationAudit.lean:118:0: 'Iut.SourceCorollary312APTStepXIInput.SourceCanonicalPaperNativeAlienCopiesGoodPlaceHullIntegralIdentification.labelwiseFiniteSupport' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PaperNativeGoodPlaceHullIdentificationAudit.lean:120:0: 'Iut.sourcePaperNativeGoodPlaceHullIdentificationStatus_exact' does not depend on any axioms
✔ [4760/5090] Built Iut.Foundations.SourceIUTIIIStepXIThetaPilotBaseNormalizationRepair (16s)
✔ [4761/5090] Built Iut.Foundations.SourceIUTIIIStepXIPackHLabelwiseFiniteSupportEvidence (4.3s)
✔ [4762/5090] Built Iut.Foundations.SourceIUTIIIStepXIGlobalArithmeticVectorBundleLocalization (5.3s)
✔ [4763/5090] Built Iut.Foundations.SourceIUTIIIStepXIFiniteEtaleTensorCoordinateIntegralReflection (5.0s)
ℹ [4764/5090] Built Iut.SourceTrace.Corollary312FourFrontHypothesisLaboratoryAudit (2.0s)
info: Iut/SourceTrace/Corollary312FourFrontHypothesisLaboratoryAudit.lean:98:0: 'Iut.stepXILaboratoryAbstractIndependenceMatrix_exact' does not depend on any axioms
info: Iut/SourceTrace/Corollary312FourFrontHypothesisLaboratoryAudit.lean:99:0: 'Iut.SourceCorollary312APTStepXIInput.StepXIPackDTopologyHypotheses.ofCommonIntegralPacketCompactness' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312FourFrontHypothesisLaboratoryAudit.lean:100:0: 'Iut.SourceCorollary312APTStepXIInput.StepXIPackDAmbientMeasurementHypotheses.generatedOutputUpperBound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312FourFrontHypothesisLaboratoryAudit.lean:101:0: 'Iut.SourceCorollary312APTStepXIInput.StepXIPackEIntegralHypotheses.labelwiseFiniteSupport' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312FourFrontHypothesisLaboratoryAudit.lean:102:0: 'Iut.SourceCorollary312APTStepXIInput.StepXIPackFHullContainmentHypotheses.recognition' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312FourFrontHypothesisLaboratoryAudit.lean:103:0: 'Iut.SourceCorollary312APTStepXIInput.StepXIFourFrontHypotheses.fullFamilyOpenPropositions' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312FourFrontHypothesisLaboratoryAudit.lean:104:0: 'Iut.SourceCorollary312APTStepXIInput.StepXIFourFrontHypotheses.paperNativeUpperRayResult' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312FourFrontHypothesisLaboratoryAudit.lean:105:0: 'Iut.SourceCorollary312APTStepXIInput.stepXILaboratory_closedInvariantCarrier_not_sufficient' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312FourFrontHypothesisLaboratoryAudit.lean:106:0: 'Iut.SourceCorollary312APTStepXIInput.stepXILaboratory_goodAndQSupport_not_exhaustive' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
✔ [4765/5090] Built Iut.Foundations.SourceIUTIIIStepXIPostLaboratoryTerminalClassification (3.7s)
ℹ [4766/5090] Built Iut.SourceTrace.Corollary312PackGTopologyAmbientMeasurementEvidenceAudit (2.9s)
info: Iut/SourceTrace/Corollary312PackGTopologyAmbientMeasurementEvidenceAudit.lean:67:0: 'Iut.sourcePackGRepositoryEvidenceStatuses_exact' does not depend on any axioms
info: Iut/SourceTrace/Corollary312PackGTopologyAmbientMeasurementEvidenceAudit.lean:68:0: 'Iut.sourcePackGRepositoryEvidenceOwners_exact' does not depend on any axioms
info: Iut/SourceTrace/Corollary312PackGTopologyAmbientMeasurementEvidenceAudit.lean:69:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalPackGAmbientMeasurementConstructor_implies_overregions_and_order' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PackGTopologyAmbientMeasurementEvidenceAudit.lean:71:0: 'Iut.SourceCorollary312APTStepXIInput.canonicalPackGAmbientMeasurementConstructor_implies_generatedOutputUpperBound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Iut/SourceTrace/Corollary312PackGTopologyAmbientMeasurementEvidenceAudit.lean:73:0: 'Iut.SourceTrace.packGConstructorIssueIds_exact' does not depend on any axioms
info: Iut/SourceTrace/Corollary312PackGTopologyAmbientMeasurementEvidenceAudit.lean:74:0: 'Iut.SourceTrace.packGTopologyAmbientMeasurementIUTIVPremiseIds_eq_empty' does not depend on any axioms
✔ [4768/5090] Built Iut.SourceTrace.IUTIVLogShellHullVolumeSourceMatrix (3.3s)
⚠ [4769/5090] Built Iut.Foundations.SourceInitialTheta11a1CompletePacketAdapter (64s)
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:132:0: automatically included section variable(s) unused in theorem `Iut.SourceInitialTheta11a1CompletePacketAdapter.tateRoot_parameter_square`:
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:147:0: automatically included section variable(s) unused in theorem `Iut.SourceInitialTheta11a1CompletePacketAdapter.kummerCharacter_qPilot_square`:
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:155:0: automatically included section variable(s) unused in theorem `Iut.SourceInitialTheta11a1CompletePacketAdapter.canonical_selectedFPlace_eq`:
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:162:0: automatically included section variable(s) unused in theorem `Iut.SourceInitialTheta11a1CompletePacketAdapter.canonical_selectedFQParameter_eq`:
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:171:0: automatically included section variable(s) unused in theorem `Iut.SourceInitialTheta11a1CompletePacketAdapter.canonicalBadPlace_residuePrime_eq_eleven`:
  [SourceSelectedPlaceFiberFiniteness (SourceInitialTheta11a1.CertifiedPresentation.toCore presentation)]
  [SourceSelectedBadPlaceFiniteness (SourceInitialTheta11a1.CertifiedPresentation.toCore presentation)]
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceSelectedPlaceFiberFiniteness
  (SourceInitialTheta11a1.CertifiedPresentation.toCore
    presentation)] [SourceSelectedBadPlaceFiniteness
  (SourceInitialTheta11a1.CertifiedPresentation.toCore
    presentation)] [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:236:0: automatically included section variable(s) unused in theorem `Iut.SourceInitialTheta11a1CompletePacketAdapter.TateKummerProvenanceBoundary.localKummerCharacter_coordinate`:
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:312:0: automatically included section variable(s) unused in theorem `Iut.SourceInitialTheta11a1CompletePacketAdapter.AllSummandLogShellProvenance.completeFiberPlace_surjective`:
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:334:0: automatically included section variable(s) unused in theorem `Iut.SourceInitialTheta11a1CompletePacketAdapter.AllSummandLogShellProvenance.packetShells_eq_selected`:
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:428:0: automatically included section variable(s) unused in theorem `Iut.SourceInitialTheta11a1CompletePacketAdapter.PartialMeasuredLogShellBoundary.admissibleShellRegion_carrier`:
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:454:0: automatically included section variable(s) unused in theorem `Iut.SourceInitialTheta11a1CompletePacketAdapter.PartialMeasuredLogShellBoundary.DirectProductDilationBoundary.valueOn_dilatedPacketAdmissibleRegion`:
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:483:7: unused variable `place`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:484:7: unused variable `label`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceInitialTheta11a1CompletePacketAdapter.lean:518:0: automatically included section variable(s) unused in theorem `Iut.SourceInitialTheta11a1CompletePacketAdapter.ResidueProperDilationBoundary.primeDilation_image_ne_univ`:
  [SourceInitialThetaRamificationFiniteness K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SourceInitialThetaRamificationFiniteness K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
✔ [4770/5090] Built Iut.Foundations.SourceGenuineLogShellOrbitRadiusAdapter (3.9s)
✔ [4771/5090] Built Iut.Foundations.SourceIUTIIIStepXIPositiveInd3FiniteStageMajorant (3.2s)
✔ [4773/5090] Built Iut.Foundations.SourceIUTIIIStepXIArchAdjacentSecondLogFixedMaximizerEstimate (5.9s)
✔ [4774/5090] Built Iut.Foundations.SourceIUTIIIStepXINonarchAdjacentSecondLogFixedMaximizerEstimate (5.0s)

/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1679-runtime-lean_checker-3083124-1787103914498581526-1 on attempt 1

lake build :blueprint

error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1679-runtime-blueprint_build-3083124-1787111115441091239-2	925696	1433600	21474836480	0	0	0	0	0	0	102223872	205553664	21474836480	0	0	0	0	0	0