Research: no two-target UT4 central word has n_b=6 (n_b=7 open; no new kappa)

research/ut4-two-target-no-six-b/CERTIFICATE.json

@@ -0,0 +1,14 @@
+{
+  "active_roles": 2,
+  "canonical_zero_sum_middles": 5582,
+  "key_pairs_abc_cba_I": 0,
+  "keys_sum": 1568064,
+  "low_rank_excluded": 182,
+  "max_keys_per_middle": 1408,
+  "n_b": 6,
+  "rank_XY_at_least_2": 5400,
+  "schema_version": 1,
+  "side_zero_key_joins": 12544512,
+  "status": "no_nb6_two_target_quotient",
+  "targets": 2
+}

research/ut4-two-target-no-six-b/PROOF.md

@@ -0,0 +1,129 @@
+# No two-target UT4 central word has n_b = 6
+
+In the formal group-algebra model of
+[CrocSwap/integer-mult-bounds#1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662),
+every legal word realizing two central targets satisfies `n_b >= 6`. This note
+proves the complementary statement:
+
+> No legal word equal to `I+([z]+1)I_2`, of any finite length and on any finite
+> restored dirty workspace, has exactly six paid `b` factors.
+
+The case `n_b = 7` is left open. There is no new κ; the selected decimal
+`0.001672660197076918` is unchanged.
+
+## 1. Model and inherited rank bound
+
+Let `G = UT4(F2)` with `a = I+E12`, `b = I+E23`, `c = I+E34`, `z = I+E14`, and
+work in `R = F2[G]`. On `r >= 2` roles a paid factor is
+`I + ([g]+1) x y^T` with `g in {a,b,c}` and `x y^T` a nonzero binary rank-one
+coupling (idempotent or nilpotent). The target is `T = I + ([z]+1) P` with
+`P = diag(I_2, 0_(r-2))`. Scalar `GL_r(F2)` mixing is free and normalized into
+the couplings; every occurrence, including restoration, is counted.
+
+Use the fixed 17-dimensional quotient
+
+```
+Q = F2<a,b,c>/(a^2,b^2,c^2,ac-ca, deg >= 4)
+```
+
+of #1662, with `z |-> 1+abc+acb+bac+cba`. Necessary conditions on a realizing
+word include vanishing of all degree-1/2 and non-target degree-3 coefficients
+in `Mat_r(Q)`, and coefficient `P` on `abc, acb, bac, cba`.
+
+Write `B_j = x_j y_j^T` for the six middle couplings in product order, and set
+
+```
+X = [x_j] (r x 6),   Y = [y_j^T] (6 x r).
+```
+
+#1662 gives `XY = 0` and `n_b >= 2 + rank X + rank Y` from the factorization of
+`UV` through `ker X / im Y`, together with `rank X, rank Y >= 2` from the `bac`
+and `acb` coefficients. At `n_b = 6` this forces
+
+```
+rank X = rank Y = 2.
+```
+
+In particular every middle coupling is supported on a fixed 2-dimensional
+active plane `H` (after a free `GL_r` change of basis that places `P` in the
+leading block). Write `e_b^x = e_b^y = 0` for this vanishing middle excess.
+
+## 2. Reduction to two active roles
+
+With all six `b`-couplings in `H x H`, an interior dirty contraction
+`v_i(u_{i+1})` in a degree-`<=3` product can involve only `a` and `c` calls:
+any factor that is a `b` call has zero dirty row and column, so contractions
+against `b` see only the active block. Same-label dirty contractions between
+two `a` calls (resp. two `c` calls) vanish in `R` because `([a]+1)^2 = 0`
+(resp. `([c]+1)^2 = 0`).
+
+Consequently the monomials that use only `{a,b}` or only `{c,b}`, and the
+cross monomials `abc` and `cba` (which never place `a` adjacent to `c`),
+receive no interior dirty contribution. Their active `H x H` blocks are
+exactly the two-role coefficients computed from:
+
+- the six active middle couplings (a zero-sum sequence in the nine nonzero
+  rank-one `2 x 2` matrices);
+- the active prefix sums `P_j` of `a`-couplings before each middle call;
+- the active suffix sums `Q_j` of `c`-couplings after each middle call.
+
+Unrestricted outer length means every 6-tuple of `2 x 2` matrices arises as
+such a profile for some finite `n_a` (resp. `n_c`): each gap increment has
+rank at most two and is a sum of at most two rank-one couplings.
+
+Therefore a realizing word with `n_b = 6` on any `r >= 2` yields a two-role
+profile pair with
+
+```
+(ab, ba, aba, bab) = (0,0,0,0),
+(cb, bc, cbc, bcb) = (0,0,0,0),
+(abc, cba) = (I_2, I_2).
+```
+
+(The remaining target equations `acb = bac = I_2` are not needed for the
+obstruction below.)
+
+## 3. Finite census on two roles
+
+Conjugation by `GL_2(F2)` fixes the two-role target `I_2` and acts on middle
+sequences. There are 33,489 zero-sum length-6 sequences of nonzero rank-one
+`2 x 2` matrices; they form 5,582 conjugation-minimal orbits (the same count
+as in #1690 / #1816). Of these, 182 have `rank X < 2` or `rank Y < 2` and are
+excluded by Section 1. The remaining **5,400** middles are searched.
+
+For each middle, the side-zero profiles are collected by a 3+3 meet-in-the-middle
+on the packed side table of #1690. Each side-zero profile determines a
+transport key `(U_0,U_1,W_0,W_1)` whose bits record `(P_j x_j)` and
+`(y_j^T P_j)`. The identity cross condition `abc = cba = I_2` is exactly
+the key-pairing equation of #1690 with target packing `9 = I_2`.
+
+**Result.** Across all 5,400 rank-adequate middles the set of side-zero keys
+admits **zero** pairs with `abc = cba = I_2`. Certificate counts:
+
+| Quantity | Count |
+|---|---:|
+| Canonical zero-sum middles | 5,582 |
+| With `rank X,Y >= 2` | 5,400 |
+| Sum of side-zero key cardinalities | 1,568,064 |
+| Key pairs with `abc = cba = I_2` | **0** |
+
+A low-rank control middle `(E_{11})^6` still produces many identity key pairs,
+so the screen is not vacuous: the obstruction is the rank-2 constraint
+together with the side-zero locus.
+
+## 4. Conclusion
+
+No two-role profile pair meets the necessary quotient conditions of Section 2.
+By the dirty-contraction reduction, no word on any finite `r >= 2` with
+`n_b = 6` reaches the degree-three quotient endpoint, hence none equals the
+formal target. Combined with #1662's bound `n_b >= 6`, every legal two-target
+word satisfies `n_b >= 7`.
+
+The value `n_b = 7` is not decided here.
+
+## Credit
+
+Model and separate-label bound: #1662 (@ToikY). Unit-tariff exactness and the
+weighted open question that motivates this package: #1816. Profile/key pipeline:
+#1690 (Aaron Wang / @navinor), as used by #1816. Workspace compression context:
+#1680. Prepared by Wentao Li with substantial AI assistance. Apache-2.0.

research/ut4-two-target-no-six-b/README.md

@@ -0,0 +1,89 @@
+# No two-target UT4 central word has n_b = 6
+
+**Result.** In the explicit `F2[UT4(F2)]` central-target alphabet of
+[CrocSwap/integer-mult-bounds#1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662),
+no legal word realizing two central targets — of any finite length, on any
+finite restored dirty workspace — has exactly six paid `b` calls. Every such
+word therefore has `n_b >= 7`. The case `n_b = 7` is left open.
+
+No new κ. Selected decimal stays `0.001672660197076918`.
+
+This answers the `n_b = 6` half of open next question 2 in
+[CrocSwap/integer-mult-bounds#1816](https://github.com/CrocSwap/integer-mult-bounds/pull/1816)
+(`research/ut4-two-target-fifteen/`).
+
+## Why it matters
+
+#1662 prices labels separately: `n_a, n_c >= 4` and `n_b >= 6`, while the direct
+word `(abcb)^2` per target uses `n_b = 8`. A realizing word with `n_b = 6` and
+only modestly larger outer counts would beat the direct word whenever `β` is
+large relative to `α+γ`. Ruling out `n_b = 6` at every length is the first
+weighted-tariff step; `n_b = 7` remains the next gate.
+
+## Method
+
+[PROOF.md](PROOF.md) records the argument. At `n_b = 6` the middle quotient of
+#1662 forces `rank X = rank Y = 2`, so every `b` coupling lies in the active
+2-plane. Interior dirty contractions then cannot touch the `{a,b}` / `{c,b}`
+side coefficients or the cross coefficients `abc` and `cba`. Those necessary
+equations reduce to a two-role profile problem with unrestricted outer length
+(every `2 x 2` profile is realizable with enough `a`/`c` calls).
+
+The census (self-contained in `core.py`, formulas matching #1690) enumerates
+all 5,582 GL2-minimal zero-sum length-6 middle sequences, keeps the 5,400 with
+both middle ranks at least two, builds every side-zero transport key via a 3+3
+meet-in-the-middle, and pairs keys for `abc = cba = I_2`. **Zero pairs survive.**
+A low-rank control middle still produces pairs, so the screen is not empty by
+accident.
+
+| Stage | Count |
+|---|---:|
+| Canonical zero-sum middles | 5,582 |
+| `rank X,Y >= 2` | 5,400 |
+| Sum of side-zero key-set sizes | 1,568,064 |
+| Key pairs with `abc = cba = I_2` | **0** |
+
+## Evidence
+
+- `verify.py` (read-only, `need()` gates survive `python -O`): source pins;
+  corrupted temporary certificate and duplicate JSON key rejection; low-rank
+  positive control; full census against `CERTIFICATE.json`.
+- `independent.py` does **not** import `verify.py`; it re-runs the census with
+  a separate base-16 half-profile MITM and matches the certificate.
+- `test_package.py`: isolated `-O` read-only replay, independent import guard,
+  certificate pair corruption, duplicate keys, SOURCES sha drift.
+
+## Reproduce
+
+```sh
+python3 -B scripts/research_package.py --package research/ut4-two-target-no-six-b
+# Direct:
+python3 -I -B research/ut4-two-target-no-six-b/verify.py
+python3 -I -O -B research/ut4-two-target-no-six-b/independent.py
+python3 -I -B research/ut4-two-target-no-six-b/test_package.py
+```
+
+## Open next questions
+
+1. **Does any two-target word have `n_b = 7`?** Why it matters: finishes the
+   first step of #1816 open question 2. First step: run the unrestricted-profile
+   key census for length-7 middles on rank patterns `(2,2)`, `(2,3)`, `(3,2)`,
+   or find an algebraic obstruction. Blocked by: `16^7` profiles, middle excess
+   when a middle rank is 3, and dirty-role structure beyond the `e_b = 0`
+   reduction used here.
+
+## Limits
+
+- Decides `n_b = 6` only; `n_b = 7` is explicitly open.
+- Does not restate the unit-tariff minimum 16 from #1816; does not reopen
+  three-target lengths 21/22.
+- Quotient-level obstruction (sufficient for the formal endpoint). No
+  proof-assistant or independent human review. No supplier or κ change.
+
+## Credit
+
+#1662 (@ToikY) for the model and `n_b >= 6` bound. #1816 for unit-tariff
+exactness and the weighted open question. #1690 (Aaron Wang / @navinor) for
+the profile/key pipeline, as used by #1816. #1680 for workspace context.
+Prepared by Wentao Li `<wentaol4@illinois.edu>` with substantial AI assistance.
+Apache-2.0.

research/ut4-two-target-no-six-b/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/bit-three-register-lower-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79",
+      "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"
+    },
+    {
+      "path": "research/ut4-central-tariff-relaxation/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "8137274359979a786568da60bc802eeba2728e7f",
+      "sha256": "4820f0771cc6d5828492bf8cb0bacda2a74d3f00b58a02b8df056ab1db040f21"
+    },
+    {
+      "path": "research/ut4-two-target-fifteen/README.md",
+      "usage": "provenance",
+      "git_blob": "3d314e22e7a9d1941269b161c833fbd3bcfc8934",
+      "sha256": "fb1026abcf357b5a409a2398eb18c9ae7c72541176dafa0b02c819b79e8f9b5f"
+    },
+    {
+      "path": "research/ut4-two-target-r2/search.py",
+      "usage": "provenance",
+      "git_blob": "62c56bd121d6d06f4b781ba869ee82be0042f9ec",
+      "sha256": "eaa1380c62866acfcae77ab7e53ed30d7c4e4319978a446a6f3bb86b65920117"
+    }
+  ]
+}

research/ut4-two-target-no-six-b/TASK.json

@@ -0,0 +1,64 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 3,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "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": "refined",
+  "actual_scope": "In CrocSwap/integer-mult-bounds#1662's explicit F2[UT4(F2)] central-target alphabet (paid factors I+([g]+1)xy^T, g in {a,b,c}, target I+([z]+1)I_2), decide whether any legal two-target word of any finite length on any finite restored dirty workspace can have n_b=6. Leave n_b=7 open.",
+  "scope_change_reason": "Takes open next question 2 of https://github.com/CrocSwap/integer-mult-bounds/pull/1816 (research/ut4-two-target-fifteen): the first step toward weighted tariffs that could beat (abcb)^2 per target is to decide n_b=6 or 7 at any length. This package decides n_b=6 only.",
+  "bottleneck_link": "Separate-label bound n_b>=6 from #1662 sits below the direct word's n_b=8; excluding n_b=6 is the first weighted-tariff step. Screening/quotient result only; no supplier or kappa change. Selected decimal stays 0.001672660197076918.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after deciding n_b=6 (exhibit or prove none). Leave n_b=7 open. Do not reopen three-target lengths 21/22 or unit-tariff minimum 16.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md: at n_b=6 the middle ranks are forced to (2,2), so all six b-couplings lie in the active 2-plane; abc/cba and the a/b and c/b side coefficients receive no interior dirty contraction and reduce to the two-role profile equations. core.py/verify.py: all 5582 GL2-minimal zero-sum 6-middles; 5400 with rank X,Y>=2; every side-zero profile's transport keys; 0 pairs with abc=cba=I. independent.py repeats the census with a separate base-16 MITM. Low-rank control (1^6) still finds pairs, so the screen is not vacuous. n_b=7 left open.",
+  "author": "Wentao Li <wentaol4@illinois.edu>",
+  "ai_assistance": "Substantial AI assistance in search design, proof writing, packaging and verification; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Does any two-target word have n_b=7 at any length and any finite dirty workspace?",
+      "why_it_matters": "Together with this n_b=6 exclusion, deciding n_b=7 would finish the first step of #1816 open question 2 on weighted tariffs versus (abcb)^2.",
+      "first_step": "Extend the unrestricted-profile key census to n_b=7 for rank patterns (2,2), (2,3) and (3,2), or find an algebraic obstruction.",
+      "blocked_by": "16^7 profiles and 49686 canonical length-7 middles; middle excess when rank X or Y is 3 needs a dirty-role argument beyond the e_b=0 reduction used here."
+    }
+  ]
+}

research/ut4-two-target-no-six-b/VERIFY.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": ["{python}", "-I", "-B", "{package}/verify.py"],
+      "timeout_seconds": 180,
+      "checks": "Full n_b=6 rank-filtered middle census; zero abc=cba=I key pairs; source pins; corrupted temporary certificate and duplicate JSON key rejection; read-only."
+    },
+    {
+      "argv": ["{python}", "-I", "-O", "-B", "{package}/independent.py"],
+      "timeout_seconds": 180,
+      "checks": "Separate base-16 half-profile MITM census matching CERTIFICATE.json; does not import verify.py."
+    },
+    {
+      "argv": ["{python}", "-I", "-B", "{package}/test_package.py"],
+      "timeout_seconds": 600,
+      "checks": "Isolated -O read-only replay, independent import guard, certificate pair corruption, duplicate JSON keys."
+    }
+  ]
+}