Verification run

Run 1186

promachina/iut-leanbranch mastertriggered via manual

failedcommit 5c48653111f4toolchain lean-v4-30-0prover leantook 38m 36s · finished 7w ago

lake build failed with exit code 1 (toolchain lean-v4-30-0, command: elan run leanprover/lean4:v4.30.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase lake build)

Open project

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

(no log excerpt)

Command runs

git_cloneexit 0duration 4s · created 7/24/2026, 9:46:19 PM

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

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

git_checkoutexit 0duration 200 ms · created 7/24/2026, 9:46:19 PM

git checkout 5c48653111f44f835827f76e22f4eaf9cf9c1b8f

Note: switching to '5c48653111f44f835827f76e22f4eaf9cf9c1b8f'.

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 5c48653 Complete connected finite-etale basepoint converse

lake_cacheexit 0duration 1m 28s · created 7/24/2026, 9:46:19 PM

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)

✔ [7/25] Built Cache.Lean (467ms)
✔ [9/25] Built Cache.Lean:c.o (1.4s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (112ms)
✔ [12/25] Built Batteries.Data.Array.Match:c.o (212ms)
✔ [13/25] Built Cache.Init (370ms)
✔ [15/25] Built Cache.IO (2.5s)
✔ [16/25] Built Cache.Init:c.o (74ms)
✔ [17/25] Built Cache.IO:c.o (1.1s)
✔ [18/25] Built Batteries.Data.String.Matcher:c.o (155ms)
✔ [19/25] Built Cache.Hashing (986ms)
✔ [20/25] Built Cache.Hashing:c.o (354ms)
✔ [21/25] Built Cache.Requests (2.3s)
✔ [22/25] Built Cache.Requests:c.o (1.7s)
✔ [23/25] Built Cache.Main (1.1s)
✔ [24/25] Built Cache.Main:c.o (500ms)
✔ [25/25] Built cache:exe (4.0s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 5 KB/s], Decompressed: 13
Downloaded: 41 file(s) [attempted 41/8459 = 0%, 121 KB/s], Decompressed: 29
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 98 KB/s], Decompressed: 58
Downloaded: 96 file(s) [attempted 96/8459 = 1%, 76 KB/s], Decompressed: 82
Downloaded: 131 file(s) [attempted 131/8459 = 1%, 490 KB/s], Decompressed: 120
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 72 KB/s], Decompressed: 148
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 173 KB/s], Decompressed: 179
Downloaded: 233 file(s) [attempted 233/8459 = 2%, 212 KB/s], Decompressed: 216
Downloaded: 271 file(s) [attempted 271/8459 = 3%, 157 KB/s], Decompressed: 233
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 498 KB/s], Decompressed: 278
Downloaded: 346 file(s) [attempted 346/8459 = 4%, 23 KB/s], Decompressed: 302
Downloaded: 387 file(s) [attempted 387/8459 = 4%, 215 KB/s], Decompressed: 360
Downloaded: 422 file(s) [attempted 422/8459 = 4%, 285 KB/s], Decompressed: 387
Downloaded: 463 file(s) [attempted 463/8459 = 5%, 866 KB/s], Decompressed: 432
Downloaded: 507 file(s) [attempted 507/8459 = 5%, 228 KB/s], Decompressed: 459
Downloaded: 545 file(s) [attempted 545/8459 = 6%, 194 KB/s], Decompressed: 511
Downloaded: 583 file(s) [attempted 583/8459 = 6%, 764 KB/s], Decompressed: 538
Downloaded: 624 file(s) [attempted 624/8459 = 7%, 160 KB/s], Decompressed: 562
Downloaded: 661 file(s) [attempted 661/8459 = 7%, 153 KB/s], Decompressed: 627
Downloaded: 706 file(s) [attempted 706/8459 = 8%, 81 KB/s], Decompressed: 655
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 233 KB/s], Decompressed: 709
Downloaded: 788 file(s) [attempted 788/8459 = 9%, 349 KB/s], Decompressed: 751
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 118 KB/s], Decompressed: 809
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 146 KB/s], Decompressed: 846
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 630 KB/s], Decompressed: 888
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 181 KB/s], Decompressed: 925
Downloaded: 990 file(s) [attempted 990/8459 = 11%, 224 KB/s], Decompressed: 963
Downloaded: 1028 file(s) [attempted 1028/8459 = 12%, 297 KB/s], Decompressed: 983
Downloaded: 1066 file(s) [attempted 1066/8459 = 12%, 184 KB/s], Decompressed: 1007
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 409 KB/s], Decompressed: 1038
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 359 KB/s], Decompressed: 1076
Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 534 KB/s], Decompressed: 1114
Downloaded: 1233 file(s) [attempted 1233/8459 = 14%, 453 KB/s], Decompressed: 1158
Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 91 KB/s], Decompressed: 1158
Downloaded: 1312 file(s) [attempted 1312/8459 = 15%, 780 KB/s], Decompressed: 1213
Downloaded: 1357 file(s) [attempted 1357/8459 = 16%, 618 KB/s], Decompressed: 1213
Downloaded: 1394 file(s) [attempted 1394/8459 = 16%, 43 KB/s], Decompressed: 1288
Downloaded: 1435 file(s) [attempted 1435/8459 = 16%, 675 KB/s], Decompressed: 1288
Downloaded: 1476 file(s) [attempted 1476/8459 = 17%, 338 KB/s], Decompressed: 1380
Downloaded: 1514 file(s) [attempted 1514/8459 = 17%, 244 KB/s], Decompressed: 1380
Downloaded: 1555 file(s) [attempted 1555/8459 = 18%, 101 KB/s], Decompressed: 1380
Downloaded: 1596 file(s) [attempted 1596/8459 = 18%, 274 KB/s], Decompressed: 1476
Downloaded: 1637 file(s) [attempted 1637/8459 = 19%, 28 KB/s], Decompressed: 1476
Downloaded: 1675 file(s) [attempted 1675/8459 = 19%, 116 KB/s], Decompressed: 1476
Downloaded: 1719 file(s) [attempted 1719/8459 = 20%, 554 KB/s], Decompressed: 1576
Downloaded: 1754 file(s) [attempted 1754/8459 = 20%, 193 KB/s], Decompressed: 1576
Downloaded: 1798 file(s) [attempted 1798/8459 = 21%, 180 KB/s], Decompressed: 1685
Downloaded: 1832 file(s) [attempted 1832/8459 = 21%, 47 KB/s], Decompressed: 1685
Downloaded: 1870 file(s) [attempted 1870/8459 = 22%, 219 KB/s], Decompressed: 1685
Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 227 KB/s], Decompressed: 1788
Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 146 KB/s], Decompressed: 1788
Downloaded: 1983 file(s) [attempted 1983/8459 = 23%, 118 KB/s], Decompressed: 1880
Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 790 KB/s], Decompressed: 1880
Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 127 KB/s], Decompressed: 1880
Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 336 KB/s], Decompressed: 1969
Downloaded: 2140 file(s) [attempted 2140/8459 = 25%, 22 KB/s], Decompressed: 1969
Downloaded: 2181 file(s) [attempted 2181/8459 = 25%, 559 KB/s], Decompressed: 2072
Downloaded: 2229 file(s) [attempted 2229/8459 = 26%, 111 KB/s], Decompressed: 2072
Downloaded: 2277 file(s) [attempted 2277/8459 = 26%, 138 KB/s], Decompressed: 2168
Downloaded: 2327 file(s) [attempted 2327/8459 = 27%, 38 KB/s], Decompressed: 2168
Downloaded: 2359 file(s) [attempted 2359/8459 = 27%, 326 KB/s], Decompressed: 2168
Downloaded: 2393 file(s) [attempted 2393/8459 = 28%, 88 KB/s], Decompressed: 2270
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 589 KB/s], Decompressed: 2270
Downloaded: 2476 file(s) [attempted 2476/8459 = 29%, 1765 KB/s], Decompressed: 2270
Downloaded: 2520 file(s) [attempted 2520/8459 = 29%, 81 KB/s], Decompressed: 2373
Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 1253 KB/s], Decompressed: 2373
Downloaded: 2599 file(s) [attempted 2599/8459 = 30%, 539 KB/s], Decompressed: 2373
Downloaded: 2633 file(s) [attempted 2633/8459 = 31%, 328 KB/s], Decompressed: 2479
Downloaded: 2678 file(s) [attempted 2678/8459 = 31%, 606 KB/s], Decompressed: 2479
Downloaded: 2719 file(s) [attempted 2719/8459 = 32%, 104 KB/s], Decompressed: 2479
Downloaded: 2760 file(s) [attempted 2760/8459 = 32%, 2744 KB/s], Decompressed: 2602
Downloaded: 2801 file(s) [attempted 2801/8459 = 33%, 131 KB/s], Decompressed: 2602
Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 264 KB/s], Decompressed: 2602
Downloaded: 2879 file(s) [attempted 2879/8459 = 34%, 701 KB/s], Decompressed: 2732
Downloaded: 2921 file(s) [attempted 2921/8459 = 34%, 575 KB/s], Decompressed: 2732
Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 1222 KB/s], Decompressed: 2732
Downloaded: 2999 file(s) [attempted 2999/8459 = 35%, 101 KB/s], Decompressed: 2732
Downloaded: 3044 file(s) [attempted 3044/8459 = 35%, 271 KB/s], Decompressed: 2869
Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 512 KB/s], Decompressed: 2869
Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 233 KB/s], Decompressed: 2869
Downloaded: 3157 file(s) [attempted 3157/8459 = 37%, 318 KB/s], Decompressed: 2869
Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 24 KB/s], Decompressed: 2869
Downloaded: 3235 file(s) [attempted 3235/8459 = 38%, 208 KB/s], Decompressed: 3023
Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 65 KB/s], Decompressed: 3023
Downloaded: 3307 file(s) [attempted 3307/8459 = 39%, 142 KB/s], Decompressed: 3023
Downloaded: 3348 file(s) [attempted 3348/8459 = 39%, 55 KB/s], Decompressed: 3023
Downloaded: 3389 file(s) [attempted 3389/8459 = 40%, 43 KB/s], Decompressed: 3023
Downloaded: 3430 file(s) [attempted 3430/8459 = 40%, 115 KB/s], Decompressed: 3023
Downloaded: 3468 file(s) [attempted 3468/8459 = 40%, 406 KB/s], Decompressed: 3023
Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 24 KB/s], Decompressed: 3211
Downloaded: 3550 file(s) [attempted 3550/8459 = 41%, 239 KB/s], Decompressed: 3211
Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 559 KB/s], Decompressed: 3211
Downloaded: 3632 file(s) [attempted 3632/8459 = 42%, 56 KB/s], Decompressed: 3211
Downloaded: 3673 file(s) [attempted 3673/8459 = 43%, 105 KB/s], Decompressed: 3211
Downloaded: 3715 file(s) [attempted 3715/8459 = 43%, 63 KB/s], Decompressed: 3211
Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 615 KB/s], Decompressed: 3211
Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 364 KB/s], Decompressed: 3211
Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 122 KB/s], Decompressed: 3211
Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 257 KB/s], Decompressed: 3211
Downloaded: 3910 file(s) [attempted 3910/8459 = 46%, 607 KB/s], Decompressed: 3478
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 373 KB/s], Decompressed: 3478
Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 126 KB/s], Decompressed: 3478
Downloaded: 4029 file(s) [attempted 4029/8459 = 47%, 103 KB/s], Decompressed: 3478
Downloaded: 4070 file(s) [attempted 4070/8459 = 48%, 289 KB/s], Decompressed: 3478
Downloaded: 4112 file(s) [attempted 4112/8459 = 48%, 36 KB/s], Decompressed: 3478
Downloaded: 4153 file(s) [attempted 4153/8459 = 49%, 43 KB/s], Decompressed: 3478
Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 394 KB/s], Decompressed: 3478
Downloaded: 4235 file(s) [attempted 4235/8459 = 50%, 83 KB/s], Decompressed: 3478
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 546 KB/s], Decompressed: 3478
Downloaded: 4313 file(s) [attempted 4313/8459 = 50%, 362 KB/s], Decompressed: 3478
Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 588 KB/s], Decompressed: 3478
Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 36 KB/s], Decompressed: 3478
Downloaded: 4437 file(s) [attempted 4437/8459 = 52%, 100 KB/s], Decompressed: 3910
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 50 KB/s], Decompressed: 3910
Downloaded: 4515 file(s) [attempted 4515/8459 = 53%, 243 KB/s], Decompressed: 3910
Downloaded: 4560 file(s) [attempted 4560/8459 = 53%, 508 KB/s], Decompressed: 3910
Downloaded: 4604 file(s) [attempted 4604/8459 = 54%, 159 KB/s], Decompressed: 3910
Downloaded: 4645 file(s) [attempted 4645/8459 = 54%, 306 KB/s], Decompressed: 3910
Downloaded: 4680 file(s) [attempted 4680/8459 = 55%, 66 KB/s], Decompressed: 3910
Downloaded: 4724 file(s) [attempted 4724/8459 = 55%, 1326 KB/s], Decompressed: 3910
Downloaded: 4772 file(s) [attempted 4772/8459 = 56%, 472 KB/s], Decompressed: 3910
Downloaded: 4810 file(s) [attempted 4810/8459 = 56%, 503 KB/s], Decompressed: 3910
Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 62 KB/s], Decompressed: 3910
Downloaded: 4892 file(s) [attempted 4892/8459 = 57%, 120 KB/s], Decompressed: 3910
Downloaded: 4929 file(s) [attempted 4929/8459 = 58%, 135 KB/s], Decompressed: 3910
Downloaded: 4971 file(s) [attempted 4971/8459 = 58%, 156 KB/s], Decompressed: 4413
Downloaded: 5018 file(s) [attempted 5018/8459 = 59%, 1462 KB/s], Decompressed: 4413
Downloaded: 5053 file(s) [attempted 5053/8459 = 59%, 207 KB/s], Decompressed: 4413
Downloaded: 5090 file(s) [attempted 5090/8459 = 60%, 200 KB/s], Decompressed: 4413
Downloaded: 5135 file(s) [attempted 5135/8459 = 60%, 33 KB/s], Decompressed: 4413
Downloaded: 5176 file(s) [attempted 5176/8459 = 61%, 665 KB/s], Decompressed: 4413
Downloaded: 5214 file(s) [attempted 5214/8459 = 61%, 448 KB/s], Decompressed: 4413
Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 90 KB/s], Decompressed: 4413
Downloaded: 5289 file(s) [attempted 5289/8459 = 62%, 152 KB/s], Decompressed: 4413
Downloaded: 5333 file(s) [attempted 5333/8459 = 63%, 200 KB/s], Decompressed: 4413
Downloaded: 5374 file(s) [attempted 5374/8459 = 63%, 173 KB/s], Decompressed: 4413
Downloaded: 5415 file(s) [attempted 5415/8459 = 64%, 311 KB/s], Decompressed: 4413
Downloaded: 5457 file(s) [attempted 5457/8459 = 64%, 290 KB/s], Decompressed: 4413
Downloaded: 5494 file(s) [attempted 5494/8459 = 64%, 237 KB/s], Decompressed: 4413
Downloaded: 5535 file(s) [attempted 5535/8459 = 65%, 226 KB/s], Decompressed: 4413
Downloaded: 5580 file(s) [attempted 5580/8459 = 65%, 38 KB/s], Decompressed: 4413
Downloaded: 5621 file(s) [attempted 5621/8459 = 66%, 300 KB/s], Decompressed: 4936
Downloaded: 5658 file(s) [attempted 5658/8459 = 66%, 173 KB/s], Decompressed: 4936
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 113 KB/s], Decompressed: 4936
Downloaded: 5741 file(s) [attempted 5741/8459 = 67%, 207 KB/s], Decompressed: 4936
Downloaded: 5785 file(s) [attempted 5785/8459 = 68%, 959 KB/s], Decompressed: 4936
Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 104 KB/s], Decompressed: 4936
Downloaded: 5867 file(s) [attempted 5867/8459 = 69%, 163 KB/s], Decompressed: 4936
Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 1900 KB/s], Decompressed: 4936
Downloaded: 5949 file(s) [attempted 5949/8459 = 70%, 74 KB/s], Decompressed: 4936
Downloaded: 5987 file(s) [attempted 5987/8459 = 70%, 563 KB/s], Decompressed: 4936
Downloaded: 6028 file(s) [attempted 6028/8459 = 71%, 318 KB/s], Decompressed: 4936
Downloaded: 6066 file(s) [attempted 6066/8459 = 71%, 494 KB/s], Decompressed: 4936
Downloaded: 6107 file(s) [attempted 6107/8459 = 72%, 312 KB/s], Decompressed: 4936
Downloaded: 6148 file(s) [attempted 6148/8459 = 72%, 348 KB/s], Decompressed: 4936
Downloaded: 6192 file(s) [attempted 6192/8459 = 73%, 446 KB/s], Decompressed: 4936
Downloaded: 6233 file(s) [attempted 6233/8459 = 73%, 138 KB/s], Decompressed: 5593
Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 86 KB/s], Decompressed: 5593
Downloaded: 6305 file(s) [attempted 6305/8459 = 74%, 352 KB/s], Decompressed: 5593
Downloaded: 6346 file(s) [attempted 6346/8459 = 75%, 389 KB/s], Decompressed: 5593
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 364 KB/s], Decompressed: 5593
Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 152 KB/s], Decompressed: 5593
Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 1842 KB/s], Decompressed: 5593
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 76 KB/s], Decompressed: 5593
Downloaded: 6545 file(s) [attempted 6545/8459 = 77%, 54 KB/s], Decompressed: 5593
Downloaded: 6589 file(s) [attempted 6589/8459 = 77%, 980 KB/s], Decompressed: 5593
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 360 KB/s], Decompressed: 5593
Downloaded: 6675 file(s) [attempted 6675/8459 = 78%, 138 KB/s], Decompressed: 5593
Downloaded: 6709 file(s) [attempted 6709/8459 = 79%, 73 KB/s], Decompressed: 5593
Downloaded: 6750 file(s) [attempted 6750/8459 = 79%, 146 KB/s], Decompressed: 5593
Downloaded: 6791 file(s) [attempted 6791/8459 = 80%, 73 KB/s], Decompressed: 5593
Downloaded: 6836 file(s) [attempted 6836/8459 = 80%, 275 KB/s], Decompressed: 5593
Downloaded: 6877 file(s) [attempted 6877/8459 = 81%, 622 KB/s], Decompressed: 6223
Downloaded: 6918 file(s) [attempted 6918/8459 = 81%, 117 KB/s], Decompressed: 6223
Downloaded: 6956 file(s) [attempted 6956/8459 = 82%, 175 KB/s], Decompressed: 6223
Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 124 KB/s], Decompressed: 6223
Downloaded: 7034 file(s) [attempted 7034/8459 = 83%, 81 KB/s], Decompressed: 6223
Downloaded: 7075 file(s) [attempted 7075/8459 = 83%, 187 KB/s], Decompressed: 6223
Downloaded: 7116 file(s) [attempted 7116/8459 = 84%, 272 KB/s], Decompressed: 6223
Downloaded: 7161 file(s) [attempted 7161/8459 = 84%, 1553 KB/s], Decompressed: 6223
Downloaded: 7198 file(s) [attempted 7198/8459 = 85%, 194 KB/s], Decompressed: 6223
Downloaded: 7233 file(s) [attempted 7233/8459 = 85%, 1029 KB/s], Decompressed: 6223
Downloaded: 7267 file(s) [attempted 7267/8459 = 85%, 581 KB/s], Decompressed: 6223
Downloaded: 7308 file(s) [attempted 7308/8459 = 86%, 35 KB/s], Decompressed: 6223
Downloaded: 7349 file(s) [attempted 7349/8459 = 86%, 108 KB/s], Decompressed: 6223
Downloaded: 7394 file(s) [attempted 7394/8459 = 87%, 459 KB/s], Decompressed: 6223
Downloaded: 7428 file(s) [attempted 7428/8459 = 87%, 99 KB/s], Decompressed: 6223
Downloaded: 7462 file(s) [attempted 7462/8459 = 88%, 946 KB/s], Decompressed: 6223
Downloaded: 7507 file(s) [attempted 7507/8459 = 88%, 82 KB/s], Decompressed: 6223
Downloaded: 7548 file(s) [attempted 7548/8459 = 89%, 620 KB/s], Decompressed: 6223
Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 153 KB/s], Decompressed: 6223
Downloaded: 7623 file(s) [attempted 7623/8459 = 90%, 99 KB/s], Decompressed: 6843
Downloaded: 7660 file(s) [attempted 7660/8459 = 90%, 138 KB/s], Decompressed: 6843
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 186 KB/s], Decompressed: 6843
Downloaded: 7746 file(s) [attempted 7746/8459 = 91%, 477 KB/s], Decompressed: 6843
Downloaded: 7791 file(s) [attempted 7791/8459 = 92%, 853 KB/s], Decompressed: 6843
Downloaded: 7828 file(s) [attempted 7828/8459 = 92%, 824 KB/s], Decompressed: 6843
Downloaded: 7862 file(s) [attempted 7862/8459 = 92%, 90 KB/s], Decompressed: 6843
Downloaded: 7903 file(s) [attempted 7903/8459 = 93%, 620 KB/s], Decompressed: 6843
Downloaded: 7945 file(s) [attempted 7945/8459 = 93%, 227 KB/s], Decompressed: 6843
Downloaded: 7986 file(s) [attempted 7986/8459 = 94%, 322 KB/s], Decompressed: 6843
Downloaded: 8023 file(s) [attempted 8023/8459 = 94%, 193 KB/s], Decompressed: 6843
Downloaded: 8064 file(s) [attempted 8064/8459 = 95%, 123 KB/s], Decompressed: 6843
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 594 KB/s], Decompressed: 6843
Downloaded: 8143 file(s) [attempted 8143/8459 = 96%, 160 KB/s], Decompressed: 6843
Downloaded: 8184 file(s) [attempted 8184/8459 = 96%, 1232 KB/s], Decompressed: 6843
Downloaded: 8225 file(s) [attempted 8225/8459 = 97%, 179 KB/s], Decompressed: 6843
Downloaded: 8266 file(s) [attempted 8266/8459 = 97%, 129 KB/s], Decompressed: 6843
Downloaded: 8307 file(s) [attempted 8307/8459 = 98%, 60 KB/s], Decompressed: 6843
Downloaded: 8342 file(s) [attempted 8342/8459 = 98%, 801 KB/s], Decompressed: 6843
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 326 KB/s], Decompressed: 6843
Downloaded: 8427 file(s) [attempted 8427/8459 = 99%, 254 KB/s], Decompressed: 7602
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 113 KB/s], Decompressed: 7602
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 113 KB/s], Decompressed: 7602

apx-runtime-resource-v1	apx-verifier-job-1495-runtime-lake_cache-1073315-1784927275159756372-0	925696	1155072	4026531840	0	0	0	0	0	0	3755253760	4027232256	4026531840	0	0	701	0	0	0

lean_checkerexit 1duration 36m 40s · created 7/24/2026, 9:46:19 PM

lake build

✔ [1/19] Built Iut.Foundations.Species (604ms)
✔ [753/760] Built Iut.Foundations.RealLineCopy (26s)
✔ [754/760] Built Iut.Foundations.TransportDiagram (1.9s)
✔ [755/760] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [756/760] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [757/760] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [758/760] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [759/781] Built Iut.Foundations.QualitativeData (2.1s)
✔ [3505/3510] Built Iut.Foundations.EtaleThetaQuotient (33s)
✔ [3506/3510] Built Iut.Foundations.Orbicurve (29s)
✔ [3953/3956] Built Iut.Foundations.InitialThetaData (28s)
✔ [3962/3973] Built Iut.Foundations.OrbicurvePullback (7.0s)
✔ [3964/3973] Built Iut.Foundations.EtaleThetaCovers (4.5s)
✔ [3967/3974] Built Iut.Foundations.SourceSemiGraph (1.9s)
✔ [3968/3974] Built Iut.Foundations.SourceSemiGraphAction (2.4s)
✔ [3969/3974] Built Iut.Foundations.SourceInitialThetaData (40s)
✔ [3971/3974] Built Iut.Foundations.SourceSemiGraphOfSubgroups (9.0s)
✔ [3972/3974] Built Iut.Foundations.SourceProfiniteCosetSystem (4.5s)
✔ [3973/3984] Built Iut.Foundations.SourceProfiniteSemiGraphSystem (76s)
✔ [4007/4011] Built Iut.Foundations.KummerFaithfulness (2.6s)
✔ [4008/4012] Built Iut.Foundations.SourceTemperedSemigraph (5.3s)
✔ [4009/4013] Built Iut.Foundations.SourceMonoThetaEnvironment (35s)
✔ [4011/4023] Built Iut.Foundations.ContinuousH1 (6.4s)
✔ [4019/4027] Built Iut.Foundations.Procession (2.5s)
✔ [4023/4027] Built Iut.Foundations.SourceMLFKummerFaithfulness (3.1s)
✔ [4024/4027] Built Iut.Foundations.Frobenioid (5.9s)
✔ [4025/4030] Built Iut.Foundations.SourceThetaHodgeTheater (22s)
✔ [4026/4041] Built Iut.Foundations.SourceProcession (11s)
✔ [4038/4057] Built Iut.Foundations.SourceModelFrobenioid (5.4s)
✔ [4045/4062] Built Iut.Foundations.SourceAnabelioid (4.4s)
⚠ [4049/4065] Built Iut.Foundations.SourceThetaEvaluation (64s)
warning: Iut/Foundations/SourceThetaEvaluation.lean:1780:0: automatically included section variable(s) unused in theorem `Iut.SourceMLFIntegralMonoid.algebraicClosure_isFractionRing`:
  [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
  [CharZero K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] in theorem ...

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

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

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:1973:10: Try `simp at underlying` instead of `simpa using underlying`

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

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:2344:0: automatically included section variable(s) unused in theorem `Iut.SourceMLFIntegralMonoid.unitToAlgebraicClosureUnit_injective`:
  [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
  [CharZero K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] in theorem ...

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

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:5486:0: automatically included section variable(s) unused in theorem `Iut.SourceMLFGaloisTMPair.KummerRootTheory.chosen_rootSystem`:
  [IsMulCommutative A]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [IsMulCommutative A] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:5732:0: automatically included section variable(s) unused in theorem `Iut.SourceMLFGaloisTMPair.LocalKummerRootTheory.chosen_rootSystem`:
  [IsMulCommutative A]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [IsMulCommutative A] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
✔ [4051/4066] Built Iut.Foundations.SourceTopologicalActionPairCategory (8.9s)
✔ [4052/4066] Built Iut.Foundations.SourceConjugateSynchronization (4.2s)
✔ [4053/4066] Built Iut.Foundations.SourceThetaSplitting (6.7s)
✔ [4054/4075] Built Iut.Foundations.SourceSplitKummerFrobenioid (8.1s)
✔ [4058/4075] Built Iut.Foundations.SourceHodgeArakelovEvaluation (3.0s)
✔ [4059/4075] Built Iut.Foundations.SourceArchimedeanKummerSystem (5.7s)
✔ [4061/4075] Built Iut.Foundations.SourceAnabelioidEquivalence (3.1s)
✔ [4062/4075] Built Iut.Foundations.SourceSemiGraphOfAnabelioids (3.2s)
✔ [4064/4075] Built Iut.Foundations.SourceAutHolomorphic (2.8s)
✔ [4065/4075] Built Iut.Foundations.SourceTimesMuPrimeStrip (9.9s)
✔ [4067/4075] Built Iut.Foundations.SourceTimesMuPrimeStripIsomorphism (17s)
✔ [4068/4075] Built Iut.Foundations.SourceContinuousAnabelioid (7.6s)
✔ [4069/4078] Built Iut.Foundations.SourceTimesMuPrimeStripFullPolyIsomorphism (8.8s)
✔ [4070/4078] Built Iut.Foundations.SourceAnabelioidSlice (17s)
✔ [4071/4081] Built Iut.Foundations.SourceTimesMuReconstructionAlgorithm (8.1s)
✔ [4073/4082] Built Iut.Foundations.SourceAnabelioidComponents (7.6s)
✔ [4075/4085] Built Iut.Foundations.SourceConnectedAnabelioidSlice (4.0s)
✔ [4079/4085] Built Iut.Foundations.SourceConnectedFiniteEtaleConverse (4.7s)
✔ [4086/4094] Built Iut.Foundations.SourceArchimedeanSemiGerm (3.3s)
✔ [4088/4095] Built Iut.Foundations.SourceFThetaBridge (3.0s)
✔ [4089/4096] Built Iut.Foundations.SourceTopologicalPseudoMonoid (4.6s)
✔ [4095/4099] Built Iut.Foundations.SourceAutHolomorphicRigidity (2.9s)
✔ [4143/4182] Built Iut.Foundations.ThetaHodgeTheater (7.4s)
✔ [4144/4182] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [4145/4182] Built Iut.SourceTrace.M1M3PaperLedger (10s)
✔ [4146/4182] Built Iut.Stage1.PilotComparison (3.6s)
✔ [4149/4183] Built Iut.Stage1.IUTStage1HodgeTheaterSource (15s)
✔ [4150/4183] Built Iut.Foundations.AlgorithmicBridge (2.9s)
⚠ [4151/4183] Built Iut.Foundations.SourceTheorem311 (138s)
warning: Iut/Foundations/SourceTheorem311.lean:771:4: try 'simp' instead of 'simpa'

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceTheorem311.lean:1021:43: unused variable `map`

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

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

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceTheorem311.lean:4956:7: unused variable `factor`

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:5112:8: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
  have : automorphism value ∈ automorphism '' (core.invariantLattice subgroup : Set M) := ⟨value, hvalue, rfl⟩
Please focus on the current goal, for instance using `·` (typed as "\.").

Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: Iut/Foundations/SourceTheorem311.lean:5115:8: The following tactic starts with 2 goals and ends with 1 goal, 1 of which is not operated on.
  simpa only [hautomorphism.2 subgroup] using this
Please focus on the current goal, for instance using `·` (typed as "\.").

Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: Iut/Foundations/SourceTheorem311.lean:5771:2: try 'simp' instead of 'simpa'

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceTheorem311.lean:7548:54: 'norm_num' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Iut/Foundations/SourceTheorem311.lean:7548:54: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Iut/Foundations/SourceTheorem311.lean:8148:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceTheorem311.lean:8140:4: `simp [Set.mem_smul_set, nnrealPacketScale, packetScale,
      Equiv.mulLeft₀, mul_comm]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Foundations/SourceTheorem311.lean:8140:4: Try this:
  [apply] simp only [mem_image, mem_image_equiv]
info: Iut/Foundations/SourceTheorem311.lean:8143:6: `rintro ⟨source, hsource, hvalue⟩` uses `⊢`!
warning: Iut/Foundations/SourceTheorem311.lean:8140:4: `simp [Set.mem_smul_set, nnrealPacketScale, packetScale,
      Equiv.mulLeft₀, mul_comm]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Foundations/SourceTheorem311.lean:8140:4: Try this:
  [apply] simp only [mem_image, mem_image_equiv]
info: Iut/Foundations/SourceTheorem311.lean:8144:6: `exact ⟨source, hsource, by simpa using hvalue⟩` uses `⊢`!
warning: Iut/Foundations/SourceTheorem311.lean:8140:4: `simp [Set.mem_smul_set, nnrealPacketScale, packetScale,
      Equiv.mulLeft₀, mul_comm]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Foundations/SourceTheorem311.lean:8140:4: Try this:
  [apply] simp only [mem_image, mem_image_equiv]
info: Iut/Foundations/SourceTheorem311.lean:8145:6: `rintro ⟨source, hsource, hvalue⟩` uses `⊢`!
warning: Iut/Foundations/SourceTheorem311.lean:8140:4: `simp [Set.mem_smul_set, nnrealPacketScale, packetScale,
      Equiv.mulLeft₀, mul_comm]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Foundations/SourceTheorem311.lean:8140:4: Try this:
  [apply] simp only [mem_image, mem_image_equiv]
info: Iut/Foundations/SourceTheorem311.lean:8146:6: `exact ⟨source, hsource, by simpa using hvalue⟩` uses `⊢`!
warning: Iut/Foundations/SourceTheorem311.lean:12454:7: unused variable `map`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12459:7: unused variable `map`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12901:12: unused variable `first`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12901:18: unused variable `second`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12904:12: unused variable `value`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12927:12: unused variable `first`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12927:18: unused variable `second`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12931:12: unused variable `value`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:14042:8: `simp [stripMap, CategoryCapsule.FullMemberMorphism.id]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Foundations/SourceTheorem311.lean:14042:8: Try this:
  [apply] simp only [Cat.of_α]
info: Iut/Foundations/SourceTheorem311.lean:14043:8: `exact Category.comp_id _` uses `⊢`!
✔ [4153/4183] Built Iut.Stage1.CorollarySchema (44s)
✔ [4154/4183] Built Iut.Foundations.SourceTheorem311Horizontal (120s)
✔ [4155/4183] Built Iut.Foundations.SourceVerticalLogLink (131s)
✔ [4156/4183] Built Iut.Foundations.SourceFiniteLocalMLFComparison (130s)
✔ [4157/4186] Built Iut.Stage1.SourceObligations (26s)
✔ [4158/4186] Built Iut.Foundations.SourceDefinition52LocalReconstruction (130s)
✔ [4160/4195] Built Iut.Stage1.IUTSourceScaffold (43s)
✔ [4162/4195] Built Iut.Foundations.SourceDefinition52LocalContinuity (124s)
✔ [4164/4195] Built Iut.Stage1.IUTStage1Data (36s)
✔ [4166/4195] Built Iut.Foundations.SourceDefinition52LocalJointContinuity (113s)
⚠ [4167/4195] Built Iut.Stage1.IUTStage1SourceCore (125s)
warning: Iut/Stage1/IUTStage1SourceCore.lean:20826:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotient_card_eq_pow_finrank`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:21074:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotientCosetHaarCharacterEndpoint`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:21141:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.unitBallHaarCharacterEndpoint`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:21239:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueSubmoduleQuotientCosetHaarCharacterNormalizationSource.ComponentwiseEqual.toResidueModuleQuotientCosetHaarCharacterNormalizationSource`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:21283:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueSubmoduleQuotientCosetHaarCharacterNormalizationSource.quotientCosetHaarCharacterEndpoint`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:21359:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueSubmoduleQuotientCosetHaarCharacterNormalizationSource.unitBallHaarCharacterEndpoint`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:21638:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:21638:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:21640:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21638:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:21638:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:21641:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21638:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:21638:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:21645:4: `have hinteger_eq : (integer : ℚ_[p]) = (p : ℚ_[p]) * (preimage : ℚ_[p]) := by
  simpa [IUTStage1PadicIntegerUnitBallSource.padicIntAddEquivIntegerAddSubgroup, hpreimage_eq] using
    hpoint_eq.symm` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21638:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:21638:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:21655:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21678:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:21680:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21678:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:21681:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21678:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:21684:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21678:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:21685:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21678:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:21686:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [4169/4195] Built Iut.Foundations.SourceDefinition52IndSystem (61s)
✔ [4170/4195] Built Iut.Stage1.IUTStage1Remark312Absorption (13s)
⚠ [4172/4195] Built Iut.Stage1.IUTStage1IUTIVAlgebra (17s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:4161: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/Stage1/IUTStage1IUTIVAlgebra.lean:4180: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/Stage1/IUTStage1IUTIVAlgebra.lean:4194: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/Stage1/IUTStage1IUTIVAlgebra.lean:4236:10: Try `simp at hkind` instead of `simpa using hkind`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:4246:10: Try `simp at hkind` instead of `simpa using hkind`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:4267: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/Stage1/IUTStage1IUTIVAlgebra.lean:4323: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/Stage1/IUTStage1IUTIVAlgebra.lean:4782: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/Stage1/IUTStage1IUTIVAlgebra.lean:4863: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/Stage1/IUTStage1IUTIVAlgebra.lean:6238: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/Stage1/IUTStage1IUTIVAlgebra.lean:6316: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/Stage1/IUTStage1IUTIVAlgebra.lean:6362: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/Stage1/IUTStage1IUTIVAlgebra.lean:6483: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/Stage1/IUTStage1IUTIVAlgebra.lean:6531: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/Stage1/IUTStage1IUTIVAlgebra.lean:6640:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [4174/4195] Built Iut.Stage1.IUTStage1FiniteLabels (5.4s)
✔ [4175/4195] Built Iut.Foundations.SourceDefinition52Sequential (27s)
⚠ [4176/4195] Built Iut.Stage1.IUTStage1StepX (7.4s)
warning: Iut/Stage1/IUTStage1StepX.lean:552:6: try 'simp' instead of 'simpa'

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

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

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [4177/4195] Built Iut.Foundations.SourceTheorem311Assembly (10s)
✔ [4178/4195] Built Iut.Stage1.IUTStage1Gaussian (11s)
✔ [4179/4195] Built Iut.Stage1.IUTStage1HodgeSHE (8.5s)
✔ [4180/4195] Built Iut.Stage1.IUTStage1HodgeArakelovPilots (6.8s)
⚠ [4181/4195] Built Iut.Stage1.IUTStage1Theorem311 (27s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4640: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/Stage1/IUTStage1Theorem311.lean:4645: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/Stage1/IUTStage1Theorem311.lean:4799: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/Stage1/IUTStage1Theorem311.lean:4831: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/Stage1/IUTStage1Theorem311.lean:4836: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/Stage1/IUTStage1Theorem311.lean:4879: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/Stage1/IUTStage1Theorem311.lean:4933: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/Stage1/IUTStage1Theorem311.lean:4968: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/Stage1/IUTStage1Theorem311.lean:4973: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/Stage1/IUTStage1Theorem311.lean:5105: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/Stage1/IUTStage1Theorem311.lean:5139: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/Stage1/IUTStage1Theorem311.lean:5144: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/Stage1/IUTStage1Theorem311.lean:5282: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/Stage1/IUTStage1Theorem311.lean:5316: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/Stage1/IUTStage1Theorem311.lean:5321: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/Stage1/IUTStage1Theorem311.lean:5464: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/Stage1/IUTStage1Theorem311.lean:5496: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/Stage1/IUTStage1Theorem311.lean:5501: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/Stage1/IUTStage1Theorem311.lean:5614: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/Stage1/IUTStage1Theorem311.lean:7746:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15549: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/Stage1/IUTStage1Theorem311.lean:16085:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:16426:6: unused variable `choice`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:17458:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:17936:5: unused variable `targetSource`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:19154:5: unused variable `data`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:22187:5: unused variable `obligations`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [4182/4195] Built Iut.Stage1.IUTStage1ConstructedTheorem311 (21s)
✖ [4183/4195] Building Iut.Stage1.IUTStage1StepXI.Core (149s)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/Iut/Stage1/IUTStage1StepXI/Core.lean -o /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI/Core.olean -i /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI/Core.ilean -c /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI/Core.c --setup /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI/Core.setup.json --json
error: Lean exited with code 137
Some required targets logged failures:
- Iut.Stage1.IUTStage1StepXI.Core

error: build failed

apx-runtime-resource-v1	apx-verifier-job-1495-runtime-lean_checker-1073315-1784927363183625951-1	827392	1122304	4026531840	0	0	0	0	0	0	21069824	4026531840	4026531840	0	0	1217	0	1	0

blueprint_buildexit 1duration 15s · created 7/24/2026, 9:46:19 PM

lake build :blueprint

error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1495-runtime-blueprint_build-1073315-1784929563371340180-2	880640	1204224	4026531840	0	0	0	0	0	0	798760960	902422528	4026531840	0	0	0	0	0	0