Prove free basis changes keep the right-vector diagonal count (no new κ)

research/right-vector-diagonal-free-basis/PROOF.md

@@ -0,0 +1,127 @@
+# Free basis changes do not shorten a right-vector diagonal
+
+## Model
+
+Let `K` be a field and `R` an associative unital `K`-algebra with `K` central.
+`R` need not be commutative, finite or local. Fix a register count `n >= 0`.
+A paid factor is
+
+```text
+F = I + u y^T,    u in R^n,    y in K^n.
+```
+
+A free map is any `S` in `GL_n(K)`. A word is
+
+```text
+W = S_0 F_1 S_1 F_2 S_2 ... F_L S_L,
+```
+
+with `L` paid factors and free maps anywhere, including at both ends. Its
+target is `diag(d_1, ..., d_n)` with `d_i` in `R`. Put
+
+```text
+t_K(d) = #{ i : d_i is not in K^x }.
+```
+
+For `K = F_2` the unit group is `{1}`, so `t_K(d)` is the count `t` of entries
+different from 1 used by `research/f2-right-vector-diagonal-minimum`.
+
+**Theorem.** The minimum number of paid factors in a word equal to
+`diag(d)` is exactly `t_K(d)`, for every `n` and every `d` in `R^n`.
+
+This answers that package's first open question: free `GL_n(F_2)` changes of
+basis between paid factors never realize a diagonal with fewer than `t` factors.
+
+## Normal form
+
+Put `A_j = S_0 S_1 ... S_{j-1}` and `S = S_0 S_1 ... S_L`. Then
+
+```text
+W = F'_1 F'_2 ... F'_L S,     F'_j = A_j F_j A_j^{-1}.
+```
+
+Since `A_j` has entries in `K`,
+
+```text
+F'_j = I + (A_j u_j) (A_j^{-T} y_j)^T,
+```
+
+and `A_j^{-T} y_j` lies in `K^n`. So each `F'_j` is again a paid factor.
+Conversely every product `F'_1 ... F'_L S` is a word. Thus the reachable
+endpoints of length `L` are exactly `Q S`, with `Q` a product of `L` paid
+factors and `S` in `GL_n(K)`.
+
+## Column bound
+
+Let `Q = F'_1 ... F'_L` and `Q_j = F'_1 ... F'_j`, `Q_0 = I`. Telescoping,
+
+```text
+Q - I = sum_j Q_{j-1} (F'_j - I) = sum_j c_j y'_j^T,    c_j = Q_{j-1} u'_j in R^n,
+```
+
+where `y'_j` lies in `K^n`. For `w` in `K^n`, `(Q - I) w = sum_j (y'_j . w) c_j`
+is a `K`-combination of the `L` fixed vectors `c_j`. The `K`-linear map
+`w -> (Q - I) w` from `K^n` to `R^n` therefore has image of `K`-dimension at
+most `L`. This is the column argument of `research/f2-right-vector-diagonal-minimum`,
+written for an arbitrary field. Note the right-hand factor `y'^T` multiplies
+`w` before `c_j`; `K` central makes `(y' . w) c_j = c_j (y' . w)`.
+
+## Kernel lemma
+
+Suppose `W = D = diag(d)`. Then `Q = D T` with `T = S^{-1}` in `GL_n(K)`.
+Let `w` in `K^n` satisfy `(D T - I) w = 0`, that is,
+
+```text
+d_i (T w)_i = w_i     for every i.
+```
+
+Both `(T w)_i` and `w_i` lie in `K`. Fix `i` with `d_i` not in `K^x`.
+
+* If `(T w)_i != 0`, then `d_i = w_i (T w)_i^{-1}` lies in `K`. Since `d_i`
+  is not in `K^x`, `d_i = 0`, and then `w_i = d_i (T w)_i = 0`.
+* If `(T w)_i = 0`, the equation gives `w_i = 0`.
+
+So the kernel lies in the coordinate subspace `{ w : w_i = 0 for d_i not in K^x }`,
+whose dimension is `n - t_K(d)`. Rank-nullity over `K` gives
+
+```text
+dim_K (D T - I) K^n >= t_K(d).
+```
+
+## Lower bound
+
+Combining the two displays, `t_K(d) <= dim_K (Q - I) K^n <= L`.
+
+## Matching construction
+
+Let `E = diag(e)` with `e_i = d_i` when `d_i` is in `K^x` and `e_i = 1`
+otherwise. `E` is a free map. For each `i` with `d_i` not in `K^x`, the factor
+`I + (d_i - 1) e_i e_i^T` is paid: its right vector `e_i` is in `K^n`.
+Increments on distinct matrix units multiply to zero, so the product of these
+`t_K(d)` factors is `diag(f)` with `f_i = d_i` off `K^x` and `f_i = 1` on it.
+Then `diag(f) E = diag(d)`. The word has `t_K(d)` paid factors.
+
+## Corollaries and boundaries
+
+* `K = F_2`, any `F_2`-algebra: the exact minimum is `t`, with or without free
+  `GL_n(F_2)` maps. This includes every group algebra `F_2[G]` and the narrower
+  legal alphabet `I + (g - 1) x y^T` with binary `x, y`, `y^T x = 1`, of the
+  `elementary-abelian-diagonal-minimum` and Q8 lineages. Free scalar mixing
+  does not lower the diagonal count in the full nonidentity-label alphabet.
+  Restricted label sets (for example only `{i, j}` in `F_2[Q8]`) can force
+  more factors; that is outside this statement.
+* Over a larger field, free maps absorb scalar diagonal entries. Over `F_3`,
+  `diag(2, 2)` is itself a free map and costs no factor.
+* The `K`-valued right vector is necessary. In `F_2[z_1, z_2]/(z_1^2, z_2^2)`
+  the single factor `I + (z_1, z_2)^T (z_2, z_1)` equals
+  `diag(1 + z_1 z_2, 1 + z_1 z_2)`, so `t = 2` drops to one factor
+  (the witness of `research/f2-right-vector-diagonal-minimum`).
+* Free maps must have entries in `K`. The kernel lemma uses that `T w` is
+  `K`-valued; with `R`-valued free maps the statement is not asserted.
+
+No native frame, hosting, routing, precision or recursive cost is priced. The
+selected multiplication exponent is unchanged.
+
+Produced by Nick Petalas. The column expansion, the right-vector alphabet and
+the sharpness witness are Wentao Li's `research/f2-right-vector-diagonal-minimum`.
+Apache-2.0.

research/right-vector-diagonal-free-basis/README.md

@@ -0,0 +1,113 @@
+# Free basis changes do not shorten a right-vector diagonal
+
+**Scoped proof, with finite controls. No new κ.** Selected κ stays
+`0.001672660197076918`.
+
+Factors are `I + u y^T` with `u` in `R^n` and `y` in `K^n`, over any field `K`
+and any associative `K`-algebra `R`. Free maps are arbitrary `GL_n(K)` changes
+of basis, placed anywhere in the word. The exact number of factors needed for
+`diag(d_1, ..., d_n)` is
+
+```text
+t_K(d) = #{ i : d_i is not in K^x }.
+```
+
+For `K = F_2` this is the count `t` of entries different from 1. So free
+`GL_n(F_2)` mixing never realizes a diagonal with fewer than `t` factors. That
+answers open question 1 of
+[`research/f2-right-vector-diagonal-minimum`](../f2-right-vector-diagonal-minimum/README.md),
+which proved the count without free maps and named the missing invariant as
+the blocker.
+
+## Argument
+
+The written proof is [PROOF.md](PROOF.md). It has three steps:
+
+1. **Normal form.** Conjugating a factor by a free map gives a factor, so every
+   word equals `Q S` with `Q` a product of the same number of factors and `S`
+   one free map.
+2. **Column bound** (from the predecessor). `Q - I` maps `K^n` onto a
+   `K`-space spanned by `L` vectors.
+3. **Kernel lemma** (new). For a diagonal `D` and any `T` in `GL_n(K)`, every
+   kernel vector of `D T - I` on `K^n` vanishes at each `i` with `d_i` not in
+   `K^x`. So the image of `D T - I` has dimension at least `t_K(d)`. Apply it
+   with `Q = D S^{-1}`.
+
+The coordinate factors, followed by one free diagonal map for the entries in
+`K^x`, attain the bound.
+
+Corollaries: every group algebra `F_2[G]`, abelian or not, has exact diagonal
+minimum `t` in the full nonidentity-label alphabet `I + (g - 1) x y^T`, with
+free scalar mixing allowed. Over `F_3`, `diag(2, 2)` costs nothing, because it
+is a free map. Restricted label alphabets, such as `{i, j}` only in `F_2[Q8]`,
+can need more factors. They are outside this statement.
+
+## Finite controls
+
+`verify.py` uses the standard library and writes nothing. It checks:
+
+| Ring | n | Word length | Factors | Free maps | Diagonals reached, each first at length `t_K` |
+|---|---:|---:|---:|---:|---:|
+| `F_2[C_2 x C_2]` | 2 | ≤ 2 | 766 | 6 | 256 of 256 |
+| `F_2[S_3]` (nonabelian) | 2 | ≤ 1 | 12,286 | 6 | 127 (all with `t ≤ 1`) |
+| `F_3[x]/(x^2)` | 2 | ≤ 1 | 321 | 48 | 32 (all with `t_K ≤ 1`) |
+
+It also checks:
+
+- Every conjugate of every factor stays in the alphabet: 93,720 checks.
+- The kernel lemma for every diagonal and every free map: 718,128 cases over
+  the three rings at `n = 2` and the Klein ring at `n = 3`.
+- Over `F_3`, `diag(2, 2)` is reached at length 0.
+- Sharpness of the `K`-valued right vector: the predecessor's ring-valued factor
+  is outside the alphabet and gives `t = 2` from one factor.
+
+These are corroboration, not the proof.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-diagonal-free-basis/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-diagonal-free-basis/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-diagonal-free-basis
+```
+
+Expected final line of `verify.py`:
+
+```text
+PASS_RIGHT_VECTOR_DIAGONAL_FREE_BASIS F2[C2xC2]:n2:L2=256 F2[S3]:n2:L1=127 F3[x]/(x^2):n2:L1=32 no_new_kappa
+```
+
+Each run takes about 20 seconds. The script prints a receipt digest bound to
+its own bytes and to the declared input.
+
+## 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.
+Free maps must have entries in `K`. With `R`-valued free maps the statement is
+not asserted. Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+1. **General targets.** For a non-diagonal target `M`, is the minimum
+   `min_T dim_K (M T - I) K^n` over `T` in `GL_n(K)`? The lower bound follows
+   from the same normal form. The upper bound needs a factorization
+   `I + C Y^T` into factors whose prefixes stay invertible. A first step is a
+   permutation target over `F_2[C_2]` at `n = 2`.
+2. **Restricted labels with free mixing.** Which part of the Q8 `{i, j}` lower
+   bounds survives when the alphabet adds one paid label outside `{i, j}`?
+   This package shows that the full label set gives `t`. Start with a single
+   `[zi]` target.
+3. **Native price.** Bind one coordinate word to an existing supplier meter.
+   This note has no physical schedule.
+
+## Credit
+
+Produced by Nick Petalas. The right-vector alphabet, the column expansion and
+the ring-valued sharpness witness are Wentao Li's
+`research/f2-right-vector-diagonal-minimum` (#4099), which builds on
+`research/bit-cyclic-root-barrier` (#2513). The graded diagonal argument for
+elementary abelian groups is `research/elementary-abelian-diagonal-minimum`
+(#4098). Apache-2.0.

research/right-vector-diagonal-free-basis/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-diagonal-free-basis/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 diagonal minimum for factors I + u y^T (u in R^n, y in K^n) over any K-algebra R when free GL_n(K) maps may appear anywhere in the word: t_K(d), the number of entries outside K^x. Answers open question 1 of research/f2-right-vector-diagonal-minimum.",
+  "scope_change_reason": "The card asks whether a larger or nonabelian register model escapes the scoped three-register obstruction. This package settles a narrower open question left by research/f2-right-vector-diagonal-minimum: whether free scalar basis changes lower the right-vector diagonal count. The answer covers every group algebra F2[G] in the full nonidentity-label alphabet, so no nonabelian group gives a shorter diagonal there.",
+  "bottleneck_link": "A legal diagonal shorter than t would be a new bit primitive. Free scalar mixing does not supply one in this alphabet; this is a side result and kappa is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Prove the normal form, the kernel lemma and the matching construction; corroborate on three small rings (one nonabelian, one over F3) with exhaustive free-map searches; then stop.",
+  "outcome": "completed",
+  "evidence": "PROOF.md is the argument. verify.py exhausts words of length at most 2 over F2[C2xC2] and at most 1 over F2[S3] and F3[x]/(x^2) at n=2, with every free map, checks every conjugate stays in the alphabet (93720 checks), checks the kernel lemma in 718128 cases, and checks the ring-valued sharpness witness.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "For a non-diagonal target M, is the minimum min over T in GL_n(K) of dim_K (M T - I) K^n?",
+      "why_it_matters": "It would give the exact cost of every target in this alphabet, not only diagonals.",
+      "first_step": "Test a permutation target over F2[C2] at n=2 against an exhaustive word search.",
+      "blocked_by": "The upper bound needs a factorization of I + C Y^T whose prefixes stay invertible; none is proved here."
+    },
+    {
+      "question": "Which restricted label sets keep a count above t once free scalar mixing is allowed?",
+      "why_it_matters": "The Q8 {i,j} lower bounds use restricted labels; this package shows the full label set gives exactly t.",
+      "first_step": "Add one paid label outside {i,j} in F2[Q8] and recompute the single [zi] target.",
+      "blocked_by": "Nothing for the formal statement; native conversion remains unpriced."
+    },
+    {
+      "question": "What native frame, hosting and precision bill does one coordinate word pay?",
+      "why_it_matters": "An exact formal call count is not a supplier invoice.",
+      "first_step": "Price one coordinate word on an existing supplier meter.",
+      "blocked_by": "No physical schedule is supplied here."
+    }
+  ]
+}

research/right-vector-diagonal-free-basis/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/f2-right-vector-diagonal-minimum/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Exhaustive free-map word searches on three rings, normal-form closure, kernel lemma, sharpness witness; read-only."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Same checks under -O; admission uses need(), not assert."
+    }
+  ]
+}