[petalas]

Result

Scoped proofs with finite certificates. No new κ. This answers open questions 2 and 3 of #4265 at n = 2, and question 1 at n = 2 for local algebras. The alphabet is #4243's: paid factors I + u y^T with u in R^n and y in K^n, plus free GL_n(K) maps. Package: research/right-vector-two-factor-criterion. Proofs are in PROOF.md.

• One factor, every n, every algebra: cost(M) <= 1 iff delta(M) <= 1, and then the two are equal.
• Two factors at n = 2, every algebra: cost(M) <= 2 iff some G, H in GL_2(K) give N = G M H with N12 in the right ideal N11 R. With the first item, this decides cost in {0, 1, 2, ≥3}.
• Over M_m(K): the condition is rank (phi ⊗ I_m) M = rank (phi ⊗ I_m) M (t ⊗ I_m) for some nonzero phi, t.
• Local algebras: every target with a unit entry, in particular every invertible target, costs exactly delta. This does not extend to every target. Over the commutative local F2[x,y]/(x,y)^2, 12 targets in M_2(J), e.g. [[x + y, y], [y, x]], are unreachable while delta <= 2.
• F2[S3]: the Refute the right-vector general-target formula: M2(F2) targets need 3 factors, not 2 (no new κ) #4265 failure lifts through the surjection F2[S3] -> M_2(F_2). An explicit lifted target costs exactly 3. Of all 2^24 targets, 120,060 fail the criterion (cost ≥ 3, delta <= 2). Of these, 18,432 = 72 · 4^4 are lifts of M2(F2) failures.
• Smaller noncommutative failure: over the 3-dimensional UT2(F2), 12 of 4,096 targets cost 3 with delta = 2.

The theorems are proofs for every algebra in scope. The counts are finite certificates.

Evidence and reproduction

verify.py --stage main computes exact minima by breadth-first search on all 77,824 targets over F2[x,y]/(x,y)^2, F2 x F2, F2[C3], UT2(F2) and M2(F2) at n = 2. It asserts that the criterion equals cost <= 2, plus Theorem A, the local statement, the M_m(K) rank form, the failure counts, and the F2[S3] lift. --stage s3 evaluates the criterion on every F2[S3] target.

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

Local results (CPython 3.12, NumPy 2.5.4, macOS arm64): --stage main prints 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 in about 25 s. --stage s3 prints PASS_RIGHT_VECTOR_TWO_FACTOR_S3 targets=16777216 three_or_more=120060 no_new_kappa in about 37 s. research_package.py prints PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed in 63 s for both stages. check_research_commit.py prints PASS_RESEARCH_COMMIT_BYTES.

Limits

This is a formal alphabet. Native frames, hosting, routing, precision and recursive cost are not priced, and no supplier changes. Theorems B–D cover n = 2 only. A general three-factor bound is not proved; cost ≤ 3 on reachable targets is checked only on the five searched algebras. Exact costs over F2[S3] beyond "at least 3" are not searched. No registered proof obligation is left unrun. Independent human and formal proof-kernel review are unclaimed.

Open next questions

1. 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.
2. What is the k-factor condition for n >= 3? It should be a flag of right ideals. Test n = 3, k = 2 by search.
3. Is delta exact for invertible targets over every commutative algebra at n = 2? Products of local algebras need a single (G, H) for all factors. Try criterion counting over F3 x F3 x F3.

Related open work

• Refute the right-vector general-target formula: M2(F2) targets need 3 factors, not 2 (no new κ) #4265 (research/right-vector-general-target) asked questions 1–3 answered here. Its 72 M2(F2) failures at n = 2 agree with the 72 criterion failures here, and its F2 x F2 and F2[C3] results (cost = delta on every target) agree with 0 failures here. Both checked numerically.
• Prove free basis changes keep the right-vector diagonal count (no new κ) #4243 (research/right-vector-diagonal-free-basis) gives the alphabet, normal form and lower bound used here. Diagonal targets are not separately rerun.
• No other open PR studies this alphabet. I checked the open PR list, a right-vector/F2[S3] search, merged package READMEs and recent handoff claims. Add S3 three-register rank lower bound #3893 (S3 three-register rank bound) studies a different model.

CI notes

Hosted CI is green on head 59c7bac0122ef2b80793c30a3d52329db6bdf17d: run 39524565982. plan passed in 2m47s and the package replay in 3m0s. No check failed.

Credit

Produced by Nick Petalas. The alphabet, normal form and lower bound come from #4243. The open questions and M2(F2) counts come from #4265. 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.