Two coordinate 3-cycles cost twelve formal calls: exact search excludes length ≤ 11 (no new κ)

research/two-three-cycle-additivity/README.md

@@ -0,0 +1,115 @@
+# Two 3-cycles cost twelve calls
+
+**Exact computer-assisted result in a formal model. No new κ.**
+The selected conditional exponent stays 60403/20000000.
+
+## Result
+
+The setting is the formal model `M_2(F2[GL_3(F2)])` of #4939/#4950/#4968:
+
+- A paid call is `D(g,N) = I + ([g]+[e])N`, where `g` is one of the six
+  coordinate CNOTs and `N = uvᵀ` is a rank-one binary idempotent.
+- Free scalar `GL_2(F2)` maps are allowed.
+- Equality is formal, on arbitrary inputs.
+
+Let `c` be a coordinate 3-cycle. Then
+
+```text
+diag([c],[c]) has no realizing word of length ≤ 11, so its cost is exactly 12.
+```
+
+The upper bound 12 is a shortest 3-cycle word (length 6) on each register. So
+two 3-cycles share no paid work across the two registers: the cost is additive.
+
+This answers the open question of [#4968](https://github.com/CrocSwap/integer-mult-bounds/pull/4968)
+for its smallest case. #4974's support lemma gives exactly `ℓ_{GL_n}(g)` for a
+single target, but support alone only bounds the largest target. The
+permutation cuts of #4968 do not even certify a single 3-cycle; they reach
+about 3.5 of 6.
+
+## Method
+
+`search.c` is an exact meet-in-the-middle search. Free scalar maps are
+normalized away (#4939 step 1). Every paid call is an involution, so a word of
+length `L ≤ 11` gives `T·W = X`, with `X` a product of at most 5 calls and `W`
+of at most 6 calls. Consecutive equal letters cancel and are skipped.
+
+- **Forward.** A depth-first search from `I` to depth ≤ 5 stores a 61-bit
+  fingerprint with the minimum depth for each of the **16,292,362** distinct
+  states.
+- **Backward.** A depth-first search from `T` to depth ≤ 6 looks up every
+  state. Fingerprints are deterministic, so a real solution always matches its
+  key. A key match would be re-verified by an exact forward re-search. The
+  run records **zero key matches**, which excludes every word of length ≤ 11.
+- **Symmetry.** The target and the generator set are fixed by 36 maps:
+  entrywise automorphisms of `GL_3(F2)` that fix `c` (conjugation by powers of
+  `c`, optionally composed with inverse-transpose), times conjugation by
+  `GL_2(F2)` on the registers. These maps are algebra automorphisms that fix
+  `T`. If `T·W = X`, then `T·φ(W) = φ(X)`, and `φ(X)` lies in the same forward
+  ball. So the backward first letter can range over orbit representatives, and
+  here all 36 generators form one orbit. The search is also repeated **without
+  this reduction**, over all 36 first letters in parallel shards, again with
+  zero key matches.
+
+## Evidence
+
+`verify.py` uses the standard library and a C11 compiler. It takes about
+75 s locally with 9 parallel shards. 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`) on 84 random words of length
+   0–6, as exact group-algebra states.
+3. **State counts.** The distinct states at depth ≤ 1, 2, 3, 4 are 37, 1,033,
+   26,551 and 663,496, matching the Python search.
+4. **Positive controls.** `diag([c],[e])`, `diag([s01],[s12])` and
+   `diag([s01],[s01])` have nothing at length ≤ 5, and their shortest length 6
+   is found. The two swap cases match #4950/#4968.
+5. **Upper bound.** The 12-call attaining word is checked in Python.
+6. **Main search.** It runs with symmetry (36 symmetries, one orbit) and
+   without it (36 first letters). Both give zero key matches.
+
+Breaking the generator product in `search.c`, or perturbing the forward-ball
+count, makes the verifier fail.
+
+## 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` and `R = 2`. It does **not** settle:
+- a third dirty, restored register;
+- spectator address coordinates (`n ≥ 4`);
+- other multi-target cases, such as transposition paths or stars on four or
+  more coordinates;
+- native operations, tariffs or κ.
+
+Base: canonical main `f259dabc7d70e0db8d6d36bfda888f008bbfecc1`, priority
+revision 7.
+Claim: [#1166 comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19139334).
+
+## Reproduce
+
+```sh
+python3.12 -I -B research/two-three-cycle-additivity/verify.py
+python3.12 -B scripts/research_package.py --package research/two-three-cycle-additivity
+```
+
+## Open next questions
+
+1. **Does a dirty third register or a spectator coordinate let two 3-cycles
+   share work?** For swaps, neither helps. For 3-cycles, only `R = 2`, `n = 3`
+   is settled here. *First step:* run the same engine at `R = 3`, with 168
+   generators. First measure the growth of the ball and add symmetry under
+   register conjugation fixing `diag(c,c,e)`. *Blocked by:* search size only.
+
+## Credit
+
+- Mihir Srivastava (#4939), for the formal model.
+- JoyboyBrian (#4974), for the single-target support lemma.
+- PR1989, the GL2 corollary, commdata2338 (PR1414/PR1495), PR1541 and Gareth
+  Davidson (PR1333), as credited in #4950/#4968.
+
+Prepared by James Reed with substantial Anthropic Claude (Claude Code)
+assistance. Apache-2.0. No independent human review is claimed.

research/two-three-cycle-additivity/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1",
+  "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"
+    }
+  ]
+}

research/two-three-cycle-additivity/TASK.json

@@ -0,0 +1,64 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1",
+  "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 whether two coordinate 3-cycles, diag([c],[c]) at n = 3 with R = 2 registers, can be realized by fewer than twelve paid calls in the formal M_R(F2[GL_n(F2)]) model (the open question of PR #4968).",
+  "scope_change_reason": "PR #4968 (merged) left additivity across several non-transposition targets open; #4974 settled single targets via support. This package settles the smallest open multi-target case exactly. It does not cover extra dirty registers (R >= 3), address spectators (n >= 4) or other targets.",
+  "bottleneck_link": "It shows that two 3-cycles share no paid work across registers in this formal model, extending the swap results. Any saving needs a changed operation or tariff.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the exact length-11 exclusion with positive controls and a symmetry-free confirmation. Do not extend to R = 3 or n = 4 in this package.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/two-three-cycle-additivity",
+  "author": "James Reed",
+  "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).",
+  "open_questions": [
+    {
+      "question": "Does a third (dirty, restored) register or a spectator address coordinate let two 3-cycles share work, i.e. is diag([c],[c],[e]) at R = 3, or the same target at n = 4, still twelve?",
+      "why_it_matters": "For swaps, dirty registers and spectators provably do not help (#4950, #4968). For 3-cycles only the R = 2, n = 3 case is now settled; permutation cuts cannot certify it, so the general case needs a new argument.",
+      "first_step": "Run the same meet-in-the-middle engine at R = 3 (168 generators); the depth-5 ball is far larger, so first measure growth and add symmetry reduction under GL_3(F2) register conjugation fixing diag(c,c,e).",
+      "blocked_by": "Search size at R = 3; nothing else."
+    }
+  ]
+}

research/two-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 with -std=c11 -Wall -Wextra -Werror; bind the C engine to the Python formal model on 84 random words by exact state comparison; reproduce distinct-state counts 37/1033/26551/663496; positive controls c3e, s01s12, s01s01 (nothing at length <= 5, shortest 6); twelve-call attaining word in Python; main search for diag([c],[c]) at depth 5+6 with symmetry reduction (36 symmetries, one first-letter orbit, 16,292,362 forward states, zero key matches) and a symmetry-free confirmation over all 36 first letters in parallel shards with zero key matches."
+    }
+  ]
+}