From 99a0f53c640bfa97c84f83b6e4644602e41d2dfd Mon Sep 17 00:00:00 2001 From: James Reed Date: Thu, 22 Oct 2026 21:29:03 -0700 Subject: [PATCH 1/3] Prove mixed transposition targets cost three calls each In the formal M_R(F2[GL_n(F2)]) model, transposition targets whose coordinate graph has components of at most three vertices cost exactly 3t paid calls for every n. The proof sums a row-pair cut or a triple-parity cut over components. Exact n=3 minima: s01+s12 and a 3-cycle cost six; an all-pairs census at R=2 finds no word shorter than min(l(g)+l(h), 6). Order-pattern cuts stop being tight for 3-cycles and for larger components. No new kappa. Co-Authored-By: Claude Opus 5.5 --- research/swap-component-cut/README.md | 146 +++++++++++++++++++++ research/swap-component-cut/SOURCES.json | 30 +++++ research/swap-component-cut/TASK.json | 64 +++++++++ research/swap-component-cut/VERIFY.json | 27 ++++ research/swap-component-cut/census.py | 45 +++++++ research/swap-component-cut/formal.py | 121 +++++++++++++++++ research/swap-component-cut/verify.py | 157 +++++++++++++++++++++++ 7 files changed, 590 insertions(+) create mode 100644 research/swap-component-cut/README.md create mode 100644 research/swap-component-cut/SOURCES.json create mode 100644 research/swap-component-cut/TASK.json create mode 100644 research/swap-component-cut/VERIFY.json create mode 100644 research/swap-component-cut/census.py create mode 100644 research/swap-component-cut/formal.py create mode 100644 research/swap-component-cut/verify.py diff --git a/research/swap-component-cut/README.md b/research/swap-component-cut/README.md new file mode 100644 index 0000000000..6b85041927 --- /dev/null +++ b/research/swap-component-cut/README.md @@ -0,0 +1,146 @@ +# 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 four minutes, 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. **Do 3-cycles and larger transposition components cost the sum of + their word lengths, `3(n − cycles)` per register?** For a 3-cycle at + `n = 3`, order-pattern cuts reach only 3. A scratch column-generation run + over all permutation cuts of the regular representation stopped at 3.51. + That run is not certified optimal, because MILP pricing was time-limited. + The exact formal search gives 6 for `R ≤ 2`, so a uniform proof probably + needs a non-permutation cut (a rank cut in another representation) or a + projection argument. *First step:* repeat that LP with rank cuts in the + natural representation tensored with itself. *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. diff --git a/research/swap-component-cut/SOURCES.json b/research/swap-component-cut/SOURCES.json new file mode 100644 index 0000000000..f95aa3add6 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/swap-component-cut/TASK.json b/research/swap-component-cut/TASK.json new file mode 100644 index 0000000000..84c3abc3ba --- /dev/null +++ b/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": "Do 3-cycles and longer transposition paths or stars cost the sum of their CNOT word lengths, 3(n - cycles) per register, in the formal model with dirty registers?", + "why_it_matters": "Order-pattern cuts certify only 3 of the 6 calls of 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 of the GL_3 regular representation stopped at 3.51 (not certified optimal). A uniform proof needs a cut outside these families or a projection argument.", + "first_step": "Repeat the column-generation LP with rank cuts in the natural representation tensored with itself, for one 3-cycle at n = 3. The exact formal search already gives 6 for R <= 2.", + "blocked_by": "nothing" + } + ] +} diff --git a/research/swap-component-cut/VERIFY.json b/research/swap-component-cut/VERIFY.json new file mode 100644 index 0000000000..597dc38b25 --- /dev/null +++ b/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": 600, + "checks": "All 28,211 pairs (g, h) in GL_3(F2)^2 at R = 2: no formal word shorter than min(l(g)+l(h), 6)." + } + ] +} diff --git a/research/swap-component-cut/census.py b/research/swap-component-cut/census.py new file mode 100644 index 0000000000..6329f2a97f --- /dev/null +++ b/research/swap-component-cut/census.py @@ -0,0 +1,45 @@ +#!/usr/bin/env python3 +"""Exact additivity census at n = 3, R = 2 (about four minutes). + +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. +""" + +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") + checked = 0 + for g, h in itertools.product(lengths, lengths): + 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 += 1 + if checked != 168 * 168 - 13: + raise SystemExit("FAIL: census size") + print(f"PASS_SWAP_COMPONENT_CENSUS pairs={checked} no_shorter_word") + + +if __name__ == "__main__": + main() diff --git a/research/swap-component-cut/formal.py b/research/swap-component-cut/formal.py new file mode 100644 index 0000000000..eb3058c359 --- /dev/null +++ b/research/swap-component-cut/formal.py @@ -0,0 +1,121 @@ +"""Formal algebra M_R(F2[GL_n(F2)]) and an exact meet-in-the-middle word search. + +Group elements are tuples of row bitmasks. Algebra elements are frozensets +of group elements (F2 coefficients). A paid call is I_R + ([g] + [I]) N with +g a coordinate CNOT and N a rank-one binary idempotent. Free scalar maps are +normalized away first (#4939 step 1), so words consist of paid calls only. +""" + +from __future__ import annotations + +from collections import deque +from functools import reduce + + +def mul(a, b, n): + return tuple(reduce(lambda acc, k: acc ^ (b[k] if a[i] >> k & 1 else 0), range(n), 0) + for i in range(n)) + + +def identity(n): + return tuple(1 << i for i in range(n)) + + +def cnots(n): + out = [] + for i in range(n): + for j in range(n): + if i != j: + g = list(identity(n)) + g[i] ^= 1 << j + out.append(tuple(g)) + return out + + +def row_permutation(n, sigma): + """Row a of the result is row sigma[a] of the identity.""" + base = identity(n) + return tuple(base[sigma[a]] for a in range(n)) + + +def word_lengths(n): + dist = {identity(n): 0} + queue = deque([identity(n)]) + while queue: + x = queue.popleft() + for g in cnots(n): + y = mul(g, x, n) + if y not in dist: + dist[y] = dist[x] + 1 + queue.append(y) + return dist + + +def algebra_product(x, y, n): + acc = set() + for g in x: + for h in y: + acc ^= {mul(g, h, n)} + return frozenset(acc) + + +def matrix_product(a, b, registers, n): + rows = [] + for i in range(registers): + row = [] + for j in range(registers): + entry = set() + for k in range(registers): + if a[i][k] and b[k][j]: + entry ^= algebra_product(a[i][k], b[k][j], n) + row.append(frozenset(entry)) + rows.append(tuple(row)) + return tuple(rows) + + +class Model: + def __init__(self, n, registers): + self.n, self.registers = n, registers + self.one = frozenset([identity(n)]) + self.zero = frozenset() + projectors = [] + for u in range(1, 1 << registers): + for v in range(1, 1 << registers): + if bin(u & v).count("1") % 2: + projectors.append((u, v)) + self.generators = [] + for g in cnots(n): + label = frozenset([g, identity(n)]) + for u, v in projectors: + self.generators.append(tuple( + tuple((self.one if a == b else self.zero) ^ (label if (u >> a & 1) and (v >> b & 1) else self.zero) + for b in range(registers)) for a in range(registers))) + + def diagonal(self, elements): + entries = [frozenset([e]) for e in elements] + [self.one] * (self.registers - len(elements)) + return tuple(tuple(entries[a] if a == b else self.zero for b in range(self.registers)) + for a in range(self.registers)) + + def layers(self, start, depth): + seen = {start: 0} + frontier = [start] + for d in range(1, depth + 1): + nxt = [] + for x in frontier: + for g in self.generators: + y = matrix_product(x, g, self.registers, self.n) + if y not in seen: + seen[y] = d + nxt.append(y) + frontier = nxt + return seen + + def shortest(self, target, forward, backward_depth): + """Least length <= max(forward) + backward_depth reaching target, or None. + + Generators are involutions, so the backward ball from the target is + the set of target * W for words W of length <= backward_depth. + """ + backward = self.layers(target, backward_depth) + common = forward.keys() & backward.keys() + return min((forward[x] + backward[x] for x in common), default=None) diff --git a/research/swap-component-cut/verify.py b/research/swap-component-cut/verify.py new file mode 100644 index 0000000000..ee321ad6f5 --- /dev/null +++ b/research/swap-component-cut/verify.py @@ -0,0 +1,157 @@ +#!/usr/bin/env python3 +"""Exact checks for component cuts on transposition targets. + +The uniform claim (transposition targets whose coordinate graph has +components of at most three vertices cost exactly 3t paid calls, for every +n) is the written proof in README.md. This verifier checks the two +exchangeability lemmas exactly, the averaged cut counts in the GL_3 regular +representation over all 5,040 orders, exact formal minima for mixed targets +at n = 3, and the attaining words. No new kappa is claimed. +""" + +from __future__ import annotations + +import hashlib +import itertools +import json +import sys +from fractions import Fraction +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "swap-component-cut" +sys.path.insert(0, str(PACKAGE)) + +import formal # noqa: E402 + + +def need(condition: bool, message: str) -> None: + if not condition: + raise SystemExit("FAIL: " + message) + + +def pins() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + for row in sources["files"]: + if row["usage"] == "input": + digest = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() + need(digest == row["sha256"], row["path"]) + selected = json.loads((ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")) + need(selected["kappa"] == "60403/20000000", "selected kappa") + + +def sign(sequence) -> int: + inversions = sum(1 for a, b in itertools.combinations(sequence, 2) if a > b) + return inversions % 2 + + +def exchangeability_lemmas() -> None: + # Pair cut {a before b}: rows a, b and the fresh vector w are uniformly ordered. + orders = list(itertools.permutations("abw")) + leave = Fraction(sum(1 for o in orders if o.index("a") < o.index("b") and o.index("w") > o.index("b")), + len(orders)) + need(leave == Fraction(1, 6), "pair cut: CNOT writing row a leaves with probability 1/6") + # Triple parity cut on rows (a, b, c) with label order a < b < c; w replaces row a. + orders = list(itertools.permutations("abcw")) + def parity(o, labels): + ranks = [o.index(x) for x in labels] + return sign(ranks) + flips = Fraction(sum(1 for o in orders + if parity(o, "abc") == 0 and parity(o, "wbc") == 1), len(orders)) + need(flips == Fraction(1, 6), "triple parity cut: CNOT writing row a leaves with probability 1/6") + stays = Fraction(sum(1 for o in orders if parity(o, "abc") == 0), len(orders)) + need(stays == Fraction(1, 2), "triple parity cut has measure 1/2") + # Any transposition of two rows of the triple flips the parity. + for x, y in itertools.combinations(range(3), 2): + for perm in itertools.permutations(range(3)): + swapped = list(perm) + swapped[x], swapped[y] = swapped[y], swapped[x] + need(sign(perm) != sign(swapped), "row transposition flips parity") + + +def regular_check() -> None: + n = 3 + group = [g for g in formal.word_lengths(n)] + need(len(group) == 168, "GL_3(F2) order") + index = {g: k for k, g in enumerate(group)} + left = lambda g: [index[formal.mul(g, x, n)] for x in group] + cnot_perms = {} + for i in range(n): + for j in range(n): + if i != j: + g = list(formal.identity(n)) + g[i] ^= 1 << j + cnot_perms[("cnot", i, j)] = left(tuple(g)) + swaps = {("swap", a, b): left(formal.row_permutation(n, tuple(b if x == a else a if x == b else x for x in range(n)))) + for a, b in itertools.combinations(range(n), 2)} + orders = list(itertools.permutations(range(1, 8))) + pair_sum = {key: 0 for key in list(cnot_perms) + list(swaps)} + parity_sum = dict(pair_sum) + for order in orders: + position = {v: k for k, v in enumerate(order)} + pair_cut = [position[x[0]] < position[x[1]] for x in group] + parity_cut = [sign([position[r] for r in x]) == 0 for x in group] + for key, perm in list(cnot_perms.items()) + list(swaps.items()): + pair_sum[key] += sum(1 for x in range(168) if pair_cut[x] and not pair_cut[perm[x]]) + parity_sum[key] += sum(1 for x in range(168) if parity_cut[x] and not parity_cut[perm[x]]) + unit = len(orders) * 168 // 6 + for key in cnot_perms: + i, j = key[1], key[2] + need(pair_sum[key] == (unit if i in (0, 1) else 0), f"pair cut CNOT({i},{j})") + need(parity_sum[key] == unit, f"parity cut CNOT({i},{j})") + need(pair_sum[("swap", 0, 1)] == 3 * unit, "pair cut on its own transposition") + for key in swaps: + need(parity_sum[key] == 3 * unit, f"parity cut on transposition {key}") + # A transposition sharing one row with the pair is worth one unit: the component rule needs + # disjoint rows, and this is why a 2-path needs the parity cut instead. + need(pair_sum[("swap", 0, 2)] == unit and pair_sum[("swap", 1, 2)] == unit, "pair cut on overlapping transpositions") + + +def formal_minima() -> None: + model = formal.Model(3, 2) + forward = model.layers(model.diagonal([]), 3) + need(len(forward) == 26551, "forward ball size n=3 R=2 depth 3") + s01 = formal.row_permutation(3, (1, 0, 2)) + s12 = formal.row_permutation(3, (0, 2, 1)) + c3 = formal.row_permutation(3, (1, 2, 0)) + lengths = formal.word_lengths(3) + need(lengths[s01] == 3 and lengths[s12] == 3 and lengths[c3] == 6, "group word lengths") + need(model.shortest(model.diagonal([s01, s12]), forward, 2) is None, "s01+s12 needs more than five") + need(model.shortest(model.diagonal([s01, s12]), forward, 3) == 6, "s01+s12 costs six") + need(model.shortest(model.diagonal([c3]), forward, 2) is None, "a 3-cycle needs more than five") + need(model.shortest(model.diagonal([c3]), forward, 3) == 6, "a 3-cycle costs six") + + +def attaining_words() -> None: + n, registers = 4, 3 + model = formal.Model(n, registers) + one, zero = model.one, model.zero + targets = [(0, 1), (1, 2), (2, 3)] + product = model.diagonal([]) + calls = 0 + for r, (a, b) in enumerate(targets): + for i, j in ((a, b), (b, a), (a, b)): + g = list(formal.identity(n)) + g[i] ^= 1 << j + entries = [one] * registers + entries[r] = frozenset([tuple(g)]) + factor = tuple(tuple(entries[x] if x == y else zero for y in range(registers)) for x in range(registers)) + product = formal.matrix_product(product, factor, registers, n) + calls += 1 + elements = [formal.row_permutation(n, tuple(b if x == a else a if x == b else x for x in range(n))) + for a, b in targets] + need(product == model.diagonal(elements) and calls == 9, "attaining word for three transpositions") + + +def main() -> None: + pins() + exchangeability_lemmas() + regular_check() + formal_minima() + attaining_words() + print("PASS_SWAP_COMPONENT_CUT uniform=3t_for_components_of_at_most_three_vertices " + "regular_check=GL3_all_orders formal_minima=s01+s12:6,c3:6 no_new_kappa") + + +if __name__ == "__main__": + main() From 4df5f85256a6d1948912ba5631f476642ad824af Mon Sep 17 00:00:00 2001 From: James Reed Date: Thu, 22 Oct 2026 22:11:22 -0700 Subject: [PATCH 2/3] Reduce the swap-component census by symmetry to fit the CI cap The all-pairs census exceeded the 600 s per-command limit on hosted CI. Formal cost and word length are invariant under coordinate-permutation conjugation, inverse transpose and register exchange, so the census now checks one representative per orbit (1,248 orbits) and verifies that the orbits cover all 28,211 pairs. Same conclusion, about 20 s locally. Co-Authored-By: Claude Opus 5.5 --- research/swap-component-cut/README.md | 2 +- research/swap-component-cut/VERIFY.json | 4 +-- research/swap-component-cut/census.py | 48 +++++++++++++++++++++++-- 3 files changed, 48 insertions(+), 6 deletions(-) diff --git a/research/swap-component-cut/README.md b/research/swap-component-cut/README.md index 6b85041927..380f04e371 100644 --- a/research/swap-component-cut/README.md +++ b/research/swap-component-cut/README.md @@ -88,7 +88,7 @@ probability `2/5` rather than `1/3`. same holds for the 3-cycle; - the nine-call word for the 3-edge path at `n = 4`, `R = 3`. -`census.py`, exact, about four minutes, checks all 28,211 pairs at `n = 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 diff --git a/research/swap-component-cut/VERIFY.json b/research/swap-component-cut/VERIFY.json index 597dc38b25..4eaa2682c3 100644 --- a/research/swap-component-cut/VERIFY.json +++ b/research/swap-component-cut/VERIFY.json @@ -20,8 +20,8 @@ "-B", "{package}/census.py" ], - "timeout_seconds": 600, - "checks": "All 28,211 pairs (g, h) in GL_3(F2)^2 at R = 2: no formal word shorter than min(l(g)+l(h), 6)." + "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)." } ] } diff --git a/research/swap-component-cut/census.py b/research/swap-component-cut/census.py index 6329f2a97f..24ec4696e9 100644 --- a/research/swap-component-cut/census.py +++ b/research/swap-component-cut/census.py @@ -1,10 +1,19 @@ #!/usr/bin/env python3 -"""Exact additivity census at n = 3, R = 2 (about four minutes). +"""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 @@ -25,8 +34,41 @@ def main() -> None: 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 @@ -35,10 +77,10 @@ def main() -> None: 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 += 1 + checked += len(orbit(g, h)) if checked != 168 * 168 - 13: raise SystemExit("FAIL: census size") - print(f"PASS_SWAP_COMPONENT_CENSUS pairs={checked} no_shorter_word") + print(f"PASS_SWAP_COMPONENT_CENSUS pairs={checked} orbits={len(representatives)} no_shorter_word") if __name__ == "__main__": From e7d050e79a6a55ecdd1706ee2855a3f3585c11e7 Mon Sep 17 00:00:00 2001 From: James Reed Date: Thu, 22 Oct 2026 22:13:58 -0700 Subject: [PATCH 3/3] Point the open question at #4974's single-target support lemma A single target costs exactly its CNOT word length, so the remaining question is additivity across several targets. Co-Authored-By: Claude Opus 5.5 --- research/swap-component-cut/README.md | 24 +++++++++++++++--------- research/swap-component-cut/TASK.json | 6 +++--- 2 files changed, 18 insertions(+), 12 deletions(-) diff --git a/research/swap-component-cut/README.md b/research/swap-component-cut/README.md index 380f04e371..19eaadc4ea 100644 --- a/research/swap-component-cut/README.md +++ b/research/swap-component-cut/README.md @@ -121,15 +121,21 @@ python3.12 -B scripts/research_package.py --package research/swap-component-cut ## Open next questions -1. **Do 3-cycles and larger transposition components cost the sum of - their word lengths, `3(n − cycles)` per register?** For a 3-cycle at - `n = 3`, order-pattern cuts reach only 3. A scratch column-generation run - over all permutation cuts of the regular representation stopped at 3.51. - That run is not certified optimal, because MILP pricing was time-limited. - The exact formal search gives 6 for `R ≤ 2`, so a uniform proof probably - needs a non-permutation cut (a rank cut in another representation) or a - projection argument. *First step:* repeat that LP with rank cuts in the - natural representation tensored with itself. *Blocked by:* nothing. +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 diff --git a/research/swap-component-cut/TASK.json b/research/swap-component-cut/TASK.json index 84c3abc3ba..a2c45bbdf3 100644 --- a/research/swap-component-cut/TASK.json +++ b/research/swap-component-cut/TASK.json @@ -55,9 +55,9 @@ "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).", "open_questions": [ { - "question": "Do 3-cycles and longer transposition paths or stars cost the sum of their CNOT word lengths, 3(n - cycles) per register, in the formal model with dirty registers?", - "why_it_matters": "Order-pattern cuts certify only 3 of the 6 calls of 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 of the GL_3 regular representation stopped at 3.51 (not certified optimal). A uniform proof needs a cut outside these families or a projection argument.", - "first_step": "Repeat the column-generation LP with rank cuts in the natural representation tensored with itself, for one 3-cycle at n = 3. The exact formal search already gives 6 for R <= 2.", + "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" } ]