Research: sharp eight-call UT4 noncentral pair with arbitrary dirty workspace

research/ut4-noncentral-shared-middle/README.md

@@ -0,0 +1,260 @@
+# Disjoint UT4 root targets cannot share the middle-generator bill
+
+**Sharp formal-algebra theorem; no new supplier or kappa.** For `p` target
+roles carrying `u=I+E13` and `q` different roles carrying `v=I+E24`, in the
+restricted `UT4(F2)` alphabet below, every word pays
+
+```
+n_x >= 2p,   n_y >= 2(p+q),   n_z >= 2q.
+```
+
+The direct `4(p+q)`-call word attains all three bounds simultaneously, for
+every finite `r>=p+q>0`. All extra roles may contain arbitrary dirty inputs
+and must be restored. The result includes every nonzero binary rank-one
+scalar coupling, both idempotent and nilpotent, and arbitrary free scalar
+mixing. Thus nonnegative uniform label prices `alpha,beta,gamma` give the
+exact tariff `2p alpha + 2(p+q) beta + 2q gamma` in this model.
+
+In particular, **the minimum in Cinna Davis's [PR1761](https://github.com/CrocSwap/integer-mult-bounds/pull/1761)
+is eight**, not five, six or seven. That predecessor proves a four-register
+length-at-most-four exclusion and gives the eight-call upper witness. This
+successor closes its explicit gap by a written all-register argument, not a
+larger finite search. It does not claim the predecessor's construction or
+bounded exclusion as new.
+
+## Model and complete formal bill
+
+Use one-based address indices and let
+
+```
+G = UT4(F2),   R = F2[G],
+x = I+E12,   y = I+E23,   z = I+E34,
+u = xyxy = I+E13,   v = yzyz = I+E24.
+```
+
+The roots `u,v` are noncentral: `[u,z]=[x,v]=I+E14`. The group has 64
+elements. Equality below is equality in the **full formal group algebra**,
+not equality only in a natural representation or on one small address set.
+For scalar register count `r`, an allowed paid factor is
+
+```
+D_N(g) = I_r + ([g]+1)N,
+g in {x,y,z},   N=a b^T != 0,   a,b in F2^r.
+```
+
+There is no restriction on `b^T a`. Since `g` is an involution,
+`([g]+1)^2=0`, so every paid factor squares to identity even when `N` is
+nilpotent. All inverses are charged occurrences, not free undo. All scalar
+register inputs are arbitrary; the target is
+
+```
+T = diag([u] repeated p, [v] repeated q, [1] repeated r-p-q).
+```
+
+Free operations are scalar `GL_r(F2)` maps only. Move them to one end by
+conjugating the `N`s; rank one is preserved. Augmentation `[g] -> 1` sends
+every paid factor and `T` to identity, forcing that final scalar map to
+identity. The displayed alphabet therefore includes every normalized word.
+This standard normalization is credited to the preceding register-model work.
+No free address map, clean allocation, COPY, ERASE or higher-rank paid call
+is permitted.
+
+The upper word applies `x,y,x,y` on each `u` coordinate and `y,z,y,z` on each
+`v` coordinate, with coordinate-projector couplings. Each four-call product
+is exactly its formal group monomial; different scalar roles do not interact.
+It uses `p+q` data roles, no additional workspace or scalar preparation, and
+exactly `2p,2(p+q),2q` calls; appended dirty roles stay identity. No restoration
+outside this word is omitted.
+
+This is a **complete abstract paid-call bill**, not a physical supplier
+invoice. Frames, common labels, hosting, precision/tape and recursive
+interfaces have not been realized. Their costs are not declared zero. No
+selected paid profile, moment or multiplication exponent is improved.
+
+## Proof: the simultaneous middle span, not two added bounds
+
+All ranks and scalar spans are over `F2`. Let
+`P=diag(I_p,0,0)` and `Q=diag(0,I_q,0)` in `M_r(F2)`. Their column spaces
+are disjoint of dimensions `p,q`; their row spaces are likewise disjoint.
+Write products in **left-to-right matrix order**. For labels `a,b` define
+
+```
+S_a  = sum_{i: g_i=a} N_i,
+C_ab = sum_{i<j: g_i=a,g_j=b} N_i N_j.
+```
+
+### Two necessary group representations
+
+Apply the natural representation `rho(g)=g` entrywise and group coordinates
+into four address blocks of size `r`. The `(1,2),(2,3),(3,4)` blocks of the
+product are `S_x,S_y,S_z`, respectively. The `(1,3),(2,4)` blocks are
+`C_xy,C_yz`. No term of degree three can enter either of those two blocks.
+The formal target consequently forces
+
+```
+S_x = S_y = S_z = 0,     C_xy = P,     C_yz = Q.       (1)
+```
+
+Use also the contragredient representation
+`rho_dual(g)=(g^-1)^T`. It is a homomorphism because inverse and transpose
+each reverse multiplication. Since the three generators are involutions,
+their images are `I+E21,I+E32,I+E43`. The target roots are involutions too,
+with images `I+E31,I+E42`. Reading the `(3,1),(4,2)` blocks gives
+
+```
+C_yx = P,     C_zy = Q.                               (2)
+```
+
+The inverse is essential: transpose alone would be an antihomomorphism.
+These representations are used **only for necessary lower-bound
+conditions**. They cannot certify a formal endpoint; the verifier includes
+a nonzero formal perturbation annihilated by both.
+
+### One rank-nullity argument for the shared label
+
+For a label `a`, write all its rank-one matrices as `N_i=a_i b_i^T` and
+collect
+
+```
+X_a = (a_i)_i,      Y_a = (b_i^T)_i.
+```
+
+Thus `X_a` has `n_a` columns, `Y_a` has `n_a` rows, and
+`X_a Y_a = S_a = 0`. Rank-nullity in the intermediate `F2^{n_a}` yields
+
+```
+rank X_a + rank Y_a <= n_a.                           (3)
+```
+
+Each summand in `C_ab` has column space in `im X_a` and row space in
+`row Y_b`. Therefore (1) and (2) force these inclusions:
+
+| Scalar span | Required target subspaces |
+| --- | --- |
+| `im X_x`, `row Y_x` | respectively `im P`, `row P` |
+| `im X_z`, `row Y_z` | respectively `im Q`, `row Q` |
+| `im X_y` | **both** `im P` (from `C_yx`) and `im Q` (from `C_yz`) |
+| `row Y_y` | **both** `row P` (from `C_xy`) and `row Q` (from `C_zy`) |
+
+The last two lines are the new shared-middle step. A single `X_y` must
+contain the **sum** `im P + im Q`, of dimension `p+q`, and a single `Y_y`
+must contain the analogous row-space sum. It is not legitimate merely to
+add two separate estimates on the same calls. Applying (3) instead gives
+
+```
+n_x >= p+p,     n_y >= (p+q)+(p+q),     n_z >= q+q.
+```
+
+The explicit upper word attains every bound. This proves the theorem for
+all finite register counts and word lengths, including arbitrary dirty
+workspace, without an exhaustive search or an unquantified extrapolation.
+Scalar conjugation preserves the direct-sum dimensions, so the same proof
+also applies to a simultaneous scalar conjugate of the target.
+
+### Why the disjoint-role hypothesis matters
+
+Putting both root actions on **one** role is a different endpoint:
+`[uv]`, not `diag([u],[v])`. In fact the full formal identity
+
+```
+xyzxyz = uv
+```
+
+costs only six calls and two middle calls. Its two root coefficients occupy
+the same scalar subspace, of dimension one rather than two. This is a
+positive countercontrol to dropping disjointness, not an improvement on the
+stated two-role target. In contrast, `xzyxzy` also has the desired degree-two
+coefficients but acquires the nontrivial `E14` term. The verifier distinguishes
+these endpoints in the full algebra.
+
+## Executable evidence and reproduction
+
+The package's standard-library checker uses exact binary arithmetic. Its
+primary representation is a scalar matrix of 64-bit formal coefficient
+vectors. A second engine uses literal binary 4-by-4 address matrices and
+replays the faithful left-regular action on **every** address/register basis
+column, including dirty workspace. It imports no primary arithmetic.
+
+Finite controls corroborate the proof and implementation; they do not prove
+the unbounded theorem. `CERTIFICATE.json` records the complete deterministic
+finite coverage. `VALIDATION.json` records only commands actually exercised.
+
+The deterministic evidence contains:
+
+| Check | Exact exercised domain |
+| --- | --- |
+| Group law and contragredient homomorphism | All 4,096 ordered group pairs each |
+| Expanded rank-one alphabet | 284 matrices at `r=1,2,3,4`: 155 idempotents, 129 nilpotents |
+| Involutions and faithful single-call action | 852 calls; 204,672 regular basis columns |
+| Coefficient recurrence and span inclusions | All 20,440 two-register words of length `0..3` over 27 factors |
+| Attaining formal/faithful witnesses | 34 fixtures through eight roles; 8,896 dirty basis columns, including two non-coordinate scalar conjugates |
+| Semantic controls | 18: eight omitted calls, wrong label, dirty restoration, rank/label/type violations, a genuine rank-two shortcut, common representation kernel, overlapping targets, and wrong class-three term |
+
+The coefficient census has lengths `1,27,729,19683`; its canonical coefficient
+digest is `b94b89bf4f84879a0dd3c7b55a553b7eeaf553855dcba33d702db719832783f8`.
+It is not a search excluding lengths five through seven: the written span
+proof excludes those lengths and all other short words uniformly.
+The verifier recomputes and compares the complete certificate, read-only by
+default; `--emit` prints it without modifying files. All semantic guards
+remain active under `-O`.
+
+From the repository root:
+
+```sh
+uv run --python 3.12 --no-project python -I -O -B research/ut4-noncentral-shared-middle/verify.py
+uv run --python 3.12 --no-project python -I -B scripts/research_package.py --package research/ut4-noncentral-shared-middle
+```
+
+The card's working example `scripts/research_baseline.py` returned
+`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`, with the complex primitive binding.
+That checks selected source bindings and arithmetic, **not** the selected
+cold replay. No native supplier, all-size realization, Lean, independent
+human proof review or hosted CI pass is claimed.
+
+## Provenance, novelty and attribution
+
+Exact base: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. One unforced chooser
+invocation sampled OS nonce `5080ba3917adb12fda1e688c38733a49`, selecting
+`bit-mechanisms`; [SELECTION.json](SELECTION.json) preserves the entire emitted
+record. [TASK.json](TASK.json) records the two proposed cards, actual refined
+scope, cost screen, stopping rule, overlap coverage and claim. The public
+[successor claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1759#discussioncomment-18925851)
+links the [round coordination thread](https://github.com/CrocSwap/integer-mult-bounds/discussions/1929).
+
+- **Cinna Davis (@1337isnot1337), PR1761**, head
+  `0f4f6d79b14573116e47d31d012f8e3f7a49cd87`: exact noncentral pair,
+  four-register `q<=4` exclusion, eight-call upper word and explicit gap.
+- **steph4n-gh, PR1573**, head `0b8c5a69297c794f2de22c04494c83e41300ae36`:
+  UT3 all-register theorem using two representations and zero-sum scalar
+  rank-nullity. Those tools, rather than their reinvention, are used here.
+- **Arham Tahir, PR1589**, head `010ec8c01c0edbbb08b541be236ab78d096f2ca1`:
+  UT3 nilpotent rank-one extension and mixed-coefficient proof.
+- PR1662/1680/1690/1816 treat the **central E14 target**, a different
+  class-three constraint. This proof neither replays nor settles their claims.
+- Credit @woklerx's PR1443, @juper997's PR1478, Gareth Davidson/@bitplane's
+  PR1333, and the eumemic/Ali Romman/David Govea register-model lineage.
+
+[SOURCES.json](SOURCES.json) pins source provenance and contextual predecessor
+heads. No predecessor code is imported, frozen evidence is unchanged, and
+no selected-frontier file is edited. Cached overlap covers 579 open PRs and
+547 discussion records with complete pagination, plus local notes; exact
+relevant heads were read live. This is not a claim of literature priority or
+a novelty guarantee from search absence. The new result is the simultaneous
+shared-middle obstruction and exact resolution of the existing noncentral
+pair gap, not a second presentation of the UT3 theorem.
+
+## Open next questions
+
+Can an actual bit-supplier implementation realize this restricted nonabelian
+alphabet at a favorable **complete** tariff and with the needed target
+interface? The first useful step is one explicit realized `x,y,z` call family,
+with every frame transition, dirty-state restoration and recursive/precision
+charge counted. The absence of such a realization blocks a supplier claim;
+more dirty registers or a longer search in the current disjoint-root model
+cannot lower the proved abstract bill. A formally cheaper enlarged primitive
+must be priced rather than simply assigned unit cost.
+
+Prepared for **Adam Gall** with substantial **OpenAI Codex GPT-6 Astra**
+assistance in research, proof, implementation and writing. The two executable
+representations are AI-assisted work from the same session, not independent
+human review. New work is Apache-2.0; predecessor notices remain unchanged.

research/ut4-noncentral-shared-middle/SELECTION.json

@@ -0,0 +1,60 @@
+{
+  "seed": "5080ba3917adb12fda1e688c38733a49",
+  "track": "bit-mechanisms",
+  "suggestions": [
+    {
+      "task_id": "bit-new-register-model",
+      "scope_key": "7f5f4426ef796683c485",
+      "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+      "method": "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "starting_points": ["research/bit-three-register-lower-bound/README.md", "certificates/selected-result.json"],
+      "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_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance."
+    },
+    {
+      "task_id": "bit-helper-contract",
+      "scope_key": "3475f46c8358c6a9211b",
+      "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?",
+      "method": "Derive a replacement interface lemma and price its implementation.",
+      "starting_points": ["research/r439-bsection-stars-seed01/README.md", "research/r439-copy-path-sharing-barrier/README.md"],
+      "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.",
+      "first_step": {
+        "command": ["python3", "-B", "research/r439-bsection-stars-seed01/verify.py"],
+        "expected": "PASS_R439_BSECTION_STARS",
+        "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.",
+        "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+      },
+      "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.",
+      "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.",
+      "allowed_variations": ["Choose one helper-star or quartet instance; narrow to one boundary implication."],
+      "scope_change_triggers": ["Changing only source count or scalar addition count without an interface argument."],
+      "overlap_terms": ["H2_D_frame0_targets_from_helpers", "K_equals_D", "helper-star"],
+      "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance."
+    }
+  ],
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "catalog_assessed_on": "2026-10-13",
+  "priority_revision": 3,
+  "priority_log": "docs/research/research-priority-log.md",
+  "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075",
+  "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
+  "selected": {
+    "kappa": "836330098538459/500000000000000000",
+    "review": "docs/research/community-batch1099-review.md",
+    "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json",
+    "reproduce": "make frontier1094-verify"
+  },
+  "status": "SUGGESTIONS_ONLY_NOT_RESERVED",
+  "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty."
+}

research/ut4-noncentral-shared-middle/SOURCES.json

@@ -0,0 +1,53 @@
+{
+  "schema_version": 1,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1",
+      "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"
+    },
+    {
+      "path": "research/bit-three-register-lower-bound/README.md",
+      "usage": "input",
+      "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79",
+      "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"
+    }
+  ],
+  "remote_context": [
+    {
+      "pr": 1761,
+      "commit": "0f4f6d79b14573116e47d31d012f8e3f7a49cd87",
+      "path": "research/ut4-noncentral-commutator-seedbfe59/README.md",
+      "author": "Cinna Davis (@1337isnot1337)",
+      "git_blob": "a3de0db4b4e8ed4be897f64ec4d55917fc240539",
+      "sha256": "d78bcf3d757587b69b486b191747f0f9590cddb0136c272edd479b3ce885ed32",
+      "usage": "Context and open gap; no executable dependency or imported proof premise."
+    },
+    {
+      "pr": 1573,
+      "commit": "0b8c5a69297c794f2de22c04494c83e41300ae36",
+      "path": "research/ut3-commutator-all-registers/README.md",
+      "author": "steph4n-gh",
+      "git_blob": "4a6a4ee9d995818348b3b853a95500dcce81228d",
+      "sha256": "fdd5405da1c0535a407013f2a4628a07dae4957fd9fb776cd14f05315d1aa26b",
+      "usage": "Credited zero-sum rank-nullity and representation method; proof restated for the new target."
+    },
+    {
+      "pr": 1589,
+      "commit": "010ec8c01c0edbbb08b541be236ab78d096f2ca1",
+      "path": "research/ut3-two-targets-any-registers/README.md",
+      "author": "Arham Tahir",
+      "git_blob": "3fc4f569a2e9bc81a1f61bc8343a276671a2d13f",
+      "sha256": "f879e3009b1fd5c625480ef92bdc454030ae62e7b378af7869e188df718e7399",
+      "usage": "Credited nilpotent rank-one extension; no imported implementation."
+    }
+  ]
+}