Exact S4 cost: two double-transposition targets need eight calls

research/s4-double-transposition-seedb270/CERTIFICATE.json

@@ -0,0 +1,79 @@
+{
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "controls": {
+    "all_28_idempotents_rank_one": true,
+    "all_3_paid_displacements_rank_one": true,
+    "all_84_factor_involutions": true,
+    "altered_dirty_role_target_rejected": true,
+    "gl3_f2_determinants_one": true,
+    "gl3_f2_order": 168,
+    "target_displacement_rank_two": true
+  },
+  "cost_screen": {
+    "best_strict_improvement_bill": 6,
+    "call_saving_required": 2,
+    "direct_bill": 8,
+    "natural_representation_rank_floor": 4,
+    "sign_determinant_forces_even_length": true
+  },
+  "direct_word": {
+    "adjacent_transposition_indices": [
+      1,
+      0,
+      2,
+      1
+    ],
+    "all_single_call_omissions_rejected": 8,
+    "formal_endpoint_verified": true,
+    "paid_call_count": 8
+  },
+  "meet_in_middle": {
+    "all_calls_involutive": true,
+    "exact_minimum": 8,
+    "exact_minimum_if_within_six": 8,
+    "intersection_count": 0,
+    "left_layer_counts": [
+      1,
+      84,
+      4697,
+      232692
+    ],
+    "left_sorted_state_sha256": "050e8b23a52a22b845208eb0a241872e53511f7843dbf5c6e42b3eda4bc757ac",
+    "left_state_count": 237474,
+    "radius_each_side": 3,
+    "right_layer_counts": [
+      1,
+      84,
+      4697,
+      232692
+    ],
+    "right_sorted_state_sha256": "caf772096918c6a120a394f7f734667e9bf69d67a871f868d4063a848f87827a",
+    "right_state_count": 237474,
+    "shortest_meeting_length": null,
+    "shortest_word_factor_ids": null
+  },
+  "model": {
+    "active_targets": 2,
+    "address_group": "S4",
+    "dirty_roles": "all three arbitrary inputs; third role restored exactly",
+    "endpoint_ring": "formal F2[S4]",
+    "field": "F2",
+    "free_scalar_mixing": "all GL3(F2), normalized by augmentation",
+    "paid_factor_count": 84,
+    "paid_letters": [
+      "(12)",
+      "(23)",
+      "(34)"
+    ],
+    "rank_one_idempotents": 28,
+    "roles": 3,
+    "target_permutation": "(13)(24)"
+  },
+  "runtime_seconds_excluded_from_receipt": true,
+  "schema_version": 1,
+  "seed": "b270b3b52d302ab6281ea2bc042d4aea",
+  "selected_frontier": "unchanged; no supplier or kappa claim",
+  "selected_result_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
+  "task_id": "bit-new-register-model",
+  "track": "bit-mechanisms"
+}

research/s4-double-transposition-seedb270/CLAIM.md

@@ -0,0 +1,18 @@
+# Local scope claim — S4 double-transposition pair
+
+- **Track / accepted draw:** `bit-mechanisms`, seed `b270b3b52d302ab6281ea2bc042d4aea`.
+- **Task / catalogue:** `bit-new-register-model`, priority revision 3; `docs/research/agent-task-catalog.json` SHA-256 `6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075`.
+- **Exact base:** `0b1cccf86e2f5132ed286a26ef0a681a495740ea` (`origin/main`).
+- **Selected record:** SHA-256 `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`.
+- **Scope key:** `032dead5b9f6bb2216f0` (first 20 hex characters of SHA-256 of the canonical scope below).
+- **Scope-key input:** `In formal F2[S4] register circuits over three dirty scalar roles, determine the minimum paid-call count for diag([(13)(24)],[(13)(24)],[e]) using each of (12),(23),(34) at cost 1, all rank-one idempotents N over F2, and arbitrary free interleaved GL3(F2) scalar mixing; compare against direct cost 8.`
+- **Canonical scope:** In formal `F2[S4]`, with three arbitrary dirty scalar roles, all 28 rank-one idempotents over F2, and the three paid adjacent transpositions `(12),(23),(34)` at one call each, determine the exact minimum for `diag([(13)(24)],[(13)(24)],[e])`, while allowing arbitrary free interleaved `GL3(F2)` mixing. Search only the complete parity-permitted radius-3 meet (all words of length at most 6); compare with the eight-call direct construction.
+- **Changed hypothesis / expense:** replace the abelian rational-address model by this fixed nonabelian Coxeter alphabet; every paid letter is counted, while free scalar mixing and the restored third dirty role are granted optimistically at no extra charge.
+- **Cost screen:** direct bill 8. The natural permutation representation gives a rank floor 4, and the sign determinant quotient forces even word length. The best possible strict improvement is therefore 6 calls (save 2/25%). If the exact radius-3 balls are disjoint, the declared endpoint has exact cost 8 and no local saving.
+- **Predecessors / overlap:** PR #1720 at head `edb4a289a5f32c8209140144e384dcd3fa8cbfd1` studies two 4-cycle targets in the same S4 / three-role / adjacent-transposition model; this claim changes the endpoint to a rank-2 double transposition, where Coxeter length exceeds displacement rank. PR #1443 (merged at `965ff75aabb16cdd0978f4bf9222bcdedf514021`) studies two-register D8 central targets. The cached complete Discussion scan (351 records, fetched 2026-10-14 07:28:35Z) contains an exact UT3 third-role follow-up but no S4 `(2,2)` target claim. A direct REST open-PR census at 2026-10-14 08:00Z found no S4 double-transposition match; nearby #1720, #1705, #1711 and the UT3/UT4 results have different target groups or endpoints. `find_overlap.py --refresh` could not refresh PRs (`gh api --slurp` unsupported by installed gh) or Discussions (GitHub GraphQL rate limit). Recent Discussions could not be freshly rechecked or written to because of that API limit, so this claim is local.
+- **Expected deliverable:** a full formal group-algebra identity for the direct eight-call word, exact complete radius-3 balls from identity and target, plus proof that they are disjoint or an extracted six-call construction. Finite controls check all 84 involutive factors, direct endpoint, call omissions and an altered dirty-role target. No selected-kappa claim.
+- **Expiry:** 2026-10-14 08:40 UTC.
+
+The selector was run from this cycle's exact-base worktree. It discarded seeds `8ccb721845414467f1587f50e18a6252` (consolidation), `1bb2bb9d8fbe33f2d7d4099fb9db95f1` (adversarial-audit) and `72d16ec637edc91f2b0fa7c754335a35` (independent-verification), then accepted the seed above. A previous selector invocation from the separate cycle-2 worktree returned `18291c3ad5e0953d9e5f16c79f345b06` against that PR branch; it was discarded before any experiment because its base was not this cycle's main commit.
+
+The live claim was initially unavailable while the GitHub API was rate-limited. After the fresh Discussion refresh at 08:09 UTC, I posted the completed finding to [coordination Discussion #1163](https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18919260), then submitted [PR #1734](https://github.com/CrocSwap/integer-mult-bounds/pull/1734). A final DONE reply records the PR head and remaining obligations.

research/s4-double-transposition-seedb270/PROOF.md

@@ -0,0 +1,100 @@
+# Exact cost of a pair of S4 double transpositions
+
+## Theorem
+
+Let `R = F2[S4]`, let the number of scalar roles be `W=3`, and define a paid
+call for `s in {(12),(23),(34)}` and a rank-one idempotent `N in M3(F2)` by
+
+```text
+D(s,N) = I + ([s]+[e])N.
+```
+
+Allow arbitrary free interleaved scalar `GL3(F2)` changes of basis. For
+arbitrary dirty inputs, the complete endpoint
+
+```text
+diag([(13)(24)], [(13)(24)], [e])
+```
+
+has exact paid-call minimum eight.
+
+## Upper bound
+
+With right multiplication as the word convention, put
+`s1=(12)`, `s2=(23)`, `s3=(34)`. Direct composition gives
+`q=s2*s1*s3*s2=(13)(24)`. Four calls with `N=E11` place `[q]` in the first
+diagonal role; four with `N=E22` place `[q]` in the second. Every other entry
+is the identity, so this is a formal `R`-matrix identity on arbitrary input,
+including the restored third dirty role. Thus the minimum is at most eight.
+
+## Normalize free scalar maps
+
+Write a free scalar map as `A tensor [e]`. Moving it to the right across a
+paid factor uses
+
+```text
+(A tensor 1) D(s,N) = D(s, A N A^-1) (A tensor 1).
+```
+
+Conjugation preserves rank one and idempotence, so the 84 factors already
+include every normalized choice. The augmentation homomorphism
+`epsilon:R->F2`, `epsilon([g])=1`, sends every paid factor to `I`. The target
+also augments to `I3`. Therefore the product of the moved free scalar maps
+must be `I3`. No extra words are introduced by free mixing.
+
+## Even-length obstruction
+
+The sign character gives a ring homomorphism
+`F2[S4] -> F2[C2]`; denote the nonidentity basis element of `C2` by `x`, so
+`x^2=1`. Every adjacent transposition maps to `x`, whereas
+`q=(13)(24)` maps to `1`. The target therefore maps to the identity matrix.
+
+For any rank-one idempotent `N=u v^T`, `v^T u=1`, and the paid factor maps to
+`I+(x+1)u v^T`. The coefficient ring is commutative, so the determinant
+lemma yields
+
+```text
+det(I+(x+1)u v^T) = 1 + (x+1)v^T u = x.
+```
+
+Each free `GL3(F2)` map has determinant one, since the only nonzero element of
+`F2` is one. Determinants multiply, so an endpoint word with `k` paid calls
+has determinant `x^k`; the target determinant is one. Since `x` has order
+two, `k` is even. Any strict improvement over the eight-call direct word
+would therefore have length at most six.
+
+## Complete six-call exclusion
+
+Each `D(s,N)` is an involution. In `R`, `a=[s]+[e]` satisfies `a^2=0` in
+characteristic two; using `N^2=N`,
+
+```text
+D(s,N)^2 = I + 2aN + a^2 N = I.
+```
+
+Consider the right-multiplication Cayley graph on all `3x3` matrices over
+`R`, starting either at identity `I3` or at target `T`. The verifier
+enumerates the full radius-three balls using all three labels and all 28
+rank-one idempotents. A word of length at most six splits as `AB` with
+`|A|,|B|<=3`. If `AB=T`, involutivity gives `A=T B^-1`, so the intermediate
+state belongs to both balls. The independently enumerated exact balls have
+layers `[1,84,4697,232692]` and empty intersection. Hence no word of length
+at most six reaches the target.
+
+The state stores every coefficient of every matrix entry in `F2[S4]` as a
+24-bit mask; the implementation packs the nine masks into 27 bytes for the
+visited-state keys. It performs no address specialization, probability
+sampling, rank pruning or assumed group-ring faithfulness. Sorted state hashes
+and counts are in `CERTIFICATE.json`; replay recomputes all states and hashes.
+
+Together with the direct word and even-length obstruction, the exact minimum
+is eight.
+
+## Exactness boundary
+
+The theorem is for this fixed finite group, paid-letter set, role count and
+endpoint. The natural permutation representation only gives the four-call
+rank floor and is not used to prove the stronger exclusion. This does not
+establish that any supplier can provide these operations, that the model
+occurs in a selected circuit, or that any recursive moment or conditional
+multiplication bound changes.

research/s4-double-transposition-seedb270/README.md

@@ -0,0 +1,158 @@
+# Two S4 double-transposition targets need eight paid calls
+
+**Scoped exact negative result; no new κ.** With three dirty scalar roles,
+free `GL3(F2)` mixing and the paid alphabet of adjacent transpositions, two
+copies of the S4 double transposition `(13)(24)` require exactly eight calls.
+The natural displacement-rank floor is only four, so this test asks whether
+register mixing can use that gap. A sign-determinant parity argument and a
+complete formal radius-three meet-in-the-middle exclude every possible
+improvement to six calls.
+
+## Exact model and optimistic cost
+
+Let `R = F2[S4]`. There are three scalar roles over `F2`, all with arbitrary
+dirty input. A call chooses one adjacent transposition
+`s in {(12),(23),(34)}` and one of the 28 rank-one idempotents
+`N = u v^T in M3(F2)` with `v^T u = 1`, and applies
+
+```text
+D(s,N) = I3 + ([s] + [e]) N.
+```
+
+Every call costs one. Arbitrary interleaved scalar `GL3(F2)` maps are free.
+The endpoint is the full formal group-algebra matrix
+`diag([(13)(24)],[(13)(24)],[e])`; therefore the third arbitrary dirty role
+is restored identically. The complete alphabet has 3×28=84 paid factors.
+
+The direct Coxeter word for `(13)(24)` has length four, so the two-target
+upper bill is eight. In the natural permutation representation on `F2^4`,
+each adjacent transposition has displacement rank one, while `(13)(24)` has
+rank two. Rank subadditivity therefore gives a four-call lower floor. The
+strict improvement objective is six calls or fewer, a two-call / 25% saving.
+This screen grants free register mixing and the third role without any
+separate hosting, allocation or restoration charge, and charges every paid
+address call. It is an optimistic local model, not a physical bit supplier.
+
+The accepted selected record is
+`κ = 836330098538459/500000000000000000`, with selected-record SHA-256
+`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`.
+Its review is `docs/research/community-batch1099-review.md`; the source
+manifest is `research/community-frontier1094-audit/SELECTED-SOURCE.json`; the
+assembly certificate is
+`research/community-frontier1094-audit/ASSEMBLY.json` (SHA-256
+`1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045`); the
+reproduction command is `make frontier1094-verify`. The binding-only baseline
+reports the complex primitive as binding. This result has no supplier
+occurrence, recursive moment or selected-κ implication.
+
+## Exact lower bound and matching construction
+
+The selected word `s2 s1 s3 s2` (where `s1=(12)`, `s2=(23)`, `s3=(34)`)
+equals `(13)(24)`. Applying it with coordinate idempotent `E11`, then with
+`E22`, gives the exact eight-call formal endpoint. All eight single-call
+omissions and an endpoint changed on the dirty third role fail exact replay.
+
+For the lower bound, augmentation `ε([g])=1` sends every paid factor to the
+identity. Move any free scalar map through a paid factor by conjugating `N`;
+the conjugate remains a rank-one idempotent. The product of all free maps is
+then the identity by augmentation, so it suffices to enumerate words in the
+84-factor alphabet.
+
+The sign homomorphism `S4 -> C2` sends every paid adjacent transposition to
+the nontrivial element `x`, with `x^2=1`, and sends the even target
+`(13)(24)` to the identity. Over the commutative ring `F2[C2]`, the matrix
+determinant lemma gives
+`det(I + (x+1) u v^T) = 1 + (x+1) v^T u = x`.
+Every scalar `GL3(F2)` map has determinant one. Hence a `k`-call word reaching
+the target must satisfy `x^k=1`, so `k` is even. A strict improvement over
+eight must consequently use at most six calls.
+
+Every paid factor is an involution because `( [s]+[e] )^2=0` in
+characteristic two. Any word of length at most six splits into two words of
+length at most three. Reversing the second part from the target would put an
+intermediate matrix in both radius-three balls. The exact search enumerates
+all such formal matrices, storing each 3×3 matrix as nine 24-bit
+`F2[S4]` coefficient masks. Each ball has layer counts
+`[1,84,4697,232692]`, for 237,474 states; their intersection is empty.
+The hashes of the sorted packed states are recorded in
+[CERTIFICATE.json](CERTIFICATE.json). The two upper/lower arguments establish
+that the exact minimum in this model is eight.
+
+This is an exact theorem about one finite paid alphabet and one endpoint,
+not a test over selected address columns. The natural representation supplies
+only the weaker rank floor; the final exclusion uses the complete formal
+group-algebra balls. The proof does not rely on faithfulness of the natural
+group-algebra representation.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+python3.12 -I -B research/s4-double-transposition-seedb270/verify.py
+python3.12 scripts/research_package.py --package research/s4-double-transposition-seedb270 --check-only
+python3.12 scripts/research_package.py --package research/s4-double-transposition-seedb270
+```
+
+Expected verifier output begins:
+
+```text
+PASS_S4_DOUBLE_TRANSPOSITION EXACT_8 direct=8 rank_floor=4 parity=even factors=84
+balls=237474,237474 intersections=0 layers=[1, 84, 4697, 232692]
+```
+
+On Python 3.12.3 the full exact replay took about 3.1 seconds and used 93 MiB
+peak resident memory as measured by `/usr/bin/time -v`. The certificate stores
+deterministic complete-ball hashes, not an unbounded or sampled search.
+
+## Scope and overlap
+
+The main nonabelian register predecessors are PR #1720 (head
+`edb4a289a5f32c8209140144e384dcd3fa8cbfd1`), which treats two 4-cycle targets
+in S4 with the same adjacent-transposition alphabet, and the completed UT3
+central-commutator results in PR #1443 and its later third-role follow-up,
+PR #1478 (head `b30fdba48f3db70e3589ba740b0782b56ec0ba2e`). The present
+endpoint changes the target cycle type to `(2,2)`, where transposition length
+four exceeds natural displacement rank two; the question is whether scalar
+mixing bridges that specific gap. PR #1333's exact binary-affine register
+formula and PR #1573's UT3 all-register rank result also use displacement-rank
+arguments, but their address groups, paid alphabets and targets differ. This
+package does not claim a new general rank method and imports no predecessor
+code. PR #1705's GL2 coordinate-SWAP targets and PR #1711's AGL2 affine targets
+are also distinct.
+
+The pre-submission PR scan used REST at 2026-10-14 08:12 UTC and covered 415 open PRs;
+the only S4 adjacent-transposition match was PR #1720's 4-cycle endpoint, and
+no double-transposition claim appeared. The overlap helper could not refresh
+its own PR cache because the installed `gh api` rejects `--slurp`, so the REST
+census was run directly. A fresh complete Discussion fetch at 08:12 UTC covered
+366 records and showed no S4 `(2,2)` target claim. The completed finding was
+posted to [coordination Discussion #1163](https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18919260).
+The full local claim is in [CLAIM.md](CLAIM.md), including the exact seed,
+catalogue revision, base, selected-record hash, scope, competitors and expiry.
+The focused result is submitted as [PR #1734](https://github.com/CrocSwap/integer-mult-bounds/pull/1734).
+
+This local model is not physically mapped to the selected bit supplier. The
+selected baseline remains complex-primitive-bound; physical address
+realization, hosting, precision, restoration cost in a native circuit and
+recursive-moment impact remain unestablished. No selected source, certificate
+or frontier value is changed.
+
+## Open next questions
+
+The exact local endpoint is closed, so no adjacent target tuple is claimed.
+The remaining question is whether any selected bit supplier exposes these
+adjacent transpositions at a fully charged unit cost while retaining the dirty
+role contract. The first step would be an explicit supplier-interface map and
+invoice; the current complex-primitive binding and absence of an identified
+supplier occurrence block a selected-bound conclusion.
+
+## Research record and credit
+
+This is a fixed nonabelian register-model negative result, not a new supplier,
+conditional bound or multiplication theorem. Sources are pinned in
+[SOURCES.json](SOURCES.json); the complete state and controls are in
+[CERTIFICATE.json](CERTIFICATE.json), and the written argument is
+[PROOF.md](PROOF.md). Prepared by Cinna Davis with substantial OpenAI Codex
+assistance in scoping, algebraic proof, exact implementation, verification and
+writing. No subagents or independent human review are claimed. Apache-2.0.