diff --git a/research/swap-row-order-cut/README.md b/research/swap-row-order-cut/README.md
new file mode 100644
index 0000000000..941c1eb4f2
--- /dev/null
+++ b/research/swap-row-order-cut/README.md
@@ -0,0 +1,187 @@
+# Address spectators never help coordinate swaps
+
+**Scoped formal-model theorem with exact finite checks. No new κ.**
+The selected conditional exponent stays 60403/20000000.
+
+## Result
+
+In the formal model of [PR #4939](https://github.com/CrocSwap/integer-mult-bounds/pull/4939),
+`t` coordinate-SWAP targets cost **exactly `3t` paid calls**. This holds for
+every address dimension `n ≥ 2` and every register count `R ≥ t`. Free
+scalar mixing and any number of restored dirty registers are allowed.
+
+For `t = 3` the minimum is nine, so spectator coordinates cannot reach the
+eight-call `(3,3,2)` row budget. This answers #4939 open question 1.
+
+The same cut reproves #4939's two-swap theorem without its projection step,
+and it reduces to PR1989's inversion cut at `n = 2`.
+
+## Model
+
+The model is #4939's, unchanged. Work in `M_R(F2[GL_n(F2)])`.
+
+- **Paid call.** A paid call is `D_N(g) = I_R + ([g] + [I_n]) N`, with
+  `g = I_n + E_ij` (`i ≠ j`) and `N = u v^T`, `v^T u = 1`. Each call costs one.
+- **Free maps.** Scalar `GL_R(F2)` maps are free.
+- **Target.** The target is `T = diag([s], …, [s], [I_n], …, [I_n])`, with `t`
+  copies of `[s]`, where `s` swaps address coordinates 0 and 1.
+- **Equality.** Equality is formal and holds on arbitrary inputs. Extra
+  registers are dirty and individually restored.
+
+## Proof
+
+**1. A representation and a cut.** Let `G = GL_n(F2)` act on itself by left
+multiplication, and use the regular representation `ρ` on `F2^G ⊗ F2^R`.
+
+- Left multiplication by `I + E_ij` adds row `j` to row `i` of `x`.
+- Left multiplication by `s` swaps rows 0 and 1 of `x`.
+
+Fix a linear order `<` on the `N = 2^n − 1` nonzero vectors of `F2^n`. Put
+
+```text
+A = { x in G : row0(x) < row1(x) },    X+ = A ⊗ F2^R,  X− = A^c ⊗ F2^R,
+q(M) = rank M[X−, X+].
+```
+
+From `(UV)[−,+] = U[−,+] V[+,+] + U[−,−] V[−,+]` we get
+`q(UV) ≤ q(U) + q(V)`.
+
+For a permutation `g` put `out(g) = |{x ∈ A : g x ∉ A}|`. Then:
+
+- **Paid call.** `ρ(D_N(g))[−,+] = P_g[A^c, A] ⊗ N` is a partial permutation
+  tensored with a rank-one matrix, so `q = out(g)`.
+- **Free maps.** A free scalar map has `q = 0`.
+- **Target.** The target has `q = t · out(s)`. Restored registers contribute
+  nothing.
+
+**2. Counting `out`.** Write `L` for the set of lines `{a, b, a+b}`. There are
+`|L| = N(N−1)/6` of them, and `|A| = c · 3|L|`, where `c` is the number of
+completions of an independent row pair to an element of `G`.
+
+- **The swap.** `s` maps `(r0, r1)` to `(r1, r0)`, so every element of `A`
+  leaves: `out(s) = |A| = 3c|L|`.
+- **Spectator-row writes.** A CNOT with `i ≥ 2` fixes rows 0 and 1:
+  `out = 0`.
+- **Active CNOTs.** Take `CNOT(0,1)`, which maps `(a, b)` to `(a+b, b)`, or
+  `CNOT(1,0)`, which maps it to `(a, a+b)`. Sort each line as `x < y < z`.
+  Of its three increasing pairs, exactly one leaves `A` under each map: `(x,y)`
+  under `CNOT(0,1)` and `(y,z)` under `CNOT(1,0)`. So for **every** order,
+  `out = c|L| = |A|/3`.
+- **Spectator reads** (`i ∈ {0,1}`, `j ≥ 2`). Given rows 0 and 1 equal to
+  `(a, b)`, row `j` is uniform over the vectors outside `span(a, b)`. Indeed,
+  any two such vectors `u, u'` are exchanged by some `h` fixing `a` and `b`,
+  and `x ↦ x h` permutes the completions. So `a + r_j` is uniform over the
+  `N − 3` nonzero vectors off the line of `(a, b)`. Let line positions be
+  `p_x < p_y < p_z`, with positions numbered `0, …, N−1`. Summing over each
+  line's increasing pairs gives
+
+  ```text
+  out(CNOT(0,j)) (N−3)/c = Σ_lines (3N − 4 − p_y − 2 p_z),
+  out(CNOT(1,j)) (N−3)/c = Σ_lines (2 p_x + p_y − 1).
+  ```
+
+**3. Average over all orders.** Under a uniformly random order, each line
+occupies a uniformly random 3-subset of positions. For a random 3-subset of
+`{0, …, N−1}`, `E[p_y + 2p_z] = 2N − 1` and `E[2p_x + p_y] = N − 2`. So
+both spectator-read counts average exactly to `c|L| = |A|/3`.
+
+Take `Q = Σ_orders q_order`. This is still subadditive. Every paid call has
+`Q = (#orders) c|L|` exactly, by step 2 for the active and spectator-row
+CNOTs and by this average for the spectator reads. The target has
+`Q = (#orders) · 3 c|L| · t`. Hence
+
+```text
+calls · (#orders) c|L|  ≥  (#orders) 3c|L| t,   so   calls ≥ 3t.
+```
+
+The same averaging shows that some single order already works. Both
+spectator conditions are equivalent to `Σ_lines (p_z − p_x) ≥ (N+1)|L|/2`,
+and the average over orders meets this with equality.
+
+**4. Attainment.** On each target register `r`, apply `a, b, a`, with
+`a = I + E_01` and `b = I + E_10`, using projector `E_rr`. Since `aba = s`,
+these `3t` calls give `T` and fix every other role.
+
+At `n = 2` there are no spectators, the regular representation is that of
+`S3`, and step 2 is PR1989's inversion count. For `n ≥ 3` a CNOT moves
+`2^{n−1}` of the nonzero vectors, which is why #4939 needed its projection.
+The row-pair cut needs no projection and has no limit on spectator writes.
+
+## Evidence
+
+`verify.py` uses only the standard library and exact integer or `Fraction`
+arithmetic. It runs in about one second.
+
+- **Regular-representation cut counts** for `GL_2` (all 6 orders),
+  `GL_3` (all 5,040 orders) and `GL_4` (eight orders, including Gray and
+  natural order; 20,160 group elements). Each check confirms that the swap
+  cuts all of `A`, that the active CNOTs cut exactly `|A|/3` and that
+  spectator-row CNOTs cut nothing. It also confirms that spectator reads match
+  the line formula and the spread criterion. For `n = 2, 3`, the all-order
+  sums equal `(#orders)|A|/3` exactly.
+- **Spread identities** `E[p_z − p_x] = (N+1)/2`, `E[p_y + 2p_z] = 2N − 1`
+  and `E[2p_x + p_y] = N − 2`, over all 3-subsets for `N ≤ 63`.
+- **The crossing-rank lemma** on actual paid factors: GL_3, `R = 2`, every
+  CNOT, the swap and every projector (42 cases).
+- **200 random subadditivity checks.**
+- **Attaining formal words** for `(n, t, R) = (2,3,3), (3,3,4), (4,2,3)`.
+
+Mutating the active-CNOT count, the all-order sum, the swap count or the
+attaining word makes the verifier fail.
+
+The cut was found by column generation over subsets of the GL_3 regular
+representation, using scipy/HiGHS in a scratch environment. The LP optimum
+over permutation cuts is exactly 3 per swap. That search is not part of the
+package; the proof above does not depend on it. Earlier, a separate formal
+meet-in-the-middle search ([review on #4939](https://github.com/CrocSwap/integer-mult-bounds/pull/4939#issuecomment-6356540020))
+found no two-swap word of length 5 or less at `(n,R) = (3,2), (4,2), (5,2)`.
+
+## Scope
+
+Card `bit-new-register-model`, scope **changed** (see `TASK.json`). This is
+a negative formal-model screen. It does not satisfy the card's native
+construction gate.
+
+The result holds for the swap of one fixed coordinate pair on every target
+register. Mixed targets, other permutations, other tariffs and native
+realizations are not covered. No supplier, hosting, precision or recursive
+profile is supplied.
+
+Base: canonical main `cef4b52f2a59009865bf8eabde1be3f159063703`, priority
+revision 7. The `find_overlap.py` search for "three swaps" found PR1541
+(three swaps at `n = 2`), the four-swap and label-saturation notes, and the
+GL2 corollary (`3t` at `n = 2`). None treats `n ≥ 3` beyond #4939's `t = 2`.
+That is a search result, not a novelty proof.
+Claim: [#1166 comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19137331).
+
+## Reproduce
+
+```sh
+python3.12 -B research/swap-row-order-cut/verify.py
+python3.12 -B scripts/research_package.py --package research/swap-row-order-cut
+```
+
+## Open next questions
+
+1. **Mixed swap targets.** Does the row-order cut extend to swaps of
+   different coordinate pairs on different registers, or to coordinate
+   3-cycles? *First step:* at `n = 3`, compute the best permutation cut for
+   swaps of `(0,1)` and `(1,2)` on two registers by the same column-generation
+   LP, and compare it with the six-call word. *Blocked by:* nothing.
+
+## Credit
+
+- Mihir Srivastava (@mihir-s-05), #4939, for the spectator model, the row
+  budget and the open question.
+- commdata2338, PR1414/PR1495, for the two-coordinate obstruction and the
+  spectator certificate.
+- Ross Richardson, PR1989, and the GL2 corollary, for the cut method and the
+  `3t` theorem at `n = 2`.
+- PR1541, for three swaps at `n = 2`.
+- Gareth Davidson/PR1333, for the alphabet and the normalization.
+
+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-row-order-cut/SOURCES.json b/research/swap-row-order-cut/SOURCES.json
new file mode 100644
index 0000000000..c7f0ac43d2
--- /dev/null
+++ b/research/swap-row-order-cut/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "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": "input",
+      "git_blob": "c34c1460063ee4690c934d3c3fb3d81896f8931c",
+      "sha256": "3650918994be00323ccb61b75cdd81ecae47104a6e0765e319196618737949d9"
+    },
+    {
+      "path": "research/symmetric-adjacent-cut-bound/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "30dad3856246c9cef3b8014ee967dd545f3a092d",
+      "sha256": "008be68867a8e85f4e18455d206e03f20aebfc28e9f08efba576180e7e1edc50"
+    },
+    {
+      "path": "research/coordinate-cnot-address-spectator/README.md",
+      "usage": "provenance",
+      "git_blob": "15b3db71d9fc13b4e9806caf42dd56213936fc88",
+      "sha256": "f433d3891cdc88fb47e055c4246798980529268a9a17250574414f805935ddd5"
+    }
+  ]
+}
diff --git a/research/swap-row-order-cut/TASK.json b/research/swap-row-order-cut/TASK.json
new file mode 100644
index 0000000000..57ea55e4fe
--- /dev/null
+++ b/research/swap-row-order-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": "Prove that t coordinate-SWAP targets cost exactly 3t paid coordinate-CNOT calls in the formal M_R(F2[GL_n(F2)]) model, for every n >= 2 and R >= t, with free scalar mixing and restored dirty registers. This answers PR #4939 open question 1 (three swaps cost nine).",
+  "scope_change_reason": "The card asks for a larger or nonabelian register model to escape the three-register obstruction. PR #4939 (pending, head 743ddd6275cfd560d9c3e7825c42545152d14e4c) showed that address spectators do not help two swaps, and asked whether they help three. This package answers that formal-model question negatively for every swap count. It is a negative formal-model screen. It does not satisfy the card's native construction gate.",
+  "bottleneck_link": "It closes the spectator-coordinate escape for the rank-one coordinate-CNOT tariff in this formal model. Any saving must come from a changed native operation or tariff, not from extra address coordinates.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the uniform written proof, exact regular-representation checks for n <= 4 and the attaining word. Do not search native operations or other tariffs.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/swap-row-order-cut",
+  "author": "James Reed",
+  "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).",
+  "open_questions": [
+    {
+      "question": "Does the row-order cut extend to SWAP targets on different coordinate pairs in different registers, or to other permutation targets (for example 3-cycles of coordinates)?",
+      "why_it_matters": "Mixed targets are the next formal-model case where spectators or shared work might lower the per-target cost. The present cut uses one coordinate pair for every register.",
+      "first_step": "For two registers carrying swaps of (0,1) and (1,2) at n = 3, compute the best permutation cut in the regular representation by the same column-generation LP and compare it with the six-call word.",
+      "blocked_by": "nothing"
+    }
+  ]
+}
diff --git a/research/swap-row-order-cut/VERIFY.json b/research/swap-row-order-cut/VERIFY.json
new file mode 100644
index 0000000000..8f832eb930
--- /dev/null
+++ b/research/swap-row-order-cut/VERIFY.json
@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/gl2-swap-cut-corollary/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Regular-representation row-order cut counts for GL_2 and GL_3 over all orders and GL_4 over eight orders: the swap cuts all of A, the two active CNOTs cut exactly |A|/3, spectator-row CNOTs cut nothing, spectator-read CNOTs follow the line formula and the spread criterion, and their all-order sums equal |A|/3. Spread identity for N <= 63, crossing-rank lemma for actual paid factors, subadditivity spot checks, and 3t-call attaining words."
+    }
+  ]
+}
diff --git a/research/swap-row-order-cut/verify.py b/research/swap-row-order-cut/verify.py
new file mode 100644
index 0000000000..5539df587e
--- /dev/null
+++ b/research/swap-row-order-cut/verify.py
@@ -0,0 +1,294 @@
+#!/usr/bin/env python3
+"""Exact finite checks for the row-order cut on coordinate-SWAP targets.
+
+The uniform claim (t SWAP targets cost 3t paid calls in F2[GL_n(F2)] for
+every n >= 2) is the written proof in README.md. This verifier checks its
+finite ingredients exactly: the cut counts in the regular representation
+for n = 2, 3, 4, the all-order average at n = 3, the spread identity for
+n <= 6, the crossing-rank lemma for actual paid factors, and the 3t-call
+attaining word. No new kappa is claimed.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import itertools
+import json
+import random
+from fractions import Fraction
+from functools import reduce
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PACKAGE = ROOT / "research" / "swap-row-order-cut"
+PREDECESSOR = ROOT / "research/gl2-swap-cut-corollary/README.md"
+
+
+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"])
+    text = PREDECESSOR.read_text(encoding="utf-8")
+    need("the exact\ncost of `t` SWAP targets is **3t paid calls**" in text, "n=2 predecessor statement")
+    selected = json.loads((ROOT / "certificates/selected-result.json").read_text(encoding="utf-8"))
+    need(selected["kappa"] == "60403/20000000", "selected kappa")
+
+
+# Matrices are tuples of row bitmasks; bit k of row i is the (i, k) entry.
+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 general_linear(n):
+    group = []
+    for rows in itertools.product(range(1, 1 << n), repeat=n):
+        span = {0}
+        for row in rows:
+            if row in span:
+                break
+            span |= {x ^ row for x in span}
+        else:
+            group.append(rows)
+    return group
+
+
+def cnot(n, i, j):
+    g = list(identity(n))
+    g[i] ^= 1 << j
+    return tuple(g)
+
+
+def swap01(n):
+    g = list(identity(n))
+    g[0], g[1] = g[1], g[0]
+    return tuple(g)
+
+
+def lines(n):
+    vectors = range(1, 1 << n)
+    return sorted({tuple(sorted((a, b, a ^ b))) for a in vectors for b in vectors if a < b and a ^ b})
+
+
+class Regular:
+    """Left regular action of GL_n(F2) on itself."""
+
+    def __init__(self, n):
+        self.n = n
+        self.group = general_linear(n)
+        self.index = {g: k for k, g in enumerate(self.group)}
+        self.cnots = {(i, j): cnot(n, i, j) for i in range(n) for j in range(n) if i != j}
+        self.perm = {key: self.left(g) for key, g in self.cnots.items()}
+        self.swap = self.left(swap01(n))
+
+    def left(self, g):
+        return [self.index[mul(g, x, self.n)] for x in self.group]
+
+    def cut(self, order):
+        position = {v: k for k, v in enumerate(order)}
+        return [position[x[0]] < position[x[1]] for x in self.group]
+
+    @staticmethod
+    def out(perm, member):
+        return sum(1 for x, inside in enumerate(member) if inside and not member[perm[x]])
+
+
+def regular_counts(reg: Regular, order) -> tuple[int, dict, int]:
+    member = reg.cut(order)
+    size = sum(member)
+    counts = {key: Regular.out(p, member) for key, p in reg.perm.items()}
+    return size, counts, Regular.out(reg.swap, member)
+
+
+def spread(order, n) -> int:
+    position = {v: k for k, v in enumerate(order)}
+    total = 0
+    for line in lines(n):
+        p = sorted(position[v] for v in line)
+        total += p[2] - p[0]
+    return total
+
+
+def check_regular(n: int, orders, average: bool) -> None:
+    reg = Regular(n)
+    vectors = (1 << n) - 1
+    line_count = len(lines(n))
+    need(line_count * 6 == vectors * (vectors - 1), f"line count n={n}")
+    completions = len(reg.group) // (vectors * (vectors - 1))
+    sums = {key: 0 for key in reg.perm}
+    for order in orders:
+        size, counts, swap_out = regular_counts(reg, order)
+        need(size == completions * line_count * 3, f"|A| n={n}")
+        need(swap_out == size, f"the swap moves all of A out, n={n}")
+        third = size // 3
+        for (i, j), value in counts.items():
+            if i >= 2:
+                need(value == 0, f"spectator-row CNOT({i},{j}) never cuts, n={n}")
+            elif j < 2:
+                need(value == third, f"CNOT({i},{j}) cuts exactly |A|/3, n={n}")
+            else:
+                # line formula: spread D decides both spectator directions
+                d = spread(order, n)
+                if i == 0:
+                    predicted = sum(3 * vectors - 4 - sorted_pos[1] - 2 * sorted_pos[2]
+                                    for sorted_pos in sorted_positions(order, n))
+                else:
+                    predicted = sum(2 * sorted_pos[0] + sorted_pos[1] - 1
+                                    for sorted_pos in sorted_positions(order, n))
+                need(Fraction(value, completions) == Fraction(predicted, vectors - 3),
+                     f"line formula CNOT({i},{j}) n={n}")
+                need((value <= third) == (2 * d >= (vectors + 1) * line_count),
+                     f"spread criterion CNOT({i},{j}) n={n}")
+            sums[(i, j)] += value
+    if average:
+        for key, total in sums.items():
+            expected = 0 if key[0] >= 2 else len(orders) * (completions * line_count)
+            need(total == expected, f"all-order average CNOT{key} n={n}")
+
+
+def sorted_positions(order, n):
+    position = {v: k for k, v in enumerate(order)}
+    return [sorted(position[v] for v in line) for line in lines(n)]
+
+
+def spread_identity() -> None:
+    # E[max - min] and E[mid + 2 max] over uniform 3-subsets of {0..N-1}.
+    for n in range(2, 7):
+        size = (1 << n) - 1
+        triples = list(itertools.combinations(range(size), 3))
+        gap = Fraction(sum(t[2] - t[0] for t in triples), len(triples))
+        need(gap == Fraction(size + 1, 2), f"mean spread N={size}")
+        upper = Fraction(sum(t[1] + 2 * t[2] for t in triples), len(triples))
+        lower = Fraction(sum(2 * t[0] + t[1] for t in triples), len(triples))
+        need(upper == 2 * size - 1 and lower == size - 2, f"spectator means N={size}")
+
+
+def rank_f2(rows):
+    rank, rows = 0, [r for r in rows if r]
+    while rows:
+        pivot = rows.pop()
+        low = pivot & -pivot
+        rows = [r ^ pivot if r & low else r for r in rows]
+        rows = [r for r in rows if r]
+        rank += 1
+    return rank
+
+
+def crossing_rank_lemma() -> None:
+    """rank of the [A^c, A] block of I + (P_g - I) (x) N equals out(g, A) rank N."""
+    n, registers = 3, 2
+    reg = Regular(n)
+    order = (1, 3, 2, 6, 7, 5, 4)
+    member = reg.cut(order)
+    inside = [x for x, m in enumerate(member) if m]
+    outside = [x for x, m in enumerate(member) if not m]
+    column = {x: k for k, x in enumerate(inside)}
+    projectors = [(u, v) for u in range(1, 4) for v in range(1, 4) if bin(u & v).count("1") % 2]
+    checked = 0
+    for key, perm in list(reg.perm.items()) + [("swap", reg.swap)]:
+        for u, v in projectors:
+            rows = []
+            for y in outside:
+                for r in range(registers):
+                    bits = 0
+                    for x in inside:
+                        if perm[x] == y and u >> r & 1:
+                            for c in range(registers):
+                                if v >> c & 1:
+                                    bits |= 1 << (column[x] * registers + c)
+                    rows.append(bits)
+            need(rank_f2(rows) == Regular.out(perm, member), f"crossing rank {key}")
+            checked += 1
+    need(checked == 7 * len(projectors), "crossing-rank cases")
+
+
+def subadditivity_spot_check() -> None:
+    random.seed(4939)
+    n = 3
+    reg = Regular(n)
+    member = reg.cut((1, 3, 2, 6, 7, 5, 4))
+    size = len(member)
+    perms = list(reg.perm.values())
+    for _ in range(200):
+        word = [random.choice(perms) for _ in range(random.randint(1, 6))]
+        composite = list(range(size))
+        for p in word:
+            composite = [p[c] for c in composite]
+        need(Regular.out(composite, member) <= sum(Regular.out(p, member) for p in word),
+             "permutation cut subadditivity")
+
+
+# Formal algebra M_R(F2[GL_n]) for the attaining word.
+def formal_product(x, y, n):
+    acc = set()
+    for g in x:
+        for h in y:
+            acc ^= {mul(g, h, n)}
+    return frozenset(acc)
+
+
+def formal_matmul(a, b, registers, n):
+    out = []
+    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 ^= formal_product(a[i][k], b[k][j], n)
+            row.append(frozenset(entry))
+        out.append(tuple(row))
+    return tuple(out)
+
+
+def attaining_word(n: int, swaps: int, registers: int) -> None:
+    one = frozenset([identity(n)])
+    zero = frozenset()
+
+    def diag(entries):
+        return tuple(tuple(entries[i] if i == j else zero for j in range(registers))
+                     for i in range(registers))
+
+    word = []
+    for r in range(swaps):
+        for g in (cnot(n, 0, 1), cnot(n, 1, 0), cnot(n, 0, 1)):
+            entries = [one] * registers
+            entries[r] = frozenset([g])  # I + ([g] + 1) E_rr
+            word.append(diag(entries))
+    product = diag([one] * registers)
+    for factor in word:
+        product = formal_matmul(product, factor, registers, n)
+    target = diag([frozenset([swap01(n)])] * swaps + [one] * (registers - swaps))
+    need(product == target and len(word) == 3 * swaps, f"attaining word n={n} t={swaps}")
+
+
+def main() -> None:
+    pins()
+    check_regular(2, list(itertools.permutations(range(1, 4))), average=True)
+    check_regular(3, list(itertools.permutations(range(1, 8))), average=True)
+    random.seed(1541)
+    sample = [tuple(random.sample(range(1, 16), 15)) for _ in range(6)]
+    gray = tuple(k ^ (k >> 1) for k in range(1, 16))
+    check_regular(4, sample + [gray, tuple(range(1, 16))], average=False)
+    spread_identity()
+    crossing_rank_lemma()
+    subadditivity_spot_check()
+    for n, swaps, registers in ((2, 3, 3), (3, 3, 4), (4, 2, 3)):
+        attaining_word(n, swaps, registers)
+    print("PASS_SWAP_ROW_ORDER_CUT uniform_minimum=3t_by_written_proof "
+          "regular_checks=n2_all_orders,n3_all_orders,n4_eight_orders no_new_kappa")
+
+
+if __name__ == "__main__":
+    main()