Mister-Meeseeks · Oct 23, 2026 · Oct 23, 2026
diff --git a/research/three-register-three-cycles/README.md b/research/three-register-three-cycles/README.md
@@ -0,0 +1,149 @@
+# A dirty third register saves at most one call on two 3-cycles
+
+**Exact computer-assisted partial result in a formal model. No new κ.**
+The selected conditional exponent stays 60403/20000000.
+
+## Result
+
+The setting is the formal model `M_3(F2[GL_3(F2)])` of #4939/#4950/#4968,
+with three scalar registers:
+
+- A paid call is `D(g,N) = I + ([g]+[e])N`, where `g` is one of the six
+  coordinate CNOTs and `N = uvᵀ` is one of the 28 rank-one binary idempotents
+  of `M_3(F2)`. This gives 168 paid factors.
+- Free scalar `GL_3(F2)` maps are allowed.
+- Equality is formal, on arbitrary inputs. The third register is arbitrary
+  and dirty, and must be restored exactly.
+
+Let `c` be a coordinate 3-cycle. Then
+
+```text
+diag([c],[c],[e]) has no realizing word of length ≤ 10, and one of length 12.
+```
+
+So the cost is 11 or 12. At `R = 2` it is exactly 12 (#5005). The third
+register can therefore save at most one of the twelve calls. Length 11 is
+open.
+
+| Check | Outcome |
+|---|---|
+| Upper bound | 12 calls (the `R = 2` word, register 2 untouched) |
+| Length ≤ 8 | excluded in the registered replay (depth 3 + 5) |
+| Length ≤ 10 | excluded in a recorded **local** run (depth 4 + 6, 53 min on 16 cores, 3.5·10¹¹ backward nodes) |
+| Length 11 | **open** |
+
+## Method
+
+`search.c` extends the exact meet-in-the-middle engine of #5005 to three
+registers. Free scalar maps are normalized away (#4939 step 1). Every paid call
+is an involution, so a word of length `L ≤ f + b` gives `T·W = X`, with `X` a
+product of at most `f` calls and `W` of at most `b` calls.
+
+- **Forward ball.** A depth-first search from `I` stores a 61-bit fingerprint
+  with the minimum depth. The distinct-state counts are 169, 22,051,
+  2,705,791 and **325,910,698** at depth ≤ 1, 2, 3, 4. The radius-two count
+  matches the merged order-7 package
+  `research/gl3-order7-dirty-register-seed39ae` (1 + 168 + 21,882).
+- **Backward search.** A depth-first search from `T` looks up every state. The
+  search runs in forked workers that share the table.
+- **Exact check of key matches.** A state at distance ≤ 4 is `A·B`, with `A`
+  in the exact radius-two ball (stored as full states) and `|B| ≤ 2`. Every
+  key match is tested this way. At depth 4 + 5 and 4 + 6 the runs record a few
+  fingerprint collisions, and all of them are rejected.
+
+Three word reductions are used. Each one keeps some shortest word, if any
+exists:
+
+1. **Cancellation.** Adjacent equal letters cancel, so they are skipped.
+2. **Commutation order.** 9,912 of the 28,056 ordered pairs of distinct calls
+   commute (an exact algebra test). Adjacent commuting letters are kept only in
+   increasing order. Every commutation class has such a word: its
+   lexicographically least one.
+3. **Symmetry.** The target and the generator set are fixed by 36 maps. These
+   are conjugation of `GL_3(F2)` by powers of `c`, optionally composed with
+   inverse-transpose, times register conjugation by the `GL_2(F2) × GL_1(F2)`
+   block matrices that fix `diag(1,1,0)`. These maps are algebra automorphisms
+   that fix `T` and the ball, so the first two backward letters can be the
+   lexicographically least pair of their orbit. That leaves 827 of the
+   28,056 pairs. The commutation order then applies from the third letter on,
+   so it never moves the chosen pair.
+
+Parity cannot shortcut the remaining case. The five calls `0, 28, 84, 0, 84`
+multiply to `I`. Their labels give the group relation `C01·C02·C12 = C12·C01`
+on one register.
+
+## 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
+   (`research/swap-component-cut/formal.py`, `R = 3`) on 36 random words of
+   length 0–5, as exact group-algebra states.
+3. **Engine self-test.** The batched leaf fingerprints equal the direct ones
+   on 33,600 children. The radius-two verifier accepts 400 words of length
+   ≤ 4. The commuting-pair count is 9,912.
+4. **State counts.** The distinct states at depth ≤ 1, 2, 3 are 169, 22,051
+   and 2,705,791.
+5. **Positive controls,** with and without symmetry:
+   - `diag([c],[e],[e])` (cost 6, `research/three-cycle-address-floor`);
+   - `diag([C7],[C7],[e])` (cost 6, the order-7 package);
+   - two swaps `diag([s01],[s01],[e])` (cost 6, #4950).
+   Each has nothing at length ≤ 5, and its length 6 is found.
+6. **Upper bound.** The 12-call word and the odd relation are checked in
+   Python.
+7. **Main search.** No word has length ≤ 6 without symmetry, or length ≤ 8
+   with it (36 symmetries, 827 pairs).
+
+`verify.py --full` reruns the two local runs: depth 4 + 5 (length ≤ 9) and
+depth 4 + 6 (length ≤ 10). Each needs about 9 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 those runs. A broken generator
+product (one dropped column update) also fails the semantic binding.
+
+## Scope
+
+Card `bit-new-register-model`, scope **changed** (see `TASK.json`). This is a
+negative formal-model screen. It does not satisfy the card's native
+construction gate.
+
+This package covers only `n = 3`, `R = 3`. It does **not** settle:
+- length 11;
+- four or more registers;
+- spectator address coordinates (`n ≥ 4`);
+- native operations, tariffs or κ.
+
+Base: canonical main `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority
+revision 7.
+Claim: [#1166 comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19148597).
+
+## Reproduce
+
+```sh
+python3.12 -I -B research/three-register-three-cycles/verify.py
+python3.12 -I -B research/three-register-three-cycles/verify.py --full   # local, about an hour
+python3.12 -B scripts/research_package.py --package research/three-register-three-cycles
+```
+
+## Open next questions
+
+1. **Is there a word of length exactly 11?** *First step:* find a structural
+   cut. Two examples: show that some call of a length-11 word must avoid
+   register 2, which reduces to #5005; or extend #4974's support lemma to two
+   targets. *Blocked by:* search size. The depth-5 forward ball has about
+   4·10¹⁰ states.
+
+## Credit
+
+- Mihir Srivastava (#4939), for the formal model.
+- JoyboyBrian (#4974), for the single-target support lemma.
+- Cinna Davis (`research/gl3-order7-dirty-register-seed39ae`), for the
+  `R = 3` ball count used as a cross-check.
+- JoyboyBrian (`research/three-cycle-address-floor`), for the single-cycle cost
+  6 used as a control.
+- The predecessors credited in #4950/#4968/#5005.
+
+Prepared by James Reed with substantial Anthropic Claude (Claude Code)
+assistance. Apache-2.0. No independent human review is claimed.
diff --git a/research/three-register-three-cycles/RESULT.json b/research/three-register-three-cycles/RESULT.json
@@ -0,0 +1,46 @@
+{
+  "schema_version": 1,
+  "target": "diag([c],[c],[e]) in M_3(F2[GL_3(F2)])",
+  "upper_bound": 12,
+  "excluded_lengths_registered": "<= 8",
+  "excluded_lengths_local": "<= 10",
+  "length_11": "open",
+  "new_kappa": false,
+  "note": "All key matches are 61-bit fingerprint collisions, each rejected by the exact radius-two split test (shortest=-1). The binary that ran was byte-identical to a fresh compile of this search.c (binary_sha256).",
+  "local_runs": [
+    {
+      "search_c_sha256": "293efe92a18693a4239462d52adc99939ca416fd519da0507645bc39ed5e2e0c",
+      "compile": "cc -std=c11 -O3 -march=native -Wall -Wextra -Werror -o search search.c",
+      "binary_sha256": "88f3a0d60a7feab698e71c4881fd3ca664bede2b2d1399418529c6a1f59eac95",
+      "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",
+      "command": "search c3c3e 4 5 sym 16 30",
+      "max_length": 9,
+      "started_local": "2026-10-23 08:16:24",
+      "finished_local": "2026-10-23 08:18:13",
+      "output": [
+        "target=c3c3e symmetries=36 first_letters=7 pairs=827 mode=sym",
+        "forward_depth=4 distinct=325910698",
+        "RESULT target=c3c3e max_length=9 shortest=-1 key_matches=8 backward_nodes=2604954447"
+      ]
+    },
+    {
+      "search_c_sha256": "293efe92a18693a4239462d52adc99939ca416fd519da0507645bc39ed5e2e0c",
+      "compile": "cc -std=c11 -O3 -march=native -Wall -Wextra -Werror -o search search.c",
+      "binary_sha256": "88f3a0d60a7feab698e71c4881fd3ca664bede2b2d1399418529c6a1f59eac95",
+      "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",
+      "command": "search c3c3e 4 6 sym 16 30",
+      "max_length": 10,
+      "started_utc": "2026-10-23T15:18:19Z",
+      "finished_utc": "2026-10-23T16:11:23Z",
+      "output": [
+        "target=c3c3e symmetries=36 first_letters=7 pairs=827 mode=sym",
+        "forward_depth=4 distinct=325910698",
+        "RESULT target=c3c3e max_length=10 shortest=-1 key_matches=72 backward_nodes=354865362444"
+      ]
+    }
+  ]
+}
diff --git a/research/three-register-three-cycles/SOURCES.json b/research/three-register-three-cycles/SOURCES.json
@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "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/swap-component-cut/README.md",
+      "usage": "provenance",
+      "git_blob": "19eaadc4ea40e312d202c917e2f1914d98ca224a",
+      "sha256": "7fe7efcb948a71af664d8f7828c8f4a056de3c6c3aa2cb82e420ec6ae7bd0106"
+    },
+    {
+      "path": "research/two-three-cycle-additivity/README.md",
+      "usage": "provenance",
+      "git_blob": "6bbd51f92adebdf1e5ca8141251cc35f5990af7c",
+      "sha256": "b292e40966b928f26b407ae5c59b4ed9b8d4687d28076efbc759a8afdf62cdfb"
+    },
+    {
+      "path": "research/gl3-order7-dirty-register-seed39ae/README.md",
+      "usage": "provenance",
+      "git_blob": "1dbb6772b4c2387fb81758426ad244eb54c65e62",
+      "sha256": "14e6ccf71e8dcdb95632bf03214ac70654016b7a33c80ba0724ee984b187be42"
+    },
+    {
+      "path": "research/three-cycle-address-floor/README.md",
+      "usage": "provenance",
+      "git_blob": "6a65c91f29e5b226cebd32d0c1d6963a60a98761",
+      "sha256": "a63c4ea4c874cac1fb064e1aff07f8ef791391eb795aec22a2154eb44a8fa81e"
+    }
+  ]
+}
diff --git a/research/three-register-three-cycles/TASK.json b/research/three-register-three-cycles/TASK.json
@@ -0,0 +1,64 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "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 how short a word for diag([c],[c],[e]) can be in M_3(F2[GL_3(F2)]): two coordinate 3-cycles with a third arbitrary dirty register restored exactly (the open question of research/two-three-cycle-additivity).",
+  "scope_change_reason": "PR #5005 settled R = 2 (exactly twelve). For swaps a dirty register provably does not help; for 3-cycles the R = 3 case was open. This package bounds it from below by exact search. It does not cover R >= 4, spectators (n >= 4) or other targets.",
+  "bottleneck_link": "A dirty register could save at most one of the twelve calls on two 3-cycles in this formal model; any larger saving needs a changed operation or tariff.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the exact length-10 exclusion with positive controls. Length 11 needs a depth-5 forward ball (about 4e10 states) or a new argument; record it as open.",
+  "outcome": "partial",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/three-register-three-cycles",
+  "author": "James Reed",
+  "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).",
+  "open_questions": [
+    {
+      "question": "Does a word of length exactly 11 realize diag([c],[c],[e]) at R = 3, or is the cost exactly twelve?",
+      "why_it_matters": "It decides whether a dirty register can make two 3-cycles share any paid work. Length <= 10 is excluded here. Parity cannot finish the case: calls 0, 28, 84, 0, 84 multiply to I, from the group relation C01 C02 C12 = C12 C01 on one register.",
+      "first_step": "Find a structural lemma that cuts the search: e.g. show that a length-11 word must leave register 2 untouched by some call position, reducing to the R = 2 result, or extend the support lemma of #4974 to two targets.",
+      "blocked_by": "Search size: the depth-5 forward ball has about 4e10 states; the depth-4 ball already has 325,910,698."
+    }
+  ]
+}
diff --git a/research/three-register-three-cycles/VERIFY.json b/research/three-register-three-cycles/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 with -std=c11 -Wall -Wextra -Werror; bind the C engine to the Python formal model at R = 3 on 36 random words by exact state comparison; engine self-test (33,600 batched fingerprints, 400 radius-two verifications) and 9,912 commuting pairs; distinct-state counts 169/22051/2705791; twelve-call attaining word and a length-five odd relation in Python; positive controls c3ee, c7c7e, s01s01e with and without symmetry (nothing at length <= 5, shortest 6); c3c3e: nothing at length <= 6 without symmetry and nothing at length <= 8 with symmetry (36 symmetries, 827 pair representatives). The length <= 9 and <= 10 runs are recorded local receipts in RESULT.json (verify.py --full), not replayed here."
+    }
+  ]
+}