Verification run

Run 1070

promachina/iut-leanbranch mastertriggered via poller

failedcommit 9c075126c95dtoolchain lean-v4-30-0prover leantook 11m 17s · finished 9w 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/13/2026, 9:11:07 AM

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

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

git_checkoutexit 0duration 78 ms · created 7/13/2026, 9:11:07 AM

git checkout 9c075126c95d000d20987df0663212e2495b5913

Note: switching to '9c075126c95d000d20987df0663212e2495b5913'.

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 9c07512 Derive packet CTheta payload internally

lake_cacheexit 0duration 34s · created 7/13/2026, 9:11:07 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)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 11 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 5 KB/s], Decompressed: 11
Downloaded: 35 file(s) [attempted 35/8459 = 0%, 22 KB/s], Decompressed: 32
Downloaded: 63 file(s) [attempted 63/8459 = 0%, 28 KB/s], Decompressed: 58
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 430 KB/s], Decompressed: 82
Downloaded: 117 file(s) [attempted 117/8459 = 1%, 277 KB/s], Decompressed: 113
Downloaded: 148 file(s) [attempted 148/8459 = 1%, 133 KB/s], Decompressed: 145
Downloaded: 186 file(s) [attempted 186/8459 = 2%, 243 KB/s], Decompressed: 182
Downloaded: 218 file(s) [attempted 218/8459 = 2%, 287 KB/s], Decompressed: 213
Downloaded: 254 file(s) [attempted 254/8459 = 3%, 234 KB/s], Decompressed: 251
Downloaded: 289 file(s) [attempted 289/8459 = 3%, 94 KB/s], Decompressed: 285
Downloaded: 326 file(s) [attempted 326/8459 = 3%, 169 KB/s], Decompressed: 319
Downloaded: 364 file(s) [attempted 364/8459 = 4%, 29 KB/s], Decompressed: 357
Downloaded: 399 file(s) [attempted 399/8459 = 4%, 630 KB/s], Decompressed: 395
Downloaded: 433 file(s) [attempted 433/8459 = 5%, 264 KB/s], Decompressed: 429
Downloaded: 469 file(s) [attempted 469/8459 = 5%, 772 KB/s], Decompressed: 463
Downloaded: 508 file(s) [attempted 508/8459 = 6%, 645 KB/s], Decompressed: 501
Downloaded: 549 file(s) [attempted 549/8459 = 6%, 534 KB/s], Decompressed: 545
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 64 KB/s], Decompressed: 580
Downloaded: 622 file(s) [attempted 622/8459 = 7%, 306 KB/s], Decompressed: 617
Downloaded: 665 file(s) [attempted 665/8459 = 7%, 65 KB/s], Decompressed: 662
Downloaded: 705 file(s) [attempted 705/8459 = 8%, 28 KB/s], Decompressed: 693
Downloaded: 738 file(s) [attempted 738/8459 = 8%, 281 KB/s], Decompressed: 735
Downloaded: 778 file(s) [attempted 778/8459 = 9%, 412 KB/s], Decompressed: 771
Downloaded: 819 file(s) [attempted 819/8459 = 9%, 1826 KB/s], Decompressed: 812
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 431 KB/s], Decompressed: 860
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 636 KB/s], Decompressed: 906
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 161 KB/s], Decompressed: 939
Downloaded: 982 file(s) [attempted 982/8459 = 11%, 590 KB/s], Decompressed: 973
Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 427 KB/s], Decompressed: 1018
Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 184 KB/s], Decompressed: 1059
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 378 KB/s], Decompressed: 1100
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 157 KB/s], Decompressed: 1145
Downloaded: 1186 file(s) [attempted 1186/8459 = 14%, 549 KB/s], Decompressed: 1175
Downloaded: 1228 file(s) [attempted 1228/8459 = 14%, 82 KB/s], Decompressed: 1223
Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 96 KB/s], Decompressed: 1264
Downloaded: 1304 file(s) [attempted 1304/8459 = 15%, 805 KB/s], Decompressed: 1299
Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 213 KB/s], Decompressed: 1343
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 475 KB/s], Decompressed: 1381
Downloaded: 1429 file(s) [attempted 1429/8459 = 16%, 28 KB/s], Decompressed: 1422
Downloaded: 1468 file(s) [attempted 1468/8459 = 17%, 468 KB/s], Decompressed: 1459
Downloaded: 1500 file(s) [attempted 1500/8459 = 17%, 152 KB/s], Decompressed: 1497
Downloaded: 1545 file(s) [attempted 1545/8459 = 18%, 533 KB/s], Decompressed: 1538
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 33 KB/s], Decompressed: 1579
Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 1414 KB/s], Decompressed: 1620
Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 602 KB/s], Decompressed: 1661
Downloaded: 1709 file(s) [attempted 1709/8459 = 20%, 468 KB/s], Decompressed: 1702
Downloaded: 1747 file(s) [attempted 1747/8459 = 20%, 1000 KB/s], Decompressed: 1743
Downloaded: 1786 file(s) [attempted 1786/8459 = 21%, 104 KB/s], Decompressed: 1781
Downloaded: 1823 file(s) [attempted 1823/8459 = 21%, 474 KB/s], Decompressed: 1819
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 105 KB/s], Decompressed: 1860
Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 270 KB/s], Decompressed: 1901
Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 146 KB/s], Decompressed: 1935
Downloaded: 1983 file(s) [attempted 1983/8459 = 23%, 134 KB/s], Decompressed: 1976
Downloaded: 2021 file(s) [attempted 2021/8459 = 23%, 119 KB/s], Decompressed: 2017
Downloaded: 2063 file(s) [attempted 2063/8459 = 24%, 83 KB/s], Decompressed: 2058
Downloaded: 2101 file(s) [attempted 2101/8459 = 24%, 1400 KB/s], Decompressed: 2093
Downloaded: 2140 file(s) [attempted 2140/8459 = 25%, 880 KB/s], Decompressed: 2137
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 83 KB/s], Decompressed: 2175
Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 113 KB/s], Decompressed: 2212
Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 277 KB/s], Decompressed: 2253
Downloaded: 2295 file(s) [attempted 2295/8459 = 27%, 781 KB/s], Decompressed: 2291
Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 77 KB/s], Decompressed: 2329
Downloaded: 2377 file(s) [attempted 2377/8459 = 28%, 1023 KB/s], Decompressed: 2373
Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 172 KB/s], Decompressed: 2411
Downloaded: 2454 file(s) [attempted 2454/8459 = 29%, 542 KB/s], Decompressed: 2445
Downloaded: 2490 file(s) [attempted 2490/8459 = 29%, 382 KB/s], Decompressed: 2486
Downloaded: 2531 file(s) [attempted 2531/8459 = 29%, 657 KB/s], Decompressed: 2524
Downloaded: 2568 file(s) [attempted 2568/8459 = 30%, 480 KB/s], Decompressed: 2565
Downloaded: 2609 file(s) [attempted 2609/8459 = 30%, 243 KB/s], Decompressed: 2602
Downloaded: 2654 file(s) [attempted 2654/8459 = 31%, 611 KB/s], Decompressed: 2647
Downloaded: 2691 file(s) [attempted 2691/8459 = 31%, 348 KB/s], Decompressed: 2688
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 71 KB/s], Decompressed: 2722
Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 344 KB/s], Decompressed: 2763
Downloaded: 2811 file(s) [attempted 2811/8459 = 33%, 100 KB/s], Decompressed: 2804
Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 342 KB/s], Decompressed: 2839
Downloaded: 2890 file(s) [attempted 2890/8459 = 34%, 30 KB/s], Decompressed: 2880
Downloaded: 2931 file(s) [attempted 2931/8459 = 34%, 739 KB/s], Decompressed: 2924
Downloaded: 2974 file(s) [attempted 2974/8459 = 35%, 183 KB/s], Decompressed: 2965
Downloaded: 3011 file(s) [attempted 3011/8459 = 35%, 369 KB/s], Decompressed: 3006
Downloaded: 3051 file(s) [attempted 3051/8459 = 36%, 781 KB/s], Decompressed: 3047
Downloaded: 3089 file(s) [attempted 3089/8459 = 36%, 309 KB/s], Decompressed: 3085
Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 103 KB/s], Decompressed: 3126
Downloaded: 3171 file(s) [attempted 3171/8459 = 37%, 179 KB/s], Decompressed: 3164
Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 215 KB/s], Decompressed: 3205
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 24 KB/s], Decompressed: 3242
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 129 KB/s], Decompressed: 3287
Downloaded: 3335 file(s) [attempted 3335/8459 = 39%, 154 KB/s], Decompressed: 3328
Downloaded: 3373 file(s) [attempted 3373/8459 = 39%, 45 KB/s], Decompressed: 3366
Downloaded: 3410 file(s) [attempted 3410/8459 = 40%, 744 KB/s], Decompressed: 3403
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 398 KB/s], Decompressed: 3444
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 397 KB/s], Decompressed: 3485
Downloaded: 3532 file(s) [attempted 3532/8459 = 41%, 107 KB/s], Decompressed: 3523
Downloaded: 3572 file(s) [attempted 3572/8459 = 42%, 502 KB/s], Decompressed: 3564
Downloaded: 3611 file(s) [attempted 3611/8459 = 42%, 177 KB/s], Decompressed: 3602
Downloaded: 3648 file(s) [attempted 3648/8459 = 43%, 374 KB/s], Decompressed: 3643
Downloaded: 3687 file(s) [attempted 3687/8459 = 43%, 198 KB/s], Decompressed: 3681
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 135 KB/s], Decompressed: 3711
Downloaded: 3759 file(s) [attempted 3759/8459 = 44%, 120 KB/s], Decompressed: 3752
Downloaded: 3800 file(s) [attempted 3800/8459 = 44%, 290 KB/s], Decompressed: 3797
Downloaded: 3841 file(s) [attempted 3841/8459 = 45%, 590 KB/s], Decompressed: 3838
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 39 KB/s], Decompressed: 3882
Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 927 KB/s], Decompressed: 3930
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 164 KB/s], Decompressed: 3971
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 39 KB/s], Decompressed: 4009
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 385 KB/s], Decompressed: 4058
Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 80 KB/s], Decompressed: 4091
Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 79 KB/s], Decompressed: 4132
Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 105 KB/s], Decompressed: 4180
Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 160 KB/s], Decompressed: 4223
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 69 KB/s], Decompressed: 4262
Downloaded: 4305 file(s) [attempted 4305/8459 = 50%, 48 KB/s], Decompressed: 4297
Downloaded: 4345 file(s) [attempted 4345/8459 = 51%, 177 KB/s], Decompressed: 4341
Downloaded: 4386 file(s) [attempted 4386/8459 = 51%, 224 KB/s], Decompressed: 4382
Downloaded: 4424 file(s) [attempted 4424/8459 = 52%, 453 KB/s], Decompressed: 4416
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 108 KB/s], Decompressed: 4461
Downloaded: 4503 file(s) [attempted 4503/8459 = 53%, 341 KB/s], Decompressed: 4498
Downloaded: 4544 file(s) [attempted 4544/8459 = 53%, 147 KB/s], Decompressed: 4540
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 158 KB/s], Decompressed: 4577
Downloaded: 4617 file(s) [attempted 4617/8459 = 54%, 283 KB/s], Decompressed: 4605
Downloaded: 4652 file(s) [attempted 4652/8459 = 54%, 750 KB/s], Decompressed: 4649
Downloaded: 4700 file(s) [attempted 4700/8459 = 55%, 233 KB/s], Decompressed: 4694
Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 149 KB/s], Decompressed: 4741
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 213 KB/s], Decompressed: 4786
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 259 KB/s], Decompressed: 4830
Downloaded: 4884 file(s) [attempted 4884/8459 = 57%, 1074 KB/s], Decompressed: 4872
Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 215 KB/s], Decompressed: 4909
Downloaded: 4954 file(s) [attempted 4954/8459 = 58%, 134 KB/s], Decompressed: 4950
Downloaded: 4992 file(s) [attempted 4992/8459 = 59%, 133 KB/s], Decompressed: 4985
Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 120 KB/s], Decompressed: 5026
Downloaded: 5070 file(s) [attempted 5070/8459 = 59%, 61 KB/s], Decompressed: 5063
Downloaded: 5111 file(s) [attempted 5111/8459 = 60%, 152 KB/s], Decompressed: 5108
Downloaded: 5156 file(s) [attempted 5156/8459 = 60%, 146 KB/s], Decompressed: 5152
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 27 KB/s], Decompressed: 5197
Downloaded: 5243 file(s) [attempted 5243/8459 = 61%, 1618 KB/s], Decompressed: 5231
Downloaded: 5273 file(s) [attempted 5273/8459 = 62%, 415 KB/s], Decompressed: 5269
Downloaded: 5313 file(s) [attempted 5313/8459 = 62%, 212 KB/s], Decompressed: 5306
Downloaded: 5354 file(s) [attempted 5354/8459 = 63%, 827 KB/s], Decompressed: 5351
Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 363 KB/s], Decompressed: 5395
Downloaded: 5447 file(s) [attempted 5447/8459 = 64%, 481 KB/s], Decompressed: 5443
Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 114 KB/s], Decompressed: 5481
Downloaded: 5525 file(s) [attempted 5525/8459 = 65%, 145 KB/s], Decompressed: 5519
Downloaded: 5563 file(s) [attempted 5563/8459 = 65%, 294 KB/s], Decompressed: 5560
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 21 KB/s], Decompressed: 5597
Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 27 KB/s], Decompressed: 5642
Downloaded: 5690 file(s) [attempted 5690/8459 = 67%, 220 KB/s], Decompressed: 5683
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 668 KB/s], Decompressed: 5724
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 288 KB/s], Decompressed: 5765
Downloaded: 5813 file(s) [attempted 5813/8459 = 68%, 648 KB/s], Decompressed: 5806
Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 358 KB/s], Decompressed: 5847
Downloaded: 5892 file(s) [attempted 5892/8459 = 69%, 179 KB/s], Decompressed: 5888
Downloaded: 5929 file(s) [attempted 5929/8459 = 70%, 60 KB/s], Decompressed: 5926
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 225 KB/s], Decompressed: 5967
Downloaded: 6011 file(s) [attempted 6011/8459 = 71%, 121 KB/s], Decompressed: 6008
Downloaded: 6050 file(s) [attempted 6050/8459 = 71%, 362 KB/s], Decompressed: 6042
Downloaded: 6091 file(s) [attempted 6091/8459 = 72%, 1343 KB/s], Decompressed: 6083
Downloaded: 6131 file(s) [attempted 6131/8459 = 72%, 237 KB/s], Decompressed: 6128
Downloaded: 6176 file(s) [attempted 6176/8459 = 73%, 687 KB/s], Decompressed: 6165
Downloaded: 6210 file(s) [attempted 6210/8459 = 73%, 160 KB/s], Decompressed: 6203
Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 99 KB/s], Decompressed: 6237
Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 435 KB/s], Decompressed: 6282
Downloaded: 6330 file(s) [attempted 6330/8459 = 74%, 594 KB/s], Decompressed: 6326
Downloaded: 6374 file(s) [attempted 6374/8459 = 75%, 185 KB/s], Decompressed: 6371
Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 85 KB/s], Decompressed: 6398
Downloaded: 6446 file(s) [attempted 6446/8459 = 76%, 317 KB/s], Decompressed: 6439
Downloaded: 6487 file(s) [attempted 6487/8459 = 76%, 183 KB/s], Decompressed: 6484
Downloaded: 6529 file(s) [attempted 6529/8459 = 77%, 261 KB/s], Decompressed: 6525
Downloaded: 6569 file(s) [attempted 6569/8459 = 77%, 23 KB/s], Decompressed: 6566
Downloaded: 6610 file(s) [attempted 6610/8459 = 78%, 307 KB/s], Decompressed: 6607
Downloaded: 6648 file(s) [attempted 6648/8459 = 78%, 50 KB/s], Decompressed: 6641
Downloaded: 6686 file(s) [attempted 6686/8459 = 79%, 225 KB/s], Decompressed: 6682
Downloaded: 6727 file(s) [attempted 6727/8459 = 79%, 1553 KB/s], Decompressed: 6723
Downloaded: 6771 file(s) [attempted 6771/8459 = 80%, 313 KB/s], Decompressed: 6764
Downloaded: 6809 file(s) [attempted 6809/8459 = 80%, 532 KB/s], Decompressed: 6804
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 124 KB/s], Decompressed: 6836
Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 674 KB/s], Decompressed: 6881
Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 220 KB/s], Decompressed: 6922
Downloaded: 6970 file(s) [attempted 6970/8459 = 82%, 529 KB/s], Decompressed: 6966
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 457 KB/s], Decompressed: 7004
Downloaded: 7048 file(s) [attempted 7048/8459 = 83%, 573 KB/s], Decompressed: 7045
Downloaded: 7087 file(s) [attempted 7087/8459 = 83%, 225 KB/s], Decompressed: 7083
Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 339 KB/s], Decompressed: 7124
Downloaded: 7172 file(s) [attempted 7172/8459 = 84%, 147 KB/s], Decompressed: 7168
Downloaded: 7213 file(s) [attempted 7213/8459 = 85%, 42 KB/s], Decompressed: 7199
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 435 KB/s], Decompressed: 7240
Downloaded: 7288 file(s) [attempted 7288/8459 = 86%, 173 KB/s], Decompressed: 7281
Downloaded: 7326 file(s) [attempted 7326/8459 = 86%, 74 KB/s], Decompressed: 7322
Downloaded: 7370 file(s) [attempted 7370/8459 = 87%, 103 KB/s], Decompressed: 7367
Downloaded: 7411 file(s) [attempted 7411/8459 = 87%, 143 KB/s], Decompressed: 7404
Downloaded: 7452 file(s) [attempted 7452/8459 = 88%, 315 KB/s], Decompressed: 7445
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 134 KB/s], Decompressed: 7486
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 567 KB/s], Decompressed: 7527
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 296 KB/s], Decompressed: 7565
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 220 KB/s], Decompressed: 7606
Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 43 KB/s], Decompressed: 7640
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 289 KB/s], Decompressed: 7685
Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 957 KB/s], Decompressed: 7730
Downloaded: 7771 file(s) [attempted 7771/8459 = 91%, 84 KB/s], Decompressed: 7764
Downloaded: 7808 file(s) [attempted 7808/8459 = 92%, 24 KB/s], Decompressed: 7801
Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 1095 KB/s], Decompressed: 7839
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 258 KB/s], Decompressed: 7883
Downloaded: 7935 file(s) [attempted 7935/8459 = 93%, 274 KB/s], Decompressed: 7931
Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 156 KB/s], Decompressed: 7972
Downloaded: 8011 file(s) [attempted 8011/8459 = 94%, 59 KB/s], Decompressed: 8003
Downloaded: 8051 file(s) [attempted 8051/8459 = 95%, 99 KB/s], Decompressed: 8044
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 105 KB/s], Decompressed: 8089
Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 498 KB/s], Decompressed: 8137
Downloaded: 8185 file(s) [attempted 8185/8459 = 96%, 116 KB/s], Decompressed: 8181
Downloaded: 8226 file(s) [attempted 8226/8459 = 97%, 868 KB/s], Decompressed: 8215
Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 486 KB/s], Decompressed: 8256
Downloaded: 8301 file(s) [attempted 8301/8459 = 98%, 585 KB/s], Decompressed: 8291
Downloaded: 8337 file(s) [attempted 8337/8459 = 98%, 79 KB/s], Decompressed: 8332
Downloaded: 8380 file(s) [attempted 8380/8459 = 99%, 49 KB/s], Decompressed: 8376
Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 656 KB/s], Decompressed: 8421
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 158 KB/s], Decompressed: 8448
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 158 KB/s], Decompressed: 8448

lean_checkerexit 1duration 7m 31s · created 7/13/2026, 9:11:07 AM

lake build

✔ [753/764] Built Iut.Foundations.RealLineCopy (24s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.5s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.6s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/775] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.7s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (34s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (2.0s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3393/3398] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (84s)
warning: Iut/Stage1/IUTStage1SourceCore.lean:19880: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:20063: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:20130: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:20530: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:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20532:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530: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:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20533:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530: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:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20537: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:20530: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:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20547:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570: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:20572:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570: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:20573:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570: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:20576:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570: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:20577:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570: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:20578:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (22s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698: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:5776: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:5822: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:5943: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:5991: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:6100:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.0s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.6s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.3s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (28s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4518: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:4523: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:4655: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:4687: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:4692: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:4735: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:4789: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:4824: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:4829: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:4961: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:4995: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:5000: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:5138: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:5172: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:5177: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:5320: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:5352: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:5357: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:5470: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:7525:6: try 'simp' instead of 'simpa'

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

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

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

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

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✖ [3418/3425] Building Iut.Stage1.IUTStage1StepXI (168s)
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.lean -o /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.olean -i /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.ilean -c /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.c --setup /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.setup.json --json
error: Lean exited with code 137
Some required targets logged failures:
- Iut.Stage1.IUTStage1StepXI

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: build failed

blueprint_buildexit 1duration 1s · created 7/13/2026, 9:11:07 AM

lake build :blueprint

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: unknown package facet `blueprint`