Prove the exact two-factor right-vector criterion at n = 2; the M2(F2) failure lifts to F2[S3] (no new κ)

research/right-vector-two-factor-criterion/PROOF.md

@@ -0,0 +1,93 @@
+# Proofs
+
+`K` is a field and `R` an associative unital `K`-algebra with `K` central. A
+paid factor is `P(u, y) = I + u y^T` with `u` in `R^n` and `y` in `K^n`; a free
+map is any `S` in `GL_n(K)`, used anywhere in a word. `cost(M)` is the least
+number of paid factors in a word equal to `M` (infinite if none exists), and
+
+```text
+delta(M) = min over T in GL_n(K) of dim_K (M T - I) K^n.
+```
+
+Facts used from #4243 and #4099: `cost(M) >= delta(M)`, and every word can be
+rewritten as `Q S` with `Q` a product of the same number of paid factors,
+because `S P(u, y) S^{-1} = P(S u, S^{-T} y)`.
+
+## Lemma 1 (merging)
+
+`P(u, y) P(v, c y) = P(u + c v + c u (y^T v), y)` for `c` in `K`. Expand:
+`(I + u y^T)(I + c v y^T) = I + u y^T + c v y^T + c u (y^T v) y^T`, and
+`y^T v` is an element of `R`. Also `P(u, 0) = P(0, y) = I`.
+
+## Theorem A (one factor, every n, every R)
+
+`cost(M) <= 1` if and only if `delta(M) <= 1`, and then `cost(M) = delta(M)`.
+
+*Proof.* `cost >= delta` gives one direction. If `delta(M) = 0`, then
+`M T = I` and `M = T^{-1}` costs 0. If `delta(M) = 1`, then
+`(M T - I) K^n = K w` for some `w` in `R^n`, so `(M T - I) e_j = c_j w` with
+`c` in `K^n`, that is `M T = I + w c^T = P(w, c)`, and `M = P(w, c) T^{-1}`.
+
+## Theorem B (two factors, n = 2, every R)
+
+`cost(M) <= 2` if and only if some `G, H` in `GL_2(K)` give `N = G M H` with
+`N12` in the right ideal `N11 R`.
+
+*Proof.* (If.) Write `N12 = N11 C` and put `A = N11`, `B = N21`,
+`D = N22 - N21 C`. Then
+
+```text
+F1 = P((A - 1, B), e1) = [[A, 0], [B, 1]],
+F2 = P((C, D - 1), e2) = [[1, C], [0, D]],
+F1 F2 = [[A, A C], [B, B C + D]] = N,
+```
+
+so `M = (G^{-1} F1 G)(G^{-1} F2 G) G^{-1} H^{-1}`, and each conjugate is a
+paid factor.
+
+(Only if.) Write `M = P(u1, y1) P(u2, y2) S`, padding with `P(0, y) = I`. If
+`y1, y2` are dependent, Lemma 1 merges the two factors into one with a nonzero
+`y` (or both are `I`); replace the second by `P(0, y2')` with `y2'`
+independent. So `y1, y2` is a basis. Choose `G` with `G^{-T} y_i = e_i`. Then
+`G M S^{-1} G^{-1} = P(u1', e1) P(u2', e2)`, which is
+`[[A, 0], [B, 1]] [[1, C], [0, D]] = [[A, A C], [B, B C + D]]` for some
+`A, B, C, D` in `R`. Its `(1, 2)` entry is `A C`, in `A R`. Take
+`H = S^{-1} G^{-1}`.
+
+## Corollary C (matrix algebras)
+
+Let `R = M_m(K)` and view `M` as a `2m x 2m` matrix. Then `cost(M) <= 2` if
+and only if there are nonzero `phi` in `(K^2)^*` and `t` in `K^2` with
+
+```text
+rank (phi ⊗ I_m) M = rank (phi ⊗ I_m) M (t ⊗ I_m).
+```
+
+*Proof.* In `M_m(K)`, `Z` lies in `A M_m(K)` exactly when the column space of
+`Z` lies in that of `A`. Let `phi` be the first row of `G` and `t, s` the
+columns of `H`. Then `N11 = (phi ⊗ I) M (t ⊗ I)`,
+`N12 = (phi ⊗ I) M (s ⊗ I)`, and since `H` is invertible the column space of
+`[N11 N12]` is that of `(phi ⊗ I) M`. So `col N12 ⊆ col N11` is the stated
+rank equality. Every nonzero `phi` is a first row and every nonzero `t` a first
+column.
+
+## Theorem D (local algebras, n = 2)
+
+Let the non-units of `R` form an ideal `J`. Every target `M` with an entry
+outside `J` (in particular every invertible `M`) has `cost(M) = delta(M)`.
+
+*Proof.* Permutation matrices `G, H` move a unit to position `(1, 1)`. Then
+`N11 R = R`, so Theorem B gives `cost(M) <= 2`. If `delta(M) <= 1`, Theorem A
+gives equality. Otherwise `2 = delta(M) <= cost(M) <= 2`.
+
+## Corollary E (quotients and F2[S3])
+
+If `rho: R -> R'` is a unital `K`-algebra homomorphism, then
+`cost_R(M) >= cost_R'(rho(M))`, because `rho` maps paid factors to paid factors
+and free maps to free maps. Since `delta(M) <= n` always, every target over
+`F2[S3]` whose image under the surjection `rho: F2[S3] -> M_2(F_2)` is one of
+the 72 cost-3 targets of #4265 costs at least 3 while `delta <= 2`. `rho`
+extends the isomorphism `S3 = GL_2(F_2)` given by the action on the three
+nonzero vectors of `F_2^2`; `verify.py` checks that it is a surjective unital
+algebra map and lifts a three-factor word to an explicit target of cost
+exactly 3.

research/right-vector-two-factor-criterion/README.md

@@ -0,0 +1,124 @@
+# Exact two-factor criterion for right-vector targets
+
+**Scoped proofs with finite certificates. 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 (#4099, #4243). #4243 proved
+`cost(M) >= delta(M) = min_T dim_K (M T - I) K^n` and equality on diagonal
+targets. #4265 showed equality fails over `M2(F2)` at `n = 2` (72 targets cost
+3 against `delta = 2`) and asked what the exact cost is over noncommutative
+algebras, whether the failure lifts to `F2[S3]`, and whether `delta` is exact
+over commutative or local algebras.
+
+## Result
+
+Proofs are in [PROOF.md](PROOF.md).
+
+1. **One factor, every `n` and every algebra:** `cost(M) <= 1` exactly when
+   `delta(M) <= 1`, and then the two are equal.
+2. **Two factors at `n = 2`, every algebra:** `cost(M) <= 2` exactly when some
+   `G, H` in `GL_2(K)` give `N = G M H` with `N12` in the right ideal `N11 R`.
+   With item 1, this decides `cost(M)` in {0, 1, 2, ≥3} for every target.
+3. **Matrix algebras.** Over `R = M_m(K)` the condition reads: some nonzero
+   `phi`, `t` in `K^2` give
+   `rank (phi ⊗ I_m) M = rank (phi ⊗ I_m) M (t ⊗ I_m)`. This answers #4265's
+   question 3 at `n = 2`.
+4. **Local algebras.** If the non-units of `R` form an ideal `J`, every target
+   with an entry outside `J`, in particular every invertible target, costs
+   exactly `delta(M)`. This answers #4265's question 1 at `n = 2` for local
+   algebras and invertible targets. It cannot be extended to every target:
+   over the commutative local algebra `F2[x,y]/(x,y)^2`, 12 targets in
+   `M_2(J)` are unreachable while `delta <= 2`, for example
+   `[[x + y, y], [y, x]]`.
+5. **`F2[S3]`.** The failure lifts. A unital surjection
+   `F2[S3] -> M_2(F_2)` maps words to words, so every lift of a #4265
+   failure costs at least 3 while `delta <= 2`. `verify.py` builds one target
+   of cost exactly 3. Over all `2^24` targets at `n = 2`, exactly **120,060**
+   fail the criterion, so they cost at least 3 against `delta <= 2`. Of these,
+   18,432 = 72 · 4^4 are lifts of `M2(F2)` failures. The rest fail because one
+   pair `(G, H)` must work in both blocks.
+6. **A smaller noncommutative failure.** Over the 3-dimensional algebra
+   `UT2(F2)` of upper triangular matrices, 12 of 4,096 targets cost 3 with
+   `delta = 2`.
+
+| Algebra `R` | Targets (n = 2) | Cost histogram 0/1/2/3 | Unreachable | Criterion failures |
+|---|---:|---|---:|---:|
+| `F2[x,y]/(x,y)^2` (local) | 4,096 | 6 / 549 / 3,529 / 0 | 12 | 12 |
+| `F2 x F2` | 256 | 6 / 117 / 133 / 0 | 0 | 0 |
+| `F2[C3]` | 4,096 | 6 / 549 / 3,541 / 0 | 0 | 0 |
+| `UT2(F2)` | 4,096 | 6 / 549 / 3,529 / 12 | 0 | 12 |
+| `M2(F2)` | 65,536 | 6 / 2,277 / 63,181 / 72 | 0 | 72 |
+| `F2[S3]` (criterion only) | 16,777,216 | — | — | 120,060 |
+
+In every exhaustively searched algebra, the criterion holds exactly on the
+targets of cost at most 2, and every criterion failure costs 3 or is
+unreachable. The 72 `M2(F2)` failures agree with #4265.
+
+Claim types: items 1–4 and the lift in item 5 are proofs for every algebra in
+scope. The counts in the table and items 5–6 are finite certificates. Cost 3 as
+an upper bound is only checked by search on the listed algebras; no general
+three-factor theorem is claimed.
+
+## Method
+
+`verify.py` builds each algebra from a structure table and checks that it is
+associative with `K` central. It precomputes right-ideal membership `z ∈ a R`
+by `F_p`-rank. Stage `main` computes the exact minimum on every target by
+breadth-first search over words `Q S`, computes `delta` over every `T`, and
+asserts: the criterion equals `cost <= 2`, Theorem A, the local statement on
+`F2[x,y]/(x,y)^2` (non-units checked to form an ideal), the rank form over
+`M2(F2)`, and the expected counts. It also checks that `rho` is a surjective
+unital algebra map, lifts a three-factor `M2(F2)` word to `F2[S3]`, and
+asserts that the lifted target fails the criterion. Stage `s3` evaluates the
+criterion on all `2^24` targets over `F2[S3]`. The script writes nothing.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-two-factor-criterion/verify.py --stage main
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-two-factor-criterion/verify.py --stage s3
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-two-factor-criterion
+```
+
+Expected final lines:
+
+```text
+PASS_RIGHT_VECTOR_TWO_FACTOR_CRITERION F2[x,y]/(x,y)^2:4096:12 F2xF2:256:0 F2[C3]:4096:0 UT2(F2):4096:12 M2(F2):65536:72 m2_rank_form=ok f2s3_lift=cost3 no_new_kappa
+PASS_RIGHT_VECTOR_TWO_FACTOR_S3 targets=16777216 three_or_more=120060 no_new_kappa
+```
+
+Each stage takes under 40 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 a formal alphabet. Native frames, hosting, routing, precision and
+recursive cost are not priced, and no supplier changes. Theorems B–D are for
+`n = 2` only. Whether every reachable target at `n = 2` costs at most 3 is
+not proved. The `F2[S3]` count gives cost at least 3; exact costs there are not
+searched. Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+1. **Three factors.** Is every reachable target at `n = 2` reachable with
+   three factors, over every algebra? Characterise the three-factor set as
+   Theorem B does for two; with it, the cost at `n = 2` would be exact.
+2. **Larger `n`.** With `y_1, ..., y_k` a basis, `k` factors are block column
+   operations. Write the `n = 3`, `k = 2` condition as a flag of right
+   ideals and test it by search over `F2[C2]` or `UT2(F2)`.
+3. **Commutative non-local algebras.** Is `delta` exact for invertible
+   targets over every commutative algebra at `n = 2`? A product of local
+   algebras needs one `(G, H)` that works in every factor. Count criterion
+   failures over `F3 x F3 x F3` first.
+
+## Credit
+
+Produced by Nick Petalas. The alphabet, normal form and lower bound come from
+#4243 (`research/right-vector-diagonal-free-basis`); the open questions and the
+`M2(F2)` counts come from #4265 (`research/right-vector-general-target`). 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-two-factor-criterion/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-two-factor-criterion/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 counts in the right-vector alphabet I + u y^T (u in R^n, y in K^n) with free GL_n(K) maps: cost <= 1 for every n and every K-algebra R, an exact two-factor criterion at n = 2 for every R, and its consequences over M_m(K), local algebras and F2[S3]. Answers open questions 2 and 3 of #4265 at n = 2, and open question 1 at n = 2 for local algebras.",
+  "scope_change_reason": "The card asks whether a larger or nonabelian register model escapes the scoped three-register obstruction. This package answers narrower open questions left by #4243 and #4265 about the exact cost in the right-vector alphabet over nonabelian and non-field coefficient algebras.",
+  "bottleneck_link": "Side result in a formal alphabet. It decides which targets cost two right-vector factors at n = 2; it prices no native frame or supplier, and kappa is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Prove the two-factor criterion, check it against exhaustive search on every target of small algebras, settle the F2[S3] lift, then stop.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves Theorems A-D. verify.py --stage main checks the criterion against breadth-first search on all 77,824 targets over five algebras (agreement everywhere; 12 + 72 cost-3 targets over UT2(F2) and M2(F2); 12 unreachable targets over F2[x,y]/(x,y)^2), the local statement, the M_m(K) rank form over M2(F2), and an explicit cost-3 target over F2[S3]. --stage s3 counts 120,060 criterion failures among all 2^24 targets over F2[S3].",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is every reachable target at n = 2 reachable with three factors, for every K-algebra?",
+      "why_it_matters": "Together with Theorem B it would give the exact cost at n = 2. Search finds maximum reachable cost 3 on all five algebras here.",
+      "first_step": "Characterise the three-factor set (G x I)[[A, 0], [B, 1]][[1, C], [0, D]][[E, 0], [F, 1]](H x I) as Theorem B does for two factors.",
+      "blocked_by": "Only the two-factor set is characterised here."
+    },
+    {
+      "question": "What is the cost <= k criterion for n >= 3?",
+      "why_it_matters": "The right-ideal condition of Theorem B should generalise to a flag condition on block-triangular factorizations.",
+      "first_step": "With y_1..y_k a basis, products of k factors are block column operations; write the n = 3, k = 2 condition and test it by search over F2[C2] or UT2(F2).",
+      "blocked_by": "Only n = 2 is proved."
+    },
+    {
+      "question": "Is delta exact for invertible targets over every commutative K-algebra at n = 2?",
+      "why_it_matters": "Theorem D proves it for local algebras; products such as F2 x F2 need one (G, H) that works in every factor at once.",
+      "first_step": "Prove the criterion for invertible M over a product of local algebras with residue field K, or find a counterexample by criterion counting over F3 x F3 x F3.",
+      "blocked_by": "Non-local commutative algebras are only checked on F2 x F2 and F2[C3] (here and in #4265)."
+    }
+  ]
+}

research/right-vector-two-factor-criterion/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": 300,
+      "checks": "Exact minimum by breadth-first search versus the Theorem B criterion on every target over F2[x,y]/(x,y)^2, F2 x F2, F2[C3], UT2(F2) and M2(F2) at n = 2 (77,824 targets); asserts agreement, Theorem A, the local statement, failure counts 12/0/0/12/72, the M_m(K) rank form over M2(F2), and an explicit F2[S3] target of cost 3."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py",
+        "--stage",
+        "s3"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Criterion on all 2^24 targets over F2[S3] at n = 2: exactly 120,060 fail (cost >= 3, delta <= 2), including all 18,432 lifts of the 72 M2(F2) failures."
+    }
+  ]
+}