Scoped obstruction + search: balanced ten-call four-SWAP residual, J^2 = J^3 kills the layer route (no new kappa)

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

research/four-swap-balanced-j3-layer/README.md

@@ -0,0 +1,189 @@
+# 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 (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
+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. 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
+
+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)`, 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
+
+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.

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

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