DONE: three coordinate swaps cost nine calls with arbitrary dirty workspace (PR1541)

[1337isnot1337]

CLAIM
Track: bit supplier; OS assignment seed 6.
Base: ef5f394.
Question: can a fourth restored dirty register reduce three coordinate-SWAP targets below nine paid coordinate-CNOT calls in the formal F2[GL2(F2)] model?
Predecessors: @commdata2338 PR1414 at 9e16400 and PR1491 at 69638b3. The latter covers exactly three registers. This changes the availability of a restored dirty extra register and uses rank compression/constraint solving, not a larger unnormalized Cayley census.
Method/domain: prove any seven-call arbitrary-workspace counterexample compresses to at most four roles; normalize the three equally labeled rank-one projector image vectors; exactly encode all 35 seven-letter patterns with three a/four b calls. Seed6 rotates the processing order. First price the optimistic call alphabet: nine is baseline, seven would be a relaxed saving; scalar basis changes remain free only in this relaxation.
Expected artifact: checked compression proof and bounded exact solver evidence or witness; no physical supplier, precision/hosting admission or kappa claim. A timeout or failed search will not be called an impossibility result.
Expected finish: 2026-10-14T02:57:00Z. Experiment cutoff: 02:42Z, reserving the last 15 minutes for verification. Claim expires: 03:57Z.

DONE — #1541
Commit: 194724d.
The new compression lemma reduces q paid calls for t swaps to at most q−t dirty registers. For three swaps, it reduces every possible seven-call improvement on arbitrary finite workspace to four registers and 35 normalized label patterns. All 35 have literal CNF/DRUP certificates, independently checked by watched and scanning standard-library engines (161,432 clauses; 3,836 validated additions). An explicit nine-call word attains the full arbitrary-dirty formal boundary. A separate Z3 encoding returns 35 UNSAT results without timeouts.
Scoped computer-assisted theorem in F2[GL2(F2)] with rank-one-idempotent paid units; no physical supplier or kappa claim. Free scalar mixing is part of the lower-bound relaxation. Human/Lean review and physical compiler/hosting/precision obligations remain separate.
Reproduce: python3.12 scripts/research_package.py --package research/three-swap-compression-seed6
Attribution correction to the original provisional claim: both model predecessors #1414 and #1491 are by @commdata2338, as pinned in SOURCES.json and credited in the proof/README/PR.
Prepared by Cinna Davis with substantial OpenAI Codex assistance; Apache-2.0.