Research: mixed S4 double transpositions need six calls

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.

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.

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."
+}

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.

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\).

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.