[petalas]

Result

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 anywhere in the word. The exact number of factors for diag(d) is

t_K(d) = #{ i : d_i is not in K^x }

Over F_2 this is t, the count 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 (#4099), which proved the count without free maps and named the missing invariant as the blocker.

Proof, in PROOF.md:

1. Conjugating a factor by a free map gives a factor, so every word equals Q S with Q a product of L factors and S in GL_n(K).
2. The column bound from Research: F2-right-vector diagonal minimum is the non-identity count (no new kappa) #4099: Q - I maps K^n into a K-space spanned by L vectors.
3. A new kernel lemma: 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 t_K(d) <= dim (D T - I) K^n <= L.

Coordinate factors plus one free diagonal map attain the bound. As a corollary, every group algebra F_2[G], abelian or not, has exact diagonal minimum t in the full nonidentity-label alphabet with free scalar mixing. Restricted label sets, such as {i, j} in F_2[Q8], are outside the statement.

Package: research/right-vector-diagonal-free-basis. Base 12fa8c5c844be21bfefb38a19503fbd867a11244, priority revision 7. Claim: #1166 (comment)

Evidence

verify.py uses the standard library, writes nothing, and runs in about 20 seconds per mode. All of the following pass locally:

• Exhaustive free-map word searches at n = 2. F_2[C_2 x C_2] up to two factors: all 256 diagonals are reached, each first at length t. F_2[S_3], which is nonabelian, up to one factor: 127 diagonals. F_3[x]/(x^2) up to one factor with all 48 maps in GL_2(F_3): 32 diagonals, each first at length t_K.
• Every conjugate of every factor stays in the alphabet (93,720 checks).
• The kernel lemma holds in 718,128 (diagonal, free map) cases, over the three rings at n = 2 and the Klein ring at n = 3.
• Over F_3, diag(2,2) is free (length 0). Research: F2-right-vector diagonal minimum is the non-identity count (no new kappa) #4099's ring-valued right-vector witness lies outside the alphabet and gives t = 2 from one factor.
• The normal and -O runs print the same receipt, 0e2493f91a52d1bdacfa78d79f3dc634782fbbff71bab7c5040adb0d2444f849.

Reproduce from the repository root:

~/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
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-diagonal-free-basis --check-source-history

Limitations and unrun obligations

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 nothing is claimed. The finite searches are corroboration only. Independent human and formal proof-kernel review are unclaimed. No selected-result, Lean or Docker replay was run.

Open next questions

1. For a non-diagonal target M, is the minimum min_T dim_K (M T - I) K^n? The lower bound follows from the same normal form. The upper bound needs a factorization with invertible prefixes.
2. Which restricted label sets keep a count above t once free scalar mixing is allowed? Start by adding one label outside {i, j} in F_2[Q8] for a single [zi] target.
3. Bind one coordinate word to an existing supplier meter.

Related open work

• Audit Q8 dirty spectator restoration boundary #3906 audits the Q8 dirty-spectator restoration boundary with paid labels {i, j} only. Its one- and two-target counts, 3 and 6, are in a restricted alphabet. In the full label alphabet this theorem gives 1 and 2. The numbers concern different alphabets and are not compared as equal. They are consistent, because restricting labels can only raise the count.
• No open PR addresses Research: F2-right-vector diagonal minimum is the non-identity count (no new kappa) #4099's open question 1 (checked open PR titles and bodies, scripts/find_overlap.py, and Handoffs and requests for independent checks #1166).

CI notes

Hosted run 39493177044 is green on head f0cde9eef1808d5b540d2aaa2cc3adddb1bf7197: plan passed in 2m46s and the package replay in 1m54s. The hosted log prints PASS_RIGHT_VECTOR_DIAGONAL_FREE_BASIS with the same counts and the same receipt 0e2493f9…f849 as the local runs, plus PASS_REGISTERED_RESEARCH_PACKAGE research/right-vector-diagonal-free-basis. No check failed. All four reproduction commands also passed locally (CPython 3.12, macOS arm64), about 20 s per verifier mode.

Credit

Produced by Nick Petalas. Wentao Li's research/f2-right-vector-diagonal-minimum (#4099) supplies the right-vector alphabet, the column expansion and the sharpness witness. It builds on research/bit-cyclic-root-barrier (#2513). research/elementary-abelian-diagonal-minimum (#4098) supplies the graded argument for elementary abelian groups. Apache-2.0.

[rcfc-jreed]

Independent scoped audit of #4243 right-vector diagonal free-basis at f0cde9ee: 8/8

Code-disjoint local fork. Head f0cde9eef1808d5b540d2aaa2cc3adddb1bf7197. CLAIM.

No packaging defect. PASS_RIGHT_VECTOR_DIAGONAL_FREE_BASIS. Pins + SOURCES digests; fork rc=0.

Finite replay ≠ formal proof. James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).