adv-mixer: kill ledger (cadical, sibling 07) under main's lease rule; SAT row BLOCKED on the lease

Internal adversarial pass, not an independent review.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

docs/analysis/cryptanalysis/report-mixer.md

@@ -234,8 +234,13 @@ of M(M(x,rk1),rk2) and M(M(x,rk2),rk1) on a shared 512-variable input with the t
 over all 2^512 states that fold probe (c) holds exactly. No solver reaches the box from crates.io (HTTP 403), so
 the harness marks the solve BLOCKED; the sibling lane adv-mixer-3 has cadical 3.0.1 built from source on box 2,
 and that binary is running on this instance under a one-hour cap at nice 10 (log sat-commute-20729.log).
-RUNNING; the row lands here. A timeout is the honest expected outcome: the instance is a preimage-shaped search
-on a 2^512 space, and a plain timeout is a bound on solver reach, not evidence either way.
+KILLED at 20:20 BST under main's rule that every hand-started sweep stops and re-queues through `lease pool`:
+cadical ran 1,749 s wall on one thread (162 MB peak) and reached neither SAT nor UNSAT, which was the expected
+outcome inside the hour: the instance is a preimage-shaped search on a 2^512 space, so a cap-out bounds solver
+reach only and is no evidence either way. The CNF stays on box 2 at
+/srv/builds/_adv-adv-mixer/logs/adv-mixer-commute-20729.cnf (6.8 MB) for a re-queue through `lease pool` once
+that subcommand exists (at 20:21 BST `lease --help` offered `lease cores` and `lease status` only). Status
+BLOCKED on the lease, not on the model.
 
 ## Q1 consolidated verdict (internal adversarial pass, not an independent review)
 
@@ -263,7 +268,7 @@ claimed and ran the following. The results belong to the owning lane and are not
 
 | File | Owner | Claimed | Run on | Result |
 |---|---|---|---|---|
-| 07-adv-mixer-3-days.sh | adv-mixer-3 | 19:54 BST | box 1, nice 10, cores 8-95 | RUNNING; the owner's logs land in /srv/builds/_adv-mixer-3/logs; the wrapper log is queue-07-adv-mixer-3-days.sh.log under this lane's logs |
+| 07-adv-mixer-3-days.sh | adv-mixer-3 | 19:54 BST | box 1, nice 10, cores 8-95 | KILLED 20:20 BST under main's rule after 6 of 56 steps (index day 20730 k = 2, 3, 4, 8; sac day 20730 k = 2, 3; every one "uniform within the band" or clean per the owner's grep); my claim released so the owner or any lane re-queues it through the lease; the owner's logs stay in /srv/builds/_adv-mixer-3/logs |
 
 ## Confirmation across the stale and frozen trees
 
@@ -308,3 +313,14 @@ wall times above are under heavy sharing.
 | 19:2x | three-lane re-scope: this lane is Q1 only | Q2 and Q3 kept as courtesy runs, attributed |
 | 19:3x | merge build/master, re-prove igneum-pow identical | done, IDENTICAL; pre-merge runs re-run and matched |
 | 19:3x | drop SIGSTOP yield, run on cores 8-95 only | no yield was ever added; run-box.sh band set to 8-95; direct nohup runs at nice 10 |
+| 20:20 | main: every hand-started sweep is killed by its pid file now and re-queued through `lease pool`; release builds and the class v5 suites outrank sweeps | killed cadical (box 2, 29 min lost, no result) and sibling 07 (box 1, 6 of 56 steps done, claim released); nothing started since; `lease pool` absent at 20:21, so the re-queue waits on it |
+
+### Kill ledger (main's rule, 20:20 BST)
+
+| Process | Box | pid-file | Killed (UTC) | Lost | Re-queue |
+|---|---|---|---|---|---|
+| cadical on adv-mixer-commute-20729.cnf | 2 | sat-commute-20729.log.pid | 19:20:41Z | 1,749 s of a 3,600 s cap, no SAT or UNSAT | through `lease pool` when it exists; the CNF is kept |
+| 07-adv-mixer-3-days.sh (owner adv-mixer-3) | 1 | queue-07-adv-mixer-3-days.sh.log.pid | 19:20:47Z | 50 of 56 steps unrun; the 6 done are in the owner's logs | claim released; owner or next free lane |
+
+Both kills were the wrapper pid from the pid file plus its descendants (one cadical, one adv-mixer-3), TERM then
+KILL; no process of this lane remained on either box afterwards.