DONE: coordinate-CNOT label saturation; four swaps need ten or twelve calls

[RossRichardson]

DONE / FINDING — PR #1722, exact head 246cd6b3a795a346bc6a741661ddcdb2d6359103. Claim released.

The label-saturation theorem is proved in the stated formal coordinate-CNOT model: for t swaps with arbitrary finite restored dirty workspace, n_a=t forces n_b>=2t, and symmetrically. At the saturated 3t boundary, the normalized paid projectors do not couple the dirty complement. The chronological covector-span argument and full sign matrix give the missing rank inequality.

Consequences: an analytic alternative proof of Cinna Davis's PR1541 three-swap minimum nine (predecessor priority retained), and a four-swap minimum of ten or twelve, strengthening Aaron Wang's PR1705 finite boundary. A ten-call word must use five of each label; PR1541's credited compression puts it on at most six roles. Neither existence nor exclusion of that balanced case is claimed.

Evidence: registered Python 3.12.12 replay and all five corruption/relocation test groups pass on the committed head; optimized Python 3.14.6 agrees. Two separately implemented formal/faithful-regular engines agree on complete small-domain state hashes and all 1,296 literal shortest two-swap words. All 648 saturated words satisfy the intermediate proof traces. Twenty-five larger positive words, 1,080 faithful columns, 235 omission controls and 15 primary controls pass. Selected-record validation passes. Full all-register proof is written, not Lean- or human-verified.

Reproduce: python3.12 -I -B scripts/research_package.py --package research/coordinate-cnot-label-saturation.

HANDOFF: the sole four-swap improvement case is a full formal ten-call 5+5 word on at most six roles, including every dirty column. First use a proof-producing encoding of that domain; the present lemma does not decide it. No new kappa, selected supplier, complete cold replay, physical/compiler/hosting/precision/tape or analytic admission. Hosted CI was 61 queued checks at readback, separate from local verification.

Final overlap at 07:49 UTC covered 408 open PRs and 358 Discussion records with complete pagination/no warnings; relevant predecessor heads were rechecked unchanged. Credit commdata2338 PR1414/1491, Gareth Davidson PR1333, Cinna Davis PR1541, Aaron Wang PR1705 and the eumemic/Ali Romman/David Govea lineage. Ross Richardson with substantial OpenAI Codex assistance, one agent; Apache-2.0.

Original bounded claim

CLAIM — coordinate-CNOT label saturation (bit-new-register-model, priority revision 3).

Question: For t coordinate-SWAP targets in formal F2[GL2(F2)] with any finite restored dirty workspace, does exactly t calls of one coordinate-CNOT label force at least 2t calls of the other? Investigate the rank-one factorization of the other-label sum, retaining augmentation and sign-quotient constraints.

Base: 0b1cccf. Chooser nonce 8e7454be62cc38c3ccc7edd6bd6d2bc2, selected-record SHA256 10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32. The nonabelian binary address alphabet deliberately replaces the rational abelian starting model; rational frames are not reduced mod 2.

Exact scope: paid calls I+([g]+1)uv^T, g in {a,b}, v^T u=1, with free scalar GL_r(F2) mixing normalized by augmentation. Target diag([aba] repeated t times, 1 on all dirty extras). Every paid call and undo is charged; no free address maps, copies, erasure or clean allocation. Direct upper bill is 3t.

Expected artifact: a short uniform proof or counterexample, exact finite corroboration and full formal controls. If saturation holds, it gives an analytic alternative to the three-swap finite step and narrows four-swap candidates to ten calls with five of each label (or the direct twelve). The ten-call balanced case is explicitly outside this session.

Predecessor credit: commdata2338 PR1414/1491 (model, sign argument, finite three-swap result), Gareth Davidson PR1333 (free-scalar normalization), Cinna Davis PR1541 at 194724d (arbitrary-workspace three-swap theorem and role compression), Aaron Wang PR1705 at ad6b7d6 (four-swap finite bounds). This complements their results; it does not repeat their census or claim a new supplier/kappa.

Entry overlap: 398 open PRs and 353 Discussion records, complete pagination at 07:30–07:32 UTC; targeted labels/saturation/four-swap search and exact proof reads. Coverage excludes arbitrary diffs/nested files and does not certify novelty.

Claim expires 2026-10-14 09:35 UTC. Prepared for Ross Richardson with substantial OpenAI Codex assistance. Apache-2.0.