Mixed transposition targets cost three calls each when components have at most three coordinates (no new κ)

research/swap-component-cut/README.md

@@ -0,0 +1,152 @@
+# Mixed transposition targets cost three calls each
+
+**Scoped formal-model theorem, exact finite minima and a census. No new κ.**
+The selected conditional exponent stays 60403/20000000.
+
+## Result
+
+The model is the formal `M_R(F2[GL_n(F2)])` model of
+[#4939](https://github.com/CrocSwap/integer-mult-bounds/pull/4939). Each
+target register `r` carries the row transposition `τ_r` of some coordinate
+pair `{a_r, b_r}`, and different registers may use different pairs. Build
+the **target graph** on the coordinates: it has one edge `{a_r, b_r}` per
+target.
+
+1. **Theorem.** Suppose every connected component of the target graph has at
+   most three vertices. Then the `t` targets cost **exactly `3t` paid calls**.
+   This holds for every `n ≥ 2` and `R ≥ t`, with free scalar mixing and
+   restored dirty registers. It answers [#4950](https://github.com/CrocSwap/integer-mult-bounds/pull/4950)'s
+   open question for these targets: mixed swaps such as `(0,1)` on one
+   register and `(1,2)` on another cost 6, with nothing shared.
+2. **Exact minima at `n = 3`, `R = 2`.**
+   - `diag([s01],[s12])` costs exactly 6.
+   - A coordinate 3-cycle costs exactly 6, even with a dirty register.
+   - For **every** pair `(g, h)` in `GL_3(F2)^2`, `diag([g],[h])` costs at
+     least `min(ℓ(g)+ℓ(h), 6)`, where `ℓ` is the CNOT word length. So the
+     cost is additive whenever `ℓ(g)+ℓ(h) ≤ 6`.
+3. **Limits of the method.** Cuts built from the relative order of the rows
+   (order patterns) do not reach every target, by exact LP over all subsets:
+   - for a 3-cycle at `n = 3` they certify only 3 of the 6 calls;
+   - at `n = 4` they certify `8.33` for the 3-edge path and `8.14` for the
+     3-edge star. Both round up to the true 9, but no clean cut exists there.
+
+## Proof of the theorem
+
+Use the regular representation of `G = GL_n(F2)`, as in #4950. For a cut
+`A ⊆ G` let `out(g) = |{x ∈ A : g x ∉ A}|`. The crossing rank
+`q(M) = rank M[A^c ⊗ F2^R, A ⊗ F2^R]` is subadditive, and it gives:
+
+- `out(g)` for a paid call;
+- 0 for a free scalar map;
+- `Σ_r out(τ_r)` for the target.
+
+Fix a linear order on the nonzero vectors, and sum every cut below over all
+orders. A CNOT writing row `i` replaces `r_i` by `w = r_i + r_j`, a vector
+distinct from all rows. Averaged over orders, the relative order of
+`r_0, …, r_{n−1}, w` is uniform. So only exchangeability of a few random
+items matters. Write `u = |G|/6` per order.
+
+- **Pair cut** on `{a, b}`: `A = {r_a < r_b}`.
+  - A CNOT writing `a` or `b` leaves with probability `P(r_a < r_b < w) = 1/6`,
+    which is `u`.
+  - A CNOT writing any other row costs 0.
+  - The transposition of `a` and `b` moves all of `A` out: `3u`.
+- **Triple parity cut** on `{a, b, c}`: `A` is the set of `x` whose rows
+  `a, b, c` appear in an even-sign relative order.
+  - Over the 24 orders of `{r_a, r_b, r_c, w}`, a CNOT writing `a` starts in
+    `A` and flips parity in exactly 4, which is `u`. The same holds for `b`
+    and `c`.
+  - CNOTs writing other rows cost 0.
+  - Each of the three transpositions inside the triple flips parity: `3u`.
+
+Give each component of the target graph one cut. A single edge, with any
+multiplicity, gets its pair cut. A 2-path or a triangle gets the parity cut
+of its three vertices. Components have disjoint vertex sets, so:
+
+- each CNOT writes a row in at most one component, which bounds every paid
+  call by `u`;
+- each target contributes `3u` to its own component's cut.
+
+Hence `calls · u ≥ 3t · u`. Each transposition takes three CNOTs on its own
+register, so `3t` is attained.
+
+A single pair cut fails on a 2-path: `τ_{12}` contributes only `u` to the
+pair cut `{0 < 1}`. That is why the parity cut is needed. The parity cut
+works only for three rows. For four rows, a reinsertion flips parity with
+probability `2/5` rather than `1/3`.
+
+## Evidence
+
+`verify.py`, exact, about three seconds, checks:
+
+- both exchangeability lemmas, over all 6 and all 24 relative orders;
+- the averaged cut counts in the `GL_3` regular representation over all
+  5,040 orders, for every CNOT and transposition under the pair and parity
+  cuts;
+- formal minima by meet-in-the-middle with a 26,551-element forward ball:
+  `s01+s12` has no word of length at most 5 and has one of length 6, and the
+  same holds for the 3-cycle;
+- the nine-call word for the 3-edge path at `n = 4`, `R = 3`.
+
+`census.py`, exact, about 20 seconds, checks all 28,211 pairs at `n = 3`,
+`R = 2`: none has a formal word shorter than `min(ℓ(g)+ℓ(h), 6)`.
+
+The LP figures in item 3 come from an exact enumeration of all 64 pattern
+subsets at `n = 3`, and from column generation with MILP pricing at `n = 4`.
+Both ran on scipy/HiGHS in a scratch environment. They are not part of the
+package, and the theorem does not use them.
+
+## Scope
+
+Card `bit-new-register-model`, scope **changed** (see `TASK.json`). This is a
+negative formal-model screen, not a native construction.
+
+The theorem does **not** cover target components with four or more
+vertices, cycles of three or more coordinates in one register, other group
+elements, or other tariffs. The census covers only `n = 3` with at most two
+registers.
+
+Base: canonical main `cef4b52f2a59009865bf8eabde1be3f159063703`, priority
+revision 7. This builds on pending #4950 and pending #4939. The overlap
+search is the one recorded for #4950. No other `n ≥ 3` mixed-target work
+was found, which is not a novelty proof.
+
+## Reproduce
+
+```sh
+python3.12 -B research/swap-component-cut/verify.py
+python3.12 -B research/swap-component-cut/census.py
+python3.12 -B scripts/research_package.py --package research/swap-component-cut
+```
+
+## Open next questions
+
+1. **Are costs additive across several targets that are not transpositions in
+   small components?** Examples are two 3-cycles on two registers, or a
+   3-edge transposition path or star. A *single* target is settled: pending
+   [#4974](https://github.com/CrocSwap/integer-mult-bounds/pull/4974)'s
+   support lemma shows that one target `[g]` costs at least the CNOT word
+   length `ℓ_{GL_n}(g)`. With the trivial one-register word, this makes the
+   cost exactly `ℓ_{GL_n}(g)`. In particular a 3-cycle costs 6 for every `n`
+   and `R`. Support bounds only the largest single target, though. For several
+   targets, order-pattern cuts are not tight: 3 of 6 for a 3-cycle at
+   `n = 3`, 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 stopped at 3.51
+   for the 3-cycle; it is not certified optimal. *First step:* run the exact
+   formal search for `diag([c3],[c3])` at `n = 3`, `R = 2`, up to length 11,
+   or find a cut that combines with the support argument. *Blocked by:*
+   nothing.
+
+## Credit
+
+- Mihir Srivastava, #4939, for the spectator model.
+- PR1989 and the GL2 corollary, for the cut method.
+- commdata2338, PR1414/PR1495.
+- PR1541.
+- Gareth Davidson/PR1333.
+
+Their notes keep their earlier credit.
+
+Prepared by James Reed with substantial Anthropic Claude (Claude Code)
+assistance. Apache-2.0. No independent human review and no formal-kernel
+acceptance are claimed.

research/swap-component-cut/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/gl2-swap-cut-corollary/README.md",
+      "usage": "provenance",
+      "git_blob": "c34c1460063ee4690c934d3c3fb3d81896f8931c",
+      "sha256": "3650918994be00323ccb61b75cdd81ecae47104a6e0765e319196618737949d9"
+    },
+    {
+      "path": "research/coordinate-cnot-address-spectator/README.md",
+      "usage": "provenance",
+      "git_blob": "15b3db71d9fc13b4e9806caf42dd56213936fc88",
+      "sha256": "f433d3891cdc88fb47e055c4246798980529268a9a17250574414f805935ddd5"
+    }
+  ]
+}

research/swap-component-cut/TASK.json

@@ -0,0 +1,64 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "For transposition targets on arbitrary coordinate pairs in the formal M_R(F2[GL_n(F2)]) model, prove the exact cost 3t whenever the targets' coordinate graph has components of at most three vertices, for every n and R. Record exact formal minima at n = 3 for mixed swaps and a 3-cycle, and an all-pairs additivity census at n = 3, R = 2.",
+  "scope_change_reason": "PR #4950 (pending) settled t swaps of one fixed coordinate pair and asked whether mixed targets admit the same per-target cut. This package answers that for transpositions whose coordinate graph has components of at most three vertices. It records where order-pattern cuts stop being tight (longer paths and stars at n = 4, and 3-cycles). It is a negative formal-model screen and does not satisfy the card's native construction gate.",
+  "bottleneck_link": "Register sharing and address spectators give no saving for these coordinate-permutation targets under the rank-one coordinate-CNOT tariff. A saving needs a changed operation or tariff.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the component theorem, the exact n = 3 formal minima and census, and the recorded limits of pattern cuts. Do not search native operations.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/swap-component-cut",
+  "author": "James Reed",
+  "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).",
+  "open_questions": [
+    {
+      "question": "Are formal costs additive across several targets that are not transpositions in small components, for example two 3-cycles, or 3-edge transposition paths and stars?",
+      "why_it_matters": "A single target costs exactly its CNOT word length (the support lemma of pending PR #4974 plus a one-register word), but support bounds only the largest single target. Order-pattern cuts are not tight for these multi-target cases (3 of 6 for a 3-cycle, 8.33 and 8.14 of 9 at n = 4).",
+      "first_step": "Run the exact formal search for diag([c3],[c3]) at n = 3, R = 2 up to length 11, or find a cut that combines with the support argument.",
+      "blocked_by": "nothing"
+    }
+  ]
+}

research/swap-component-cut/VERIFY.json

@@ -0,0 +1,27 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Exchangeability lemmas for the pair and triple-parity cuts; averaged cut counts in the GL_3 regular representation over all 5,040 orders; exact formal minima s01+s12 = 6 and 3-cycle = 6 at n = 3, R = 2; the nine-call attaining word for three transpositions at n = 4."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/census.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "All 28,211 pairs (g, h) in GL_3(F2)^2 at R = 2, reduced to 1,248 orbit representatives under coordinate-permutation conjugation, inverse transpose and register exchange (orbit coverage checked): no formal word shorter than min(l(g)+l(h), 6)."
+    }
+  ]
+}

research/swap-component-cut/census.py

@@ -0,0 +1,87 @@
+#!/usr/bin/env python3
+"""Exact additivity census at n = 3, R = 2.
+
+For every pair (g, h) in GL_3(F2) x GL_3(F2), with word lengths l(g), l(h)
+in coordinate CNOTs, search for a formal word of length <= min(l(g)+l(h)-1, 5)
+realizing diag([g], [h]). None exists, so the formal cost is at least
+min(l(g)+l(h), 6), and equals l(g)+l(h) whenever that sum is at most six.
+
+Symmetry reduction: conjugation by a coordinate permutation and the
+inverse-transpose map g -> g^(-T) are automorphisms of GL_3(F2) that map the
+coordinate-CNOT set onto itself, so they extend to algebra automorphisms of
+F2[GL_3] preserving every paid call (projectors unchanged) and word lengths.
+Exchanging the two registers conjugates every rank-one idempotent projector
+by the register swap. Hence the formal cost and l(g)+l(h) are constant on
+orbits of this 24-element group, and one representative per orbit suffices.
+The orbit sizes are checked to cover all pairs.
+"""
+
+from __future__ import annotations
+
+import itertools
+import sys
+from pathlib import Path
+
+PACKAGE = Path(__file__).resolve().parent
+sys.path.insert(0, str(PACKAGE))
+
+import formal  # noqa: E402
+
+
+def main() -> None:
+    model = formal.Model(3, 2)
+    forward = model.layers(model.diagonal([]), 3)
+    lengths = formal.word_lengths(3)
+    if sorted(lengths.values()).count(6) != 2 or len(lengths) != 168:
+        raise SystemExit("FAIL: GL_3 word lengths")
+    n = 3
+
+    def transpose(g):
+        return tuple(sum(((g[r] >> c) & 1) << r for r in range(n)) for c in range(n))
+
+    def inverse(g):
+        return next(x for x in lengths if formal.mul(g, x, n) == formal.identity(n))
+
+    autos = []
+    for sigma in itertools.permutations(range(n)):
+        p = formal.row_permutation(n, sigma)
+        p_inv = inverse(p)
+        conj = {g: formal.mul(formal.mul(p, g, n), p_inv, n) for g in lengths}
+        autos.append(conj)
+        autos.append({g: inverse(transpose(conj[g])) for g in lengths})
+    cnots = set(formal.cnots(n))
+    for auto in autos:
+        if {auto[c] for c in cnots} != cnots or any(lengths[auto[g]] != lengths[g] for g in lengths):
+            raise SystemExit("FAIL: symmetry does not preserve CNOTs and lengths")
+
+    def orbit(g, h):
+        return {pair for a in autos for pair in ((a[g], a[h]), (a[h], a[g]))}
+
+    covered = 0
+    checked = 0
+    representatives = []
+    for g, h in itertools.product(lengths, lengths):
+        members = orbit(g, h)
+        if (g, h) != min(members):
+            continue
+        covered += len(members)
+        representatives.append((g, h))
+    if covered != 168 * 168:
+        raise SystemExit("FAIL: orbits do not cover all pairs")
+    for g, h in representatives:
+        total = lengths[g] + lengths[h]
+        if total <= 1:
+            continue
+        budget = min(total - 1, 5)
+        target = model.diagonal([g, h])
+        best = model.shortest(target, forward, max(0, budget - 3)) if budget > 3 else forward.get(target)
+        if best is not None and best <= budget:
+            raise SystemExit(f"FAIL: shorter word for {g}, {h}: {best} < {total}")
+        checked += len(orbit(g, h))
+    if checked != 168 * 168 - 13:
+        raise SystemExit("FAIL: census size")
+    print(f"PASS_SWAP_COMPONENT_CENSUS pairs={checked} orbits={len(representatives)} no_shorter_word")
+
+
+if __name__ == "__main__":
+    main()