[jwr404]

Result

This follows up the open question of #4950 (pending): do mixed coordinate-swap targets also cost three calls each in #4939's formal M_R(F2[GL_n(F2)]) model?

1. Theorem. Assign a row transposition τ_r to each target register, possibly on different coordinate pairs. If every component of the target graph on coordinates has at most 3 vertices, the targets cost exactly 3t paid calls, for every n and R. The proof sums a cut per component in the regular representation:

   • a row-pair cut {r_a < r_b} for a single edge;
   • a triple-parity cut, the even relative orders of rows a, b, c, for a 2-path or a triangle.

   Averaged over all orders of the nonzero vectors, every CNOT costs at most one unit and every target earns three. This follows from exchangeability of 3 or 4 random vectors.

2. Exact formal minima at n = 3, R = 2.

   • diag([s01],[s12]) = 6.
   • A 3-cycle = 6.
   • A census of all 28,211 pairs (g,h) ∈ GL_3(F2)^2 finds none below min(ℓ(g)+ℓ(h), 6), where ℓ is the CNOT word length.

3. Limits. Order-pattern cuts certify only 3 of 6 for a 3-cycle, and 8.33 and 8.14 of 9 for the 3-edge path and star at n = 4. A scratch column-generation run over all permutation cuts of the GL_3 regular representation stopped at 3.51 for the 3-cycle (not certified optimal). That is recorded as the open question.

No new κ. The selected exponent stays 60403/20000000. This is a negative formal-model screen.

Task and overlap

Card bit-new-register-model, scope changed (see TASK.json). Base: canonical main cef4b52f2a59009865bf8eabde1be3f159063703. This builds on pending #4950 and #4939. The overlap search is the one recorded for #4950; no n >= 3 mixed-target work was found. The LP figures came from scipy/HiGHS in a scratch environment and are not part of the package.

Test plan

python3.12 -B scripts/research_package.py --package research/swap-component-cut --check-only
python3.12 -B scripts/research_package.py --package research/swap-component-cut
python3.12 -I -O -W error -B research/swap-component-cut/verify.py
python3.12 -B scripts/check_research_commit.py --package research/swap-component-cut

All four pass locally on Linux with Python 3.12.

• verify.py takes about 3 s. It checks the exchangeability lemmas, the averaged regular-representation counts over all 5,040 GL_3 orders, the exact formal minima and the attaining word.
• census.py takes about 20 seconds. It is the all-pairs census, reduced to 1,248 orbit representatives under coordinate-permutation conjugation, inverse transpose and register exchange, with orbit coverage of all 28,211 pairs checked. (The first CI run timed out before this reduction.)
• Three mutations make the verifier fail.
• --check-source-history was not run locally because the checkout is shallow.

Credit

• Mihir Srivastava (Prove six-call two-SWAP cost with arbitrary address spectators #4939).
• PR1989 and the GL2 corollary.
• commdata2338 (PR1414/PR1495).
• PR1541.
• Gareth Davidson (PR1333).

Prepared by James Reed with substantial Anthropic Claude (Claude Code) assistance. Apache-2.0. No independent human review.

🤖 Generated with Claude Code