Research: no two-target UT4 word has n_b=7 with middle ranks (2,2) (n_b=7 open; no new kappa)

research/ut4-two-target-nb7-ranks-22/CERTIFICATE.json

@@ -0,0 +1,15 @@
+{
+  "active_roles": 2,
+  "canonical_zero_sum_middles": 49686,
+  "key_pairs_abc_cba_I": 0,
+  "keys_sum": 46169088,
+  "low_rank_excluded": 546,
+  "max_keys_per_middle": 4096,
+  "middle_ranks": [2, 2],
+  "n_b": 7,
+  "rank_XY_exactly_2_2": 49140,
+  "schema_version": 1,
+  "side_zero_key_joins": 738705408,
+  "status": "no_nb7_ranks_22_two_target_quotient",
+  "targets": 2
+}

research/ut4-two-target-nb7-ranks-22/PROOF.md

@@ -0,0 +1,130 @@
+# No two-target UT4 word has n_b = 7 with middle ranks (2,2)
+
+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`, and
+[CrocSwap/integer-mult-bounds#3887](https://github.com/CrocSwap/integer-mult-bounds/pull/3887)
+excludes `n_b = 6`, so every such word has `n_b >= 7`. This note proves the
+scoped statement:
+
+> No legal word equal to `I+([z]+1)I_2`, of any finite length and on any finite
+> restored dirty workspace, has exactly seven paid `b` factors with middle ranks
+> `(rank X, rank Y) = (2, 2)`, under the same unrestricted side-zero profile
+> reduction that #3887 used for `n_b = 6`.
+
+Middle-rank patterns `(2,3)` and `(3,2)`, and unrestricted `n_b = 7`, are left
+open. There is no new κ; the selected decimal `0.001672660197076918` is
+unchanged.
+
+## 1. Model and the (2,2) slice at n_b = 7
+
+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. 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.
+
+Use the fixed 17-dimensional quotient
+
+```
+Q = F2<a,b,c>/(a^2,b^2,c^2,ac-ca, deg >= 4)
+```
+
+of #1662. Write `B_j = x_j y_j^T` for the seven middle couplings in product
+order, and set
+
+```
+X = [x_j] (r x 7),   Y = [y_j^T] (7 x r).
+```
+
+#1662 gives `XY = 0` and `n_b >= 2 + rank X + rank Y`, together with
+`rank X, rank Y >= 2` from the `bac` and `acb` coefficients. At `n_b = 7` the
+admissible patterns are therefore
+
+```
+(2,2), (2,3), (3,2).
+```
+
+This package treats only `(2,2)`. In that case 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). The patterns `(2,3)` and
+`(3,2)` require an extra dirty role and are out of scope.
+
+## 2. Reduction to two active roles
+
+With all seven `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`, receive no interior dirty contribution. Their
+active `H x H` blocks are exactly the two-role coefficients computed from:
+
+- the seven 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 7-tuple of `2 x 2` matrices arises as
+such a profile for some finite `n_a` (resp. `n_c`). This is the same
+unrestricted side-zero reduction #3887 used at `n_b = 6` (there labelled
+`e_b = 0` because ranks forced equality with the paid count).
+
+Therefore a realizing word with `n_b = 7` and middle ranks `(2,2)` 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).
+```
+
+## 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 49,686 conjugation-minimal zero-sum length-7 sequences of
+nonzero rank-one `2 x 2` matrices. Of these, 546 have `rank X != 2` or
+`rank Y != 2` on the active plane (they are the rank patterns `(1,2)` and
+`(2,1)`); the remaining **49,140** have ranks exactly `(2,2)` and are searched.
+
+For each such middle, the side-zero profiles are collected by a 3+4
+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 49,140 rank-`(2,2)` middles the set of side-zero keys
+admits **zero** pairs with `abc = cba = I_2`. Certificate counts:
+
+| Quantity | Count |
+|---|---:|
+| Canonical zero-sum middles | 49,686 |
+| With `rank X = rank Y = 2` | 49,140 |
+| Sum of side-zero key cardinalities | 46,169,088 |
+| Key pairs with `abc = cba = I_2` | **0** |
+
+A low-rank control middle with ranks `(1,2)` still produces many identity key
+pairs, so the screen is not vacuous: the obstruction is the rank-`(2,2)`
+constraint together with the side-zero locus.
+
+## 4. Conclusion
+
+No two-role profile pair meets the necessary quotient conditions of Section 2
+for middle ranks `(2,2)`. By the dirty-contraction reduction, no word on any
+finite `r >= 2` with `n_b = 7` and middle ranks `(2,2)` reaches the degree-three
+quotient endpoint, hence none equals the formal target.
+
+The patterns `(2,3)` and `(3,2)`, and the unrestricted statement that no
+`n_b = 7` word exists at all, are not decided here.
+
+## Credit
+
+Model and separate-label bound: #1662 (@ToikY). Unit-tariff exactness and the
+weighted open question: #1816. `n_b = 6` exclusion and the unrestricted
+side-zero reduction reused here: #3887. 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-nb7-ranks-22/README.md

@@ -0,0 +1,99 @@
+# No two-target UT4 word has n_b = 7 with middle ranks (2,2)
+
+**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 seven paid `b` calls with middle
+ranks `(rank X, rank Y) = (2, 2)`, under the same unrestricted side-zero
+profile reduction used by
+[CrocSwap/integer-mult-bounds#3887](https://github.com/CrocSwap/integer-mult-bounds/pull/3887).
+
+Middle-rank patterns `(2,3)` and `(3,2)`, and unrestricted `n_b = 7` (any middle
+ranks), are explicitly left open. This package does **not** claim that every
+`n_b = 7` word is impossible.
+
+No new κ. Selected decimal stays `0.001672660197076918`.
+
+## Why it matters
+
+#3887 ruled out `n_b = 6`, so every realizing word has `n_b >= 7`. At `n_b = 7`
+the #1662 rank bound `n_b >= 2 + rank X + rank Y` with `rank X, rank Y >= 2`
+permits patterns `(2,2)`, `(2,3)` and `(3,2)`. The `(2,2)` slice still places
+every middle coupling in a fixed 2-plane, so the #3887 dirty-contraction /
+unrestricted-profile screen applies directly. Closing that slice narrows the
+remaining weighted-tariff gate toward `(abcb)^2`.
+
+## Method
+
+[PROOF.md](PROOF.md) records the argument. With `rank X = rank Y = 2`, all seven
+`b` couplings lie in an active 2-plane `H`. Interior dirty contractions 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.
+
+The census (self-contained in `core.py`, formulas matching #1690) enumerates
+all 49,686 GL2-minimal zero-sum length-7 middle sequences, keeps the 49,140
+with ranks exactly `(2,2)`, builds every side-zero transport key via a 3+4
+meet-in-the-middle, and pairs keys for `abc = cba = I_2`. **Zero pairs survive.**
+A low-rank control middle with ranks `(1,2)` still produces pairs, so the screen
+is not empty by accident.
+
+| Stage | Count |
+|---|---:|
+| Canonical zero-sum middles | 49,686 |
+| `rank X = rank Y = 2` | 49,140 |
+| Sum of side-zero key-set sizes | 46,169,088 |
+| 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-nb7-ranks-22
+# Direct:
+python3 -I -B research/ut4-two-target-nb7-ranks-22/verify.py
+python3 -I -O -B research/ut4-two-target-nb7-ranks-22/independent.py
+python3 -I -B research/ut4-two-target-nb7-ranks-22/test_package.py
+```
+
+## Open next questions
+
+1. **Does any two-target word have `n_b = 7` with middle ranks `(2,3)` or
+   `(3,2)`?** Why it matters: those patterns saturate
+   `n_b = 2 + rank X + rank Y` and need dirty roles beyond the two-plane
+   reduction used here. First step: extend the profile/key analysis to `r >= 3`
+   with one middle-excess role, or find an algebraic obstruction. Blocked by:
+   dirty-role structure beyond the unrestricted two-role reduction.
+
+2. **Is every `n_b = 7` two-target word impossible?** Why it matters: finishes
+   the first step of #1816 open question 2 once `(2,3)` and `(3,2)` are decided.
+   First step: combine this `(2,2)` exclusion with a `(2,3)/(3,2)` argument; do
+   not treat the present package as that claim. Blocked by: open mixed-rank
+   cases above.
+
+## Limits
+
+- Decides only `n_b = 7` with middle ranks `(2,2)` under the #3887 unrestricted
+  side-zero reduction. Does **not** decide `(2,3)`, `(3,2)`, or full `n_b = 7`.
+- Does not restate the unit-tariff minimum 16 from #1816; does not reopen
+  three-target lengths 21/22; does not reprint the #3887 `n_b = 6` census as new.
+- 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. #3887 for the `n_b = 6` exclusion and
+the unrestricted side-zero reduction reused here. #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-nb7-ranks-22/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-nb7-ranks-22/TASK.json

@@ -0,0 +1,70 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 6,
+  "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), prove that no legal two-target word of any finite length on any finite restored dirty workspace can have n_b=7 with middle ranks (rank X, rank Y)=(2,2), under the same e_b=0-style unrestricted side-zero profile reduction used by #3887. Explicitly leave middle-rank patterns (2,3) and (3,2), and unrestricted n_b=7, open. Do not claim every n_b=7 word is impossible.",
+  "scope_change_reason": "Follows #3887 (n_b=6 exclusion) and open next question 2 of https://github.com/CrocSwap/integer-mult-bounds/pull/1816 (research/ut4-two-target-fifteen). Packages only the finished rank pattern (2,2) of the length-7 unrestricted-profile census; mixed ranks (2,3)/(3,2) were not finished and stay open.",
+  "bottleneck_link": "After #3887 every realizing word has n_b>=7; excluding the (2,2) slice at n_b=7 under the same unrestricted-profile reduction narrows the remaining weighted-tariff gate. Screening/quotient result only; no supplier or kappa change. Selected decimal stays 0.001672660197076918.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after deciding the n_b=7 middle-ranks-(2,2) case (exhibit or prove none under the #3887 reduction). Leave (2,3), (3,2), and unrestricted n_b=7 open. Do not claim full n_b=7 impossibility. Do not reopen three-target lengths 21/22 or unit-tariff minimum 16.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md: at n_b=7 with rank X=rank Y=2 all seven b-couplings lie in the active 2-plane, so abc/cba and the a/b and c/b side coefficients receive no interior dirty contraction and reduce to the two-role unrestricted side-zero profile equations (same reduction as #3887). core.py/verify.py: all 49686 GL2-minimal zero-sum 7-middles; 49140 with ranks exactly (2,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 (ranks (1,2)) still finds pairs, so the screen is not vacuous. Patterns (2,3), (3,2) and unrestricted 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 with middle ranks (2,3) or (3,2)?",
+      "why_it_matters": "Those patterns saturate n_b = 2 + rank X + rank Y and require dirty roles beyond the two-plane reduction used here; together with this (2,2) exclusion they would decide all of n_b=7.",
+      "first_step": "Extend the profile/key analysis to r>=3 with one middle excess role, or find an algebraic obstruction for (2,3)/(3,2).",
+      "blocked_by": "Middle excess when rank X or Y is 3 needs a dirty-role argument beyond the unrestricted two-role e_b=0-style reduction; 16^7 two-role profiles do not cover that case."
+    },
+    {
+      "question": "Is every n_b=7 two-target word impossible (unrestricted over middle ranks)?",
+      "why_it_matters": "Finishes the first step of #1816 open question 2 on weighted tariffs versus (abcb)^2 once (2,3) and (3,2) are decided.",
+      "first_step": "Combine this (2,2) exclusion with a (2,3)/(3,2) argument; do not treat the present package as that claim.",
+      "blocked_by": "Open (2,3) and (3,2) cases above."
+    }
+  ]
+}

research/ut4-two-target-nb7-ranks-22/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": 550,
+      "checks": "Full n_b=7 middle-rank-(2,2) 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": 550,
+      "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": 100,
+      "checks": "Isolated -O controls-only replay, independent import guard, subsample zero pairs, certificate mismatch, duplicate JSON keys, SOURCES base drift."
+    }
+  ]
+}