diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/CLAIM.md b/research/s4-mixed-v4-double-transposition-seed0cdbb4/CLAIM.md
new file mode 100644
index 0000000000..c826affe48
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/CLAIM.md
@@ -0,0 +1,43 @@
+# Cycle F local claim
+
+- Track: `bit-mechanisms`; seed `0cdbb418f7a976685134143f77494c2c`.
+- Task: `bit-new-register-model`; priority revision 3; catalogue SHA-256
+  `6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075`.
+- Base: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`; selected-record SHA-256
+  `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`.
+- Object: in formal `F2[S4]` on three arbitrary dirty roles, use paid adjacent
+  transpositions `s1=(12), s2=(23), s3=(34)` and every rank-one idempotent
+  `N` in `M3(F2)`. Test whether `diag([p],[q],[e])`, with
+  `p=(13)(24)=s2*s1*s3*s2` and `q=(12)(34)=s1*s3`, has a four-call word.
+- Baseline and objective: the direct word costs six calls. Both targets have
+  displacement rank two, so PR #1333 gives the optimistic full-alphabet floor
+  four. Every candidate call is charged one; a four-call word would save two
+  calls in this finite model. No free interface, extra role, hosting or
+  supplier operation is counted.
+- Method: complete two-plus-two meet over all 84 paid factors, 7,056 ordered
+  pair words and 49,787,136 length-four words. Check the exact formal
+  `3x3` group-algebra endpoint. A positive control is `diag([q],[q],[e])`,
+  which has a four-call direct word; `diag([p],[p],[e])` is a negative control.
+  If the mixed target has no four-call word, the sign quotient makes all valid
+  word lengths even, and the group-word length of `p` excludes lengths below
+  four. The direct six-call word then proves the exact minimum six.
+- Closest overlap: PR #1734 studies `diag([p],[p],[e])` in the same alphabet
+  and role count, with minimum eight; this changes the target to two distinct
+  commuting double transpositions and direct bill six. PR #1720 treats two
+  identical 4-cycles; Discussion #1740 / PR #1749 treats distinct noncommuting
+  3-cycles. PR #1333 supplies the broader rank-floor benchmark. Current exact
+  search found no `p,q` target match: authenticated REST overlap read 456 open
+  PRs and 140 Discussions at 10:03 UTC. The overlap helper's discussion
+  snapshot was stale/rate-limited, so live PR and Discussion reads were used.
+- Expected evidence: complete exact four-call exclusion or a checked
+  four-call witness, six-call positive word, positive/negative controls,
+  source pins and reproducible package. Stop after the complete meet and
+  parity proof; no supplier or kappa claim.
+- Predecessor attribution: PR #1333 and PR #1734 are the closest sources;
+  neither executable is imported. Prepared with substantial OpenAI Codex
+  assistance; no independent human review is claimed.
+- Intended expiry: `2026-10-14T12:03:00Z` (approximately two hours after scope selection).
+
+The remote Discussion claim could not yet be posted because GitHub's GraphQL
+comment mutation is rate-limited. This local claim preserves the full scope
+while the exact experiment proceeds.
diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/NOTICE.md b/research/s4-mixed-v4-double-transposition-seed0cdbb4/NOTICE.md
new file mode 100644
index 0000000000..a7342b7573
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/NOTICE.md
@@ -0,0 +1,21 @@
+# Attribution and scope
+
+The exact target considered here is
+`diag([(13)(24)],[(12)(34)],[e])` in formal `F2[S4]`, with only the adjacent
+transpositions `(12),(23),(34)` as paid address labels. The closest group
+predecessor is PR #1734, which studies the repeated target
+`diag([(13)(24)],[(13)(24)],[e])` in the same three-role model. PR #1333
+supplies the broader binary-affine rank theorem used for the optimistic floor;
+it does not make the restricted adjacent-label search redundant.
+
+No predecessor code or certificates are imported. The base commit, selected
+record, current review, source manifest, assembly certificate, task catalogue
+and lower-bound references are pinned in `SOURCES.json`.
+
+Prepared with substantial OpenAI Codex assistance in scope selection,
+mathematical formulation, exact search design, implementation, proof,
+verification and packaging. No subagents or independent human review are
+claimed. Repository licensing applies.
+
+This contribution is released under Apache-2.0, consistent with the
+repository license.
diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/OVERLAP.json b/research/s4-mixed-v4-double-transposition-seed0cdbb4/OVERLAP.json
new file mode 100644
index 0000000000..1a391705ca
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/OVERLAP.json
@@ -0,0 +1,65 @@
+{
+  "schema_version": 1,
+  "searched_at_utc": "2026-10-14T10:17:02Z",
+  "coverage": {
+    "open_prs": 460,
+    "discussions": 435,
+    "pagination_complete": true,
+    "discussion_source": "complete find_overlap.py refresh; targeted overlap query replayed against this snapshot"
+  },
+  "search_terms": [
+    "double-transposition",
+    "(13)(24)",
+    "(12)(34)",
+    "commuting S4",
+    "V4",
+    "bit-new-register-model",
+    "group algebra"
+  ],
+  "exact_target_match": false,
+  "nearest": [
+    {
+      "id": "PR1734",
+      "head": "48855b620b23af3a7fe87d53bde05cd2211342c8",
+      "scope": "F2[S4], three roles, adjacent transpositions, repeated target diag([(13)(24)],[(13)(24)],[e]); exact minimum eight.",
+      "relationship": "Same group, alphabet and role count; the current target changes the second active entry to (12)(34), giving two distinct commuting V4 targets and direct bill six.",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1734"
+    },
+    {
+      "id": "PR1720",
+      "head": "edb4a289a5f32c8209140144e384dcd3fa8cbfd1",
+      "scope": "Two identical 4-cycle targets in F2[S4].",
+      "relationship": "Different cycle type and repeated target; current target consists of distinct involutions.",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1720"
+    },
+    {
+      "id": "Discussion1740 / PR1749",
+      "scope": "Four-role S4 target pairs of distinct noncommuting 3-cycles.",
+      "relationship": "Current target has three roles and a commuting pair of double transpositions.",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1749"
+    },
+    {
+      "id": "PR1333",
+      "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2",
+      "scope": "Exact paid-rank theorem for the larger binary-affine rank-one alphabet.",
+      "relationship": "Sets the optimistic rank floor four; does not establish an implementation in the adjacent-transposition subset.",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1333"
+    },
+    {
+      "id": "PR1741",
+      "head": "bf29e15b2e5987d3a824e2563835a7ed94451c96",
+      "scope": "Order-seven target pair in F2[GL3(F2)] with coordinate CNOT labels.",
+      "relationship": "Different address group and target element.",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1741"
+    }
+  ],
+  "active_discussions_checked": [
+    "#1738 UT3(F2) central commutator and third dirty role",
+    "#1759 UT4 noncentral root pair",
+    "#1769 UT5 height-three root pair",
+    "#1773 four-role D8 heterogeneous target",
+    "#1774 previous local claim; exact GL2 target is unrelated and local release update is unposted",
+    "#1163 coordination comments, including the S4 repeated-target result"
+  ],
+  "limits": "Overlap snapshots identify related work; they do not establish novelty. Targeted query matched PR #1734, PR #1749 and older coordination records, but no exact p,q target."
+}
diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/PR-BODY.md b/research/s4-mixed-v4-double-transposition-seed0cdbb4/PR-BODY.md
new file mode 100644
index 0000000000..9e72a1cb6e
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/PR-BODY.md
@@ -0,0 +1,53 @@
+## Result
+
+This adds an exact six-call minimum for one mixed target in the formal group
+algebra `F2[S4]`:
+
+```text
+diag([(13)(24)], [(12)(34)], [e])
+```
+
+There are three arbitrary dirty roles. Paid calls are
+`I + ([s] + [e])N` for an adjacent transposition `s` in
+`{(12),(23),(34)}` and every rank-one idempotent `N` in `M3(F2)`. Each call
+costs one. Free interleaved scalar `GL3(F2)` changes are included through the
+standard augmentation normalization.
+
+The direct word costs six: four calls for `(13)(24)=(23)(12)(34)(23)` and
+two for `(12)(34)=(12)(34)`. A complete exact two-plus-two meet over all 84
+factors excludes every four-call word: all 7,056 ordered pair words were
+indexed, covering 49,787,136 four-call words, with 4,698 distinct pair
+products. The pair-state SHA-256 and deterministic receipt are in
+`RESULT.json`. The sign quotient forces even word length, and the target
+coefficient `(13)(24)` has adjacent-transposition length four. Together the
+four-call exclusion proves the exact minimum is six.
+
+Positive controls include the six-call mixed word and a found/replayed
+four-call word for `diag([(12)(34)],[(12)(34)],[e])`. The repeated
+`(13)(24)` target is a negative control. The Python verifier rebuilds the
+formal algebra independently and cross-checks a separate C++ implementation.
+
+Reproduce with:
+
+```sh
+python3 -I -B research/s4-mixed-v4-double-transposition-seed0cdbb4/verify.py
+python3 scripts/research_package.py --package research/s4-mixed-v4-double-transposition-seed0cdbb4 --check-only
+```
+
+## Relation to prior work
+
+PR #1734 uses the same group, label alphabet and role count for the repeated
+target `diag([(13)(24)],[(13)(24)],[e])`, with exact minimum eight. This
+submission changes the second active target to the distinct commuting
+double transposition `(12)(34)` and gives direct bill six; it does not claim
+priority for the common pair-state method or the general rank floor.
+
+The selected conditional bound remains complex-bound. No rational-frame
+supplier mapping, paid-moment change or new `kappa` is claimed.
+
+Research seed `0cdbb418f7a976685134143f77494c2c`; task
+`bit-new-register-model`; priority revision 3; exact base
+`0b1cccf86e2f5132ed286a26ef0a681a495740ea`; selected-record SHA-256
+`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`.
+Prepared with substantial OpenAI Codex assistance; no independent human
+review is claimed.
diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/PROOF.md b/research/s4-mixed-v4-double-transposition-seed0cdbb4/PROOF.md
new file mode 100644
index 0000000000..2f69069588
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/PROOF.md
@@ -0,0 +1,111 @@
+# Exact minimum for a mixed S4 double-transposition target
+
+## Formal model
+
+Let (S_4) act on (mathbb F_2^4) by permutation matrices. Put
+
+\[
+s_1=(12),\quad s_2=(23),\quad s_3=(34),\qquad
+p=(13)(24),\quad q=(12)(34).
+\]
+
+The target on three arbitrary dirty scalar roles is
+
+\[
+T=\operatorname{diag}([p],[q],[e])\in M_3(\mathbb F_2[S_4]).
+\]
+
+A paid call is
+
+\[
+D_N([s_i])=I+([s_i]+[e])N,
+\]
+
+where (N=xy^T\in M_3(\mathbb F_2)), (x,y\ne0), and (y^Tx=1). There
+are (7\cdot4=28) such rank-one idempotents and 84 paid factors. Every call
+costs one. Arbitrary interleaved free scalar (GL_3(\mathbb F_2)) changes
+are included by moving them to the end and conjugating each (N); augmentation
+maps every paid factor to (I), so the final scalar map must be (I) for this
+endpoint. The resulting normalized alphabet is exactly the 84 factors above.
+
+No address operation outside the three paid adjacent transpositions, clean
+inputs, extra roles, hosting, frame changes, restoration wrappers or supplier
+conversions are present in this finite model.
+
+## Cost screen and direct word
+
+The adjacent-transposition lengths are \(\ell(p)=4\) and \(\ell(q)=2\), so
+the direct bill is six calls. In the full rank-one-displacement alphabet of
+PR #1333, each target has displacement rank two and the exact paid-rank floor
+for this target is (2+2=4). Thus a four-call word is the optimistic saving
+candidate; every one of its four calls would still be fully charged.
+
+An attaining six-call word is
+
+```text
+D_E00(s2), D_E00(s1), D_E00(s3), D_E00(s2), D_E11(s1), D_E11(s3)
+```
+
+The first four factors multiply to ([p]) on role 0; the final two multiply
+to ([q]) on role 1. Role 2 remains exactly the identity. Both the C++ and
+Python implementations replay equality in every coefficient of the formal
+group algebra.
+
+## Lower bound below six
+
+Any coefficient in a product of (k) calls is the ordered product of a
+subsequence of the (k) adjacent-transposition labels: each factor expands as
+\(I+[s_i]N+[e]N\). Since the target has a nonzero ([p]) coefficient and
+\(\ell(p)=4\), no word with (k<4) can reach the endpoint.
+
+For parity, map (S_4\) to (C_2=\{1,t\}) by the sign character and extend
+linearly to group algebras over \(\mathbb F_2\). Each adjacent transposition
+maps to (t), so a paid factor maps to (I+(t+1)N). A rank-one idempotent is
+conjugate over \(\mathbb F_2\) to \(\operatorname{diag}(1,0,0)\); therefore
+
+\[
+\det(I+(t+1)N)=t.
+\]
+
+The target (p,q,e) consists of even permutations, so its determinant after
+this quotient is 1. A word of length (k) has determinant (t^k); equality
+requires (t^k=1) in \(\mathbb F_2[C_2]\), hence (k) is even. Below six,
+the only remaining possible length is four.
+
+The complete exact four-call meet finds no word. All 84 factors are formed as
+24-bit coefficient masks in each of nine matrix entries. The verifier stores
+all 7,056 ordered pair products (A=F_1F_2) and indexes the 4,698 distinct
+states. For each ordered suffix pair (F_3,F_4), every factor is an
+involution, so
+
+\[
+A F_3F_4=T\quad\Longleftrightarrow\quad
+A=T(F_4F_3).
+\]
+
+It checks all 7,056 ordered inverse-suffix pair words against the complete
+prefix index. There are no hits for (T). Therefore lengths 0 through 5 are
+excluded; the six-call word proves the exact minimum is six.
+
+The pair-state digest, exact counts, and hit receipts are in `RESULT.json`.
+The C++ implementation exhausts the full domain, and `verify.py` independently
+rebuilds the group law, idempotents, factors and pair meet in Python before
+cross-checking the native replay.
+
+## Controls and scope
+
+The positive control \(\operatorname{diag}([q],[q],[e])\) has the
+four-call word
+
+```text
+D_E00(s3), D_E11(s3), D_E11(s1), D_E00(s1)
+```
+
+which is found and replayed by both implementations. The negative
+control \(\operatorname{diag}([p],[p],[e])\) has no four-call word. The mixed
+six-call direct word is a separate positive control.
+
+This is an exact result for one target and one restricted alphabet. It does
+not determine costs for other S4 tuples or for other transposition sets. No
+operation is mapped into the selected rational-frame supplier, so the result
+changes no paid profile or \(\kappa\).
diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/README.md b/research/s4-mixed-v4-double-transposition-seed0cdbb4/README.md
new file mode 100644
index 0000000000..aad6415d4b
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/README.md
@@ -0,0 +1,87 @@
+# Mixed double transpositions keep the six-call bill in S4
+
+For three arbitrary dirty roles over \(\mathbb F_2[S_4]\), the heterogeneous
+target
+
+\[
+\operatorname{diag}([(13)(24)],[(12)(34)],[e])
+\]
+
+has exact minimum **six** paid adjacent-transposition calls in the alphabet
+\(\{(12),(23),(34)\}\), even with free scalar \(GL_3(\mathbb F_2)\) mixing.
+The direct word costs four calls for the first target and two for the second.
+A complete formal group-algebra meet excludes all four-call words. A sign
+quotient excludes odd lengths, and the target element \((13)(24)\) has
+adjacent-transposition length four, so no shorter length was overlooked.
+
+## Why this target
+
+The target pair consists of two distinct commuting double transpositions in
+the Klein four subgroup of (S_4). In the broader rank-one-displacement
+alphabet of [PR #1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333),
+the two active entries each have displacement rank two, so the optimistic
+lower-cost screen is four. With only adjacent transpositions, the direct bill
+is six. The question was whether rank-one coupling across the dirty roles can
+meet that four-call floor.
+
+The nearest predecessor is [PR #1734](https://github.com/CrocSwap/integer-mult-bounds/pull/1734),
+which uses the same S4 group, paid alphabet and role count for the repeated
+target \(\operatorname{diag}([(13)(24)],[(13)(24)],[e])\), whose direct bill
+and exact minimum are eight. This package changes the target relation to the
+distinct pair \(((13)(24),(12)(34))\), with direct bill six. PR #1720 treats
+two identical 4-cycles; Discussion #1740 / PR #1749 treats distinct
+noncommuting 3-cycles. Current overlap details are in `OVERLAP.json`.
+
+## Exact evidence
+
+The complete alphabet has 84 factors: three adjacent transpositions times 28
+binary rank-one idempotents. The verifier forms all 7,056 ordered pair words,
+with 4,698 distinct products, then checks all 7,056 target-relative joins.
+This excludes all 49,787,136 four-call words. Pair-state digest and exact
+counts are in `RESULT.json`; the proof and parity argument are in `PROOF.md`.
+
+Positive controls are the exact six-call mixed word and the found/replayed
+four-call word `D_E00(s3), D_E11(s3), D_E11(s1), D_E00(s1)` for
+\(\operatorname{diag}([(12)(34)],[(12)(34)],[e])\). The
+repeated \((13)(24)) target is a negative control. Python recomputes the
+formal algebra independently of the C++ search.
+
+## Reproduce
+
+From the repository root, with Python 3 and a C++17 compiler:
+
+```sh
+python3 -I -B research/s4-mixed-v4-double-transposition-seed0cdbb4/verify.py
+```
+
+Expected prefix:
+
+```text
+PASS_S4_MIXED_V4_DOUBLE_TRANSPOSITION
+```
+
+`VERIFY.json` registers this command. The local replay was run with CPython
+3.14.7 and GCC 16.2.1. Python 3.12 was unavailable locally. Exact base pins,
+the selected record, review and source manifest are listed in `SOURCES.json`.
+
+## Relation to the selected bound
+
+The current selected record remains the complex-bound conditional construction
+and keeps the PR589 rational-address bit supplier. This finite nonabelian
+address result has no exact simulation into that supplier and makes no paid
+moment or \(\kappa\) change. It is a scoped register-model result only.
+
+## Open next questions
+
+Can a different generating set in (S_4) realize this same heterogeneous
+target in four fully charged calls? The first step is to price the new label
+set against its direct word and repeat the complete pair meet; any resulting
+word still needs a source-bound supplier map before it can affect the selected
+conditional bound.
+
+## Credit
+
+The target search, exact implementations, proof and package were prepared with
+substantial OpenAI Codex assistance. PR #1333 and PR #1734 are credited as the
+rank-bound and nearest group-model predecessors. No predecessor code is
+imported, and no independent human review is claimed.
diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/RESULT.json b/research/s4-mixed-v4-double-transposition-seed0cdbb4/RESULT.json
new file mode 100644
index 0000000000..c710f70f9f
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/RESULT.json
@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "group": "S4",
+  "group_order": 24,
+  "roles": 3,
+  "labels": ["s1=(12)", "s2=(23)", "s3=(34)"],
+  "target": ["p=(13)(24)", "q=(12)(34)", "e"],
+  "idempotents": 28,
+  "factors": 84,
+  "direct_word": [
+    "D_E00(s2)",
+    "D_E00(s1)",
+    "D_E00(s3)",
+    "D_E00(s2)",
+    "D_E11(s1)",
+    "D_E11(s3)"
+  ],
+  "q_q_positive_control_word": [
+    "D_E00(s3)",
+    "D_E11(s3)",
+    "D_E11(s1)",
+    "D_E00(s1)"
+  ],
+  "direct_cost": 6,
+  "ordered_pair_words": 7056,
+  "distinct_pair_products": 4698,
+  "pair_products_sha256_sorted_little_endian_u32": "4294d7227bb7e9838624bdf59210011beb7542b759dbd13b5cdbc6bc05c73524",
+  "length_four_words": 49787136,
+  "mixed_target_four_call_hits": 0,
+  "mixed_target_pair_lookups": 7056,
+  "repeated_p_control_hits": 0,
+  "all_six_omissions_rejected": true,
+  "wrong_label_rejected": true,
+  "wrong_target_rejected": true,
+  "q_q_positive_control_hit": true,
+  "q_q_witness_replayed": true,
+  "rank_floor": 4,
+  "word_length_p": 4,
+  "exact_minimum": 6,
+  "direct_mixed_six_call_word_replayed": true,
+  "new_kappa": false
+}
diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/SOURCES.json b/research/s4-mixed-v4-double-transposition-seed0cdbb4/SOURCES.json
new file mode 100644
index 0000000000..596158f3c5
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/SOURCES.json
@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1",
+      "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"
+    },
+    {
+      "path": "docs/research/community-batch1099-review.md",
+      "usage": "provenance",
+      "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099",
+      "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb"
+    },
+    {
+      "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json",
+      "usage": "provenance",
+      "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8",
+      "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b"
+    },
+    {
+      "path": "research/community-frontier1094-audit/ASSEMBLY.json",
+      "usage": "provenance",
+      "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0",
+      "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045"
+    },
+    {
+      "path": "research/bit-three-register-lower-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79",
+      "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"
+    },
+    {
+      "path": "research/binary-affine-register-bound/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "b1152a39b559f7a058489ec74231488e4f8edd83",
+      "sha256": "36a33434222798434b0a17476ae5f9bc8a2a3891871c46e77cc50ce2e132206b"
+    },
+    {
+      "path": "scripts/research_baseline.py",
+      "usage": "provenance",
+      "git_blob": "6b607b36eefd65718120ade3c8187681f11bf879",
+      "sha256": "59d9b04dc33e1bb3f81506d187243435de4902138a038b935e36ebaa5f37db67"
+    }
+  ]
+}
diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/TASK.json b/research/s4-mixed-v4-double-transposition-seed0cdbb4/TASK.json
new file mode 100644
index 0000000000..7cb8859e3d
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/TASK.json
@@ -0,0 +1,104 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 3,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075",
+  "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
+  "chooser_seed": "0cdbb418f7a976685134143f77494c2c",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json"
+    ],
+    "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.",
+    "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": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.",
+    "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."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "refined",
+  "scope_change_reason": "Refine the nonabelian register-model card to a heterogeneous pair of distinct commuting S4 double transpositions; PR #1734 covers the repeated target pair, and the new question is whether shared rank-one calls meet the full-alphabet rank floor.",
+  "actual_scope": "F2[S4], exactly three arbitrary dirty scalar roles, paid adjacent transpositions s1=(12), s2=(23), s3=(34), all 28 binary rank-one idempotents per label, target diag([(13)(24)],[(12)(34)],[e]); exact four-call search.",
+  "changed_assumption_or_expense": "The label alphabet is restricted to the three adjacent transpositions rather than every rank-one binary linear displacement; compare a six-call direct bill with a four-call target-specific rank floor.",
+  "bottleneck_link": "A four-call construction would meet the optimistic rank floor for two active roles, but this finite label restriction has no source-bound translation into the selected rational-address supplier.",
+  "method": "Build all 84 paid factors and all 7,056 ordered pair products in F2[S4] matrices. Use the complete two-plus-two meet for every length-four word; confirm an exact four-call positive target control and the direct six-call mixed word. Use the sign quotient to exclude odd lengths and the Coxeter length of p to exclude lengths below four.",
+  "optimistic_cost_screen": "Direct bill 6 (four factors for p, two for q). A four-call construction would save two calls and meet the rank floor 2+2=4 in PR #1333's larger alphabet. All four calls are fully charged; no extra roles or free address operations are used.",
+  "overlap": {
+    "open_prs": 460,
+    "discussions": 435,
+    "complete_pagination": true,
+    "searched_at_utc": "2026-10-14T10:17:02Z",
+    "warnings": [],
+    "nearest": [
+      {
+        "id": "PR1734",
+        "scope": "same F2[S4] alphabet and three roles; repeated target diag([p],[p],[e]), exact minimum eight",
+        "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1734"
+      },
+      {
+        "id": "PR1720",
+        "scope": "same adjacent-transposition alphabet; two identical 4-cycle targets",
+        "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1720"
+      },
+      {
+        "id": "PR1333",
+        "scope": "binary-affine exact paid-rank theorem; gives optimistic rank floor four with larger operation alphabet",
+        "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1333"
+      },
+      {
+        "id": "Discussion1740 / PR1749",
+        "scope": "four-role S4 model with distinct noncommuting 3-cycles",
+        "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1749"
+      }
+    ],
+    "exact_target_match": false,
+    "note": "Fresh complete find_overlap.py snapshots; targeted cached query found PR #1734 as the nearest S4 double-transposition result and no p,q target match."
+  },
+  "predecessor_heads": {
+    "PR1333": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2",
+    "PR1734": "48855b620b23af3a7fe87d53bde05cd2211342c8"
+  },
+  "claim_url": null,
+  "claim_expiry_utc": "2026-10-14T12:03:00Z",
+  "budget_minutes": 60,
+  "stop_rule": "Complete the exact length-four meet, controls and six-call upper word. If no four-call word exists, finish the parity and support argument; do not expand to other target tuples in this cycle.",
+  "expected_evidence": "Complete all 49,787,136 length-four words via 7,056 ordered-pair states; exact F2[S4] coefficient equality; q,q positive control; p,p negative control; direct six-call mixed witness.",
+  "open_questions": [
+    {
+      "question": "Can another paid transposition set realize the same mixed target at four fully charged calls?",
+      "why_it_matters": "The present exact minimum is two calls above the full rank-one-displacement floor, so a different generating set could expose a concrete sharing mechanism.",
+      "first_step": "Name the new label set, compute the direct target word and full factor alphabet, then run a target-relative pair meet through the optimistic rank floor.",
+      "blocked_by": "Any shorter finite address word still needs a source-bound rational-frame supplier simulation before it can change the selected conditional exponent."
+    }
+  ],
+  "outcome": "negative-result",
+  "evidence": "RESULT.json, PROOF.md, Python exact replay, and a separately implemented C++ complete pair meet.",
+  "author": "OpenAI Codex research agent",
+  "ai_assistance": "Substantial OpenAI Codex assistance in scope selection, exact meet design, implementation, verification and writing; no subagents or independent human review are claimed."
+}
diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/VERIFY.json b/research/s4-mixed-v4-double-transposition-seed0cdbb4/VERIFY.json
new file mode 100644
index 0000000000..d253339e1a
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/VERIFY.json
@@ -0,0 +1,23 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/s4-mixed-v4-double-transposition-seed0cdbb4/verify.py",
+    "research/s4-mixed-v4-double-transposition-seed0cdbb4/search.cpp",
+    "research/s4-mixed-v4-double-transposition-seed0cdbb4/RESULT.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "research/s4-mixed-v4-double-transposition-seed0cdbb4/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Independent Python and C++ exact formal group-algebra pair meets; all 49,787,136 four-call words; state digest/counts; two controls; six-call word; rank and parity bounds."
+    }
+  ]
+}
diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/search.cpp b/research/s4-mixed-v4-double-transposition-seed0cdbb4/search.cpp
new file mode 100644
index 0000000000..53b046a8b0
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/search.cpp
@@ -0,0 +1,264 @@
+#include <algorithm>
+#include <array>
+#include <cstdint>
+#include <iostream>
+#include <map>
+#include <numeric>
+#include <string>
+#include <utility>
+#include <vector>
+
+using Perm = std::array<int, 4>;
+using State = std::array<std::uint32_t, 9>;
+
+struct Factor {
+  int label;
+  int idem;
+  State matrix;
+};
+
+struct PairWord {
+  int first;
+  int second;
+};
+
+static std::array<std::array<int, 24>, 24> group_product{};
+static std::array<Perm, 24> group_elements{};
+
+static Perm compose(const Perm& a, const Perm& b) {
+  Perm c{};
+  for (int i = 0; i < 4; ++i) c[i] = a[b[i]];
+  return c;
+}
+
+static int gid(const Perm& p) {
+  for (int i = 0; i < 24; ++i) if (group_elements[i] == p) return i;
+  return -1;
+}
+
+static std::uint32_t group_mul(std::uint32_t x, std::uint32_t y) {
+  std::uint32_t out = 0;
+  while (x) {
+    int a = __builtin_ctz(x);
+    x &= x - 1;
+    std::uint32_t yy = y;
+    while (yy) {
+      int b = __builtin_ctz(yy);
+      yy &= yy - 1;
+      out ^= (std::uint32_t(1) << group_product[a][b]);
+    }
+  }
+  return out;
+}
+
+static State multiply(const State& a, const State& b) {
+  State c{};
+  for (int i = 0; i < 3; ++i)
+    for (int j = 0; j < 3; ++j)
+      for (int k = 0; k < 3; ++k)
+        c[3 * i + j] ^= group_mul(a[3 * i + k], b[3 * k + j]);
+  return c;
+}
+
+static State identity_state(int e) {
+  State s{};
+  for (int i = 0; i < 3; ++i) s[3 * i + i] = std::uint32_t(1) << e;
+  return s;
+}
+
+static State target_state(int p, int q, int e) {
+  State s{};
+  s[0] = std::uint32_t(1) << p;
+  s[4] = std::uint32_t(1) << q;
+  s[8] = std::uint32_t(1) << e;
+  return s;
+}
+
+static std::vector<std::pair<int, int>> idempotents() {
+  std::vector<std::pair<int, int>> ns;
+  for (int x = 1; x < 8; ++x)
+    for (int y = 1; y < 8; ++y)
+      if (__builtin_parity(unsigned(x & y))) ns.emplace_back(x, y);
+  return ns;
+}
+
+static std::vector<Factor> make_factors(const std::array<int, 3>& labels,
+                                       const std::vector<std::pair<int, int>>& ns,
+                                       int e) {
+  std::vector<Factor> fs;
+  for (int li = 0; li < 3; ++li) {
+    for (int ni = 0; ni < int(ns.size()); ++ni) {
+      auto [x, y] = ns[ni];
+      State s{};
+      for (int i = 0; i < 3; ++i) {
+        for (int j = 0; j < 3; ++j) {
+          bool nij = ((x >> i) & 1) && ((y >> j) & 1);
+          if (i == j) s[3 * i + j] ^= (std::uint32_t(1) << e);
+          if (nij) {
+            s[3 * i + j] ^= (std::uint32_t(1) << e);
+            s[3 * i + j] ^= (std::uint32_t(1) << labels[li]);
+          }
+        }
+      }
+      fs.push_back(Factor{li, ni, s});
+    }
+  }
+  return fs;
+}
+
+static State translate_left_diagonal(const State& diagonal_target,
+                                     const State& right) {
+  State out{};
+  for (int i = 0; i < 3; ++i) {
+    int g = __builtin_ctz(diagonal_target[3 * i + i]);
+    for (int j = 0; j < 3; ++j) {
+      std::uint32_t cell = right[3 * i + j];
+      while (cell) {
+        int h = __builtin_ctz(cell);
+        cell &= cell - 1;
+        out[3 * i + j] ^= (std::uint32_t(1) << group_product[g][h]);
+      }
+    }
+  }
+  return out;
+}
+
+struct SearchResult {
+  bool found = false;
+  std::array<int, 4> word{};
+  std::size_t lookups = 0;
+};
+
+static SearchResult search_four(const State& target,
+                                const std::vector<Factor>& fs,
+                                const std::vector<State>& pair_states,
+                                const std::map<State, PairWord>& pair_index) {
+  SearchResult result;
+  const int n = int(fs.size());
+  for (int f4 = 0; f4 < n; ++f4) {
+    for (int f3 = 0; f3 < n; ++f3) {
+      ++result.lookups;
+      const State& inverse_suffix = pair_states[f4 * n + f3];
+      State needed_prefix = translate_left_diagonal(target, inverse_suffix);
+      auto hit = pair_index.find(needed_prefix);
+      if (hit != pair_index.end()) {
+        result.found = true;
+        result.word = {hit->second.first, hit->second.second, f3, f4};
+        return result;
+      }
+    }
+  }
+  return result;
+}
+
+static bool is_direct(const std::vector<Factor>& fs,
+                      const std::vector<int>& word,
+                      const State& target) {
+  State acc = identity_state(0);
+  for (int f : word) acc = multiply(acc, fs[f].matrix);
+  return acc == target;
+}
+
+static bool is_four_word(const std::vector<Factor>& fs,
+                         const std::array<int, 4>& word,
+                         const State& target) {
+  State acc = identity_state(0);
+  for (int f : word) acc = multiply(acc, fs[f].matrix);
+  return acc == target;
+}
+
+static std::string word_text(const std::vector<Factor>& fs,
+                             const std::array<int, 4>& word) {
+  std::string out;
+  const char* label_names[] = {"s1", "s2", "s3"};
+  for (int i = 0; i < 4; ++i) {
+    if (i) out += ",";
+    const Factor& f = fs[word[i]];
+    out += label_names[f.label];
+    out += ":N" + std::to_string(f.idem);
+  }
+  return out;
+}
+
+int main() {
+  Perm p{0, 1, 2, 3};
+  int k = 0;
+  do { group_elements[k++] = p; } while (std::next_permutation(p.begin(), p.end()));
+  if (k != 24) return 2;
+  for (int a = 0; a < 24; ++a)
+    for (int b = 0; b < 24; ++b)
+      group_product[a][b] = gid(compose(group_elements[a], group_elements[b]));
+
+  int e = gid(Perm{0, 1, 2, 3});
+  int s1 = gid(Perm{1, 0, 2, 3});
+  int s2 = gid(Perm{0, 2, 1, 3});
+  int s3 = gid(Perm{0, 1, 3, 2});
+  int p13p24 = gid(Perm{2, 3, 0, 1});
+  int p12p34 = gid(Perm{1, 0, 3, 2});
+  int p14p23 = gid(Perm{3, 2, 1, 0});
+  int p_word = group_product[group_product[group_product[s2][s1]][s3]][s2];
+  int q_word = group_product[s1][s3];
+  if (p_word != p13p24 || q_word != p12p34 ||
+      group_product[p13p24][p12p34] != p14p23) return 3;
+
+  const std::array<int, 3> labels{s1, s2, s3};
+  auto ns = idempotents();
+  auto fs = make_factors(labels, ns, e);
+  if (ns.size() != 28 || fs.size() != 84) return 4;
+  auto idem_id = [&](int x, int y) {
+    for (int i = 0; i < int(ns.size()); ++i)
+      if (ns[i] == std::make_pair(x, y)) return i;
+    return -1;
+  };
+  const int e00 = idem_id(1, 1);
+  const int e11 = idem_id(2, 2);
+  if (e00 < 0 || e11 < 0) return 6;
+
+  std::vector<State> pair_states;
+  pair_states.reserve(fs.size() * fs.size());
+  std::map<State, PairWord> pair_index;
+  for (int f1 = 0; f1 < int(fs.size()); ++f1) {
+    for (int f2 = 0; f2 < int(fs.size()); ++f2) {
+      State state = multiply(fs[f1].matrix, fs[f2].matrix);
+      pair_states.push_back(state);
+      pair_index.emplace(state, PairWord{f1, f2});
+    }
+  }
+
+  State mixed = target_state(p13p24, p12p34, e);
+  State repeated = target_state(p13p24, p13p24, e);
+  State easy = target_state(p12p34, p12p34, e);
+  SearchResult mixed_result = search_four(mixed, fs, pair_states, pair_index);
+  SearchResult repeated_result = search_four(repeated, fs, pair_states, pair_index);
+  SearchResult easy_result = search_four(easy, fs, pair_states, pair_index);
+  bool mixed_witness_ok = !mixed_result.found || is_four_word(fs, mixed_result.word, mixed);
+  bool repeated_witness_ok = !repeated_result.found || is_four_word(fs, repeated_result.word, repeated);
+  bool easy_witness_ok = easy_result.found && is_four_word(fs, easy_result.word, easy);
+
+  std::vector<int> direct_mixed{
+      28 * 1 + e00, 28 * 0 + e00, 28 * 2 + e00, 28 * 1 + e00,
+      28 * 0 + e11, 28 * 2 + e11};
+  bool direct_ok = is_direct(fs, direct_mixed, mixed);
+  std::vector<int> direct_easy{28 * 0 + e00, 28 * 2 + e00,
+                               28 * 0 + e11, 28 * 2 + e11};
+  bool easy_direct_ok = is_direct(fs, direct_easy, easy);
+
+  std::cout << "RESULT group_order=24 idempotents=" << ns.size()
+            << " factors=" << fs.size()
+            << " pair_words=" << pair_states.size()
+            << " unique_pair_states=" << pair_index.size()
+            << " four_call_words=" << (std::size_t(fs.size()) * fs.size() * fs.size() * fs.size())
+            << " mixed=" << (mixed_result.found ? "hit" : "none")
+            << " mixed_lookups=" << mixed_result.lookups
+            << " repeated=" << (repeated_result.found ? "hit" : "none")
+            << " easy_positive=" << (easy_result.found ? "hit" : "none")
+            << " witnesses=" << ((mixed_witness_ok && repeated_witness_ok && easy_witness_ok) ? "pass" : "FAIL")
+            << " easy_direct=" << (easy_direct_ok ? "pass" : "FAIL")
+            << " direct_mixed_six=" << (direct_ok ? "pass" : "FAIL") << "\n";
+  if (mixed_result.found)
+    std::cout << "MIXED_WITNESS " << word_text(fs, mixed_result.word) << "\n";
+  if (easy_result.found)
+    std::cout << "EASY_WITNESS " << word_text(fs, easy_result.word) << "\n";
+  return (!direct_ok || !easy_direct_ok || !easy_result.found ||
+          !mixed_witness_ok || !repeated_witness_ok || !easy_witness_ok) ? 5 : 0;
+}
diff --git a/research/s4-mixed-v4-double-transposition-seed0cdbb4/verify.py b/research/s4-mixed-v4-double-transposition-seed0cdbb4/verify.py
new file mode 100644
index 0000000000..a2abaef91f
--- /dev/null
+++ b/research/s4-mixed-v4-double-transposition-seed0cdbb4/verify.py
@@ -0,0 +1,276 @@
+#!/usr/bin/env python3
+"""Independent exact pair-meet replay for the mixed S4 target."""
+
+from __future__ import annotations
+
+import hashlib
+import itertools
+import json
+from pathlib import Path
+import struct
+import subprocess
+import tempfile
+
+
+PACKAGE = Path(__file__).resolve().parent
+
+
+def compose(a, b):
+    return tuple(a[b[i]] for i in range(4))
+
+
+def ga_mul(a, b, group_product):
+    out = 0
+    while a:
+        abit = a & -a
+        i = abit.bit_length() - 1
+        a ^= abit
+        bb = b
+        while bb:
+            bbit = bb & -bb
+            j = bbit.bit_length() - 1
+            bb ^= bbit
+            out ^= 1 << group_product[i][j]
+    return out
+
+
+def mat_mul(a, b, group_product):
+    out = [0] * 9
+    for i in range(3):
+        for j in range(3):
+            cell = 0
+            for k in range(3):
+                cell ^= ga_mul(a[3 * i + k], b[3 * k + j], group_product)
+            out[3 * i + j] = cell
+    return tuple(out)
+
+
+def rank_f2(rows, ncols):
+    rows = [int(r) for r in rows]
+    pivot = 0
+    for col in range(ncols):
+        hit = next((r for r in range(pivot, len(rows)) if (rows[r] >> col) & 1), None)
+        if hit is None:
+            continue
+        rows[pivot], rows[hit] = rows[hit], rows[pivot]
+        for r in range(len(rows)):
+            if r != pivot and ((rows[r] >> col) & 1):
+                rows[r] ^= rows[pivot]
+        pivot += 1
+        if pivot == len(rows):
+            break
+    return pivot
+
+
+def linear_displacement_rank(perm):
+    # Columns of the permutation matrix are e_i -> e_perm[i].
+    rows = []
+    for r in range(4):
+        row = 0
+        for c in range(4):
+            value = int(perm[c] == r) ^ int(r == c)
+            row |= value << c
+        rows.append(row)
+    return rank_f2(rows, 4)
+
+
+def exact_search(target, pair_states, pair_index, n_factors, group_product):
+    lookups = 0
+    for f4 in range(n_factors):
+        for f3 in range(n_factors):
+            lookups += 1
+            inverse_suffix = pair_states[f4 * n_factors + f3]
+            needed_prefix = [0] * 9
+            for i in range(3):
+                g = (target[3 * i + i] & -target[3 * i + i]).bit_length() - 1
+                for j in range(3):
+                    cell = inverse_suffix[3 * i + j]
+                    while cell:
+                        bit = cell & -cell
+                        h = bit.bit_length() - 1
+                        cell ^= bit
+                        needed_prefix[3 * i + j] ^= 1 << group_product[g][h]
+            prefix = tuple(needed_prefix)
+            if prefix in pair_index:
+                left = pair_index[prefix]
+                return (left[0], left[1], f3, f4), lookups
+    return None, lookups
+
+
+def main():
+    permutations = list(itertools.permutations(range(4)))
+    group_id = {p: i for i, p in enumerate(permutations)}
+    group_product = [
+        [group_id[compose(a, b)] for b in permutations]
+        for a in permutations
+    ]
+    e = group_id[(0, 1, 2, 3)]
+    s1 = group_id[(1, 0, 2, 3)]
+    s2 = group_id[(0, 2, 1, 3)]
+    s3 = group_id[(0, 1, 3, 2)]
+    p = group_id[(2, 3, 0, 1)]
+    q = group_id[(1, 0, 3, 2)]
+    r = group_id[(3, 2, 1, 0)]
+    assert group_product[group_product[group_product[s2][s1]][s3]][s2] == p
+    assert group_product[s1][s3] == q
+    assert group_product[p][q] == r
+
+    idempotents = [
+        (x, y)
+        for x in range(1, 8)
+        for y in range(1, 8)
+        if (x & y).bit_count() & 1
+    ]
+    assert len(idempotents) == 28
+    label_values = (s1, s2, s3)
+    factors = []
+    for label, g in enumerate(label_values):
+        for idem, (x, y) in enumerate(idempotents):
+            state = [0] * 9
+            for i in range(3):
+                for j in range(3):
+                    nij = ((x >> i) & 1) and ((y >> j) & 1)
+                    if i == j:
+                        state[3 * i + j] ^= 1 << e
+                    if nij:
+                        state[3 * i + j] ^= (1 << e) | (1 << g)
+            factors.append((label, idem, tuple(state)))
+    assert len(factors) == 84
+    identity = [0] * 9
+    for i in range(3):
+        identity[3 * i + i] = 1 << e
+    identity = tuple(identity)
+    assert all(mat_mul(factor[2], factor[2], group_product) == identity for factor in factors)
+
+    pair_states = []
+    pair_index = {}
+    for f1, f2 in itertools.product(range(84), repeat=2):
+        state = mat_mul(factors[f1][2], factors[f2][2], group_product)
+        pair_states.append(state)
+        pair_index.setdefault(state, (f1, f2))
+    assert len(pair_states) == 7056
+
+    pair_digest = hashlib.sha256(
+        b"".join(struct.pack("<9I", *state) for state in sorted(pair_index))
+    ).hexdigest()
+
+    def target_state(g0, g1):
+        out = [0] * 9
+        out[0] = 1 << g0
+        out[4] = 1 << g1
+        out[8] = 1 << e
+        return tuple(out)
+
+    mixed = target_state(p, q)
+    repeated = target_state(p, p)
+    easy = target_state(q, q)
+    mixed_word, mixed_lookups = exact_search(mixed, pair_states, pair_index, 84, group_product)
+    repeated_word, repeated_lookups = exact_search(repeated, pair_states, pair_index, 84, group_product)
+    easy_word, easy_lookups = exact_search(easy, pair_states, pair_index, 84, group_product)
+
+    idem_id = {xy: i for i, xy in enumerate(idempotents)}
+    e00 = idem_id[(1, 1)]
+    e11 = idem_id[(2, 2)]
+    direct_mixed = [28 + e00, e00, 56 + e00, 28 + e00, e11, 56 + e11]
+    direct_easy = [e00, 56 + e00, e11, 56 + e11]
+    coupled_easy = [56 + e00, 56 + e11, e11, e00]
+
+    def replay(word):
+        acc = [0] * 9
+        for i in range(3):
+            acc[3 * i + i] = 1 << e
+        for f in word:
+            acc = mat_mul(tuple(acc), factors[f][2], group_product)
+        return tuple(acc)
+
+    assert replay(direct_mixed) == mixed
+    assert replay(direct_easy) == easy
+    assert all(replay(direct_mixed[:i] + direct_mixed[i + 1:]) != mixed for i in range(6))
+    wrong_label_word = direct_mixed.copy()
+    wrong_label_word[0] = e00
+    assert replay(wrong_label_word) != mixed
+    assert replay(direct_mixed) != target_state(p, r)
+    assert mixed_word is None and mixed_lookups == 7056
+    assert repeated_word is None and repeated_lookups == 7056
+    assert easy_word is not None and easy_lookups <= 7056
+    assert replay(easy_word) == easy
+    assert easy_word == tuple(coupled_easy)
+
+    # Any subword yielding p needs at least four adjacent transpositions.
+    p_perm = permutations[p]
+    q_perm = permutations[q]
+    p_length = sum(p_perm[i] > p_perm[j] for i in range(4) for j in range(i + 1, 4))
+    q_length = sum(q_perm[i] > q_perm[j] for i in range(4) for j in range(i + 1, 4))
+    assert p_length == 4 and q_length == 2
+    assert linear_displacement_rank(p_perm) == 2
+    assert linear_displacement_rank(q_perm) == 2
+    assert p_length % 2 == 0 and q_length % 2 == 0
+
+    receipt = {
+        "schema_version": 1,
+        "group": "S4",
+        "group_order": 24,
+        "roles": 3,
+        "labels": ["s1=(12)", "s2=(23)", "s3=(34)"],
+        "target": ["p=(13)(24)", "q=(12)(34)", "e"],
+        "direct_word": [
+            "D_E00(s2)", "D_E00(s1)", "D_E00(s3)", "D_E00(s2)",
+            "D_E11(s1)", "D_E11(s3)",
+        ],
+        "direct_cost": 6,
+        "q_q_positive_control_word": [
+            "D_E00(s3)", "D_E11(s3)", "D_E11(s1)", "D_E00(s1)"
+        ],
+        "idempotents": len(idempotents),
+        "factors": len(factors),
+        "ordered_pair_words": len(pair_states),
+        "distinct_pair_products": len(pair_index),
+        "pair_products_sha256_sorted_little_endian_u32": pair_digest,
+        "length_four_words": 84**4,
+        "mixed_target_four_call_hits": 0,
+        "mixed_target_pair_lookups": mixed_lookups,
+        "repeated_p_control_hits": 0,
+        "all_six_omissions_rejected": True,
+        "wrong_label_rejected": True,
+        "wrong_target_rejected": True,
+        "q_q_positive_control_hit": True,
+        "q_q_witness_replayed": True,
+        "direct_mixed_six_call_word_replayed": True,
+        "rank_floor": 4,
+        "word_length_p": 4,
+        "exact_minimum": 6,
+        "new_kappa": False,
+    }
+
+    # Cross-check the independent C++ implementation.
+    with tempfile.TemporaryDirectory(prefix="s4-mixed-v4-") as tmp:
+        exe = Path(tmp) / "search"
+        subprocess.run(
+            ["g++", "-std=c++17", "-O2", "-Wall", "-Wextra", "-Werror",
+             str(PACKAGE / "search.cpp"), "-o", str(exe)],
+            check=True, capture_output=True, text=True,
+        )
+        native = subprocess.run([str(exe)], check=True, capture_output=True, text=True)
+    fields = dict(token.split("=", 1) for token in native.stdout.splitlines()[0].split()[1:])
+    assert fields["group_order"] == "24"
+    assert fields["idempotents"] == "28"
+    assert fields["factors"] == "84"
+    assert fields["pair_words"] == "7056"
+    assert fields["unique_pair_states"] == str(len(pair_index))
+    assert fields["four_call_words"] == str(84**4)
+    assert fields["mixed"] == "none" and fields["mixed_lookups"] == "7056"
+    assert fields["repeated"] == "none"
+    assert fields["easy_positive"] == "hit" and fields["witnesses"] == "pass"
+    assert fields["easy_direct"] == "pass" and fields["direct_mixed_six"] == "pass"
+    assert native.stdout.splitlines()[1] == "EASY_WITNESS s3:N0,s3:N4,s1:N4,s1:N0"
+
+    expected_path = PACKAGE / "RESULT.json"
+    if expected_path.exists():
+        expected = json.loads(expected_path.read_text())
+        assert receipt == expected, "deterministic exact-search receipt changed"
+
+    print("PASS_S4_MIXED_V4_DOUBLE_TRANSPOSITION " + json.dumps(receipt, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()