diff --git a/research/swap-component-cut/README.md b/research/swap-component-cut/README.md
new file mode 100644
index 0000000000..19eaadc4ea
--- /dev/null
+++ b/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.
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..a2c45bbdf3
--- /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": "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"
+    }
+  ]
+}
diff --git a/research/swap-component-cut/VERIFY.json b/research/swap-component-cut/VERIFY.json
new file mode 100644
index 0000000000..4eaa2682c3
--- /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": 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
new file mode 100644
index 0000000000..24ec4696e9
--- /dev/null
+++ b/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()
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()