Mister-Meeseeks · Oct 24, 2026 · Oct 23, 2026
diff --git a/research/spectator-three-cycle-additivity/README.md b/research/spectator-three-cycle-additivity/README.md
@@ -0,0 +1,131 @@
+# A spectator coordinate does not help two 3-cycles
+
+**Exact computer-assisted result in a formal model. No new κ.**
+The selected conditional exponent stays 15108879/5000000000 (#4610).
+
+## Result
+
+The setting is the formal model `M_R(F2[GL_n(F2)])` of #4939/#4950/#4968
+at `n = 4`, `R = 2`:
+
+- A paid call is `D(g,N) = I + ([g]+[e])N`, where `g` is one of the 12
+  coordinate CNOTs of `GL_4(F2)` and `N = uvᵀ` is one of the 6 rank-one binary
+  idempotents of `M_2(F2)`. This gives 72 paid factors.
+- Free scalar `GL_2(F2)` maps are allowed.
+- Equality is formal, on arbitrary inputs.
+
+Let `c` be the coordinate 3-cycle on coordinates 0, 1, 2. Address coordinate 3
+is a spectator: the endpoint fixes it, but calls may write it. Then
+
+```text
+diag([c],[c]) has no realizing word of length ≤ 11, so its cost is exactly 12.
+```
+
+The upper bound is #5005's word: a shortest 3-cycle word on each register.
+So a spectator coordinate gives two 3-cycles no shared paid work, just as at
+`n = 3` (#5005). This answers the `n ≥ 4` part of #5005's open question for its
+smallest case. A single 3-cycle already costs 6 with any spectators
+(`research/three-cycle-address-floor`).
+
+| Check | Outcome |
+|---|---|
+| Upper bound | 12 calls |
+| Length ≤ 9 | excluded in the registered replay (depth 4 + 5) |
+| Length ≤ 10 | excluded in a recorded **local** run (depth 4 + 6) |
+| Length ≤ 11 | excluded in a recorded **local** run (depth 5 + 6, 721,626,127 forward states) |
+
+## Method
+
+`search.c` is an exact meet-in-the-middle search with a **sparse** state.
+Each of the four matrix entries is a sorted set of `GL_4(F2)` indices with F2
+coefficients. A product of `L` calls has at most `2^L` terms per entry, so the
+20,160-element group needs no dense bitsets. The search structure is the same
+as in #5005 and #5292:
+
+- **Cancellation.** Adjacent equal letters cancel.
+- **Commutation order.** 1,584 of the 5,112 ordered pairs of distinct calls
+  commute (an exact algebra test). Adjacent commuting letters are kept only in
+  increasing order.
+- **Symmetry.** The target and the generator set are fixed by 36 maps:
+  conjugation of `GL_4` by the coordinate permutations commuting with `c`,
+  optionally composed with inverse-transpose, times `GL_2(F2)` register
+  conjugation. The first two backward letters are the lexicographically least
+  pair of their orbit, which leaves 142 of 5,112 pairs. The commutation order
+  applies only from the fourth backward letter on.
+- **Exact check of key matches.** A state at distance ≤ 5 is `A·B`, with `A`
+  in the exact radius-two ball (4,297 stored states) and `|B| ≤ 3`. Every key
+  match is tested this way. The final run recorded one key match, and the exact
+  test rejected it. An earlier length-11 run used a build whose exact test only
+  reached distance 4. It was discarded and rerun with the final source.
+
+The distinct-state counts are 73, 4,297, 240,565, 13,231,207 and 721,626,127
+at depth ≤ 1, …, 5.
+
+## Evidence
+
+`verify.py` uses the standard library and a C11 compiler. In default mode it
+checks:
+
+1. **Compilation.** `search.c` compiles with `-Wall -Wextra -Werror`.
+2. **Semantics.** The C products agree with the merged Python formal model at
+   `n = 4`, `R = 2` on 36 random words of length 0–5, as exact group-algebra
+   states.
+3. **Engine self-test.** There are 1,584 commuting pairs and the exact
+   radius-two ball. Twelve random words of length 3–5 verify within their
+   length, and `diag(c,c)` is rejected at distance ≤ 5.
+4. **State counts.** The distinct states at depth ≤ 1, 2, 3, 4 are as listed
+   above.
+5. **Positive controls,** with and without symmetry:
+   - `diag([c],[e])` (cost 6, as in `three-cycle-address-floor`);
+   - two swaps `diag([s01],[s01])` (cost 6, as in #4950).
+   Each has nothing at length ≤ 5, and its length 6 is found.
+6. **Mixed target.** `diag([c],[s01])` has nothing at length ≤ 8. A recorded
+   local depth 4 + 5 run finds its length 9.
+7. **Upper bound.** The 12-call word is checked in Python.
+8. **Main search.** Nothing at length ≤ 6 without symmetry, and nothing at
+   length ≤ 9 with it.
+
+`verify.py --full` reruns the local depth 4 + 6 and 5 + 6 runs. The second needs
+about 8 GB of memory. `RESULT.json` records their outputs, times, machine and
+the hash of the compiled source.
+
+Changing `search.c` fails the hash binding to the recorded runs. Dropping one
+column update in the generator product fails the semantic binding.
+
+## Scope
+
+Card `bit-new-register-model`, scope **changed** (see `TASK.json`). This covers
+only `n = 4` (one spectator) with `R = 2`. It does **not** settle:
+- `n ≥ 5`;
+- a dirty third register (#5292 leaves length 11 open at `R = 3`);
+- other targets;
+- native operations, tariffs or κ.
+
+Base: canonical main `1ec1119972c9aefe42525172d07b332fcff81cb4`, priority
+revision 7.
+
+## Reproduce
+
+```sh
+python3.12 -I -B research/spectator-three-cycle-additivity/verify.py
+python3.12 -I -B research/spectator-three-cycle-additivity/verify.py --full   # local, about 8 GB
+python3.12 -B scripts/research_package.py --package research/spectator-three-cycle-additivity
+```
+
+## Open next questions
+
+1. **Every `n ≥ 4`.** *First step:* adapt the written-spectator reduction of
+   `three-cycle-address-floor`. A short word can write only a few spectator
+   rows. Restrict the unwritten ones to their zero subspace, which reduces the
+   question to finitely many `n`, including this one. *Blocked by:* a written
+   argument for two targets.
+
+## Credit
+
+- Mihir Srivastava (#4939), for the formal model.
+- JoyboyBrian (#4974, `three-cycle-address-floor`), for the single-cycle
+  spectator theorem.
+- The predecessors credited in #4950/#4968/#5005/#5292.
+
+Prepared by James Reed with substantial Anthropic Claude (Claude Code)
+assistance. Apache-2.0. No independent human review is claimed.
diff --git a/research/spectator-three-cycle-additivity/RESULT.json b/research/spectator-three-cycle-additivity/RESULT.json
@@ -0,0 +1,63 @@
+{
+  "schema_version": 1,
+  "target": "diag([c],[c]) in M_2(F2[GL_4(F2)]), c the 3-cycle on coordinates 0,1,2, coordinate 3 a spectator",
+  "upper_bound": 12,
+  "excluded_lengths_registered": "<= 9",
+  "excluded_lengths_local": "<= 11",
+  "exact_cost": 12,
+  "new_kappa": false,
+  "note": "Every key match is checked exactly (distance <= 5 via the stored radius-two ball and words of length <= 3); the single key match of the length-11 run is a fingerprint collision. An earlier length-11 run used a build whose exact check only covered distance <= 4; it was discarded and rerun with this source.",
+  "local_runs": [
+    {
+      "search_c_sha256": "6111e6a9f12f5aba5fd0841332fc660305306eaa9670a5f25d0313c77e08b890",
+      "compile": "cc -std=c11 -O3 -march=native -Wall -Wextra -Werror -o search search.c",
+      "compiler": "cc (GCC) 16.2.1 20260810",
+      "machine": "AMD Ryzen 9 7940HS w/ Radeon 780M Graphics, 16 threads, 25 GB RAM, Linux 7.2.8-9-omarchy",
+      "label": "local-only receipt; not replayed by the registered harness",
+      "name": "c3c3 length <= 11",
+      "command": "search c3c3 5 6 sym 16 30",
+      "max_length": 11,
+      "started_utc": "2026-10-23T20:23:00Z",
+      "finished_utc": "2026-10-23T20:32:54Z",
+      "output": [
+        "target=c3c3 symmetries=36 pairs=142 mode=sym",
+        "forward_depth=5 distinct=721626127 ball2=4297",
+        "RESULT target=c3c3 max_length=11 shortest=-1 key_matches=1 backward_nodes=2177858439"
+      ]
+    },
+    {
+      "search_c_sha256": "6111e6a9f12f5aba5fd0841332fc660305306eaa9670a5f25d0313c77e08b890",
+      "compile": "cc -std=c11 -O3 -march=native -Wall -Wextra -Werror -o search search.c",
+      "compiler": "cc (GCC) 16.2.1 20260810",
+      "machine": "AMD Ryzen 9 7940HS w/ Radeon 780M Graphics, 16 threads, 25 GB RAM, Linux 7.2.8-9-omarchy",
+      "label": "local-only receipt; not replayed by the registered harness",
+      "name": "c3c3 length <= 10",
+      "command": "search c3c3 4 6 sym 16 27",
+      "max_length": 10,
+      "started_utc": "2026-10-23T20:33:04Z",
+      "finished_utc": "2026-10-23T20:34:05Z",
+      "output": [
+        "target=c3c3 symmetries=36 pairs=142 mode=sym",
+        "forward_depth=4 distinct=13231207 ball2=4297",
+        "RESULT target=c3c3 max_length=10 shortest=-1 key_matches=0 backward_nodes=2177858439"
+      ]
+    },
+    {
+      "search_c_sha256": "6111e6a9f12f5aba5fd0841332fc660305306eaa9670a5f25d0313c77e08b890",
+      "compile": "cc -std=c11 -O3 -march=native -Wall -Wextra -Werror -o search search.c",
+      "compiler": "cc (GCC) 16.2.1 20260810",
+      "machine": "AMD Ryzen 9 7940HS w/ Radeon 780M Graphics, 16 threads, 25 GB RAM, Linux 7.2.8-9-omarchy",
+      "label": "local-only receipt; not replayed by the registered harness",
+      "name": "c3s01 shortest 9",
+      "command": "search c3s01 4 5 sym 16 27",
+      "max_length": 9,
+      "started_utc": "2026-10-23T20:34:05Z",
+      "finished_utc": "2026-10-23T20:34:28Z",
+      "output": [
+        "target=c3s01 symmetries=2 pairs=2556 mode=sym",
+        "forward_depth=4 distinct=13231207 ball2=4297",
+        "RESULT target=c3s01 max_length=9 shortest=9 key_matches=2241 backward_nodes=658795849"
+      ]
+    }
+  ]
+}
diff --git a/research/spectator-three-cycle-additivity/SOURCES.json b/research/spectator-three-cycle-additivity/SOURCES.json
@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b288ae44032fd84dd5564243422836cbcd29835e",
+      "sha256": "f9ed52bb642cd1e1486cf2743557ac5fa23cf1514a3277d786a644e39a565038"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/swap-component-cut/formal.py",
+      "usage": "input",
+      "git_blob": "eb3058c3593e3373a417f9b6c2d566ca409b591d",
+      "sha256": "e23c71e52a52ee6466a8d07c3608ebe38015cdc959c92f9e8a57557c9ef68628"
+    },
+    {
+      "path": "research/two-three-cycle-additivity/README.md",
+      "usage": "provenance",
+      "git_blob": "6bbd51f92adebdf1e5ca8141251cc35f5990af7c",
+      "sha256": "b292e40966b928f26b407ae5c59b4ed9b8d4687d28076efbc759a8afdf62cdfb"
+    },
+    {
+      "path": "research/three-register-three-cycles/README.md",
+      "usage": "provenance",
+      "git_blob": "555f72cae779edc92e9f89f5c87047aec6429e95",
+      "sha256": "ff1433a69b5be638dd93cdf299ef2f94b0260bdfae86aae9f2616e6f537285ae"
+    },
+    {
+      "path": "research/three-cycle-address-floor/README.md",
+      "usage": "provenance",
+      "git_blob": "6a65c91f29e5b226cebd32d0c1d6963a60a98761",
+      "sha256": "a63c4ea4c874cac1fb064e1aff07f8ef791391eb795aec22a2154eb44a8fa81e"
+    },
+    {
+      "path": "research/swap-component-cut/README.md",
+      "usage": "provenance",
+      "git_blob": "19eaadc4ea40e312d202c917e2f1914d98ca224a",
+      "sha256": "7fe7efcb948a71af664d8f7828c8f4a056de3c6c3aa2cb82e420ec6ae7bd0106"
+    }
+  ]
+}
diff --git a/research/spectator-three-cycle-additivity/TASK.json b/research/spectator-three-cycle-additivity/TASK.json
@@ -0,0 +1,64 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "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. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "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": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "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.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Decide by exact search the cost of diag([c],[c]) in M_2(F2[GL_4(F2)]): two coordinate 3-cycles on coordinates 0,1,2 with one spectator address coordinate that must be restored (the n >= 4 open question of research/two-three-cycle-additivity).",
+  "scope_change_reason": "PR #5005 settled n = 3, R = 2 (exactly twelve) and PR #5292 bounded R = 3 below by eleven. Spectators are known not to help a single 3-cycle (#4974) or swaps (#4950). This package settles the smallest spectator case for two 3-cycles exactly. It does not cover n >= 5, R >= 3 or other targets.",
+  "bottleneck_link": "A spectator address coordinate cannot make two 3-cycles share paid work in this formal model at n = 4, R = 2; any saving needs a changed operation or tariff.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the exact length-11 exclusion with positive controls. Do not extend to n = 5 or R = 3 in this package.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/spectator-three-cycle-additivity",
+  "author": "James Reed",
+  "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).",
+  "open_questions": [
+    {
+      "question": "Does the n = 4 answer extend to every n >= 4 (all spectators), and does it combine with a dirty third register?",
+      "why_it_matters": "Together with #4974's uniform single-cycle argument, an all-n statement would close the spectator direction for two 3-cycles; the R = 3 length-11 case (#5292) is still open.",
+      "first_step": "Adapt #4974's written-spectator reduction: a word of length <= 11 can write at most a bounded number of spectator rows; restrict unwritten spectators to the zero subspace and reduce to this n = 4 search.",
+      "blocked_by": "A written argument for the reduction; the n = 5 search alone is much larger."
+    }
+  ]
+}
diff --git a/research/spectator-three-cycle-additivity/VERIFY.json b/research/spectator-three-cycle-additivity/VERIFY.json
@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/swap-component-cut/formal.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Compile search.c (-Wall -Wextra -Werror); bind the sparse C engine to the Python formal model at n = 4, R = 2 on 36 random words; 1,584 commuting pairs and the exact 4,297-state radius-two ball; distinct-state counts 73/4297/240565/13231207; twelve-call attaining word in Python; positive controls c3e and s01s01 with and without symmetry (nothing at length <= 5, shortest 6); c3c3 nothing at length <= 6 without symmetry; c3s01 nothing at length <= 8; c3c3 nothing at length <= 9 with symmetry (36 symmetries, 142 pairs). Lengths <= 10 and <= 11 are recorded local receipts in RESULT.json (verify.py --full)."
+    }
+  ]
+}