Refute the right-vector general-target formula: M2(F2) targets need 3 factors, not 2 (no new κ)

research/right-vector-general-target/README.md

@@ -0,0 +1,115 @@
+# The right-vector column bound is not exact for every target
+
+**Finite certificate with a sharp counterexample. No new κ.** Selected κ stays
+`0.001672660197076918`.
+
+Paid factors are `I + u y^T` with `u` in `R^n` and `y` in `K^n`. Free maps are
+`GL_n(K)` changes of basis anywhere in a word. #4243 proved that a diagonal
+target costs exactly `t_K(d)` factors, and asked in its open question 1 whether
+every target `M` costs
+
+```text
+delta(M) = min over T in GL_n(K) of dim_K (M T - I) K^n.
+```
+
+`delta(M)` is always a lower bound: that is #4243's normal form plus the column
+bound of #4099. This package tests the upper bound on every target of eleven
+small domains.
+
+## Result
+
+| Algebra `R` over `K` | n | Targets | Max cost | Formula failures | Gaps with no free map |
+|---|---:|---:|---:|---:|---:|
+| `F2` | 2 | 16 | 2 | 0 | 0 |
+| `F3` | 2 | 81 | 2 | 0 | 0 |
+| `F2` | 3 | 512 | 3 | 0 | 0 |
+| `F4` over `F2` | 2 | 256 | 2 | 0 | 0 |
+| `F2[C2]` | 2 | 256 | 2 | 0 | 0 |
+| `F2 x F2` | 2 | 256 | 2 | 0 | **2** |
+| `F3 x F3` | 2 | 6,561 | 2 | 0 | 0 |
+| `F2[C3]` | 2 | 4,096 | 2 | 0 | **6** |
+| `F2[x]/(x^3)` | 2 | 4,096 | 2 | 0 | 0 |
+| `M2(F2)` (noncommutative) | 2 | 65,536 | 3 | **72** | **684** |
+| `F2[C2]` | 3 | 262,144 | 3 | 0 | 0 |
+
+1. **The answer to #4243's question is no in general.** Over the matrix
+   algebra `M2(F2)` at `n = 2`, exactly 72 of 65,536 targets cost 3 factors
+   while `delta = 2`. One is the target `[[E11, E01], [E10, E00]]`. In
+   `M_2(M_2(F_2)) = M_4(F_2)` it is the transposition of coordinates 0 and 3.
+   A separate enumeration in `M_4(F_2)` confirms that no two-factor word
+   reaches it, that a three-factor word does, and that `T = I` already gives
+   image dimension 2.
+2. **The formula holds on all ten commutative domains checked**: 278,274
+   targets, local and non-local, including `F2[C3] = F2 x F4` and
+   `F3 x F3 = F3[C2]`.
+3. **The minimum over `T` cannot be dropped.** Without any free map, the cost
+   of `M` exceeds `dim_K (M - I) K^n` on 2 targets over `F2 x F2`, 6 over
+   `F2[C3]` and 684 over `M2(F2)`; each such target costs 3 against dimension 2.
+   Over `F2 x F2` the two targets are `(A, A^{-1})` and its swap, with `A` of
+   order three in `GL_2(F_2)`. The fields and local algebras in the table have
+   no such gap.
+
+All counts are enumerated. Statement 1 is a counterexample to the proposed
+formula; statements 2 and 3 are finite certificates on the listed domains, not
+theorems for every algebra.
+
+## Method
+
+`verify.py` builds each algebra from a structure table and checks that it is
+associative with `K` central. It computes the exact minimum by breadth-first
+search over words in #4243's normal form `Q S`: products of paid factors
+followed by one free map. It computes `delta` by enumerating every `T` in
+`GL_n(K)` and taking `F_p`-ranks. It asserts `cost >= delta` everywhere and
+records every target with `cost != delta`. A second search from `I` alone
+gives the no-free-map cost, compared with `dim_K (M - I) K^n`. The script
+writes nothing and prints a digest bound to its own bytes and results.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-general-target/verify.py --stage main
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-general-target/verify.py --stage large
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-general-target
+```
+
+Expected final lines:
+
+```text
+PASS_RIGHT_VECTOR_GENERAL_TARGET F2:n2:16 F3:n2:81 F2:n3:512 F4:n2:256 F2[C2]:n2:256 F2xF2:n2:256 F3xF3:n2:6561 F2[C3]:n2:4096 F2[x]/(x^3):n2:4096 M2(F2):n2:65536 formula_failures=M2(F2):72 no_free_map_gaps=F2xF2:2,F2[C3]:6,M2(F2):684 no_new_kappa
+PASS_RIGHT_VECTOR_GENERAL_TARGET_LARGE F2[C2]:n3:262144 formula_failures=0 no_free_map_gaps=0 no_new_kappa
+```
+
+Each stage takes about 100 seconds on one core (CPython 3.12, NumPy 2.5.4,
+macOS arm64). The asserts are the checks, so do not run with `-O`.
+
+## Limits
+
+This is an exact count in a formal alphabet. Native frames, hosting, routing,
+precision and recursive cost are not priced, and no supplier changes. The
+commutative agreement is checked only on the listed domains; no general proof
+of the upper bound is claimed. Whether the `M2(F2)` failure transfers to a
+nonabelian group algebra is not checked. Independent human and formal
+proof-kernel review are unclaimed.
+
+## Open next questions
+
+1. **Commutative algebras.** Is `delta(M)` exact for every commutative
+   `K`-algebra, or every local one with residue field `K`? A one-factor peel
+   `A = A' (I + u y^T)` with `dim_K (A' - I) K^n = d - 1` exists exactly when
+   some `y` vanishing on the `K`-kernel of `A - I` and some `x1` with
+   `y . x1 = 1` give `A x1` in `A (ker y ⊗ R) + x1 R`. Proving this for a
+   minimizing `T` would settle the question.
+2. **Group algebras.** Does the failure lift to `F2[S3]`, which has `M2(F2)` as
+   a block? Fix an explicit isomorphism and project words onto that block.
+3. **Exact noncommutative cost.** What replaces `delta` over `M2(K)`? Compare
+   the cost with ranks in `M_n(M_2(K)) = M_2n(K)`.
+
+## Credit
+
+Produced by Nick Petalas. The alphabet, normal form and lower bound come from
+#4243 (`research/right-vector-diagonal-free-basis`), which asked this question.
+The column bound and right-vector alphabet are Wentao Li's
+`research/f2-right-vector-diagonal-minimum` (#4099), building on
+`research/bit-cyclic-root-barrier` (#2513). Apache-2.0.

research/right-vector-general-target/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/f2-right-vector-diagonal-minimum/PROOF.md",
+      "usage": "input",
+      "git_blob": "274c950b24091733f919c6cdf6d75b1a783efae1",
+      "sha256": "e2ebc7a25d764cf24b586aa5054ae1e721d24c238eb7fac8eaa39e46e21b15d1"
+    }
+  ]
+}

research/right-vector-general-target/TASK.json

@@ -0,0 +1,76 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "Exact paid-factor minimum for general (non-diagonal) targets in the right-vector alphabet I + u y^T (u in R^n, y in K^n) with free GL_n(K) maps: tests the formula min_T dim_K (M T - I) K^n proposed in open question 1 of #4243 on every target over eleven small (algebra, n) domains.",
+  "scope_change_reason": "The card asks whether a larger or nonabelian register model escapes the scoped three-register obstruction. This package answers a narrower open question left by #4243: whether its diagonal count extends to all targets. The answer is no for the noncommutative algebra M2(F2), and the trailing free map is necessary even over commutative non-local algebras.",
+  "bottleneck_link": "A legal target cheaper than its column bound would be a new bit primitive; this package shows the column bound is attained on ten commutative domains and is not attained in general. Kappa is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Exhaust every target on small algebras, record each place the formula or its no-free-map form fails, independently confirm one failure, then stop.",
+  "outcome": "completed",
+  "evidence": "verify.py --stage main and --stage large compute exact minima by breadth-first search over all words and the formula by enumerating every T in GL_n(K), on 343,810 targets in total. Formula failures: 72, all over M2(F2) at n=2 (cost 3, formula 2). No-free-map gaps: 2 over F2xF2, 6 over F2[C3], 684 over M2(F2). The transposition witness is rechecked in M_4(F_2) by a separate enumeration of all two- and three-factor products.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does the formula hold for every commutative K-algebra, or every local algebra with residue field K?",
+      "why_it_matters": "It holds on all ten commutative domains checked here, which include the group algebras F2[C2], F2[C3] and F3[C2]-type products.",
+      "first_step": "Prove the one-step peeling condition A x1 in A(H R) + x1 R for a minimizing T, starting with local R.",
+      "blocked_by": "No general factorization argument is proved here."
+    },
+    {
+      "question": "Does the M2(F2) failure lift to a nonabelian group algebra such as F2[S3]?",
+      "why_it_matters": "#4243 covers diagonals in every F2[G]; a failure inside F2[S3] would bound how far its count extends for nonabelian registers.",
+      "first_step": "Fix an explicit K-algebra isomorphism F2[S3] = F2[C2] x M2(F2) and project words onto the matrix block.",
+      "blocked_by": "The isomorphism and projection argument are not checked here."
+    },
+    {
+      "question": "What is the exact cost for noncommutative algebras?",
+      "why_it_matters": "The formula undercounts M2(F2) targets by one at n=2.",
+      "first_step": "Compare cost with the K^2n rank of M - I in the Morita picture M_n(M_2(K)) = M_2n(K).",
+      "blocked_by": "Only n=2 over M2(F2) is enumerated."
+    }
+  ]
+}

research/right-vector-general-target/VERIFY.json

@@ -0,0 +1,39 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [
+    "numpy==2.5.4"
+  ],
+  "inputs": [
+    "research/f2-right-vector-diagonal-minimum/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py",
+        "--stage",
+        "main"
+      ],
+      "timeout_seconds": 420,
+      "checks": "Exact minimum versus min_T dim_K (M T - I) K^n on every target over ten (algebra, n) domains, including M2(F2) at n=2; asserts the #4243 lower bound everywhere, exactly 72 formula failures (all M2(F2), cost 3 versus 2), the no-free-map gap counts 2, 6 and 684, and an independent M_4(F_2) recheck of the transposition witness."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py",
+        "--stage",
+        "large"
+      ],
+      "timeout_seconds": 420,
+      "checks": "Same comparison on all 262,144 targets over F2[C2] at n=3: no formula failure and no no-free-map gap."
+    }
+  ]
+}