Research: four-role mixed D8 target has exact five-call minimum

research/d8-mixed-target-seeda97c8e/README.md

@@ -0,0 +1,118 @@
+# Four-role mixed-target word in the order-eight dihedral model
+
+This package gives the exact minimum of five paid factors for one four-role
+target in a fixed nonabelian group-algebra model. It is a scoped finite-model
+result; it does not improve the selected integer-multiplication bound.
+
+## Model and result
+
+Let `G = <a,b | a^2=b^2=e, (ab)^4=e>` be the dihedral group of order eight,
+represented in the verifier by `a=(0 1)(2 3)` and `b=(1 2)`. Work over the
+full group algebra `F2[G]`. There are four scalar roles and a paid factor is
+
+```text
+D_(g,N) = I + ([g] + [e]) N,
+g in {a,b}, N = x y^T in M4(F2), x,y nonzero, y^T x = 1.
+```
+
+One paid factor costs one. The alphabet contains 120 rank-one idempotents and
+240 labeled factors. The target is
+
+```text
+diag([a], [ab], [ba], [e]).
+```
+
+The matrix identity acts on every arbitrary four-tuple of group-algebra
+register values. The fourth role is restored exactly. A direct word has five
+factors:
+
+```text
+D_(a,E00) D_(a,E11) D_(b,E11) D_(b,E22) D_(a,E22).
+```
+
+The first three roles receive `a`, `ab`, and `ba`; the fourth remains the
+identity. Because `ab != ba`, the order of the middle labels matters.
+
+**Result.** The exact minimum is five in this model. No word of at most four
+factors equals the target in `M4(F2[G])`.
+
+## Exact finite exclusion
+
+`verify.py` builds all eight group elements and the complete `F2[G]`
+convolution table. Each matrix entry is an eight-bit coefficient mask, so
+state equality checks every group coefficient exactly. It then enumerates all
+240 factors and all 57,600 ordered two-factor products, retaining 32,651
+distinct pair states.
+
+The checks cover every length up to four:
+
+- Lengths zero, one, and two are direct membership checks.
+- For length three, a first factor `A` must leave pair state `A*T`, since
+  every paid factor is an involution.
+- For length four, split `A B C D = T` into pairs. For each right pair
+  `Q=C D`, the left pair must be `T*Q^-1 = T*D*C`; exact pair-state lookup
+  decides whether such a word exists.
+
+This uses the complete declared alphabet and group algebra, not a bounded
+address sample. The search does not consider free inter-call `GL4(F2)` maps,
+other paid labels, extra roles, or a different target. The count of pair
+states alone is not used as the lower-bound argument; the verifier performs
+the target-specific membership tests above.
+
+The positive controls check the group presentation, the paid-factor
+involutions, and the five-factor word. Seven negative controls reject a
+non-idempotent matrix, ensure the reversed `ab`/`ba` word misses the target,
+and show each deletion from the displayed direct word changes the map.
+
+## Task, overlap, and limits
+
+- Track `bit-mechanisms`, task `bit-new-register-model`, seed
+  `a97c8efa02e2955139574300f12b9c03`, priority revision 3, exact base
+  `0b1cccf86e2f5132ed286a26ef0a681a495740ea`.
+- The selected-record SHA-256 is
+  `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`.
+- The first considered `F2[GL2(F2)]` scope was dropped after finding open
+  PR [#1763](https://github.com/CrocSwap/integer-mult-bounds/pull/1763), which
+  uses the same four-role factor alphabet and pair-state method for even
+  repeated order-three targets. This package changes the group relation to
+  `D8` and the target to one reflection, both orientations of an order-four
+  rotation, and one identity role.
+- D8 predecessor [#1742](https://github.com/CrocSwap/integer-mult-bounds/pull/1742),
+  by 1337isnot1337, proves an eight-call minimum for a three-role duplicated
+  central-commutator target. Its claim explicitly left four-role models open;
+  it does not include this target. The exact predecessor head is recorded in
+  `TASK.json`.
+- The fully charged local baseline is five paid factors, so the search tests
+  whether the heterogeneous target can be completed for four. Every role and
+  restoration is included. The model has no source access, helper hosting,
+  recursion, or arithmetic-supplier interface. No source occurrence, supplier
+  adoption, paid-moment change, or new kappa is claimed.
+- The selector's `research_baseline.py` first-step could not complete in this
+  sparse worktree because the selected certificate package inventory is not
+  materialized. The exact selected-record pin and the new package replay do
+  run here; the failed orientation attempt is not counted as a pass.
+
+The work was prepared with substantial OpenAI Codex assistance. No independent
+human review is claimed. No predecessor executable is imported.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/d8-mixed-target-seeda97c8e
+```
+
+Expected marker:
+
+```text
+PASS_D8_MIXED_TARGET min=5 roles=4 group_order=8 generators=2 idempotents=120 factors=240 pair_states=32651 words_le4=0 controls=7 no_new_kappa
+PASS_REGISTERED_RESEARCH_PACKAGE research/d8-mixed-target-seeda97c8e outcome=negative-result
+```
+
+## Open next questions
+
+Can this four-role D8 operation alphabet be mapped onto an actual bit or
+integer-multiplication supplier primitive so its exact factor cost affects a
+paid moment? It matters only if the labels and rank-one role updates occur in
+a realizable source interval. The first step is to identify one source-pinned
+supplier word with `a` and `b` as its paid labels; no such mapping is known,
+so this result alone does not justify supplier replay or a kappa claim.

research/d8-mixed-target-seeda97c8e/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "files": [
+    {
+      "path": "autoresearch.md",
+      "usage": "input",
+      "git_blob": "8d5403e0f10f68a61d0cb9294fa2e83e872d1d82",
+      "sha256": "215b3222f6a943edc69422a28ac21ea1f397ddf54770f1d87ac4195385d73699"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "input",
+      "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1",
+      "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"
+    },
+    {
+      "path": "docs/research/current-status.md",
+      "usage": "input",
+      "git_blob": "d73b4ff9da41f044e793422db4318be17e234a6c",
+      "sha256": "adb54af005eb11edaf84d782fe729338680ff908f6d4fbf39ba1062d2e7d8a77"
+    },
+    {
+      "path": "research/bit-three-register-lower-bound/README.md",
+      "usage": "input",
+      "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79",
+      "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"
+    }
+  ]
+}

research/d8-mixed-target-seeda97c8e/TASK.json

@@ -0,0 +1,87 @@
+{
+  "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": "Four scalar roles over F2[D8], paid labels the two involutions a,b, all 120 binary rank-one idempotents, and target diag([a],[ab],[ba],[e]); exact minimum paid length five.",
+  "scope_change_reason": "The initially considered GL2(F2) four-role alphabet overlaps open PR #1763, which uses the same pair-state method for repeated order-three targets. The single bounded pivot changes the group to D8 and tests a heterogeneous reflection/order-four target; D8 PR #1742 covers a different three-role central-commutator target and states that four-role models remain open.",
+  "bottleneck_link": "A four-factor identity would reduce this target's paid bit-word cost from five; supplier adoption still requires an actual source-word occurrence.",
+  "budget_minutes": 60,
+  "stop_rule": "Enumerate every word of length at most four using exact full F2[D8] matrix products and verify the explicit five-factor upper word; stop after all pair-state meetings and controls.",
+  "outcome": "negative-result",
+  "evidence": "verify.py: exact eight-element group algebra, all 240 factors, 32,651 ordered pair states, no word of length at most four, direct five-factor word and seven controls.",
+  "author": "Cinna Davis, with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no independent human review is claimed.",
+  "open_questions": [
+    {
+      "question": "Can this four-role D8 operation alphabet be mapped onto an actual bit or integer-multiplication supplier primitive?",
+      "why_it_matters": "Only a realized source interval can change a paid supplier moment or support a kappa claim.",
+      "first_step": "Locate a source-pinned supplier word whose paid labels implement the D8 generators a and b.",
+      "blocked_by": "No source occurrence or supplier mapping is currently known."
+    }
+  ],
+  "seed": "a97c8efa02e2955139574300f12b9c03",
+  "rejected_seeds": [
+    "d5391c9d7dbe6d52989e58edf8243ee4",
+    "6a643449cb3597d8eec7dca52107ceec"
+  ],
+  "scope_key": "7f5f4426ef796683c485",
+  "catalogue_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075",
+  "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
+  "predecessors": [
+    {
+      "reference": "https://github.com/CrocSwap/integer-mult-bounds/pull/1742",
+      "head": "679f3624a0a41ed14942825dd7f413132412d1e3",
+      "author": "1337isnot1337",
+      "scope": "Three-role D8 duplicated central-commutator target; exact minimum eight."
+    },
+    {
+      "reference": "https://github.com/CrocSwap/integer-mult-bounds/pull/1763",
+      "head": "07910c7bee862dadbb3b3d30ea5dfcdbbbe23fda",
+      "author": "Aaron Wang with opencode assistance",
+      "scope": "Four-role GL2(F2) even repeated order-three targets; the initial candidate was dropped for overlap."
+    }
+  ],
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1773",
+  "overlap_snapshot_utc": "2026-10-14T09:25:09Z",
+  "open_pr_count_at_snapshot": 442,
+  "latest_open_pr_at_snapshot": 1772,
+  "claim_expiry_utc": "2026-10-14T11:30:00Z"
+}

research/d8-mixed-target-seeda97c8e/VERIFY.json

@@ -0,0 +1,26 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "autoresearch.md",
+    "certificates/selected-result.json",
+    "docs/research/agent-task-catalog.json",
+    "docs/research/current-status.md",
+    "research/bit-three-register-lower-bound/README.md",
+    "research/d8-mixed-target-seeda97c8e/verify.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Full F2[D8] exact arithmetic; all 240 paid factors and 32,651 pair states; excludes target words through length four; verifies the direct length-five word and seven controls."
+    }
+  ]
+}