Prove a fourth dirty role keeps the S3 xyx double at six calls (no new κ)

research/s3-xyx-four-role-minimum/README.md

@@ -0,0 +1,107 @@
+# A fourth dirty role does not lower the S3 xyx double minimum
+
+**Finite exact minimum. No new κ.** The selected record is unchanged.
+
+## Result
+
+In `M4(F2[S3])`, with paid labels `x = (1 2)`, `y = (2 3)` and calls
+
+```text
+D_N(g) = I + ([g] + [e]) N,    g in {x, y},
+```
+
+where `N` ranges over all 120 rank-one idempotents of `M4(F2)`, the target
+
+```text
+diag([xyx], [xyx], [e], [e])
+```
+
+needs exactly **six** paid calls. Roles 2 and 3 are arbitrary dirty roles that
+must be returned unchanged. No word of length at most five over the 240 paid
+factors equals the target. The direct word `x y x` on role 0 followed by
+`x y x` on role 1 attains six.
+
+This answers open question 1 of Wentao Li's
+[PR #4084](https://github.com/CrocSwap/integer-mult-bounds/pull/4084)
+([`research/s3-three-role-xyx`](../s3-three-role-xyx/README.md)), which proves
+the same minimum with three roles. The answer is no: a fourth restored dirty
+role does not save a call. The statement covers four roles only.
+
+## Method
+
+`Phi : F2[S3] -> M2(F2) x F2[C2]` sends `[g]` to `(rho(g), c^sign(g))`, where
+`rho` is the action of `S3` on the three nonzero vectors of `F2^2`. The
+verifier checks that `rho` and `sign` are homomorphisms and that `Phi` is
+bijective on the six basis elements, so `Phi` is an algebra isomorphism and
+acts entrywise on `M4`. In the `C2` block every paid factor is `I + delta N`
+with `delta = c + 1` and `delta^2 = 0`, so a word maps to
+`I + delta * (sum of its N)`. In the `M2` block a paid factor is a transvection
+of `F2^8` with rank-one difference `(u (x) p)(v (x) q)^T`.
+
+Each paid factor is an involution, so the inverse of a word is the reversed
+word. The target has a word of length at most five exactly when
+`ball(I,3)` meets `T * ball(I,2)`. The verifier builds `ball(I,2)`
+(layers `1, 240, 32650`), forms `T * ball(I,2)`, and tests every element of
+`ball(I,2)` and every one-call extension. There are zero hits. The `M8(F2)`
+image alone already has zero hits, so the `C2` block is not needed for this
+target.
+
+## Controls
+
+- Three-role calibration: the same engine gives ball layers
+  `[1, 56, 1750, 45396]`, equal to the pinned
+  [PR #4084 certificate](../s3-three-role-xyx/CERTIFICATE.json). This checks
+  the encoding against a fully different implementation; it is not a new check
+  of that result.
+- An independent engine multiplies directly in `M4(F2[S3])`. Its `ball(I,2)`
+  maps under `Phi` to exactly the fast engine's set of 32,891 states.
+- Every paid factor squares to the identity in both engines.
+- Positive controls: the same search finds words of length at most five for
+  `diag([xyx],[xy],[e],[e])` and `diag([x],[y],[xy],[e])`, whose direct
+  words have lengths 5 and 4.
+- The direct six-call word equals the target in `M4(F2[S3])`. Each of its six
+  one-call omissions does not.
+
+## Reproduce
+
+From the repository root, Python 3.12, standard library only:
+
+```sh
+python3.12 -I -B research/s3-xyx-four-role-minimum/verify.py
+python3.12 -I -O -B research/s3-xyx-four-role-minimum/verify.py
+python3.12 -B scripts/research_package.py --package research/s3-xyx-four-role-minimum
+```
+
+Each direct run prints `PASS_S3_XYX_FOUR_ROLE ... short_hits=0
+rho_quotient_hits=0 direct=6 target_minimum=6` in about 11 seconds.
+
+## Scope and limits
+
+This is a finite exact minimum for one target, four roles and the stated
+optimistic unit-cost alphabet. It does not cover five or more roles, other
+`S3` targets, free address maps, native source generation, hosting, or any
+supplier price. No κ, selected result or multiplication theorem changes.
+
+## Open next questions
+
+1. Does a fifth or any larger number of restored dirty roles lower the
+   six-call minimum? Three and four roles give six, and a uniform answer would
+   close the workspace question for this target. A first step is a uniform
+   argument in the `M_{2m}(F2)` block, where the restricted transvections
+   already exclude length five at four roles. Five roles have 992 factors, so
+   `ball(I,2)` has up to about `5 x 10^5` states (an estimate, not computed),
+   which is slow for this pure-Python search.
+2. Is the `rho` quotient enough for every role count? At four roles the
+   `M8(F2)` image alone excludes length five. Characterizing products of at
+   most five such transvections that act as the partial swap on two coordinate
+   planes would give a cleaner certificate. Only the four-role observation is
+   available here.
+
+## Credit
+
+The target, alphabet, three-role minimum and this open question are from
+Wentao Li / VictorLiwentao's PR #4084. The alphabet lineage includes Cinna
+Davis's two-register `S3` census
+([`research/bit-s3-two-target-census-seed36501`](../bit-s3-two-target-census-seed36501/README.md))
+and the two-dimensional representation bound of PR #3893. The four-role
+search, its controls and this note were produced by Nick Petalas. Apache-2.0.

research/s3-xyx-four-role-minimum/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/s3-three-role-xyx/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "33597da093477b22ab19077625950b97e3bcb0b5",
+      "sha256": "e19387a1c6e385a85c537a28a81dd8eb65af782573dfc1794402461330ff05d7"
+    }
+  ]
+}

research/s3-xyx-four-role-minimum/TASK.json

@@ -0,0 +1,84 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "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": "refined",
+  "actual_scope": "Exact paid-call minimum for diag([xyx],[xyx],[e],[e]) in M4(F2[S3]) with two restored dirty scalar roles, paid labels {x,y} and all 120 rank-one idempotents of M4(F2). Answers open question 1 of research/s3-three-role-xyx (PR #4084): a fourth role does not lower the six-call minimum.",
+  "scope_change_reason": "The card asks whether a larger or nonabelian register model escapes the three-register obstruction. This package fixes the nonabelian S3 alphabet of PR #4084 and increases the dirty role count from three to four for its one target; it is a finite exact minimum, not a new operation alphabet or a supplier.",
+  "bottleneck_link": "Side result for the bit register model: tests whether more restored dirty workspace compresses one nonabelian S3 target. A shorter word would still need a native supplier map before any kappa consequence; none is claimed.",
+  "budget_minutes": 60,
+  "stop_rule": "Exclude every word of length 0..5 over the 240 paid factors by exact involution meet-in-the-middle, verify the direct six-call word, calibrate the engine on the three-role layer sizes and stop. Do not extend to five roles or other targets.",
+  "outcome": "completed",
+  "evidence": "verify.py: Phi = (rho, sign) is checked to be an algebra isomorphism F2[S3] -> M2(F2) x F2[C2]; three-role ball layers [1,56,1750,45396] match the pinned PR #4084 certificate; four-role ball(I,2) layers [1,240,32650] agree with an independent M4(F2[S3]) engine under Phi; zero hits for ball(I,3) cap T*ball(I,2); length-4 and length-5 positive controls hit; direct six-call word exact, each one-call omission misses.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does a fifth or any larger number of restored dirty roles lower the six-call minimum for diag([xyx],[xyx],[e],...)?",
+      "why_it_matters": "Three and four roles give six; a uniform statement for every role count would close the workspace question for this target.",
+      "first_step": "Try a uniform argument in the M_{2m}(F2) rho block, where the search shows four roles already need six calls; the transvections there have the restricted shapes (u(x)p)(v(x)q)^T.",
+      "blocked_by": "Five roles give 992 factors and a ball(I,2) of up to about 5 x 10^5 states (estimate, not computed), which is slow for this pure-Python meet-in-the-middle; no uniform proof is known."
+    },
+    {
+      "question": "Is the rho quotient alone enough for every role count?",
+      "why_it_matters": "At four roles the M8(F2) image already has no length-5 hit, so the C2 block is not needed; a proof in GL_{2m}(F2) would be a cleaner certificate.",
+      "first_step": "Characterize products of at most five restricted transvections that act as the partial swap on two coordinate planes.",
+      "blocked_by": "Only a finite four-role observation is available."
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 4084,
+      "credit": "Wentao Li / VictorLiwentao; target, alphabet, three-role six-call minimum and this open question"
+    },
+    {
+      "ref": "research/bit-s3-two-target-census-seed36501",
+      "credit": "Cinna Davis; two-register S3 no-sharing census and alphabet lineage"
+    },
+    {
+      "pr": 3893,
+      "credit": "two-dimensional representation rank bound for this S3 alphabet"
+    }
+  ]
+}

research/s3-xyx-four-role-minimum/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/s3-three-role-xyx/CERTIFICATE.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Isomorphism check, three-role calibration against the pinned PR #4084 layers, independent M4(F2[S3]) ball(I,2) under Phi, zero length<=5 meet-in-the-middle hits, positive length-4/5 controls, direct witness and omission controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Same checks under -O; admission uses need(), not assert."
+    }
+  ]
+}