From bf73c0845196229b8050364ea7e26edd81f381ab Mon Sep 17 00:00:00 2001
From: Aaron Wang <warhawk947@gmail.com>
Date: Wed, 14 Oct 2026 04:45:31 -0400
Subject: [PATCH 1/2] Add balanced ten-call four-SWAP J3-layer obstruction and
 scoped search

Package research/four-swap-balanced-j3-layer: for T = diag([S],[S],[S],[S])
at r = 4 in the formal F2[GL_2(F2)] rank-one-idempotent register model, the
handoff-proposed J^2-coefficient-layer bound in F2[G]/J^3 is shown vacuous:
augmentation dims (5,4,4) give J^2 = J^3, so R/J^3 is the sign quotient and
the layer equation is machine-checked equivalent to sum N_i = I_r (200/200).
A bounded exact full-formal search of the balanced (5a,5b) profile checks
5,771,556 labelings from 6,000,000 conditioned samples with zero witnesses
(scoped search failure, not an impossibility theorem). No new kappa.

Task card bit-new-register-model refined to the balanced ten-call residual of
https://github.com/CrocSwap/integer-mult-bounds/pull/1705, the case
https://github.com/CrocSwap/integer-mult-bounds/discussions/1715 explicitly
leaves open, and the next task named in
https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18918391

Prepared by Aaron Wang, with help from opencode. Apache-2.0.
---
 .../four-swap-balanced-j3-layer/EXPECTED.json |  34 ++
 .../four-swap-balanced-j3-layer/README.md     | 175 ++++++
 .../four-swap-balanced-j3-layer/SOURCES.json  |  47 ++
 .../four-swap-balanced-j3-layer/TASK-CARD.md  |  80 +++
 .../four-swap-balanced-j3-layer/TASK.json     |  65 +++
 .../four-swap-balanced-j3-layer/VERIFY.json   |  30 ++
 .../test_verify.py                            | 108 ++++
 .../four-swap-balanced-j3-layer/verify.py     | 496 ++++++++++++++++++
 8 files changed, 1035 insertions(+)
 create mode 100644 research/four-swap-balanced-j3-layer/EXPECTED.json
 create mode 100644 research/four-swap-balanced-j3-layer/README.md
 create mode 100644 research/four-swap-balanced-j3-layer/SOURCES.json
 create mode 100644 research/four-swap-balanced-j3-layer/TASK-CARD.md
 create mode 100644 research/four-swap-balanced-j3-layer/TASK.json
 create mode 100644 research/four-swap-balanced-j3-layer/VERIFY.json
 create mode 100644 research/four-swap-balanced-j3-layer/test_verify.py
 create mode 100644 research/four-swap-balanced-j3-layer/verify.py

diff --git a/research/four-swap-balanced-j3-layer/EXPECTED.json b/research/four-swap-balanced-j3-layer/EXPECTED.json
new file mode 100644
index 0000000000..e15d8e08f4
--- /dev/null
+++ b/research/four-swap-balanced-j3-layer/EXPECTED.json
@@ -0,0 +1,34 @@
+{
+ "default": {
+  "dims_J1_J2_J3": [
+   5,
+   4,
+   4
+  ],
+  "full_hits": 0,
+  "labelings": 1956528,
+  "layer_hits": 1956528,
+  "mode": "default",
+  "r1_control_full_hits": 4000,
+  "r2_control_full_hits": 3254,
+  "r2_control_layer_hits": 601940,
+  "samples": 2000000,
+  "valid": 7764
+ },
+ "full": {
+  "dims_J1_J2_J3": [
+   5,
+   4,
+   4
+  ],
+  "full_hits": 0,
+  "labelings": 5771556,
+  "layer_hits": 5771556,
+  "mode": "full",
+  "r1_control_full_hits": 4000,
+  "r2_control_full_hits": 3254,
+  "r2_control_layer_hits": 601940,
+  "samples": 6000000,
+  "valid": 22903
+ }
+}
\ No newline at end of file
diff --git a/research/four-swap-balanced-j3-layer/README.md b/research/four-swap-balanced-j3-layer/README.md
new file mode 100644
index 0000000000..2dddd1922a
--- /dev/null
+++ b/research/four-swap-balanced-j3-layer/README.md
@@ -0,0 +1,175 @@
+# The balanced ten-call four-SWAP residual: the J^2 layer cannot decide it
+
+**Scoped obstruction plus scoped search failure; no new kappa.** The selected
+result, the selected bit supplier and `upstream/` are unchanged.
+
+Four coordinate-SWAP targets `T = diag([S],[S],[S],[S])`, `S = aba = bab`, at
+exactly `r = 4` registers in the formal `F2[GL_2(F2)]` rank-one-idempotent
+register model: can a **ten-call word with exactly five `a`-labels and five
+`b`-labels** realize `T`? This is the balanced residual of the four-SWAP line
+after [PR1705](https://github.com/CrocSwap/integer-mult-bounds/pull/1705)
+narrowed the minimum to `q in {8,10,12}` and the concurrent label-saturation
+claim
+[discussion 1715](https://github.com/CrocSwap/integer-mult-bounds/discussions/1715)
+put "the ten-call balanced case" outside its session. The handoff
+[comment 18918391](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18918391)
+proposed deriving the `J^2`-coefficient-layer bound in `F_2[G]/J^3`
+(`sum E_i + sum_{i<j} E_i E_j = T - I`) to exclude `q = 10` in writing.
+
+This package does that derivation and records the exact obstruction: **the
+route is empty in this algebra.** The balanced question itself remains open.
+
+## Model and reduction
+
+`R = F2[GL_2(F2)]`, `a = [[1,1],[0,1]]`, `b = [[1,0],[1,1]]`,
+`S = aba = bab = [[0,1],[1,0]]`. Paid calls are `I + ([g]+1) N` with
+`g in {a,b}` and `N = u v^T` a binary rank-one idempotent (`v^T u = 1`);
+free scalar `GL_r(F2)` mixing is granted between calls; every call is charged
+and all four registers carry arbitrary dirty inputs restored exactly.
+
+Free mixing normalizes away: absorbing the scalar factors conjugates the `N`
+(which stay rank-one idempotent), and the augmentation of the boundary
+`[s] I_r` forces the accumulated scalar to the identity. So a word is a pure
+product `prod (1 + eps_i)`, `eps_i = ([g_i]+1) N_i`, and any word realizing
+`T` satisfies `sum_i N_i = I_r` by the sign quotient (every label is odd).
+
+## Result 1: `J^2 = J^3`, so the proposed layer bound is vacuous
+
+Exact linear algebra on `R` (bit vectors, `verify.py`):
+
+| subspace | `J^1` | `J^2` | `J^3` |
+|---|---|---|---|
+| dimension | 5 | 4 | 4 |
+
+The augmentation powers stabilize at the second step: `J^3 = J^2`, so
+`R/J^3 = R/J^2` is just the sign quotient `F2[z]/(z^2)`, in which
+`red([a]+1) = red([b]+1) = red([s]+1) = z` and both pair terms
+`P = ([a]+1)([b]+1)` and `Q = ([b]+1)([a]+1)` vanish. The word expansion
+lemma
+
+```
+prod (1 + eps_i) = 1 + sum eps_i + sum_{i<j} eps_i eps_j    (mod J^3 M_r)
+```
+
+is exact and is checked on seeded random words (same-label pairs already
+vanish identically because `([a]+1)^2 = ([b]+1)^2 = 0`). But after reduction
+the whole layer equation collapses entrywise to `sum_i N_i = I_r`, nothing
+more. The verifier machine-checks the equivalence
+(`layer check holds  <=>  sum N_i = I_r`) on 200/200 random instances, and
+the search below confirms it exhaustively on its own domain: every one of the
+5,771,556 balanced labelings passed the layer check, because the sampler
+conditions on `sum N_i = I_r` — a condition the sign quotient already forces
+on any candidate word.
+
+So the handoff's proposed `J^2`-coefficient-layer bound cannot exclude
+`q = 10`, `q = 8`, or anything else above the two-call case: in `F2[G]` there
+is no second augmentation layer to read a coefficient bound off. Any written
+exclusion of the balanced profile must use word order or a different quotient
+of `F2[G]` (for example the natural two-dimensional image `M_2(F2)`, as in
+PR1705's census, or the commutator `[([a]+1),([b]+1)] = [ab]+[ba]`, which
+survives in `J^2` but is invisible in `R/J^3`).
+
+## Result 2: bounded exact search of the balanced profile
+
+With `sum N_i = I_r` justified as a lossless reduction, the sampler draws
+ordered ten-tuples of the 120 binary rank-one idempotents conditioned on
+`sum N_i = I_4` (each valid ordered tuple uniform), and checks all 252 ways
+to place the five `a`-labels, first at the `J^3` layer and then, for every
+layer-feasible labeling, at **full formal level** in `M_4(F2[G])` (96-bit
+states, exact bit arithmetic).
+
+Recorded run (`--full`, seed 20261014): 6,000,000 samples, 22,903 valid
+tuples, 5,771,556 labelings, **0 full-formal hits**. This is a scoped search
+failure over that sampled domain, not an impossibility theorem: it does not
+cover the unsampled valid tuples, `q = 8` profiles, `r = 5`, or any word with
+a different label profile.
+
+Controls: the four direct words (`aba` at `r = 1`; `aba|bab` at `r = 2`;
+`aba` on three registers at `r = 3`; four disjoint `aba`/`bab` words at
+`r = 4`, 6a6b balanced) hit their targets exactly in `M_r(F2[G])`; four
+mutation controls (dropped call, flipped label, dropped target, perturbed
+`N`) fail; the search finds known-solvable instances at `r = 1` (`q = 3`)
+and `r = 2` (`q = 6` balanced, 3,254 witnesses); a strict-relaxation honesty
+control exhibits a layer-feasible word that fails full equality; conjugation
+of `N` by `GL_r(F2)` preserves the idempotent family; and two hand-derived
+pins (`([a]+1)^2 = 0`; `([a]+1)([b]+1)([a]+1) = [aba]+[ab]+[ba]+[b]`) bind
+the group algebra implementation.
+
+## Reproduce
+
+Python 3.12 and the standard library suffice. From the repository root:
+
+```sh
+python3 -I -B research/four-swap-balanced-j3-layer/verify.py --full
+python3 -I -B research/four-swap-balanced-j3-layer/test_verify.py
+python3 scripts/research_package.py --package research/four-swap-balanced-j3-layer --check-only
+```
+
+Expected direct-replay line (`--full`, about 6 minutes):
+
+```text
+PASS_FOUR_SWAP_BALANCED_J3_LAYER balanced_5a5b_unrealized_in_search layer_hits=5771556 no_new_kappa
+```
+
+`EXPECTED.json` pins the deterministic counts for both the default and the
+full budget; the verifier fails on any mismatch. `--emit` prints a receipt
+without comparing.
+
+## Task and overlap
+
+Base `0b1cccf86e2f5132ed286a26ef0a681a495740ea`; card `bit-new-register-model`,
+scope key `7084092dd726e7ba1f2f`, priority revision 3, chooser nonce
+`cd67986ec4d736b6ed683332001aecde`, track `bit-mechanisms`. Claim:
+[discussion 1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18919080).
+[TASK-CARD.md](TASK-CARD.md) records the pre-computation card; [TASK.json](TASK.json)
+the refined scope; [SOURCES.json](SOURCES.json) the exact pins.
+
+Refined-object overlap searches (`find_overlap.py` with 'balanced ten-call',
+'five of each label', 'ten-call balanced', 'augmentation layer', 'F2[G]/J3'
+at 07:53–07:54 UTC over 410 open PRs and 358 discussions, complete
+pagination) matched only
+[discussion 1715](https://github.com/CrocSwap/integer-mult-bounds/discussions/1715),
+which explicitly excludes this case. Coverage excludes arbitrary diffs and
+nested files; no match is not a novelty certificate.
+
+## Limitations and remaining obligations
+
+Not checked: Lean or independent human proof review; a selected-supplier cold
+replay; physical, compiler, hosting, precision or tape admission; the `q = 8`
+profiles; `r = 5` with a restored dirty extra; label profiles other than
+(5,5); unsampled valid tuples of the balanced domain. No claim is made that a
+balanced ten-call word does or does not exist; no new supplier, recursive
+profile or kappa follows; the selected frontier is unchanged.
+
+## Open next questions
+
+1. **Order-sensitive exclusion (or construction) for the balanced (5,5)
+   profile.** It decides whether the four-SWAP minimum is 10 or 12 once
+   saturation lands. First step: evaluate every balanced candidate at the
+   natural image `M_2(F2)` (PR1705's homomorphic image) with a 5+5 meet, or
+   derive a commutator-layer bound using `[ab]+[ba] in J^2`, which `R/J^3`
+   cannot see. Blocked by: the `J^2 = J^3` collapse recorded here rules out
+   any purely augmentation-layer argument.
+2. **The same balanced question at `r = 5` with one restored dirty extra.**
+   Smallest falsifying instance of "workspace cheapens the tariff". First
+   step: rerun the conditioned sampler at `r = 5`, target
+   `diag([S],[S],[S],[S],1)`, `sum N_i = I_5` (the sign-quotient lemma is
+   register-count independent). Blocked by: nothing; it is open compute.
+
+## Credit and license
+
+Prepared by Aaron Wang, with help from opencode. Predecessor credit:
+commdata2338 ([PR1414](https://github.com/CrocSwap/integer-mult-bounds/pull/1414),
+[PR1491](https://github.com/CrocSwap/integer-mult-bounds/pull/1491) — model,
+sign parity, three-SWAP finite result), Gareth Davidson
+([PR1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333) —
+free-scalar normalization), Cinna Davis
+([PR1541](https://github.com/CrocSwap/integer-mult-bounds/pull/1541) —
+arbitrary-workspace three-SWAP theorem), Aaron Wang
+([PR1705](https://github.com/CrocSwap/integer-mult-bounds/pull/1705) —
+four-SWAP `r = 4` bounds and the 4+4 obstruction measurement), Ross
+Richardson
+([discussion 1715](https://github.com/CrocSwap/integer-mult-bounds/discussions/1715) —
+concurrent saturation claim, complementary). New work is Apache-2.0;
+predecessor sources and notices remain unchanged. No general rank principle
+or literature-priority claim is made.
diff --git a/research/four-swap-balanced-j3-layer/SOURCES.json b/research/four-swap-balanced-j3-layer/SOURCES.json
new file mode 100644
index 0000000000..66f7d1281d
--- /dev/null
+++ b/research/four-swap-balanced-j3-layer/SOURCES.json
@@ -0,0 +1,47 @@
+{
+ "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": "research/coordinate-cnot-register-bound/README.md",
+   "usage": "provenance",
+   "git_blob": "cdcc5a9e7f11ab3dbf7745a175ddcca208c68211",
+   "sha256": "e1666512fb71cf34c427c69ffb61a18b61e897a7f8f91f87820edf744e85a9fe"
+  }
+ ],
+ "research_context": [
+  {
+   "repository": "https://github.com/CrocSwap/integer-mult-bounds",
+   "head": "ad6b7d641b3e8576a95add7981fa75b6a8278fbc",
+   "path": "research/four-swap-r4-cnot/",
+   "author": "Aaron Wang (with help from opencode)",
+   "usage": "Concurrent predecessor (open PR 1705); model and q in {8,10,12} narrowing reused as context only; no files imported."
+  },
+  {
+   "repository": "https://github.com/CrocSwap/integer-mult-bounds",
+   "head": "9e1640094f649ba6db9742796825a8d6c238989b",
+   "path": "(PR 1414 / PR 1491 packages)",
+   "author": "commdata2338",
+   "usage": "Research context only; coordinate-CNOT model conventions and sign-quotient parity; not a runtime dependency."
+  },
+  {
+   "repository": "https://github.com/CrocSwap/integer-mult-bounds",
+   "head": "194724d87505ec2517fdca1c1884da12398f4c33",
+   "path": "(PR 1541 package)",
+   "author": "Cinna Davis (1337isnot1337)",
+   "usage": "Research context only; arbitrary-workspace three-SWAP theorem; not a runtime dependency."
+  }
+ ]
+}
\ No newline at end of file
diff --git a/research/four-swap-balanced-j3-layer/TASK-CARD.md b/research/four-swap-balanced-j3-layer/TASK-CARD.md
new file mode 100644
index 0000000000..3ff0a6b44a
--- /dev/null
+++ b/research/four-swap-balanced-j3-layer/TASK-CARD.md
@@ -0,0 +1,80 @@
+# Task card — agent-24 (local, pre-computation)
+
+Task ID / proposed scope key: `bit-new-register-model` / `7084092dd726e7ba1f2f`,
+refined to `coordinate-CNOT/GL2(F2)/four-SWAP/r=4/balanced-5a5b-at-q=10/J3-augmentation-layer`.
+
+Base commit: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`
+(selected-record SHA-256 `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`,
+priority revision 3). Branch `research/agent-24-four-swap-balanced-cd67986e`.
+Chooser nonce `cd67986ec4d736b6ed683332001aecde`, track `bit-mechanisms`.
+
+Exact predecessor and dependency heads (read-only, no files imported):
+- https://github.com/CrocSwap/integer-mult-bounds/pull/1705 head `ad6b7d641b3e8576a95add7981fa75b6a8278fbc`
+  (four-SWAP r=4: q in {8,10,12}), package `research/four-swap-r4-cnot/` on its branch;
+- commdata2338 https://github.com/CrocSwap/integer-mult-bounds/pull/1414 and
+  https://github.com/CrocSwap/integer-mult-bounds/pull/1491 (model, sign-quotient parity, three-SWAP finite result);
+- Gareth Davidson https://github.com/CrocSwap/integer-mult-bounds/pull/1333 (free-scalar normalization);
+- Cinna Davis https://github.com/CrocSwap/integer-mult-bounds/pull/1541 (arbitrary-workspace three-SWAP theorem);
+- local `research/coordinate-cnot-register-bound/` (two-SWAP all-register theorem, PROOF.md) — model reference.
+
+Concrete object and question:
+In the formal group-algebra register model `R = F2[GL_2(F2)]` on exactly `r = 4` registers,
+paid calls `I + ([g]+1) u v^T` with `g in {a,b}` the two coordinate CNOTs of `GL_2(F2)`
+(`a = [[1,1],[0,1]]`, `b = [[1,0],[1,1]]`, `S = aba = bab = [[0,1],[1,0]]`), `v^T u = 1`
+binary rank-one idempotents, free scalar `GL_4(F2)` mixing between calls, all four registers
+arbitrary dirty inputs restored exactly: can the complete formal boundary
+`T = diag([S],[S],[S],[S])` be realized by a **10-call word with exactly 5 a-labels and
+5 b-labels** (the balanced profile)?
+
+Scope status: refined (card `bit-new-register-model`, allowed variation "fixed larger register
+count"; the concrete residual of the four-SWAP r=4 line).
+
+Existing restriction being changed / exact claim being audited:
+PR1705 narrows the four-SWAP r=4 minimum to `q in {8,10,12}` and leaves `q = 10` open. The live
+label-saturation claim (discussions/1715, Ross Richardson, expires 2026-10-14 09:35 UTC) would
+leave exactly the balanced (5 a, 5 b) ten-call profile as the only sub-12 candidate, and states
+"The ten-call balanced case is explicitly outside this session." The handoff
+(discussions/1166#discussioncomment-18918391) names "derive the `J^2`-coefficient-layer bound in
+`F_2[G]/J^3` (`sum E_i + sum_{i<j} E_i E_j = T - I`) to exclude `q = 10` in writing" as a
+smallest useful next task.
+
+Method; explicit parameter ranges/candidate alphabet:
+1. Exact `F2[S3]` algebra with bit-linear algebra (stdlib only): augmentation ideal `J`, `J^2`,
+   `J^3`, quotient `R/J^3`; verify `([a]+1)^2 = ([b]+1)^2 = 0` (a, b involutions).
+2. Derive the word expansion `prod(1+eps_i) = 1 + sum eps_i + sum_{i<j} eps_i eps_j` exactly in
+   `(R/J^3) M_r` and record it as L1/L2 necessary equations (label-order aware; same-label pairs
+   vanish by involution).
+3. Positive controls: the exact 3-call word at r=1, 6-call word at r=2, 9-call word at r=3 and the
+   four-disjoint-`aba` 12-call word at r=4 must satisfy the layer equations and the full formal
+   equation. Negative controls: mutated words/targets must fail.
+4. Main bounded search: decide feasibility of the balanced (5,5) layer system at r=4 over the
+   120 binary rank-one idempotents `u v^T` (`v^T u = 1`), all 252 interleavings, seeded and
+   time-capped. Any hit is replayed at full formal level (`M_4(F2[G])`, 96-bit states) as a
+   candidate; if no hit, report the exact searched domain as a scoped search failure.
+
+Nearest overlapping PRs and why this adds something:
+PR1705 (same model/target) excludes q in {2,4,6} by a natural-image census and leaves q = 10
+open; this work isolates the balanced (5,5) residual at the augmentation layer, which PR1705 does
+not decide and discussion 1715 explicitly excludes from its session. It is not a re-run of any
+census: the layer equations are a written algebraic reduction, and the search domain is the
+balanced profile only.
+
+Optimistic full cost budget; required observable improvement:
+The priced budget is the paid-call bill: a balanced 10-call word would beat the 12-call direct
+bill (`q = 10 < 12`); required observable improvement is either an exact certificate that the
+balanced (5,5) layer system is infeasible (then, with PR1705 and any saturation result, the
+four-SWAP minimum is narrowed further) or an explicit layer-satisfying balanced assignment with
+its exact word-level status, i.e. a precise obstruction for this route.
+
+Success evidence; falsification test; time/compute cap:
+Success = exact-arithmetic certificate (`verify.py` PASS with counts) plus written lemmas.
+Falsification of the layer route = a balanced (5,5) assignment satisfying L1/L2 found.
+Controls above falsify the machinery if they fail. Search cap: one bounded seeded pass
+(~10-20 min wall), one bounded pivot maximum.
+
+Predecessor authors; intended artifact and reproduction command:
+Credit Aaron Wang, with help from opencode; predecessors as listed above (commdata2338, Gareth
+Davidson, Cinna Davis, Aaron Wang PR1705, Ross Richardson discussion 1715 as concurrent).
+Artifact: `research/four-swap-balanced-j3-layer/` (README, TASK.json, verify.py, exact certificate).
+Reproduce: `python3 -B research/four-swap-balanced-j3-layer/verify.py` (expected PASS in seconds
+to a few minutes; exact stdlib arithmetic, no network).
diff --git a/research/four-swap-balanced-j3-layer/TASK.json b/research/four-swap-balanced-j3-layer/TASK.json
new file mode 100644
index 0000000000..6901b71fc4
--- /dev/null
+++ b/research/four-swap-balanced-j3-layer/TASK.json
@@ -0,0 +1,65 @@
+{
+ "schema_version": 1,
+ "task_id": "bit-new-register-model",
+ "priority_revision": 3,
+ "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+ "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",
+ "actual_scope": "Balanced (5 a-labels, 5 b-labels) ten-call words for T = diag([S],[S],[S],[S]) at exactly r = 4 in the formal F2[GL_2(F2)] rank-one-idempotent register model, via the proposed J^2-coefficient-layer expansion in F2[G]/J^3 plus a bounded exact full-formal search over the balanced profile.",
+ "scope_change_reason": "The card permits a fixed larger register count. This is the named residual of the four-SWAP r=4 line: https://github.com/CrocSwap/integer-mult-bounds/pull/1705 narrows the minimum to q in {8,10,12}; the concurrent saturation claim https://github.com/CrocSwap/integer-mult-bounds/discussions/1715 explicitly leaves 'the ten-call balanced case' outside its session; and the handoff https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18918391 names the J^2-layer bound in F2[G]/J^3 as a smallest useful next task.",
+ "bottleneck_link": "A balanced ten-call word would price four coordinate-SWAP targets below the 12-call direct bill inside the bit register model; scalar or partial words alone change nothing, and no kappa or selected-supplier change follows either way.",
+ "stop_rule": "One bounded seeded search pass at the stated budget (6,000,000 conditioned samples), one route decision: if the J^3 layer cannot separate the balanced profile, record the exact obstruction and stop the layer route rather than raising the budget.",
+ "evidence": "research/four-swap-balanced-j3-layer/verify.py exact bit arithmetic: augmentation dims (5,4,4) with J^2 = J^3 so R/J^3 is the sign quotient F2[z]/(z^2); the layer equation is machine-checked equivalent to sum N_i = I_r (200/200 random instances); expansion identity prod(1+eps) = 1 + sum eps + sum_{i<j} eps_i eps_j mod J^3 checked on seeded random words; four direct control words (3/6/9/12 calls) hit their targets; four mutation controls fail; r=1 and r=2 balanced search controls find known witnesses; 6,000,000 conditioned samples (22,903 valid tuples x 252 labelings = 5,771,556 exact M_4(F2[G]) checks) find no balanced ten-call word realizing the target.",
+ "outcome": "partial",
+ "author": "Aaron Wang",
+ "ai_assistance": "with help from opencode",
+ "open_questions": [
+  {
+   "question": "Can the balanced (5,5) ten-call profile realize T = diag([S],[S],[S],[S]) at r = 4 at all, now that the J^3 layer is known to be vacuous for it?",
+   "why_it_matters": "It is the only sub-12 four-SWAP candidate left once label saturation is proved, so it decides whether the four-SWAP minimum is 10 or 12.",
+   "first_step": "Use the surviving full-word structure instead of the augmentation layer: the natural 2-dimensional image in M_8(F2), or an order-sensitive invariant from the commutator [([a]+1),([b]+1)] = [ab]+[ba] in J^2, on the same balanced domain.",
+   "blocked_by": "J^2 = J^3 in F2[G], so no second augmentation layer exists; any further exclusion must use word order or a different quotient of F2[G]."
+  },
+  {
+   "question": "Does the balanced-profile obstruction at r = 4 persist at r = 5 with one restored dirty extra register?",
+   "why_it_matters": "It is the smallest falsifying instance of 'workspace cheapens the tariff' for four SWAP targets and tests whether register growth changes the picture.",
+   "first_step": "Rerun the same conditioned search at r = 5 with target diag([S] x 4, 1) and the identical sum N_i = I_5 reduction, which the sign-quotient lemma still justifies.",
+   "blocked_by": "The r = 5 balanced question itself is open; only the r = 4 balanced domain was searched here."
+  }
+ ]
+}
\ No newline at end of file
diff --git a/research/four-swap-balanced-j3-layer/VERIFY.json b/research/four-swap-balanced-j3-layer/VERIFY.json
new file mode 100644
index 0000000000..55f8490772
--- /dev/null
+++ b/research/four-swap-balanced-j3-layer/VERIFY.json
@@ -0,0 +1,30 @@
+{
+ "schema_version": 1,
+ "status": "ready",
+ "python": "3.12",
+ "requirements": [],
+ "inputs": [],
+ "commands": [
+  {
+   "argv": [
+    "{python}",
+    "-I",
+    "-B",
+    "{package}/verify.py",
+    "--full"
+   ],
+   "timeout_seconds": 600,
+   "checks": "Hand algebra pins ([a]+1)^2 = 0 and the ([a]+1)([b]+1)([a]+1) coefficient pin; J^2 = J^3 obstruction; layer-check equivalence with sum N_i = I_r (200/200); J^3 expansion identity on seeded random words; four direct control words and four mutation controls; r=1/r=2 balanced search finders; the recorded 6,000,000 sample balanced (5a,5b) search with exact M_4(F2[G]) equality."
+  },
+  {
+   "argv": [
+    "{python}",
+    "-I",
+    "-B",
+    "{package}/test_verify.py"
+   ],
+   "timeout_seconds": 120,
+   "checks": "Independent hand-derived algebra pins, layer expansion identity, direct-word and mutation controls, conjugation closure of rank-one idempotents, known-solvable search instances, and the strict-relaxation honesty control."
+  }
+ ]
+}
\ No newline at end of file
diff --git a/research/four-swap-balanced-j3-layer/test_verify.py b/research/four-swap-balanced-j3-layer/test_verify.py
new file mode 100644
index 0000000000..85c701020d
--- /dev/null
+++ b/research/four-swap-balanced-j3-layer/test_verify.py
@@ -0,0 +1,108 @@
+#!/usr/bin/env python3
+"""Independent pins for verify.py of research/four-swap-balanced-j3-layer.
+
+The algebraic expectations here were derived by hand (2x2 matrix products over
+F2 and the expansion of ([a]+1)([b]+1)([a]+1)) before verify.py existed, so a
+failure indicates a bug in the checker, not in the expectation. Stdlib only.
+"""
+import importlib.util
+import itertools
+import pathlib
+import random
+import unittest
+
+HERE = pathlib.Path(__file__).resolve().parent
+spec = importlib.util.spec_from_file_location("j3verify", HERE / "verify.py")
+V = importlib.util.module_from_spec(spec)
+spec.loader.exec_module(V)
+
+
+class AlgebraPins(unittest.TestCase):
+    def setUp(self):
+        V.build()
+
+    def test_involution_squares_vanish(self):
+        for g in (V.A, V.B, V.S):
+            x = V.gplus(g)
+            self.assertEqual(V.rmul(x, x), 0)
+
+    def test_one_swap_word_at_r1(self):
+        # The three-call word aba at r=1 (N = [1]) equals [s] exactly:
+        # each factor I + ([g]+1) collapses to [g] in dimension one.
+        labels = (V.A, V.B, V.A)
+        word = V.word_value(1, labels, (V.idem(1, 1, 1),) * 3)
+        self.assertEqual(word, (1 << V.idx(V.S),))
+
+    def test_xyx_pin(self):
+        # Hand expansion: ([a]+1)([b]+1)([a]+1) = [aba] + [ab] + [ba] + [b]
+        # with NO identity term (the two [1] summands cancel over F2).
+        x, y = V.gplus(V.A), V.gplus(V.B)
+        got = V.rmul(V.rmul(x, y), x)
+        ab = V.idx(V.mm2(V.A, V.B))
+        ba = V.idx(V.mm2(V.B, V.A))
+        want = (1 << V.idx(V.S)) ^ (1 << ab) ^ (1 << ba) ^ (1 << V.idx(V.B))
+        self.assertEqual(got, want)
+
+    def test_layer_expansion_identity(self):
+        # prod(1+eps_i) == 1 + sum eps_i + sum_{i<j} eps_i eps_j  (mod J^3),
+        # in the exact quotient for seeded random words.
+        rng = random.Random(20261014)
+        idems = V.rank_one_idempotents(4)
+        lab = (V.A, V.B)
+        for _ in range(50):
+            q = rng.randrange(1, 8)
+            labels = tuple(lab[rng.randrange(2)] for _ in range(q))
+            mats = tuple(rng.choice(idems) for _ in range(q))
+            self.assertTrue(V.layer_expansion_holds(4, labels, mats))
+
+
+class WordControls(unittest.TestCase):
+    def setUp(self):
+        V.build()
+
+    def test_direct_words_hit_targets(self):
+        for r, labels, mats, k in V.direct_control_words():
+            self.assertEqual(V.word_value(r, labels, mats), V.target(r, k),
+                             "direct word must realize the target")
+
+    def test_mutated_words_fail(self):
+        for r, labels, mats, k, mut in V.mutation_controls():
+            self.assertNotEqual(V.word_value(r, labels, mats), V.target(r, k),
+                                "mutation control must fail: " + mut)
+
+    def test_conjugation_closure(self):
+        rng = random.Random(7)
+        idems = V.rank_one_idempotents(4)
+        gl = V.gl_elements(4)
+        for _ in range(50):
+            n = rng.choice(idems)
+            u = rng.choice(gl)
+            c = V.conjugate(4, u, n)
+            self.assertIn(c, idems)
+
+
+class SearchControls(unittest.TestCase):
+    def setUp(self):
+        V.build()
+
+    def test_search_finds_known_small_instances(self):
+        # Smallest falsifying instances first: where a balanced word is known
+        # to exist, the search must actually find one.
+        r1 = V.search(1, 3, 1, 1, samples=2000, seed=11)
+        self.assertIsNotNone(r1["full_witness"], "r=1, q=3, 1a2b must find bab")
+        r2 = V.search(2, 6, 3, 2, samples=20000, seed=12)
+        self.assertIsNotNone(r2["full_witness"], "r=2, q=6, 3a3b must find aba|bab")
+
+    def test_layer_is_a_strict_relaxation(self):
+        # Honesty control: a word that passes the J^3 layer check but fails
+        # full formal equality must exist at a known-solvable instance.
+        r2 = V.search(2, 6, 3, 2, samples=20000, seed=12)
+        self.assertGreater(r2["layer_hits"], 0)
+        self.assertIsNotNone(r2["layer_only_witness"])
+        labels, mats = r2["layer_only_witness"]
+        self.assertTrue(V.layer_value_ok(2, labels, mats, 2))
+        self.assertNotEqual(V.word_value(2, labels, mats), V.target(2, 2))
+
+
+if __name__ == "__main__":
+    unittest.main(verbosity=2)
diff --git a/research/four-swap-balanced-j3-layer/verify.py b/research/four-swap-balanced-j3-layer/verify.py
new file mode 100644
index 0000000000..a497771895
--- /dev/null
+++ b/research/four-swap-balanced-j3-layer/verify.py
@@ -0,0 +1,496 @@
+#!/usr/bin/env python3
+"""Exact checker for the balanced (5a,5b) ten-call four-SWAP residual.
+
+Model (see research/coordinate-cnot-register-bound/README.md and the pinned
+predecessors): R = F2[GL_2(F2)], paid calls I + ([g]+1) N with g in {a,b} the
+two coordinate CNOTs, N = u v^T a binary rank-one idempotent (v^T u = 1),
+free scalar GL_r(F2) mixing normalizable to identity by augmentation, complete
+formal boundary T = diag([S],...,[S]) on r target registers.
+
+This program derives the exact J^3 augmentation-layer equations
+
+    prod_i (1 + eps_i) = 1 + sum eps_i + sum_{i<j} eps_i eps_j   (mod J^3 M_r)
+
+(same-label pairs vanish since ([a]+1)^2 = ([b]+1)^2 = 0), checks them and the
+full formal equality against control words, and runs a bounded seeded search
+for a balanced (5 a-labels, 5 b-labels) ten-call word at r = 4 realizing
+T = diag([S],[S],[S],[S]).  Exact bit arithmetic throughout; stdlib only.
+No new kappa; the selected frontier is unchanged.
+"""
+import argparse
+import itertools
+import json
+import pathlib
+import random
+import sys
+import time
+
+HERE = pathlib.Path(__file__).resolve().parent
+
+# ---------------------------------------------------------------- group GL2(F2)
+def m2(row0, row1):
+    """2x2 binary matrix as int: row p in bits 2p, 2p+1 (c0 low bit)."""
+    return row0 | (row1 << 2)
+
+
+def mm2(x, y):
+    """Product of two encoded 2x2 binary matrices over F2."""
+    return m2(_row_mult(x & 3, y), _row_mult((x >> 2) & 3, y))
+
+
+def _row_mult(row, mat):
+    out = 0
+    for c in (0, 1):
+        if (row >> c) & 1:
+            out ^= (mat >> (2 * c)) & 3
+    return out
+
+
+def det2(x):
+    a = x & 1
+    b = (x >> 1) & 1
+    c = (x >> 2) & 1
+    d = (x >> 3) & 1
+    return (a & d) ^ (b & c)
+
+
+def build():
+    global ELEMS, IDX, GPROD, RMUL, A, B, S, IDE, GP1, BP1, SP1, PAB, QBA
+    global J1, J2, J3, ECHELON, RED, DIMS
+    ELEMS = [x for x in range(16) if det2(x)]
+    assert len(ELEMS) == 6
+    IDX = {g: i for i, g in enumerate(ELEMS)}
+    GPROD = [[0] * 6 for _ in range(6)]
+    for i, g in enumerate(ELEMS):
+        for j, h in enumerate(ELEMS):
+            GPROD[i][j] = 1 << IDX[mm2(g, h)]
+    RMUL = [[0] * 64 for _ in range(64)]
+    for x in range(64):
+        for y in range(64):
+            v = 0
+            for i in range(6):
+                if (x >> i) & 1:
+                    for j in range(6):
+                        if (y >> j) & 1:
+                            v ^= GPROD[i][j]
+            RMUL[x][y] = v
+    A = m2(3, 2)   # [[1,1],[0,1]]
+    B = m2(1, 3)   # [[1,0],[1,1]]
+    S = m2(2, 1)   # [[0,1],[1,0]]
+    assert mm2(mm2(A, B), A) == S and mm2(mm2(B, A), B) == S
+    IDE = m2(1, 2)
+    assert mm2(IDE, IDE) == IDE
+    GP1, BP1, SP1 = gplus(A), gplus(B), gplus(S)
+    PAB, QBA = RMUL[GP1][BP1], RMUL[BP1][GP1]
+    J1 = [gplus(g) for g in ELEMS if g != IDE]
+    J2 = _span([RMUL[x][y] for x in J1 for y in J1])
+    J3 = _span([RMUL[RMUL[x][y]][z] for x in J1 for y in J1 for z in J1])
+    ECHELON = _echelon(J3)
+    RED = [0] * 64
+    for x in range(64):
+        RED[x] = _reduce(x)
+    DIMS = (len(J1), len(J2), len(J3))
+
+
+def idx(g):
+    return IDX[g]
+
+
+def gen(i):
+    return 1 << i
+
+
+def gplus(g):
+    return (1 << IDX[g]) ^ (1 << IDX[IDE])
+
+
+def rmul(x, y):
+    return RMUL[x][y]
+
+
+def _span(vecs):
+    """Reduced row-echelon basis of the F2 span of 6-bit vectors."""
+    rows = [v for v in vecs if v]
+    r = 0
+    for col in range(5, -1, -1):
+        sel = next((i for i in range(r, len(rows)) if (rows[i] >> col) & 1), None)
+        if sel is None:
+            continue
+        rows[r], rows[sel] = rows[sel], rows[r]
+        for i in range(len(rows)):
+            if i != r and (rows[i] >> col) & 1:
+                rows[i] ^= rows[r]
+        r += 1
+    return sorted(rows[:r], reverse=True)
+
+
+def _echelon(vecs):
+    """(pivot, vector) rows in increasing pivot order; pivot = msb."""
+    rows = []
+    for v in _span(vecs):
+        rows.append((v.bit_length() - 1, v))
+    rows.sort()
+    return rows
+
+
+def _reduce(x):
+    for piv, v in ECHELON:
+        if (x >> piv) & 1:
+            x ^= v
+    return x
+
+
+# ------------------------------------------------------------- M_r(F2) / M_r(R)
+def rank_one_idempotents(r):
+    out = []
+    for u in range(1, 1 << r):
+        for v in range(1, 1 << r):
+            if bin(u & v).count("1") & 1:
+                n = 0
+                for p in range(r):
+                    if (u >> p) & 1:
+                        n |= v << (p * r)
+                out.append(n)
+    return sorted(set(out))
+
+
+def idem(r, u, v):
+    n = 0
+    for p in range(r):
+        if (u >> p) & 1:
+            n |= v << (p * r)
+    return n
+
+
+def matmul(r, x, y):
+    out = 0
+    for p in range(r):
+        xp = (x >> (p * r)) & ((1 << r) - 1)
+        row = 0
+        for k in range(r):
+            if (xp >> k) & 1:
+                row ^= (y >> (k * r)) & ((1 << r) - 1)
+        out |= row << (p * r)
+    return out
+
+
+def ident_m(r):
+    n = 0
+    for p in range(r):
+        n |= 1 << (p * r + p)
+    return n
+
+
+def gl_elements(r):
+    out = []
+    for x in range(1 << (r * r)):
+        # invertible iff some power reaches identity (r is tiny)
+        seen = {x}
+        y = x
+        for _ in range(r * r + 2):
+            y = matmul(r, y, x)
+            if y in seen:
+                break
+            seen.add(y)
+        if ident_m(r) in seen:
+            out.append(x)
+    return out
+
+
+def conjugate(r, u, n):
+    inv = None
+    for w in gl_elements_cache(r):
+        if matmul(r, u, w) == ident_m(r):
+            inv = w
+            break
+    assert inv is not None
+    return matmul(r, matmul(r, u, n), inv)
+
+
+_GL_CACHE = {}
+
+
+def gl_elements_cache(r):
+    if r not in _GL_CACHE:
+        _GL_CACHE[r] = gl_elements(r)
+    return _GL_CACHE[r]
+
+
+# ------------------------------------------------------------------ M_r(R) ops
+def mR_ident(r):
+    t = [0] * (r * r)
+    e = 1 << IDX[IDE]
+    for p in range(r):
+        t[p * r + p] = e
+    return tuple(t)
+
+
+def mR_mul(r, x, y):
+    t = [0] * (r * r)
+    for p in range(r):
+        for q in range(r):
+            v = 0
+            for k in range(r):
+                a, b = x[p * r + k], y[k * r + q]
+                if a and b:
+                    v ^= RMUL[a][b]
+            t[p * r + q] = v
+    return tuple(t)
+
+
+def factor(r, g, n):
+    t = [0] * (r * r)
+    gp = gplus(g)
+    for e in range(r * r):
+        if (n >> e) & 1:
+            t[e] = gp
+    return tuple(t)
+
+
+def mR_add(x, y):
+    return tuple(a ^ b for a, b in zip(x, y))
+
+
+def word_value(r, labels, mats):
+    acc = mR_ident(r)
+    for g, n in zip(labels, mats):
+        fac = list(mR_ident(r))
+        gp = gplus(g)
+        for e in range(r * r):
+            if (n >> e) & 1:
+                fac[e] ^= gp
+        acc = mR_mul(r, acc, tuple(fac))
+    return acc
+
+
+def target(r, k):
+    t = [0] * (r * r)
+    sp = 1 << IDX[S]
+    ip = 1 << IDX[IDE]
+    for p in range(r):
+        t[p * r + p] = sp if p < k else ip
+    return tuple(t)
+
+
+def layer_lhs(r, labels, mats):
+    """1 + sum eps_i + sum_{i<j} eps_i eps_j in M_r(R)."""
+    acc = list(mR_ident(r))
+    facs = []
+    for g, n in zip(labels, mats):
+        f = [0] * (r * r)
+        gp = gplus(g)
+        for e in range(r * r):
+            if (n >> e) & 1:
+                f[e] = gp
+        facs.append(f)
+        acc = [a ^ b for a, b in zip(acc, f)]
+    for i in range(len(facs)):
+        for j in range(i + 1, len(facs)):
+            prod = mR_mul(r, tuple(facs[i]), tuple(facs[j]))
+            acc = [a ^ b for a, b in zip(acc, prod)]
+    return tuple(acc)
+
+
+def layer_expansion_holds(r, labels, mats):
+    lhs = layer_lhs(r, labels, mats)
+    full = word_value(r, labels, mats)
+    return all(RED[a ^ b] == 0 for a, b in zip(lhs, full))
+
+
+def layer_value_ok(r, labels, mats, k):
+    lhs = layer_lhs(r, labels, mats)
+    tgt = target(r, k)
+    return all(RED[a ^ b] == 0 for a, b in zip(lhs, tgt))
+
+
+# ------------------------------------------------------------------- controls
+def direct_control_words():
+    """(r, labels, mats, k): known direct words realizing diag([S]^k, 1..)."""
+    out = []
+    one = idem(1, 1, 1)
+    out.append((1, (A, B, A), (one, one, one), 1))
+    e1, e2 = idem(2, 1, 1), idem(2, 2, 2)
+    out.append((2, (A, B, A, B, A, B), (e1, e1, e1, e2, e2, e2), 2))
+    e3 = idem(3, 4, 4)
+    out.append((3, (A, B, A) * 3, (idem(3, 1, 1),) * 3 + (idem(3, 2, 2),) * 3 + (e3,) * 3, 3))
+    f1, f2, f3, f4 = (idem(4, 1, 1), idem(4, 2, 2), idem(4, 4, 4), idem(4, 8, 8))
+    out.append((4, (A, B, A) * 2 + (B, A, B) * 2,
+                (f1,) * 3 + (f2,) * 3 + (f3,) * 3 + (f4,) * 3, 4))
+    return out
+
+
+def mutation_controls():
+    """(r, labels, mats, k, name): each must FAIL full formal equality."""
+    out = []
+    r, labels, mats, k = direct_control_words()[3]
+    out.append((r, labels[:-1], mats[:-1], k, "drop-last-call"))
+    flipped = list(labels)
+    flipped[0] = B
+    out.append((r, tuple(flipped), mats, k, "flip-first-label"))
+    out.append((r, labels, mats, k - 1, "drop-one-target"))
+    bad = list(mats)
+    bad[0] = bad[0] ^ 1
+    out.append((r, labels, tuple(bad), k, "perturb-first-N"))
+    return out
+
+
+# -------------------------------------------------------------------- search
+def search(r, q, n_a, k, samples, seed, budget_note=""):
+    idems = rank_one_idempotents(r)
+    idem_set = set(idems)
+    ident = ident_m(r)
+    rng = random.Random(seed)
+    stat = {"r": r, "q": q, "n_a": n_a, "k": k, "samples": samples, "seed": seed,
+            "valid": 0, "labelings": 0, "layer_hits": 0, "full_hits": 0,
+            "full_witness": None, "layer_only_witness": None}
+    for _ in range(samples):
+        ns = [rng.choice(idems) for _ in range(q - 1)]
+        last = ident
+        for n in ns:
+            last ^= n
+        if last not in idem_set:
+            continue
+        ns.append(last)
+        stat["valid"] += 1
+        pairs = [[matmul(r, ns[i], ns[j]) for j in range(q)] for i in range(q)]
+        total = ident
+        for apos in itertools.combinations(range(q), n_a):
+            stat["labelings"] += 1
+            labels = [B] * q
+            asum = 0
+            for i in apos:
+                labels[i] = A
+                asum ^= ns[i]
+            bsum = total ^ asum
+            xsum = 0
+            ysum = 0
+            a_set = set(apos)
+            for i in range(q):
+                for j in range(i + 1, q):
+                    if i in a_set and j not in a_set:
+                        xsum ^= pairs[i][j]
+                    elif i not in a_set and j in a_set:
+                        ysum ^= pairs[i][j]
+            # layer equation: 1 + ([a]+1)A_sum + ([b]+1)B_sum + P X + Q Y = T
+            ok = True
+            for e in range(r * r):
+                v = (1 << IDX[IDE]) if (e % r == e // r) else 0
+                if (asum >> e) & 1:
+                    v ^= GP1
+                if (bsum >> e) & 1:
+                    v ^= BP1
+                if (xsum >> e) & 1:
+                    v ^= PAB
+                if (ysum >> e) & 1:
+                    v ^= QBA
+                if RED[v ^ target(r, k)[e]]:
+                    ok = False
+                    break
+            if not ok:
+                continue
+            stat["layer_hits"] += 1
+            labels_t = tuple(labels)
+            mats_t = tuple(ns)
+            full = word_value(r, labels_t, mats_t) == target(r, k)
+            if full:
+                stat["full_hits"] += 1
+                if stat["full_witness"] is None:
+                    stat["full_witness"] = (labels_t, mats_t)
+            elif stat["layer_only_witness"] is None:
+                stat["layer_only_witness"] = (labels_t, mats_t)
+    return stat
+
+
+# ---------------------------------------------------------------------- main
+def run_controls():
+    lines = []
+    for r, labels, mats, k in direct_control_words():
+        assert word_value(r, labels, mats) == target(r, k), "direct word fails"
+        assert layer_value_ok(r, labels, mats, k), "direct word fails layer"
+    lines.append("direct_words=4")
+    for r, labels, mats, k, name in mutation_controls():
+        assert word_value(r, labels, mats) != target(r, k), "mutation passes: " + name
+    lines.append("mutation_controls=4")
+    r1 = search(1, 3, 1, 1, samples=4000, seed=11)
+    assert r1["full_witness"] is not None, "r=1 control search found nothing"
+    r2 = search(2, 6, 3, 2, samples=40000, seed=12)
+    assert r2["full_witness"] is not None, "r=2 control search found nothing"
+    assert r2["layer_hits"] > 0 and r2["layer_only_witness"] is not None, \
+        "no strict-relaxation witness at r=2"
+    lines.append("search_controls=r1:%d/%d r2:%d/%d/%d" %
+                 (r1["full_hits"], r1["valid"], r2["full_hits"], r2["layer_hits"], r2["valid"]))
+    # Obstruction check: the augmentation powers of F2[GL_2(F2)] stabilize at
+    # J^2 = J^3, so R/J^3 is the sign quotient F2[z]/(z^2) and the J^2-layer
+    # equation carries no information beyond sum N_i = I_r.
+    assert DIMS[1] == DIMS[2] and _span(J2) == _span(J3), "expected J^2 = J^3"
+    rng = random.Random(20261015)
+    idems = rank_one_idempotents(4)
+    equiv = 0
+    for _ in range(200):
+        q = rng.randrange(2, 8)
+        labels = tuple((A, B)[rng.randrange(2)] for _ in range(q))
+        mats = tuple(rng.choice(idems) for _ in range(q))
+        total = 0
+        for n in mats:
+            total ^= n
+        if layer_value_ok(4, labels, mats, 4) == (total == ident_m(4)):
+            equiv += 1
+    assert equiv == 200, "layer check must be equivalent to sum N_i = I_r"
+    lines.append("j2_eq_j3=1 layer_iff_sum=200/200")
+    return lines, r1, r2
+
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--full", action="store_true", help="run the recorded full search budget")
+    ap.add_argument("--samples", type=int, default=0)
+    ap.add_argument("--emit", action="store_true", help="print receipt without comparing EXPECTED.json")
+    args = ap.parse_args()
+    build()
+    t0 = time.time()
+    lines, r1, r2 = run_controls()
+    samples = args.samples or (6000000 if args.full else 2000000)
+    mode = "full" if args.full else "default"
+    main_stat = search(4, 10, 5, 4, samples=samples, seed=20261014)
+    elapsed = time.time() - t0
+    receipt = {
+        "mode": mode,
+        "dims_J1_J2_J3": list(DIMS),
+        "samples": samples,
+        "valid": main_stat["valid"],
+        "labelings": main_stat["labelings"],
+        "layer_hits": main_stat["layer_hits"],
+        "full_hits": main_stat["full_hits"],
+        "r1_control_full_hits": r1["full_hits"],
+        "r2_control_full_hits": r2["full_hits"],
+        "r2_control_layer_hits": r2["layer_hits"],
+    }
+    expected_path = HERE / "EXPECTED.json"
+    if args.emit:
+        print(json.dumps(receipt, indent=1, sort_keys=True))
+    elif expected_path.exists():
+        expected = json.loads(expected_path.read_text(encoding="utf-8"))
+        want = expected[mode]
+        for key, value in want.items():
+            assert receipt[key] == value, "receipt mismatch %s: got %r want %r" % (
+                key, receipt[key], value)
+    print("controls: " + " ".join(lines))
+    print("augmentation dims (J1,J2,J3)=%s with J2=J3; R/J3 is the sign quotient" % (DIMS,))
+    print("main search r=4 q=10 (5a,5b) k=4 samples=%d valid=%d labelings=%d "
+          "layer_hits=%d full_hits=%d" % (samples, main_stat["valid"],
+                                          main_stat["labelings"], main_stat["layer_hits"],
+                                          main_stat["full_hits"]))
+    if main_stat["full_witness"] is not None:
+        labels, mats = main_stat["full_witness"]
+        print("CANDIDATE_FOUND labels=" + "".join("a" if g == A else "b" for g in labels))
+        print("CANDIDATE_MATS=" + json.dumps(list(mats)))
+        print("PASS_FOUR_SWAP_BALANCED_J3_LAYER candidate_found no_new_kappa")
+    else:
+        print("PASS_FOUR_SWAP_BALANCED_J3_LAYER balanced_5a5b_unrealized_in_search "
+              "layer_hits=%d no_new_kappa" % main_stat["layer_hits"])
+    print("elapsed_seconds=%.1f" % elapsed)
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())

From f41de0127d4557fac52fc3dce386ed869526c17a Mon Sep 17 00:00:00 2001
From: Aaron Wang <warhawk947@gmail.com>
Date: Wed, 14 Oct 2026 13:31:27 -0400
Subject: [PATCH 2/2] Correct r=5 restored-role follow-up: sum N_i =
 diag(I_4,0), not I_5

Review follow-up on https://github.com/CrocSwap/integer-mult-bounds/pull/1755:
the r=5 open question proposed conditioning on sum N_i = I_5 for the endpoint
diag([S],[S],[S],[S],1). The restored fifth role carries the identity
boundary, so its target augmentation is zero and the sign quotient forces
sum N_i = diag(I_4, 0); I_5 would exclude every solution to that endpoint.
Corrected in README.md, TASK.json and VERIFY.json (this package has no
CERTIFICATE.json), with exact regression controls in verify.py and
test_verify.py: permutation-sign quotient matching the J^2 = J^3 reduction,
zero fifth-role augmentation, a 12-call disjoint witness realizing the
endpoint with sum N_i = diag(I_4,0) != I_5, the I_5 total failing the
endpoint layer equation, and r=5 layer equivalence with diag(I_4,0)
(200/200).

The retained r=4 computation is unchanged: augmentation dims (5,4,4) with
J^2 = J^3, layer equivalence with sum N_i = I_r (200/200), and the
6,000,000-sample balanced (5a,5b) search over 5,771,556 labelings with 0
full-formal hits all reproduce exactly (PASS_FOUR_SWAP_BALANCED_J3_LAYER
balanced_5a5b_unrealized_in_search layer_hits=5771556 no_new_kappa).

Prepared by Aaron Wang, with help from opencode. Apache-2.0.
---
 .../four-swap-balanced-j3-layer/README.md     | 22 ++++-
 .../four-swap-balanced-j3-layer/TASK.json     |  2 +-
 .../four-swap-balanced-j3-layer/VERIFY.json   |  4 +-
 .../test_verify.py                            | 69 ++++++++++++++
 .../four-swap-balanced-j3-layer/verify.py     | 89 +++++++++++++++++++
 5 files changed, 179 insertions(+), 7 deletions(-)

diff --git a/research/four-swap-balanced-j3-layer/README.md b/research/four-swap-balanced-j3-layer/README.md
index 2dddd1922a..4178ba91e2 100644
--- a/research/four-swap-balanced-j3-layer/README.md
+++ b/research/four-swap-balanced-j3-layer/README.md
@@ -54,7 +54,10 @@ prod (1 + eps_i) = 1 + sum eps_i + sum_{i<j} eps_i eps_j    (mod J^3 M_r)
 is exact and is checked on seeded random words (same-label pairs already
 vanish identically because `([a]+1)^2 = ([b]+1)^2 = 0`). But after reduction
 the whole layer equation collapses entrywise to `sum_i N_i = I_r`, nothing
-more. The verifier machine-checks the equivalence
+more (for a target that restores a role with the identity boundary, the
+right-hand side is the target's own z-coefficient matrix instead: `diag(I_4,0)`
+at `r = 5` with one restored fifth role, whose target augmentation is zero).
+The verifier machine-checks the equivalence
 (`layer check holds  <=>  sum N_i = I_r`) on 200/200 random instances, and
 the search below confirms it exhaustively on its own domain: every one of the
 5,771,556 balanced labelings passed the layer check, because the sampler
@@ -93,7 +96,10 @@ and `r = 2` (`q = 6` balanced, 3,254 witnesses); a strict-relaxation honesty
 control exhibits a layer-feasible word that fails full equality; conjugation
 of `N` by `GL_r(F2)` preserves the idempotent family; and two hand-derived
 pins (`([a]+1)^2 = 0`; `([a]+1)([b]+1)([a]+1) = [aba]+[ab]+[ba]+[b]`) bind
-the group algebra implementation.
+the group algebra implementation. A restored-role regression control pins the
+corrected `r = 5` sign quotient: the fifth role's target augmentation is zero,
+`sum N_i = diag(I_4, 0)`, and an `I_5` total fails the endpoint layer equation
+(see open question 2).
 
 ## Reproduce
 
@@ -153,8 +159,16 @@ profile or kappa follows; the selected frontier is unchanged.
 2. **The same balanced question at `r = 5` with one restored dirty extra.**
    Smallest falsifying instance of "workspace cheapens the tariff". First
    step: rerun the conditioned sampler at `r = 5`, target
-   `diag([S],[S],[S],[S],1)`, `sum N_i = I_5` (the sign-quotient lemma is
-   register-count independent). Blocked by: nothing; it is open compute.
+   `diag([S],[S],[S],[S],1)`, conditioning on `sum N_i = diag(I_4, 0)`:
+   the restored fifth role carries the identity boundary, so its target
+   augmentation is zero and the sign quotient (register-count independent)
+   forces the fifth diagonal entry of `sum N_i` to be 0. The earlier
+   `sum N_i = I_5` wording was wrong and would exclude every solution to that
+   endpoint: the four disjoint `aba`/`bab` control word with the fifth role
+   restored realizes `diag([S],[S],[S],[S],1)` exactly and has
+   `sum N_i = diag(I_4, 0) != I_5`, so an `I_5`-conditioned sampler rejects
+   it. `verify.py` and `test_verify.py` pin the corrected condition by exact
+   check. Blocked by: nothing; it is open compute.
 
 ## Credit and license
 
diff --git a/research/four-swap-balanced-j3-layer/TASK.json b/research/four-swap-balanced-j3-layer/TASK.json
index 6901b71fc4..c9471dfc3f 100644
--- a/research/four-swap-balanced-j3-layer/TASK.json
+++ b/research/four-swap-balanced-j3-layer/TASK.json
@@ -58,7 +58,7 @@
   {
    "question": "Does the balanced-profile obstruction at r = 4 persist at r = 5 with one restored dirty extra register?",
    "why_it_matters": "It is the smallest falsifying instance of 'workspace cheapens the tariff' for four SWAP targets and tests whether register growth changes the picture.",
-   "first_step": "Rerun the same conditioned search at r = 5 with target diag([S] x 4, 1) and the identical sum N_i = I_5 reduction, which the sign-quotient lemma still justifies.",
+   "first_step": "Rerun the same conditioned search at r = 5 with target diag([S] x 4, 1), conditioning on sum N_i = diag(I_4, 0): the restored fifth role carries the identity boundary, so its target augmentation is zero and the sign quotient forces diag(I_4, 0), not I_5 (corrected after review follow-up; the earlier I_5 wording would exclude every solution to that endpoint).",
    "blocked_by": "The r = 5 balanced question itself is open; only the r = 4 balanced domain was searched here."
   }
  ]
diff --git a/research/four-swap-balanced-j3-layer/VERIFY.json b/research/four-swap-balanced-j3-layer/VERIFY.json
index 55f8490772..66290e0c14 100644
--- a/research/four-swap-balanced-j3-layer/VERIFY.json
+++ b/research/four-swap-balanced-j3-layer/VERIFY.json
@@ -14,7 +14,7 @@
     "--full"
    ],
    "timeout_seconds": 600,
-   "checks": "Hand algebra pins ([a]+1)^2 = 0 and the ([a]+1)([b]+1)([a]+1) coefficient pin; J^2 = J^3 obstruction; layer-check equivalence with sum N_i = I_r (200/200); J^3 expansion identity on seeded random words; four direct control words and four mutation controls; r=1/r=2 balanced search finders; the recorded 6,000,000 sample balanced (5a,5b) search with exact M_4(F2[G]) equality."
+   "checks": "Hand algebra pins ([a]+1)^2 = 0 and the ([a]+1)([b]+1)([a]+1) coefficient pin; J^2 = J^3 obstruction; layer-check equivalence with sum N_i = I_r (200/200); J^3 expansion identity on seeded random words; four direct control words and four mutation controls; r=1/r=2 balanced search finders; restored-role sign-quotient control at r = 5 (endpoint diag([S],[S],[S],[S],1) forces sum N_i = diag(I_4,0), fifth-role target augmentation zero, 12-call disjoint witness, I_5 shown to overconstrain, r=5 layer equivalence 200/200); the recorded 6,000,000 sample balanced (5a,5b) search with exact M_4(F2[G]) equality."
   },
   {
    "argv": [
@@ -24,7 +24,7 @@
     "{package}/test_verify.py"
    ],
    "timeout_seconds": 120,
-   "checks": "Independent hand-derived algebra pins, layer expansion identity, direct-word and mutation controls, conjugation closure of rank-one idempotents, known-solvable search instances, and the strict-relaxation honesty control."
+   "checks": "Independent hand-derived algebra pins, layer expansion identity, direct-word and mutation controls, conjugation closure of rank-one idempotents, known-solvable search instances, the strict-relaxation honesty control, and the restored-role regression pins (permutation-sign quotient matching the J^2 = J^3 reduction, zero fifth-role target augmentation, endpoint witness with sum N_i = diag(I_4,0) != I_5, and r = 5 layer equivalence with diag(I_4,0))."
   }
  ]
 }
\ No newline at end of file
diff --git a/research/four-swap-balanced-j3-layer/test_verify.py b/research/four-swap-balanced-j3-layer/test_verify.py
index 85c701020d..135fd0ac58 100644
--- a/research/four-swap-balanced-j3-layer/test_verify.py
+++ b/research/four-swap-balanced-j3-layer/test_verify.py
@@ -104,5 +104,74 @@ def test_layer_is_a_strict_relaxation(self):
         self.assertNotEqual(V.word_value(2, labels, mats), V.target(2, 2))
 
 
+class RestoredRoleSignQuotient(unittest.TestCase):
+    """Regression control for the review follow-up on
+    https://github.com/CrocSwap/integer-mult-bounds/pull/1755.
+
+    At r = 5 with endpoint diag([S],[S],[S],[S],1) the fifth role is restored
+    with the identity boundary: its target augmentation is zero, so the sign
+    quotient forces sum N_i = diag(I_4, 0), not I_5.  Conditioning on I_5
+    would exclude every solution to that endpoint.  Hand derivation: rho([g])
+    = 1 + sign(g) z is the sign quotient F2[G] -> F2[z]/(z^2) with z^2 = 0,
+    every paid factor 1 + ([g]+1) N reduces to 1 + z N (a and b are odd), so
+    the word reduces to 1 + z sum N_i while the endpoint reduces to
+    1 + z diag(I_4, 0); comparing z-coefficients gives sum N_i = diag(I_4,0).
+    """
+
+    def setUp(self):
+        V.build()
+
+    def test_sign_quotient_is_permutation_sign(self):
+        # The quotient is determined by the permutation sign of GL_2(F2) on
+        # the three nonzero vectors: even elements (identity, the two
+        # 3-cycles) reduce to 0, odd ones (the three transpositions, incl.
+        # a, b, S) to z.  This must agree with the J^2 = J^3 reduction.
+        for g in V.ELEMS:
+            self.assertEqual(V.RED[V.gplus(g)] == 0, V.perm_sign(g) == 0)
+        self.assertEqual([V.perm_sign(g) for g in (V.A, V.B, V.S)], [1, 1, 1])
+        self.assertEqual(V.perm_sign(V.IDE), 0)
+
+    def test_fifth_role_target_augmentation_is_zero(self):
+        zt = V.zcoef_mR(5, V.target(5, 4))
+        self.assertEqual(zt, V.diag_m(5, 4), "endpoint z-coefficient is diag(I_4,0)")
+        self.assertEqual((zt >> 24) & 1, 0, "fifth role's augmentation must be zero")
+        self.assertNotEqual(zt, V.ident_m(5), "I_5 must not be the forced condition")
+        self.assertEqual(zt ^ V.ident_m(5), 1 << 24, "they differ only in the (5,5) entry")
+        # The retained r = 4 statement is unchanged: all four roles swapped.
+        self.assertEqual(V.zcoef_mR(4, V.target(4, 4)), V.ident_m(4))
+
+    def test_endpoint_witness_and_i5_overconstraint(self):
+        labels = (V.A, V.B, V.A) * 2 + (V.B, V.A, V.B) * 2
+        mats = (V.idem(5, 1, 1),) * 3 + (V.idem(5, 2, 2),) * 3 + \
+               (V.idem(5, 4, 4),) * 3 + (V.idem(5, 8, 8),) * 3
+        self.assertEqual(V.word_value(5, labels, mats), V.target(5, 4),
+                         "12-call disjoint word must realize the endpoint")
+        total = 0
+        for n in mats:
+            total ^= n
+        self.assertEqual(total, V.diag_m(5, 4))
+        self.assertNotEqual(total, V.ident_m(5),
+                            "I_5 conditioning would reject this solution")
+        self.assertTrue(V.layer_value_ok(5, labels, mats, 4))
+        # Forcing the total to I_5 must break the endpoint layer equation.
+        self.assertEqual(total ^ V.idem(5, 16, 16), V.ident_m(5))
+        self.assertFalse(V.layer_value_ok(5, labels + (V.A,),
+                                          mats + (V.idem(5, 16, 16),), 4))
+
+    def test_layer_iff_sum_is_diag_i4_zero(self):
+        rng = random.Random(20261016)
+        idems = V.rank_one_idempotents(5)
+        zt = V.diag_m(5, 4)
+        for _ in range(200):
+            q = rng.randrange(2, 8)
+            labels = tuple((V.A, V.B)[rng.randrange(2)] for _ in range(q))
+            mats = tuple(rng.choice(idems) for _ in range(q))
+            total = 0
+            for n in mats:
+                total ^= n
+            self.assertEqual(V.layer_value_ok(5, labels, mats, 4), total == zt,
+                             "r=5 layer check must be equivalent to sum N_i = diag(I_4,0)")
+
+
 if __name__ == "__main__":
     unittest.main(verbosity=2)
diff --git a/research/four-swap-balanced-j3-layer/verify.py b/research/four-swap-balanced-j3-layer/verify.py
index a497771895..341d81ae78 100644
--- a/research/four-swap-balanced-j3-layer/verify.py
+++ b/research/four-swap-balanced-j3-layer/verify.py
@@ -303,6 +303,47 @@ def layer_value_ok(r, labels, mats, k):
     return all(RED[a ^ b] == 0 for a, b in zip(lhs, tgt))
 
 
+# ------------------------------------------------------- sign quotient (exact)
+def _m2_vec(g, v):
+    """Action of g in GL_2(F2) on column vector v (bit0 = x, bit1 = y)."""
+    x = bin((g & 3) & v).count("1") & 1
+    y = bin(((g >> 2) & 3) & v).count("1") & 1
+    return x | (y << 1)
+
+
+def perm_sign(g):
+    """Sign of g: parity of its permutation of the 3 nonzero vectors of F2^2."""
+    vecs = (1, 2, 3)
+    perm = [vecs.index(_m2_vec(g, v)) for v in vecs]
+    return sum(1 for i, j in itertools.combinations(range(3), 2)
+               if perm[i] > perm[j]) & 1
+
+
+def zcoef(x):
+    """z-coefficient of the sign-quotient image rho(x) in F2[z]/(z^2)."""
+    c = 0
+    for i in range(6):
+        if (x >> i) & 1:
+            c ^= perm_sign(ELEMS[i])
+    return c
+
+
+def zcoef_mR(r, x):
+    """Entrywise z-coefficient matrix of rho applied to x in M_r(R)."""
+    out = 0
+    for e in range(r * r):
+        if zcoef(x[e]):
+            out |= 1 << e
+    return out
+
+
+def diag_m(r, k):
+    n = 0
+    for p in range(k):
+        n |= 1 << (p * r + p)
+    return n
+
+
 # ------------------------------------------------------------------- controls
 def direct_control_words():
     """(r, labels, mats, k): known direct words realizing diag([S]^k, 1..)."""
@@ -437,6 +478,54 @@ def run_controls():
             equiv += 1
     assert equiv == 200, "layer check must be equivalent to sum N_i = I_r"
     lines.append("j2_eq_j3=1 layer_iff_sum=200/200")
+    # Restored-role sign quotient (review follow-up on
+    # https://github.com/CrocSwap/integer-mult-bounds/pull/1755): at r = 5 with
+    # endpoint diag([S],[S],[S],[S],1) the fifth role is restored with the
+    # identity boundary, so its target augmentation is zero and the quotient
+    # forces sum N_i = diag(I_4, 0), NOT I_5.  Conditioning on I_5 would
+    # exclude every solution to that endpoint.  Exact checks below: the
+    # permutation sign agrees with the J^2 = J^3 reduction, the endpoint's
+    # z-coefficient matrix is diag(I_4,0) with a zero fifth diagonal entry, a
+    # 12-call disjoint witness realizes the endpoint with sum N_i =
+    # diag(I_4,0) != I_5, forcing the total to I_5 breaks the endpoint layer
+    # equation, and the r = 5 layer equation stays equivalent to
+    # sum N_i = diag(I_4,0) on 200/200 random instances.
+    assert all(perm_sign(g) == (0 if RED[gplus(g)] == 0 else 1) for g in ELEMS), \
+        "sign quotient must match the J^2 = J^3 reduction"
+    zt = zcoef_mR(5, target(5, 4))
+    assert zt == diag_m(5, 4) and not (zt >> 24) & 1, \
+        "fifth role's target augmentation must be zero"
+    labels5 = (A, B, A) * 2 + (B, A, B) * 2
+    mats5 = (idem(5, 1, 1),) * 3 + (idem(5, 2, 2),) * 3 + \
+            (idem(5, 4, 4),) * 3 + (idem(5, 8, 8),) * 3
+    assert word_value(5, labels5, mats5) == target(5, 4), \
+        "restored-role control word must realize diag([S],[S],[S],[S],1)"
+    total5 = 0
+    for n in mats5:
+        total5 ^= n
+    assert total5 == zt and total5 != ident_m(5), \
+        "I_5 conditioning must overconstrain the restored-role endpoint"
+    assert layer_value_ok(5, labels5, mats5, 4), "witness must pass the layer check"
+    forced5 = total5 ^ idem(5, 16, 16)
+    assert forced5 == ident_m(5)
+    assert not layer_value_ok(5, labels5 + (A,), mats5 + (idem(5, 16, 16),), 4), \
+        "an I_5 total must fail the endpoint layer equation"
+    rng = random.Random(20261016)
+    idems5 = rank_one_idempotents(5)
+    equiv5 = 0
+    for _ in range(200):
+        q = rng.randrange(2, 8)
+        labels = tuple((A, B)[rng.randrange(2)] for _ in range(q))
+        mats = tuple(rng.choice(idems5) for _ in range(q))
+        total = 0
+        for n in mats:
+            total ^= n
+        if layer_value_ok(5, labels, mats, 4) == (total == zt):
+            equiv5 += 1
+    assert equiv5 == 200, \
+        "r=5 layer check must be equivalent to sum N_i = diag(I_4,0)"
+    lines.append("r5_restored_role=1 fifth_role_zcoef=0 i5_overconstrains=1 "
+                 "layer_iff_sum_diagI4zero=200/200")
     return lines, r1, r2