Verification run

Run 1187

promachina/iut-leanbranch mastertriggered via poller

failedcommit 5c48653111f4toolchain lean-v4-30-0prover leantook 27m 48s · 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/25/2026, 4:15:47 AM

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

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

git_checkoutexit 0duration 176 ms · created 7/25/2026, 4:15:47 AM

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 38s · created 7/25/2026, 4:15:47 AM

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 (386ms)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (3.4s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (100ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (164ms)
✔ [13/25] Built Cache.Lean:c.o (123ms)
✔ [15/25] Built Cache.IO (3.3s)
✔ [16/25] Built Cache.Init (348ms)
✔ [17/25] Built Cache.IO:c.o (1.2s)
✔ [18/25] Built Cache.Init:c.o (76ms)
✔ [19/25] Built Cache.Hashing (1.1s)
✔ [20/25] Built Cache.Hashing:c.o (351ms)
✔ [21/25] Built Cache.Requests (2.0s)
✔ [22/25] Built Cache.Requests:c.o (1.7s)
✔ [23/25] Built Cache.Main (934ms)
✔ [24/25] Built Cache.Main:c.o (517ms)
✔ [25/25] Built cache:exe (14s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 2 KB/s], Decompressed: 12
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 15 KB/s], Decompressed: 27
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 54 KB/s], Decompressed: 61
Downloaded: 92 file(s) [attempted 92/8459 = 1%, 240 KB/s], Decompressed: 79
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 252 KB/s], Decompressed: 110
Downloaded: 155 file(s) [attempted 155/8459 = 1%, 97 KB/s], Decompressed: 148
Downloaded: 192 file(s) [attempted 192/8459 = 2%, 467 KB/s], Decompressed: 175
Downloaded: 226 file(s) [attempted 226/8459 = 2%, 195 KB/s], Decompressed: 199
Downloaded: 257 file(s) [attempted 257/8459 = 3%, 37 KB/s], Decompressed: 233
Downloaded: 292 file(s) [attempted 292/8459 = 3%, 649 KB/s], Decompressed: 257
Downloaded: 333 file(s) [attempted 333/8459 = 3%, 133 KB/s], Decompressed: 288
Downloaded: 370 file(s) [attempted 370/8459 = 4%, 118 KB/s], Decompressed: 322
Downloaded: 411 file(s) [attempted 411/8459 = 4%, 159 KB/s], Decompressed: 387
Downloaded: 449 file(s) [attempted 449/8459 = 5%, 67 KB/s], Decompressed: 411
Downloaded: 487 file(s) [attempted 487/8459 = 5%, 268 KB/s], Decompressed: 459
Downloaded: 531 file(s) [attempted 531/8459 = 6%, 685 KB/s], Decompressed: 487
Downloaded: 569 file(s) [attempted 569/8459 = 6%, 71 KB/s], Decompressed: 521
Downloaded: 607 file(s) [attempted 607/8459 = 7%, 609 KB/s], Decompressed: 559
Downloaded: 648 file(s) [attempted 648/8459 = 7%, 238 KB/s], Decompressed: 600
Downloaded: 689 file(s) [attempted 689/8459 = 8%, 692 KB/s], Decompressed: 638
Downloaded: 730 file(s) [attempted 730/8459 = 8%, 69 KB/s], Decompressed: 675
Downloaded: 775 file(s) [attempted 775/8459 = 9%, 69 KB/s], Decompressed: 706
Downloaded: 809 file(s) [attempted 809/8459 = 9%, 284 KB/s], Decompressed: 740
Downloaded: 853 file(s) [attempted 853/8459 = 10%, 38 KB/s], Decompressed: 816
Downloaded: 888 file(s) [attempted 888/8459 = 10%, 35 KB/s], Decompressed: 816
Downloaded: 936 file(s) [attempted 936/8459 = 11%, 76 KB/s], Decompressed: 853
Downloaded: 977 file(s) [attempted 977/8459 = 11%, 589 KB/s], Decompressed: 898
Downloaded: 1007 file(s) [attempted 1007/8459 = 11%, 135 KB/s], Decompressed: 942
Downloaded: 1049 file(s) [attempted 1049/8459 = 12%, 628 KB/s], Decompressed: 987
Downloaded: 1090 file(s) [attempted 1090/8459 = 12%, 471 KB/s], Decompressed: 1035
Downloaded: 1131 file(s) [attempted 1131/8459 = 13%, 238 KB/s], Decompressed: 1035
Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 808 KB/s], Decompressed: 1035
Downloaded: 1216 file(s) [attempted 1216/8459 = 14%, 180 KB/s], Decompressed: 1079
Downloaded: 1257 file(s) [attempted 1257/8459 = 14%, 68 KB/s], Decompressed: 1079
Downloaded: 1291 file(s) [attempted 1291/8459 = 15%, 171 KB/s], Decompressed: 1185
Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 49 KB/s], Decompressed: 1185
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 145 KB/s], Decompressed: 1185
Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 102 KB/s], Decompressed: 1185
Downloaded: 1463 file(s) [attempted 1463/8459 = 17%, 102 KB/s], Decompressed: 1285
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 1768 KB/s], Decompressed: 1285
Downloaded: 1538 file(s) [attempted 1538/8459 = 18%, 92 KB/s], Decompressed: 1285
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 548 KB/s], Decompressed: 1422
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 338 KB/s], Decompressed: 1422
Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 226 KB/s], Decompressed: 1422
Downloaded: 1702 file(s) [attempted 1702/8459 = 20%, 123 KB/s], Decompressed: 1422
Downloaded: 1736 file(s) [attempted 1736/8459 = 20%, 430 KB/s], Decompressed: 1576
Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 224 KB/s], Decompressed: 1576
Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 295 KB/s], Decompressed: 1576
Downloaded: 1860 file(s) [attempted 1860/8459 = 21%, 1742 KB/s], Decompressed: 1576
Downloaded: 1901 file(s) [attempted 1901/8459 = 22%, 537 KB/s], Decompressed: 1726
Downloaded: 1928 file(s) [attempted 1928/8459 = 22%, 77 KB/s], Decompressed: 1726
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 160 KB/s], Decompressed: 1726
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 24 KB/s], Decompressed: 1726
Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 470 KB/s], Decompressed: 1726
Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 299 KB/s], Decompressed: 1726
Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 565 KB/s], Decompressed: 1726
Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 547 KB/s], Decompressed: 1726
Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 203 KB/s], Decompressed: 1873
Downloaded: 2250 file(s) [attempted 2250/8459 = 26%, 903 KB/s], Decompressed: 1873
Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 368 KB/s], Decompressed: 1873
Downloaded: 2335 file(s) [attempted 2335/8459 = 27%, 48 KB/s], Decompressed: 1873
Downloaded: 2373 file(s) [attempted 2373/8459 = 28%, 977 KB/s], Decompressed: 1873
Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 173 KB/s], Decompressed: 1873
Downloaded: 2452 file(s) [attempted 2452/8459 = 28%, 352 KB/s], Decompressed: 1873
Downloaded: 2493 file(s) [attempted 2493/8459 = 29%, 49 KB/s], Decompressed: 1873
Downloaded: 2534 file(s) [attempted 2534/8459 = 29%, 28 KB/s], Decompressed: 1873
Downloaded: 2571 file(s) [attempted 2571/8459 = 30%, 157 KB/s], Decompressed: 1873
Downloaded: 2610 file(s) [attempted 2610/8459 = 30%, 238 KB/s], Decompressed: 2205
Downloaded: 2647 file(s) [attempted 2647/8459 = 31%, 121 KB/s], Decompressed: 2205
Downloaded: 2688 file(s) [attempted 2688/8459 = 31%, 403 KB/s], Decompressed: 2205
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 370 KB/s], Decompressed: 2205
Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 251 KB/s], Decompressed: 2205
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 66 KB/s], Decompressed: 2205
Downloaded: 2845 file(s) [attempted 2845/8459 = 33%, 74 KB/s], Decompressed: 2205
Downloaded: 2883 file(s) [attempted 2883/8459 = 34%, 595 KB/s], Decompressed: 2205
Downloaded: 2927 file(s) [attempted 2927/8459 = 34%, 385 KB/s], Decompressed: 2205
Downloaded: 2968 file(s) [attempted 2968/8459 = 35%, 243 KB/s], Decompressed: 2205
Downloaded: 3003 file(s) [attempted 3003/8459 = 35%, 40 KB/s], Decompressed: 2585
Downloaded: 3047 file(s) [attempted 3047/8459 = 36%, 159 KB/s], Decompressed: 2585
Downloaded: 3092 file(s) [attempted 3092/8459 = 36%, 378 KB/s], Decompressed: 2585
Downloaded: 3126 file(s) [attempted 3126/8459 = 36%, 845 KB/s], Decompressed: 2585
Downloaded: 3167 file(s) [attempted 3167/8459 = 37%, 504 KB/s], Decompressed: 2585
Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 509 KB/s], Decompressed: 2585
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 249 KB/s], Decompressed: 2585
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 176 KB/s], Decompressed: 2585
Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 275 KB/s], Decompressed: 2585
Downloaded: 3359 file(s) [attempted 3359/8459 = 39%, 63 KB/s], Decompressed: 2585
Downloaded: 3410 file(s) [attempted 3410/8459 = 40%, 761 KB/s], Decompressed: 2585
Downloaded: 3458 file(s) [attempted 3458/8459 = 40%, 85 KB/s], Decompressed: 2979
Downloaded: 3495 file(s) [attempted 3495/8459 = 41%, 1896 KB/s], Decompressed: 2979
Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 68 KB/s], Decompressed: 2979
Downloaded: 3571 file(s) [attempted 3571/8459 = 42%, 532 KB/s], Decompressed: 2979
Downloaded: 3608 file(s) [attempted 3608/8459 = 42%, 38 KB/s], Decompressed: 2979
Downloaded: 3656 file(s) [attempted 3656/8459 = 43%, 320 KB/s], Decompressed: 2979
Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 40 KB/s], Decompressed: 2979
Downloaded: 3738 file(s) [attempted 3738/8459 = 44%, 189 KB/s], Decompressed: 2979
Downloaded: 3776 file(s) [attempted 3776/8459 = 44%, 102 KB/s], Decompressed: 2979
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 101 KB/s], Decompressed: 2979
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 83 KB/s], Decompressed: 2979
Downloaded: 3903 file(s) [attempted 3903/8459 = 46%, 227 KB/s], Decompressed: 2979
Downloaded: 3947 file(s) [attempted 3947/8459 = 46%, 343 KB/s], Decompressed: 2979
Downloaded: 3988 file(s) [attempted 3988/8459 = 47%, 312 KB/s], Decompressed: 2979
Downloaded: 4023 file(s) [attempted 4023/8459 = 47%, 1828 KB/s], Decompressed: 2979
Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 256 KB/s], Decompressed: 2979
Downloaded: 4101 file(s) [attempted 4101/8459 = 48%, 616 KB/s], Decompressed: 3458
Downloaded: 4142 file(s) [attempted 4142/8459 = 48%, 535 KB/s], Decompressed: 3458
Downloaded: 4183 file(s) [attempted 4183/8459 = 49%, 448 KB/s], Decompressed: 3458
Downloaded: 4224 file(s) [attempted 4224/8459 = 49%, 376 KB/s], Decompressed: 3458
Downloaded: 4259 file(s) [attempted 4259/8459 = 50%, 47 KB/s], Decompressed: 3458
Downloaded: 4300 file(s) [attempted 4300/8459 = 50%, 114 KB/s], Decompressed: 3458
Downloaded: 4337 file(s) [attempted 4337/8459 = 51%, 146 KB/s], Decompressed: 3458
Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 850 KB/s], Decompressed: 3458
Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 788 KB/s], Decompressed: 3458
Downloaded: 4457 file(s) [attempted 4457/8459 = 52%, 152 KB/s], Decompressed: 3458
Downloaded: 4498 file(s) [attempted 4498/8459 = 53%, 125 KB/s], Decompressed: 3458
Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 1073 KB/s], Decompressed: 3458
Downloaded: 4580 file(s) [attempted 4580/8459 = 54%, 490 KB/s], Decompressed: 3458
Downloaded: 4621 file(s) [attempted 4621/8459 = 54%, 362 KB/s], Decompressed: 3458
Downloaded: 4659 file(s) [attempted 4659/8459 = 55%, 771 KB/s], Decompressed: 3458
Downloaded: 4697 file(s) [attempted 4697/8459 = 55%, 157 KB/s], Decompressed: 3458
Downloaded: 4741 file(s) [attempted 4741/8459 = 56%, 1164 KB/s], Decompressed: 3458
Downloaded: 4782 file(s) [attempted 4782/8459 = 56%, 623 KB/s], Decompressed: 3458
Downloaded: 4823 file(s) [attempted 4823/8459 = 57%, 300 KB/s], Decompressed: 3458
Downloaded: 4861 file(s) [attempted 4861/8459 = 57%, 72 KB/s], Decompressed: 3458
Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 598 KB/s], Decompressed: 4081
Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 304 KB/s], Decompressed: 4081
Downloaded: 4984 file(s) [attempted 4984/8459 = 58%, 66 KB/s], Decompressed: 4081
Downloaded: 5029 file(s) [attempted 5029/8459 = 59%, 115 KB/s], Decompressed: 4081
Downloaded: 5070 file(s) [attempted 5070/8459 = 59%, 61 KB/s], Decompressed: 4081
Downloaded: 5107 file(s) [attempted 5107/8459 = 60%, 717 KB/s], Decompressed: 4081
Downloaded: 5145 file(s) [attempted 5145/8459 = 60%, 866 KB/s], Decompressed: 4081
Downloaded: 5186 file(s) [attempted 5186/8459 = 61%, 739 KB/s], Decompressed: 4081
Downloaded: 5227 file(s) [attempted 5227/8459 = 61%, 304 KB/s], Decompressed: 4081
Downloaded: 5268 file(s) [attempted 5268/8459 = 62%, 157 KB/s], Decompressed: 4081
Downloaded: 5309 file(s) [attempted 5309/8459 = 62%, 25 KB/s], Decompressed: 4081
Downloaded: 5350 file(s) [attempted 5350/8459 = 63%, 85 KB/s], Decompressed: 4081
Downloaded: 5388 file(s) [attempted 5388/8459 = 63%, 769 KB/s], Decompressed: 4081
Downloaded: 5429 file(s) [attempted 5429/8459 = 64%, 196 KB/s], Decompressed: 4081
Downloaded: 5470 file(s) [attempted 5470/8459 = 64%, 24 KB/s], Decompressed: 4081
Downloaded: 5511 file(s) [attempted 5511/8459 = 65%, 97 KB/s], Decompressed: 4081
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 79 KB/s], Decompressed: 4081
Downloaded: 5604 file(s) [attempted 5604/8459 = 66%, 696 KB/s], Decompressed: 4081
Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 646 KB/s], Decompressed: 4081
Downloaded: 5686 file(s) [attempted 5686/8459 = 67%, 3252 KB/s], Decompressed: 4081
Downloaded: 5723 file(s) [attempted 5723/8459 = 67%, 170 KB/s], Decompressed: 4081
Downloaded: 5761 file(s) [attempted 5761/8459 = 68%, 470 KB/s], Decompressed: 4081
Downloaded: 5806 file(s) [attempted 5806/8459 = 68%, 294 KB/s], Decompressed: 4081
Downloaded: 5843 file(s) [attempted 5843/8459 = 69%, 343 KB/s], Decompressed: 4081
Downloaded: 5884 file(s) [attempted 5884/8459 = 69%, 229 KB/s], Decompressed: 4081
Downloaded: 5925 file(s) [attempted 5925/8459 = 70%, 573 KB/s], Decompressed: 4878
Downloaded: 5963 file(s) [attempted 5963/8459 = 70%, 531 KB/s], Decompressed: 4878
Downloaded: 6001 file(s) [attempted 6001/8459 = 70%, 465 KB/s], Decompressed: 4878
Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 66 KB/s], Decompressed: 4878
Downloaded: 6086 file(s) [attempted 6086/8459 = 71%, 135 KB/s], Decompressed: 4878
Downloaded: 6127 file(s) [attempted 6127/8459 = 72%, 159 KB/s], Decompressed: 4878
Downloaded: 6168 file(s) [attempted 6168/8459 = 72%, 53 KB/s], Decompressed: 4878
Downloaded: 6206 file(s) [attempted 6206/8459 = 73%, 506 KB/s], Decompressed: 4878
Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 64 KB/s], Decompressed: 4878
Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 118 KB/s], Decompressed: 4878
Downloaded: 6322 file(s) [attempted 6322/8459 = 74%, 326 KB/s], Decompressed: 4878
Downloaded: 6367 file(s) [attempted 6367/8459 = 75%, 233 KB/s], Decompressed: 4878
Downloaded: 6401 file(s) [attempted 6401/8459 = 75%, 67 KB/s], Decompressed: 4878
Downloaded: 6439 file(s) [attempted 6439/8459 = 76%, 741 KB/s], Decompressed: 4878
Downloaded: 6476 file(s) [attempted 6476/8459 = 76%, 239 KB/s], Decompressed: 4878
Downloaded: 6523 file(s) [attempted 6523/8459 = 77%, 111 KB/s], Decompressed: 4878
Downloaded: 6559 file(s) [attempted 6559/8459 = 77%, 279 KB/s], Decompressed: 4878
Downloaded: 6596 file(s) [attempted 6596/8459 = 77%, 440 KB/s], Decompressed: 4878
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 93 KB/s], Decompressed: 4878
Downloaded: 6675 file(s) [attempted 6675/8459 = 78%, 58 KB/s], Decompressed: 4878
Downloaded: 6719 file(s) [attempted 6719/8459 = 79%, 499 KB/s], Decompressed: 4878
Downloaded: 6760 file(s) [attempted 6760/8459 = 79%, 342 KB/s], Decompressed: 4878
Downloaded: 6801 file(s) [attempted 6801/8459 = 80%, 194 KB/s], Decompressed: 4878
Downloaded: 6836 file(s) [attempted 6836/8459 = 80%, 44 KB/s], Decompressed: 4878
Downloaded: 6873 file(s) [attempted 6873/8459 = 81%, 601 KB/s], Decompressed: 4878
Downloaded: 6914 file(s) [attempted 6914/8459 = 81%, 185 KB/s], Decompressed: 4878
Downloaded: 6959 file(s) [attempted 6959/8459 = 82%, 139 KB/s], Decompressed: 4878
Downloaded: 6997 file(s) [attempted 6997/8459 = 82%, 461 KB/s], Decompressed: 4878
Downloaded: 7038 file(s) [attempted 7038/8459 = 83%, 884 KB/s], Decompressed: 4878
Downloaded: 7079 file(s) [attempted 7079/8459 = 83%, 577 KB/s], Decompressed: 4878
Downloaded: 7116 file(s) [attempted 7116/8459 = 84%, 351 KB/s], Decompressed: 4878
Downloaded: 7161 file(s) [attempted 7161/8459 = 84%, 216 KB/s], Decompressed: 4878
Downloaded: 7205 file(s) [attempted 7205/8459 = 85%, 267 KB/s], Decompressed: 4878
Downloaded: 7243 file(s) [attempted 7243/8459 = 85%, 442 KB/s], Decompressed: 4878
Downloaded: 7287 file(s) [attempted 7287/8459 = 86%, 44 KB/s], Decompressed: 4878
Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 72 KB/s], Decompressed: 4878
Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 122 KB/s], Decompressed: 5891
Downloaded: 7404 file(s) [attempted 7404/8459 = 87%, 104 KB/s], Decompressed: 5891
Downloaded: 7445 file(s) [attempted 7445/8459 = 88%, 166 KB/s], Decompressed: 5891
Downloaded: 7489 file(s) [attempted 7489/8459 = 88%, 744 KB/s], Decompressed: 5891
Downloaded: 7530 file(s) [attempted 7530/8459 = 89%, 122 KB/s], Decompressed: 5891
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 262 KB/s], Decompressed: 5891
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 330 KB/s], Decompressed: 5891
Downloaded: 7650 file(s) [attempted 7650/8459 = 90%, 253 KB/s], Decompressed: 5891
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 47 KB/s], Decompressed: 5891
Downloaded: 7732 file(s) [attempted 7732/8459 = 91%, 143 KB/s], Decompressed: 5891
Downloaded: 7777 file(s) [attempted 7777/8459 = 91%, 103 KB/s], Decompressed: 5891
Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 136 KB/s], Decompressed: 5891
Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 474 KB/s], Decompressed: 5891
Downloaded: 7893 file(s) [attempted 7893/8459 = 93%, 64 KB/s], Decompressed: 5891
Downloaded: 7934 file(s) [attempted 7934/8459 = 93%, 319 KB/s], Decompressed: 5891
Downloaded: 7975 file(s) [attempted 7975/8459 = 94%, 1003 KB/s], Decompressed: 5891
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 443 KB/s], Decompressed: 5891
Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 170 KB/s], Decompressed: 5891
Downloaded: 8088 file(s) [attempted 8088/8459 = 95%, 215 KB/s], Decompressed: 5891
Downloaded: 8133 file(s) [attempted 8133/8459 = 96%, 180 KB/s], Decompressed: 5891
Downloaded: 8177 file(s) [attempted 8177/8459 = 96%, 54 KB/s], Decompressed: 5891
Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 455 KB/s], Decompressed: 5891
Downloaded: 8263 file(s) [attempted 8263/8459 = 97%, 107 KB/s], Decompressed: 5891
Downloaded: 8304 file(s) [attempted 8304/8459 = 98%, 62 KB/s], Decompressed: 5891
Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 77 KB/s], Decompressed: 5891
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 76 KB/s], Decompressed: 5891
Downloaded: 8427 file(s) [attempted 8427/8459 = 99%, 258 KB/s], Decompressed: 5891
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 117 KB/s], Decompressed: 5891
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 117 KB/s], Decompressed: 5891

apx-runtime-resource-v1	apx-verifier-job-1496-runtime-lake_cache-1113525-1784951293087581442-0	786432	1302528	4026531840	0	0	0	0	0	0	3109269504	3438006272	4026531840	0	0	0	0	0	0

lean_checkerexit 1duration 25m 53s · created 7/25/2026, 4:15:47 AM

lake build

✔ [1/8] Built Iut.Foundations.Species (501ms)
✔ [753/760] Built Iut.Foundations.RealLineCopy (63s)
✔ [754/760] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [755/760] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [756/760] Built Iut.Foundations.RegionMeasure (1.6s)
✔ [757/760] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [758/760] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [759/767] Built Iut.Foundations.QualitativeData (2.2s)
✔ [3505/3510] Built Iut.Foundations.EtaleThetaQuotient (60s)
✔ [3506/3510] Built Iut.Foundations.Orbicurve (55s)
✔ [3953/3962] Built Iut.Foundations.InitialThetaData (33s)
✔ [3962/3973] Built Iut.Foundations.OrbicurvePullback (14s)
✔ [3964/3973] Built Iut.Foundations.EtaleThetaCovers (4.9s)
✔ [3967/3973] Built Iut.Foundations.SourceSemiGraph (1.9s)
✔ [3968/3974] Built Iut.Foundations.SourceSemiGraphAction (2.4s)
✔ [3969/3974] Built Iut.Foundations.SourceInitialThetaData (42s)
✔ [3970/3974] Built Iut.Foundations.SourceSemiGraphOfSubgroups (11s)
✔ [3972/3974] Built Iut.Foundations.SourceProfiniteCosetSystem (4.3s)
✔ [3973/3974] Built Iut.Foundations.SourceProfiniteSemiGraphSystem (77s)
✔ [4007/4012] Built Iut.Foundations.KummerFaithfulness (5.1s)
✔ [4008/4013] Built Iut.Foundations.SourceTemperedSemigraph (6.6s)
✔ [4010/4013] Built Iut.Foundations.SourceMonoThetaEnvironment (56s)
✔ [4012/4023] Built Iut.Foundations.ContinuousH1 (14s)
✔ [4020/4027] Built Iut.Foundations.Procession (2.8s)
✔ [4023/4027] Built Iut.Foundations.SourceMLFKummerFaithfulness (3.9s)
✔ [4024/4027] Built Iut.Foundations.Frobenioid (6.0s)
✔ [4025/4027] Built Iut.Foundations.SourceThetaHodgeTheater (25s)
✔ [4026/4041] Built Iut.Foundations.SourceProcession (16s)
✔ [4038/4057] Built Iut.Foundations.SourceModelFrobenioid (5.9s)
✔ [4039/4057] Built Iut.Foundations.SourceAnabelioid (5.5s)
⚠ [4050/4075] 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`
✔ [4053/4075] Built Iut.Foundations.SourceTopologicalActionPairCategory (16s)
✔ [4054/4075] Built Iut.Foundations.SourceConjugateSynchronization (6.8s)
✔ [4055/4075] Built Iut.Foundations.SourceThetaSplitting (8.6s)
✔ [4056/4075] Built Iut.Foundations.SourceSplitKummerFrobenioid (11s)
✔ [4060/4075] Built Iut.Foundations.SourceAnabelioidEquivalence (4.4s)
✔ [4061/4075] Built Iut.Foundations.SourceSemiGraphOfAnabelioids (3.1s)
✔ [4062/4075] Built Iut.Foundations.SourceAutHolomorphic (2.5s)
✔ [4063/4075] Built Iut.Foundations.SourceHodgeArakelovEvaluation (4.3s)
✔ [4064/4075] Built Iut.Foundations.SourceArchimedeanKummerSystem (7.2s)
✔ [4066/4075] Built Iut.Foundations.SourceTimesMuPrimeStrip (11s)
✔ [4067/4075] Built Iut.Foundations.SourceContinuousAnabelioid (10s)
✔ [4068/4075] Built Iut.Foundations.SourceTimesMuPrimeStripIsomorphism (17s)
✔ [4069/4078] Built Iut.Foundations.SourceAnabelioidSlice (24s)
✔ [4070/4081] Built Iut.Foundations.SourceTimesMuPrimeStripFullPolyIsomorphism (14s)
✔ [4071/4081] Built Iut.Foundations.SourceAnabelioidComponents (10s)
✔ [4073/4081] Built Iut.Foundations.SourceTimesMuReconstructionAlgorithm (10s)
✔ [4074/4085] Built Iut.Foundations.SourceConnectedAnabelioidSlice (7.7s)
✔ [4076/4087] Built Iut.Foundations.SourceConnectedFiniteEtaleConverse (4.7s)
✔ [4086/4095] Built Iut.Foundations.SourceArchimedeanSemiGerm (3.2s)
✔ [4088/4095] Built Iut.Foundations.SourceFThetaBridge (4.5s)
✔ [4092/4096] Built Iut.Foundations.SourceTopologicalPseudoMonoid (5.6s)
✔ [4095/4099] Built Iut.Foundations.SourceAutHolomorphicRigidity (3.2s)
✔ [4143/4182] Built Iut.Foundations.ThetaHodgeTheater (7.3s)
✔ [4144/4182] Built Iut.Foundations.AlgorithmicOutput (1.8s)
✔ [4145/4182] Built Iut.SourceTrace.M1M3PaperLedger (9.7s)
✔ [4147/4183] Built Iut.Stage1.PilotComparison (1.5s)
✔ [4149/4183] Built Iut.Stage1.IUTStage1HodgeTheaterSource (13s)
✔ [4150/4183] Built Iut.Foundations.AlgorithmicBridge (2.7s)
⚠ [4151/4183] Built Iut.Foundations.SourceTheorem311 (130s)
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 (31s)
✔ [4154/4183] Built Iut.Foundations.SourceTheorem311Horizontal (32s)
✔ [4155/4183] Built Iut.Foundations.SourceVerticalLogLink (7.2s)
✔ [4156/4183] Built Iut.Foundations.SourceFiniteLocalMLFComparison (10s)
✔ [4157/4186] Built Iut.Stage1.SourceObligations (3.1s)
✔ [4158/4194] Built Iut.Foundations.SourceDefinition52LocalReconstruction (28s)
✔ [4160/4195] Built Iut.Stage1.IUTSourceScaffold (2.5s)
✔ [4162/4195] Built Iut.Foundations.SourceDefinition52LocalContinuity (14s)
✔ [4164/4195] Built Iut.Stage1.IUTStage1Data (3.3s)
✔ [4166/4195] Built Iut.Foundations.SourceDefinition52LocalJointContinuity (4.8s)
⚠ [4167/4195] Built Iut.Stage1.IUTStage1SourceCore (82s)
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 (39s)
✔ [4170/4195] Built Iut.Stage1.IUTStage1Remark312Absorption (4.3s)
⚠ [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 (4.6s)
✔ [4175/4195] Built Iut.Foundations.SourceDefinition52Sequential (10s)
⚠ [4176/4195] Built Iut.Stage1.IUTStage1StepX (5.3s)
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 (7.9s)
✔ [4178/4195] Built Iut.Stage1.IUTStage1Gaussian (9.5s)
✔ [4179/4195] Built Iut.Stage1.IUTStage1HodgeSHE (8.6s)
✔ [4180/4195] Built Iut.Stage1.IUTStage1HodgeArakelovPilots (6.7s)
⚠ [4181/4195] Built Iut.Stage1.IUTStage1Theorem311 (24s)
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 (9.7s)
✖ [4183/4195] Building Iut.Stage1.IUTStage1StepXI.Core (154s)
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-1496-runtime-lean_checker-1113525-1784951391125149261-1	1122304	1236992	4026531840	0	0	0	0	0	0	14450688	4026531840	4026531840	0	0	72	0	1	0

blueprint_buildexit 1duration 3s · created 7/25/2026, 4:15:47 AM

lake build :blueprint

error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1496-runtime-blueprint_build-1113525-1784952944252696945-2	901120	1302528	4026531840	0	0	0	0	0	0	71262208	174698496	4026531840	0	0	0	0	0	0