Verification run

Run 1208

promachina/iut-leanbranch mastertriggered via poller

succeededcommit c41758e303c3toolchain lean-v4-30-0prover leantook 2h 50m · finished 6w ago

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 8/1/2026, 8:53:40 AM

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

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

git_checkoutexit 0duration 215 ms · created 8/1/2026, 8:53:40 AM

git checkout c41758e303c39318eedd0d90caa8a8140b89575f

Note: switching to 'c41758e303c39318eedd0d90caa8a8140b89575f'.

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 c41758e feat: construct canonical source prime strips (#38)

lake_cacheexit 0duration 1m 23s · created 8/1/2026, 8:53:40 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 (660ms)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (4.0s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (136ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (166ms)
✔ [13/25] Built Cache.Lean:c.o (133ms)
✔ [15/25] Built Cache.Init (340ms)
✔ [16/25] Built Cache.IO (3.6s)
✔ [17/25] Built Cache.Init:c.o (90ms)
✔ [18/25] Built Cache.IO:c.o (1.2s)
✔ [19/25] Built Cache.Hashing (1.0s)
✔ [20/25] Built Cache.Hashing:c.o (346ms)
✔ [21/25] Built Cache.Requests (2.2s)
✔ [22/25] Built Cache.Requests:c.o (1.9s)
✔ [23/25] Built Cache.Main (1.0s)
✔ [24/25] Built Cache.Main:c.o (560ms)
✔ [25/25] Built cache:exe (14s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 16 KB/s], Decompressed: 1
Downloaded: 40 file(s) [attempted 40/8459 = 0%, 17 KB/s], Decompressed: 18
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 205 KB/s], Decompressed: 30
Downloaded: 99 file(s) [attempted 99/8459 = 1%, 317 KB/s], Decompressed: 70
Downloaded: 131 file(s) [attempted 131/8459 = 1%, 40 KB/s], Decompressed: 70
Downloaded: 168 file(s) [attempted 168/8459 = 1%, 256 KB/s], Decompressed: 99
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 372 KB/s], Decompressed: 134
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 255 KB/s], Decompressed: 175
Downloaded: 264 file(s) [attempted 264/8459 = 3%, 286 KB/s], Decompressed: 175
Downloaded: 305 file(s) [attempted 305/8459 = 3%, 340 KB/s], Decompressed: 220
Downloaded: 350 file(s) [attempted 350/8459 = 4%, 605 KB/s], Decompressed: 271
Downloaded: 387 file(s) [attempted 387/8459 = 4%, 137 KB/s], Decompressed: 271
Downloaded: 422 file(s) [attempted 422/8459 = 4%, 336 KB/s], Decompressed: 271
Downloaded: 459 file(s) [attempted 459/8459 = 5%, 878 KB/s], Decompressed: 336
Downloaded: 501 file(s) [attempted 501/8459 = 5%, 155 KB/s], Decompressed: 336
Downloaded: 542 file(s) [attempted 542/8459 = 6%, 191 KB/s], Decompressed: 336
Downloaded: 579 file(s) [attempted 579/8459 = 6%, 195 KB/s], Decompressed: 439
Downloaded: 620 file(s) [attempted 620/8459 = 7%, 292 KB/s], Decompressed: 439
Downloaded: 661 file(s) [attempted 661/8459 = 7%, 769 KB/s], Decompressed: 439
Downloaded: 703 file(s) [attempted 703/8459 = 8%, 227 KB/s], Decompressed: 548
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 458 KB/s], Decompressed: 548
Downloaded: 788 file(s) [attempted 788/8459 = 9%, 210 KB/s], Decompressed: 548
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 168 KB/s], Decompressed: 672
Downloaded: 870 file(s) [attempted 870/8459 = 10%, 405 KB/s], Decompressed: 672
Downloaded: 918 file(s) [attempted 918/8459 = 10%, 895 KB/s], Decompressed: 672
Downloaded: 963 file(s) [attempted 963/8459 = 11%, 178 KB/s], Decompressed: 809
Downloaded: 1004 file(s) [attempted 1004/8459 = 11%, 537 KB/s], Decompressed: 809
Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 701 KB/s], Decompressed: 925
Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 85 KB/s], Decompressed: 925
Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 706 KB/s], Decompressed: 1025
Downloaded: 1172 file(s) [attempted 1172/8459 = 13%, 221 KB/s], Decompressed: 1025
Downloaded: 1216 file(s) [attempted 1216/8459 = 14%, 395 KB/s], Decompressed: 1114
Downloaded: 1257 file(s) [attempted 1257/8459 = 14%, 210 KB/s], Decompressed: 1114
Downloaded: 1298 file(s) [attempted 1298/8459 = 15%, 446 KB/s], Decompressed: 1189
Downloaded: 1336 file(s) [attempted 1336/8459 = 15%, 1214 KB/s], Decompressed: 1189
Downloaded: 1380 file(s) [attempted 1380/8459 = 16%, 263 KB/s], Decompressed: 1268
Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 80 KB/s], Decompressed: 1268
Downloaded: 1469 file(s) [attempted 1469/8459 = 17%, 1743 KB/s], Decompressed: 1350
Downloaded: 1511 file(s) [attempted 1511/8459 = 17%, 324 KB/s], Decompressed: 1350
Downloaded: 1552 file(s) [attempted 1552/8459 = 18%, 361 KB/s], Decompressed: 1435
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 413 KB/s], Decompressed: 1435
Downloaded: 1630 file(s) [attempted 1630/8459 = 19%, 77 KB/s], Decompressed: 1435
Downloaded: 1673 file(s) [attempted 1673/8459 = 19%, 120 KB/s], Decompressed: 1534
Downloaded: 1716 file(s) [attempted 1716/8459 = 20%, 258 KB/s], Decompressed: 1534
Downloaded: 1757 file(s) [attempted 1757/8459 = 20%, 74 KB/s], Decompressed: 1634
Downloaded: 1795 file(s) [attempted 1795/8459 = 21%, 283 KB/s], Decompressed: 1719
Downloaded: 1839 file(s) [attempted 1839/8459 = 21%, 460 KB/s], Decompressed: 1719
Downloaded: 1873 file(s) [attempted 1873/8459 = 22%, 217 KB/s], Decompressed: 1795
Downloaded: 1918 file(s) [attempted 1918/8459 = 22%, 384 KB/s], Decompressed: 1795
Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 128 KB/s], Decompressed: 1870
Downloaded: 2003 file(s) [attempted 2003/8459 = 23%, 108 KB/s], Decompressed: 1870
Downloaded: 2044 file(s) [attempted 2044/8459 = 24%, 66 KB/s], Decompressed: 1938
Downloaded: 2082 file(s) [attempted 2082/8459 = 24%, 93 KB/s], Decompressed: 1938
Downloaded: 2116 file(s) [attempted 2116/8459 = 25%, 109 KB/s], Decompressed: 2010
Downloaded: 2157 file(s) [attempted 2157/8459 = 25%, 117 KB/s], Decompressed: 2010
Downloaded: 2202 file(s) [attempted 2202/8459 = 26%, 523 KB/s], Decompressed: 2099
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 361 KB/s], Decompressed: 2099
Downloaded: 2284 file(s) [attempted 2284/8459 = 27%, 762 KB/s], Decompressed: 2198
Downloaded: 2328 file(s) [attempted 2328/8459 = 27%, 475 KB/s], Decompressed: 2198
Downloaded: 2369 file(s) [attempted 2369/8459 = 28%, 316 KB/s], Decompressed: 2198
Downloaded: 2390 file(s) [attempted 2390/8459 = 28%, 2741 KB/s], Decompressed: 2198
Downloaded: 2411 file(s) [attempted 2411/8459 = 28%, 96 KB/s], Decompressed: 2198
Downloaded: 2455 file(s) [attempted 2455/8459 = 29%, 80 KB/s], Decompressed: 2284
Downloaded: 2489 file(s) [attempted 2489/8459 = 29%, 713 KB/s], Decompressed: 2284
Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 303 KB/s], Decompressed: 2284
Downloaded: 2554 file(s) [attempted 2554/8459 = 30%, 115 KB/s], Decompressed: 2284
Downloaded: 2595 file(s) [attempted 2595/8459 = 30%, 1816 KB/s], Decompressed: 2435
Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 91 KB/s], Decompressed: 2435
Downloaded: 2674 file(s) [attempted 2674/8459 = 31%, 171 KB/s], Decompressed: 2565
Downloaded: 2715 file(s) [attempted 2715/8459 = 32%, 1189 KB/s], Decompressed: 2565
Downloaded: 2760 file(s) [attempted 2760/8459 = 32%, 1139 KB/s], Decompressed: 2565
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 69 KB/s], Decompressed: 2674
Downloaded: 2845 file(s) [attempted 2845/8459 = 33%, 105 KB/s], Decompressed: 2674
Downloaded: 2890 file(s) [attempted 2890/8459 = 34%, 978 KB/s], Decompressed: 2674
Downloaded: 2927 file(s) [attempted 2927/8459 = 34%, 234 KB/s], Decompressed: 2794
Downloaded: 2968 file(s) [attempted 2968/8459 = 35%, 835 KB/s], Decompressed: 2794
Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 387 KB/s], Decompressed: 2903
Downloaded: 3047 file(s) [attempted 3047/8459 = 36%, 156 KB/s], Decompressed: 2903
Downloaded: 3095 file(s) [attempted 3095/8459 = 36%, 192 KB/s], Decompressed: 2999
Downloaded: 3136 file(s) [attempted 3136/8459 = 37%, 1014 KB/s], Decompressed: 2999
Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 24 KB/s], Decompressed: 3087
Downloaded: 3215 file(s) [attempted 3215/8459 = 38%, 42 KB/s], Decompressed: 3087
Downloaded: 3256 file(s) [attempted 3256/8459 = 38%, 211 KB/s], Decompressed: 3160
Downloaded: 3294 file(s) [attempted 3294/8459 = 38%, 772 KB/s], Decompressed: 3232
Downloaded: 3338 file(s) [attempted 3338/8459 = 39%, 482 KB/s], Decompressed: 3232
Downloaded: 3376 file(s) [attempted 3376/8459 = 39%, 268 KB/s], Decompressed: 3290
Downloaded: 3413 file(s) [attempted 3413/8459 = 40%, 214 KB/s], Decompressed: 3345
Downloaded: 3454 file(s) [attempted 3454/8459 = 40%, 566 KB/s], Decompressed: 3394
Downloaded: 3499 file(s) [attempted 3499/8459 = 41%, 1868 KB/s], Decompressed: 3441
Downloaded: 3540 file(s) [attempted 3540/8459 = 41%, 3046 KB/s], Decompressed: 3489
Downloaded: 3581 file(s) [attempted 3581/8459 = 42%, 155 KB/s], Decompressed: 3489
Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 1009 KB/s], Decompressed: 3540
Downloaded: 3667 file(s) [attempted 3667/8459 = 43%, 624 KB/s], Decompressed: 3597
Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 84 KB/s], Decompressed: 3649
Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 488 KB/s], Decompressed: 3649
Downloaded: 3793 file(s) [attempted 3793/8459 = 44%, 644 KB/s], Decompressed: 3704
Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 109 KB/s], Decompressed: 3759
Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 1273 KB/s], Decompressed: 3810
Downloaded: 3916 file(s) [attempted 3916/8459 = 46%, 131 KB/s], Decompressed: 3810
Downloaded: 3958 file(s) [attempted 3958/8459 = 46%, 113 KB/s], Decompressed: 3862
Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 83 KB/s], Decompressed: 3920
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 121 KB/s], Decompressed: 3971
Downloaded: 4081 file(s) [attempted 4081/8459 = 48%, 174 KB/s], Decompressed: 3971
Downloaded: 4122 file(s) [attempted 4122/8459 = 48%, 99 KB/s], Decompressed: 4026
Downloaded: 4166 file(s) [attempted 4166/8459 = 49%, 57 KB/s], Decompressed: 4091
Downloaded: 4211 file(s) [attempted 4211/8459 = 49%, 49 KB/s], Decompressed: 4091
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 50 KB/s], Decompressed: 4091
Downloaded: 4289 file(s) [attempted 4289/8459 = 50%, 330 KB/s], Decompressed: 4091
Downloaded: 4331 file(s) [attempted 4331/8459 = 51%, 188 KB/s], Decompressed: 4091
Downloaded: 4368 file(s) [attempted 4368/8459 = 51%, 215 KB/s], Decompressed: 4091
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 309 KB/s], Decompressed: 4166
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 244 KB/s], Decompressed: 4166
Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 322 KB/s], Decompressed: 4166
Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 142 KB/s], Decompressed: 4166
Downloaded: 4591 file(s) [attempted 4591/8459 = 54%, 585 KB/s], Decompressed: 4166
Downloaded: 4635 file(s) [attempted 4635/8459 = 54%, 140 KB/s], Decompressed: 4399
Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 403 KB/s], Decompressed: 4399
Downloaded: 4717 file(s) [attempted 4717/8459 = 55%, 312 KB/s], Decompressed: 4399
Downloaded: 4758 file(s) [attempted 4758/8459 = 56%, 91 KB/s], Decompressed: 4399
Downloaded: 4806 file(s) [attempted 4806/8459 = 56%, 413 KB/s], Decompressed: 4399
Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 62 KB/s], Decompressed: 4597
Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 899 KB/s], Decompressed: 4597
Downloaded: 4947 file(s) [attempted 4947/8459 = 58%, 95 KB/s], Decompressed: 4597
Downloaded: 4988 file(s) [attempted 4988/8459 = 58%, 318 KB/s], Decompressed: 4597
Downloaded: 5025 file(s) [attempted 5025/8459 = 59%, 118 KB/s], Decompressed: 4597
Downloaded: 5066 file(s) [attempted 5066/8459 = 59%, 519 KB/s], Decompressed: 4854
Downloaded: 5111 file(s) [attempted 5111/8459 = 60%, 487 KB/s], Decompressed: 4854
Downloaded: 5155 file(s) [attempted 5155/8459 = 60%, 209 KB/s], Decompressed: 4854
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 93 KB/s], Decompressed: 4854
Downloaded: 5237 file(s) [attempted 5237/8459 = 61%, 49 KB/s], Decompressed: 5060
Downloaded: 5275 file(s) [attempted 5275/8459 = 62%, 1563 KB/s], Decompressed: 5060
Downloaded: 5316 file(s) [attempted 5316/8459 = 62%, 149 KB/s], Decompressed: 5060
Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 158 KB/s], Decompressed: 5060
Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 247 KB/s], Decompressed: 5060
Downloaded: 5450 file(s) [attempted 5450/8459 = 64%, 146 KB/s], Decompressed: 5060
Downloaded: 5487 file(s) [attempted 5487/8459 = 64%, 110 KB/s], Decompressed: 5224
Downloaded: 5522 file(s) [attempted 5522/8459 = 65%, 545 KB/s], Decompressed: 5224
Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 39 KB/s], Decompressed: 5224
Downloaded: 5610 file(s) [attempted 5610/8459 = 66%, 135 KB/s], Decompressed: 5224
Downloaded: 5652 file(s) [attempted 5652/8459 = 66%, 45 KB/s], Decompressed: 5224
Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 53 KB/s], Decompressed: 5456
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 679 KB/s], Decompressed: 5456
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 49 KB/s], Decompressed: 5456
Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 710 KB/s], Decompressed: 5456
Downloaded: 5853 file(s) [attempted 5853/8459 = 69%, 100 KB/s], Decompressed: 5662
Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 171 KB/s], Decompressed: 5662
Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 96 KB/s], Decompressed: 5662
Downloaded: 5973 file(s) [attempted 5973/8459 = 70%, 1958 KB/s], Decompressed: 5662
Downloaded: 6014 file(s) [attempted 6014/8459 = 71%, 1047 KB/s], Decompressed: 5819
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 230 KB/s], Decompressed: 5819
Downloaded: 6103 file(s) [attempted 6103/8459 = 72%, 28 KB/s], Decompressed: 5819
Downloaded: 6144 file(s) [attempted 6144/8459 = 72%, 68 KB/s], Decompressed: 5819
Downloaded: 6185 file(s) [attempted 6185/8459 = 73%, 695 KB/s], Decompressed: 6001
Downloaded: 6223 file(s) [attempted 6223/8459 = 73%, 304 KB/s], Decompressed: 6001
Downloaded: 6257 file(s) [attempted 6257/8459 = 73%, 72 KB/s], Decompressed: 6001
Downloaded: 6298 file(s) [attempted 6298/8459 = 74%, 705 KB/s], Decompressed: 6001
Downloaded: 6343 file(s) [attempted 6343/8459 = 74%, 57 KB/s], Decompressed: 6001
Downloaded: 6381 file(s) [attempted 6381/8459 = 75%, 37 KB/s], Decompressed: 6158
Downloaded: 6428 file(s) [attempted 6428/8459 = 75%, 295 KB/s], Decompressed: 6158
Downloaded: 6476 file(s) [attempted 6476/8459 = 76%, 1708 KB/s], Decompressed: 6158
Downloaded: 6521 file(s) [attempted 6521/8459 = 77%, 996 KB/s], Decompressed: 6158
Downloaded: 6565 file(s) [attempted 6565/8459 = 77%, 125 KB/s], Decompressed: 6158
Downloaded: 6606 file(s) [attempted 6606/8459 = 78%, 533 KB/s], Decompressed: 6377
Downloaded: 6641 file(s) [attempted 6641/8459 = 78%, 136 KB/s], Decompressed: 6377
Downloaded: 6682 file(s) [attempted 6682/8459 = 78%, 158 KB/s], Decompressed: 6377
Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 264 KB/s], Decompressed: 6377
Downloaded: 6774 file(s) [attempted 6774/8459 = 80%, 108 KB/s], Decompressed: 6377
Downloaded: 6815 file(s) [attempted 6815/8459 = 80%, 645 KB/s], Decompressed: 6589
Downloaded: 6860 file(s) [attempted 6860/8459 = 81%, 147 KB/s], Decompressed: 6589
Downloaded: 6897 file(s) [attempted 6897/8459 = 81%, 904 KB/s], Decompressed: 6589
Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 472 KB/s], Decompressed: 6589
Downloaded: 6979 file(s) [attempted 6979/8459 = 82%, 700 KB/s], Decompressed: 6589
Downloaded: 7020 file(s) [attempted 7020/8459 = 82%, 332 KB/s], Decompressed: 6589
Downloaded: 7068 file(s) [attempted 7068/8459 = 83%, 1271 KB/s], Decompressed: 6777
Downloaded: 7116 file(s) [attempted 7116/8459 = 84%, 301 KB/s], Decompressed: 6777
Downloaded: 7157 file(s) [attempted 7157/8459 = 84%, 99 KB/s], Decompressed: 6777
Downloaded: 7198 file(s) [attempted 7198/8459 = 85%, 91 KB/s], Decompressed: 6777
Downloaded: 7240 file(s) [attempted 7240/8459 = 85%, 95 KB/s], Decompressed: 6777
Downloaded: 7281 file(s) [attempted 7281/8459 = 86%, 177 KB/s], Decompressed: 6777
Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 73 KB/s], Decompressed: 6777
Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 82 KB/s], Decompressed: 6777
Downloaded: 7404 file(s) [attempted 7404/8459 = 87%, 428 KB/s], Decompressed: 7068
Downloaded: 7445 file(s) [attempted 7445/8459 = 88%, 615 KB/s], Decompressed: 7068
Downloaded: 7486 file(s) [attempted 7486/8459 = 88%, 485 KB/s], Decompressed: 7068
Downloaded: 7530 file(s) [attempted 7530/8459 = 89%, 615 KB/s], Decompressed: 7068
Downloaded: 7578 file(s) [attempted 7578/8459 = 89%, 65 KB/s], Decompressed: 7068
Downloaded: 7623 file(s) [attempted 7623/8459 = 90%, 107 KB/s], Decompressed: 7068
Downloaded: 7660 file(s) [attempted 7660/8459 = 90%, 76 KB/s], Decompressed: 7068
Downloaded: 7702 file(s) [attempted 7702/8459 = 91%, 417 KB/s], Decompressed: 7394
Downloaded: 7743 file(s) [attempted 7743/8459 = 91%, 87 KB/s], Decompressed: 7394
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 639 KB/s], Decompressed: 7394
Downloaded: 7828 file(s) [attempted 7828/8459 = 92%, 1890 KB/s], Decompressed: 7394
Downloaded: 7876 file(s) [attempted 7876/8459 = 93%, 570 KB/s], Decompressed: 7394
Downloaded: 7921 file(s) [attempted 7921/8459 = 93%, 32 KB/s], Decompressed: 7394
Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 184 KB/s], Decompressed: 7394
Downloaded: 7996 file(s) [attempted 7996/8459 = 94%, 113 KB/s], Decompressed: 7394
Downloaded: 8040 file(s) [attempted 8040/8459 = 95%, 850 KB/s], Decompressed: 7394
Downloaded: 8085 file(s) [attempted 8085/8459 = 95%, 537 KB/s], Decompressed: 7681
Downloaded: 8126 file(s) [attempted 8126/8459 = 96%, 363 KB/s], Decompressed: 7681
Downloaded: 8170 file(s) [attempted 8170/8459 = 96%, 790 KB/s], Decompressed: 7681
Downloaded: 8218 file(s) [attempted 8218/8459 = 97%, 157 KB/s], Decompressed: 7681
Downloaded: 8256 file(s) [attempted 8256/8459 = 97%, 1166 KB/s], Decompressed: 7681
Downloaded: 8294 file(s) [attempted 8294/8459 = 98%, 99 KB/s], Decompressed: 7681
Downloaded: 8331 file(s) [attempted 8331/8459 = 98%, 48 KB/s], Decompressed: 7681
Downloaded: 8376 file(s) [attempted 8376/8459 = 99%, 54 KB/s], Decompressed: 7681
Downloaded: 8420 file(s) [attempted 8420/8459 = 99%, 111 KB/s], Decompressed: 7681
Downloaded: 8454 file(s) [attempted 8454/8459 = 99%, 740 KB/s], Decompressed: 8047
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 740 KB/s], Decompressed: 8047

apx-runtime-resource-v1	apx-verifier-job-1536-runtime-lake_cache-893525-1785564208381277729-0	909312	1417216	21474836480	0	0	0	0	0	0	8566116352	8876122112	21474836480	0	0	0	0	0	0

lean_checkerexit 0duration 32m 1s · created 8/1/2026, 8:53:40 AM

lake build

✔ [1/79] Built Iut.Foundations.Species (447ms)
✔ [753/760] Built Iut.Foundations.RealLineCopy (1.9s)
✔ [754/760] Built Iut.Foundations.TransportDiagram (1.8s)
✔ [755/760] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [756/760] Built Iut.Foundations.RegionMeasure (1.6s)
✔ [757/760] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [758/760] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [759/835] Built Iut.Foundations.QualitativeData (2.1s)
✔ [3505/3508] Built Iut.Foundations.EtaleThetaQuotient (19s)
✔ [3506/3552] Built Iut.Foundations.Orbicurve (4.5s)
✔ [3953/3966] Built Iut.Foundations.InitialThetaData (19s)
✔ [3962/3968] Built Iut.Foundations.OrbicurvePullback (3.8s)
✔ [3965/3968] Built Iut.Foundations.EtaleThetaCovers (4.4s)
✔ [3967/3990] Built Iut.Foundations.SourceInitialThetaData (37s)
✔ [4109/4118] Built Iut.Foundations.SourceSemiGraph (1.0s)
✔ [4111/4119] Built Iut.Foundations.SourceSemiGraphAction (2.4s)
✔ [4113/4119] Built Iut.Foundations.SourceSemiGraphOfSubgroups (2.3s)
✔ [4116/4119] Built Iut.Foundations.SourceProfiniteCosetSystem (2.0s)
✔ [4117/4119] Built Iut.Foundations.SourceProfiniteSemiGraphSystem (75s)
✔ [4118/4145] Built Iut.Foundations.SourceInitialThetaDefinition (11s)
✔ [4152/4157] Built Iut.Foundations.KummerFaithfulness (2.1s)
✔ [4153/4158] Built Iut.Foundations.SourceTemperedSemigraph (5.3s)
✔ [4155/4158] Built Iut.Foundations.SourceMonoThetaEnvironment (7.8s)
✔ [4157/4168] Built Iut.Foundations.ContinuousH1 (6.4s)
✔ [4165/4172] Built Iut.Foundations.Procession (2.7s)
✔ [4168/4172] Built Iut.Foundations.SourceMLFKummerFaithfulness (3.1s)
✔ [4169/4172] Built Iut.Foundations.Frobenioid (6.4s)
✔ [4170/4172] Built Iut.Foundations.SourceThetaHodgeTheater (18s)
✔ [4171/4201] Built Iut.Foundations.SourceProcession (7.1s)
✔ [4186/4201] Built Iut.Foundations.SourceModelFrobenioid (5.6s)
✔ [4190/4207] Built Iut.Foundations.SourceAutHolomorphic (2.7s)
⚠ [4193/4212] 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`
✔ [4196/4212] Built Iut.Foundations.SourceTopologicalActionPairCategory (3.3s)
✔ [4197/4212] Built Iut.Foundations.SourceConjugateSynchronization (4.0s)
✔ [4198/4212] Built Iut.Foundations.SourceThetaSplitting (6.4s)
✔ [4199/4212] Built Iut.Foundations.SourceSplitKummerFrobenioid (7.6s)
✔ [4203/4212] Built Iut.Foundations.SourceHodgeArakelovEvaluation (4.0s)
✔ [4204/4212] Built Iut.Foundations.SourceArchimedeanKummerSystem (5.9s)
✔ [4206/4220] Built Iut.Foundations.SourceTimesMuPrimeStrip (9.6s)
✔ [4208/4220] Built Iut.Foundations.SourceTimesMuPrimeStripIsomorphism (15s)
✔ [4210/4220] Built Iut.Foundations.SourceFThetaBridge (3.8s)
✔ [4211/4220] Built Iut.Foundations.SourceTopologicalPseudoMonoid (4.7s)
✔ [4212/4221] Built Iut.Foundations.SourceArchimedeanSemiGerm (3.0s)
✔ [4214/4222] Built Iut.Foundations.SourceTimesMuPrimeStripFullPolyIsomorphism (8.0s)
✔ [4217/4222] Built Iut.Foundations.SourceTimesMuReconstructionAlgorithm (7.7s)
✔ [4221/4235] Built Iut.Foundations.SourceAutHolomorphicRigidity (2.6s)
⚠ [4255/4261] Built Iut.Foundations.SourceTheorem311 (121s)
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 `⊢`!
✔ [4256/4264] Built Iut.Foundations.SourceFiniteLocalMLFComparison (9.7s)
✔ [4257/4270] Built Iut.Foundations.SourceDefinition52LocalReconstruction (29s)
✔ [4259/4270] Built Iut.Foundations.SourceDefinition52LocalContinuity (14s)
✔ [4262/4270] Built Iut.Foundations.SourceAnabelioid (4.4s)
✔ [4263/4272] Built Iut.Foundations.SourceDefinition52LocalJointContinuity (5.1s)
✔ [4265/4275] Built Iut.Foundations.SourceDefinition52IndSystem (9.7s)
✔ [4270/4278] Built Iut.Foundations.SourceDefinition52Sequential (6.0s)
✔ [4273/4284] Built Iut.Foundations.SourcePrimeStripConstructions (3.9s)
✔ [4281/4327] Built Iut.Foundations.SourceAnabelioidEquivalence (2.0s)
✔ [4283/4327] Built Iut.Foundations.SourceSemiGraphOfAnabelioids (3.1s)
✔ [4284/4327] Built Iut.Foundations.ThetaHodgeTheater (6.9s)
✔ [4285/4327] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [4286/4327] Built Iut.SourceTrace.M1M3PaperLedger (8.5s)
✔ [4287/4327] Built Iut.Stage1.PilotComparison (1.6s)
✔ [4288/4327] Built Iut.Foundations.SourceContinuousAnabelioid (4.8s)
✔ [4290/4327] Built Iut.Foundations.SourceVerticalLogLink (5.7s)
✔ [4291/4327] Built Iut.Foundations.SourceTheorem311Horizontal (10s)
✔ [4292/4327] Built Iut.Foundations.SourceFiberFunctorComparison (2.3s)
✔ [4293/4327] Built Iut.Stage1.IUTStage1HodgeTheaterSource (2.0s)
✔ [4294/4327] Built Iut.Foundations.AlgorithmicBridge (2.8s)
✔ [4295/4327] Built Iut.Foundations.SourceAnabelioidSlice (17s)
✔ [4296/4327] Built Iut.Foundations.SourceTheorem311Assembly (7.5s)
✔ [4297/4327] Built Iut.Stage1.CorollarySchema (2.6s)
✔ [4298/4327] Built Iut.Foundations.SourceAnabelioidComponents (7.0s)
✔ [4299/4327] Built Iut.Stage1.SourceObligations (2.0s)
✔ [4300/4327] Built Iut.Foundations.SourceConnectedAnabelioidSlice (4.1s)
✔ [4301/4327] Built Iut.Stage1.IUTSourceScaffold (2.5s)
✔ [4302/4327] Built Iut.Foundations.SourceConnectedFiniteEtaleConverse (4.7s)
✔ [4303/4327] Built Iut.Stage1.IUTStage1Data (3.5s)
✔ [4304/4327] Built Iut.Foundations.SourceAnabelioidGrothendieck (3.8s)
⚠ [4305/4327] Built Iut.Stage1.IUTStage1SourceCore (74s)
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 `⊢`!
✔ [4306/4327] Built Iut.Stage1.IUTStage1Remark312Absorption (2.8s)
⚠ [4307/4327] 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`
✔ [4308/4327] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
⚠ [4309/4327] Built Iut.Stage1.IUTStage1StepX (5.5s)
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`
✔ [4310/4327] Built Iut.Stage1.IUTStage1Gaussian (7.9s)
✔ [4311/4327] Built Iut.Stage1.IUTStage1HodgeSHE (8.4s)
✔ [4312/4327] Built Iut.Stage1.IUTStage1HodgeArakelovPilots (6.6s)
⚠ [4313/4327] Built Iut.Stage1.IUTStage1Theorem311 (23s)
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`
✔ [4314/4327] Built Iut.Stage1.IUTStage1ConstructedTheorem311 (8.9s)
ℹ [4315/4327] Built Iut.Stage1.IUTStage1StepXI.Core (510s)
info: stderr:
PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x7e3d597c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7e3d597bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7e3d597bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x7e3d596eba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x7e3d596ebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7e3d597caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7e3d59632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7e3d59632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7e3d59633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7e3d596341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7e3d597c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7e3d59415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7e3d597c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7e3d597c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7e3d5979b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7e3d59415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7e3d54822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7e3d5460cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7e3d54169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7e3d54169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7e3d5104524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7e3d51045305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x6302eaf6a8da]
PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x7e3d597c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7e3d597bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7e3d597bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7e3d596f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7e3d596f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7e3d597caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7e3d59632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7e3d59632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7e3d59633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7e3d596341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7e3d597c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7e3d59415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7e3d597c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7e3d597c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7e3d5979b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7e3d59415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7e3d54822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7e3d5460cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7e3d54169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7e3d54169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7e3d5104524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7e3d51045305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x6302eaf6a8da]
✔ [4316/4327] Built Iut.Stage1.IUTStage1StepXI (2.6s)
ℹ [4317/4327] Built Iut.Stage1.IUTStage1FrobenioidShift (217s)
info: stderr:
PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x7ae73a3c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7ae73a3bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7ae73a3bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7ae73a2f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7ae73a2f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7ae73a3caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7ae73a232923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7ae73a232b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7ae73a233827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7ae73a2341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7ae73a3c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7ae73a015adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7ae73a3c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7ae73a3c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7ae73a39b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7ae73a015c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7ae735422638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7ae73520cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7ae734d69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7ae734d69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7ae731c4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7ae731c45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x6306e0b198da]
✔ [4318/4327] Built Iut.Stage1.IUTStage1EndpointAudit (3.6s)
✔ [4319/4327] Built Iut.Stage1.IUTStage1Source (3.5s)
✔ [4320/4327] Built Iut.Stage1.IUTStage1Experiments.Diagnostics (46s)
✔ [4321/4327] Built Iut.Stage1.IUTStage1Experiments.ClosedEndpoints (4.5s)
⚠ [4322/4327] Built Iut.Stage1.IUTStage1Experiments.AdditiveHaar (168s)
warning: Iut/Stage1/IUTStage1Experiments/AdditiveHaar.lean:41363:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
info: stderr:
PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x7fb2c4dc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7fb2c4dbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7fb2c4dbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x7fb2c4ceba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x7fb2c4cebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7fb2c4dcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7fb2c4c32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7fb2c4c32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7fb2c4c33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7fb2c4c341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7fb2c4dc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7fb2c4a15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7fb2c4dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7fb2c4dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7fb2c4d9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7fb2c4a15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7fb2bfe22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7fb2bfc0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7fb2bf769a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7fb2bf769f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7fb2bc64524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7fb2bc645305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x6444bf4e48da]
PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x7fb2c4dc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7fb2c4dbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7fb2c4dbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7fb2c4cf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7fb2c4cf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7fb2c4dcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7fb2c4c32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7fb2c4c32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7fb2c4c33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7fb2c4c341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7fb2c4dc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7fb2c4a15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7fb2c4dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7fb2c4dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7fb2c4d9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7fb2c4a15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7fb2bfe22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7fb2bfc0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7fb2bf769a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7fb2bf769f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7fb2bc64524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7fb2bc645305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x6444bf4e48da]
✔ [4323/4327] Built Iut.Stage1.IUTStage1StepXI.AdditiveHaarBridge (11s)
ℹ [4324/4327] Built Iut.Stage1.IUTStage1StepXIDependencyAudit (38s)
info: Iut/Stage1/IUTStage1StepXIDependencyAudit.lean:3961:0: 'Iut.Stage1.IUTStage1SourcePackage.IUTStage1Theorem311HullDetSourceConstructor.IUTStage1Theorem311OneSidedMultiradialConstructionSource.IUTStage1ConcreteTheorem311PrimitiveSourcePacket.ofSourceSpineDataOneSidedComponentSHECodomainSelectedLabelQPilotBridgeAlignmentOutputFlagCalibrationSource_packetConstructionAudit' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
✔ [4325/4327] Built Iut.Basic (3.1s)
✔ [4326/4327] Built Iut (3.1s)
Build completed successfully (4327 jobs).

apx-runtime-resource-v1	apx-verifier-job-1536-runtime-lean_checker-893525-1785564291536707917-1	933888	1179648	21474836480	0	0	0	0	0	0	1362489344	11202916352	21474836480	0	0	0	0	0	0

blueprint_buildexit 1duration 2s · created 8/1/2026, 8:53:40 AM

lake build :blueprint

error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1536-runtime-blueprint_build-893525-1785566212055662553-2	802816	1327104	21474836480	0	0	0	0	0	0	3317760	108191744	21474836480	0	0	0	0	0	0