Prove three-factor sufficiency for every two-role matrix-algebra target (no new κ)

research/matrix-algebra-three-factor/PROOF.md

@@ -0,0 +1,159 @@
+# Three factors for every full-matrix-algebra target
+
+Let K be any field, let m>=1, and put R=M_m(K). There are two data
+roles. A paid factor is I+u y^T, with u in R^2 and y in K^2.
+Arbitrary GL_2(K) maps are free, including maps at either endpoint.
+The cost of a target M in M_2(R) is the least number of paid factors.
+Ordinary rank below is rank on K^(2m).
+
+## Theorem
+
+Every target M has cost at most three. This includes every singular
+target, with no ordinary-rank restriction. More precisely, after possibly
+swapping its two block rows and its two block columns, M has a factorization
+
+```text
+N = [I  0] [I  B] [E  0]
+    [b  I] [0  d] [F  I].
+```
+
+The right vectors of these three paid factors are e1,e2,e1. No auxiliary
+roles are used. The bound is sharp for every m>=2 and every field.
+
+This extends the invertible semilocal theorem of Nick Petalas #4749 to all
+targets over a single full matrix algebra. It resolves the full-matrix-algebra
+case of the three-factor question in Nick Petalas #4276. The all-algebra
+version is false by #4763's polynomial example. No theorem for singular
+radical extensions or products of matrix algebras is asserted here.
+
+## A classical subspace lemma
+
+Let V and Z be subspaces of a finite-dimensional space W, with
+dim(Z)<=dim(V). Then there is a complement U to V in W such that
+U intersects Z only at zero.
+
+Here is a constructive proof, including the binary field. Start with U=0.
+If dim(U)<dim(W)-dim(V), both V+U and Z+U are proper subspaces of W.
+Their union cannot be W. To see this, choose x outside V+U. If x is outside
+Z+U, use x. Otherwise choose y outside Z+U. If y is outside V+U, use y.
+In the remaining case x+y is outside both subspaces. Adjoin that vector to
+U. Both intersections remain zero. Repeat exactly dim(W)-dim(V) times.
+The resulting U is the required complement.
+
+## Choosing the row and column
+
+Write r=rank(M). The ranks of its two block rows sum to at least r,
+as do the ranks of its two block columns. Choose a block row of rank
+at least r/2 and a block column of rank at least r/2. Independent free
+block swaps put the selected row first and the selected column second.
+Write the transformed matrix as
+
+```text
+N = [A B]
+    [C D].
+```
+
+Let W=im(N), V=im([B;D]), and let pi be projection onto the first K^m
+output block. Set Z=W intersect ker(pi). Then
+
+```text
+dim(Z) = r - rank([A B]) <= rank([B;D]) = dim(V).
+```
+
+The lemma supplies W=U direct-sum V with U intersect ker(pi)=0.
+
+## Lifting the complement to a graph
+
+Let E2=0 direct-sum K^m in the input. Since N(E2)=V and W=U+V,
+the preimage N^(-1)(U) surjects onto K^(2m)/E2. Choose a linear section
+of that surjection. Its image L is a complement to E2 contained in
+N^(-1)(U), so L is the graph of a map -F:K^m -> K^m.
+Equivalently, for each standard input column, solve
+
+```text
+[B;D] F + U X = [A;C].
+```
+
+These equations are solvable because U+V=W. Thus
+
+```text
+N [I;-F] = [A-BF; C-DF]
+```
+
+has image inside U. Projection pi is injective on U, so
+ker(A-BF) is contained in ker(C-DF). A linear map on im(A-BF) therefore
+sends (A-BF)x to (C-DF)x. Extend it to K^m and call the extension b.
+We obtain
+
+```text
+C-DF = b(A-BF).
+```
+
+Define E=A-BF and d=D-bB. Direct multiplication now gives
+
+```text
+[I 0] [I B] [E 0] = [E+BF      B] = [A B].
+[b I] [0 d] [F I]   [bE+DF     D]   [C D]
+```
+
+The factors equal I+(0,b)^T e1^T, I+(B,d-I)^T e2^T, and
+I+(E-I,F)^T e1^T. Their left coefficients belong to R; their right
+vectors belong to K^2. Undoing the free block swaps proves the theorem.
+The zero target is included. One may take b=F=0, E=d=0 in that case.
+
+## Sharpness and exact cost decision
+
+For m>=2, take the identity on K^(2m) and transpose coordinates 1 and
+m+2, leaving every other coordinate fixed. On the first two internal
+coordinates its four blocks are
+
+```text
+A=E22, B=E12, C=E21, D=E11.
+```
+
+The other m-2 internal coordinates carry a two-role identity.
+For every nonzero scalar block row phi, the compressed row (phi tensor I)M
+has rank m, because M is invertible. For every nonzero scalar input t,
+the further compression on the first two internal coordinates is
+
+```text
+[phi2*t2  phi1*t2]
+[phi2*t1  phi1*t1],
+```
+
+of rank one. On the remaining coordinates it is the scalar
+phi1*t1+phi2*t2 times I_(m-2). Its total rank is at most m-1.
+The cited two-factor criterion of #4276 therefore excludes cost at most
+two. The new construction supplies three, proving sharpness. The m=2
+example is already the sharp predecessor example; its extension and the
+universal upper bound are included to state the theorem's full range.
+
+Together with #4276's one/two-factor criteria, the upper bound decides
+every cost. Define delta(M)=min over T in GL_2(K) of dim_K((MT-I)K^2).
+Then cost is delta if delta<=1, is two if delta=2 and some nonzero scalar
+phi,t satisfy
+
+```text
+rank((phi tensor I)M) = rank((phi tensor I)M(t tensor I)),
+```
+
+and is three otherwise. These low-factor criteria are cited predecessor
+theorems, not new claims of this package. For m=1 all targets already cost
+at most two. For m>=2 the maximum is exactly three.
+
+## Scope and credit
+
+The universal statement is a written scoped algebraic proof. The finite
+verifier corroborates the new constructor, not every field or block size.
+No physical cost for coefficient preparation, overwriting, restoration,
+routing, frames, precision or stock is supplied. No new kappa, native
+supplier or complete multiplication theorem follows.
+
+This contribution was produced by Nick Petalas. Nick Petalas #4276
+supplies the exact one/two-factor criteria; #4749 supplies the invertible
+comparison; #4265/#4243 supply the cost question and free-map framework.
+ToikY #4334 supplies the related field-product three-factor construction.
+Wentao Li #4099, following #2513, supplies the alphabet and column bound.
+The subspace-complement lemma, rank inequalities, linear sections and
+extension of a linear map are classical linear algebra. The new result is
+their stated all-target restricted-alphabet consequence. Apache-2.0.

research/matrix-algebra-three-factor/README.md

@@ -0,0 +1,128 @@
+# Three factors for every two-role full-matrix target
+
+Scoped algebraic proof with finite constructive corroboration. For every
+field K, every m>=1 and every target M in M_2(M_m(K)), the paid right-vector
+cost is at most three. Singular targets of every ordinary rank are included.
+For every m>=2 the maximum cost is exactly three. No new kappa is claimed.
+
+The alphabet is I+u y^T with u in M_m(K)^2, y in K^2 and arbitrary free
+GL_2(K) maps anywhere. There are two data roles and no auxiliary roles.
+After free block row and column swaps, the new construction gives
+
+```text
+[A B] = [I 0] [I B] [E 0],
+[C D]   [b I] [0 d] [F I]
+
+E=A-BF, d=D-bB, C-DF=b(A-BF).
+```
+
+[PROOF.md](PROOF.md) chooses a block row and column whose ranks sum to at
+least rank(M). A common complement in im(M) then supplies F and b. The
+classical complement argument works over every field, including F2.
+The three right vectors are e1,e2,e1 in the transformed chart.
+
+This removes the invertible-target hypothesis of Nick Petalas's #4749 for
+a single full matrix algebra and resolves that algebra's case of the
+three-factor question in #4276. Combined with #4276's cited exact zero,
+one and two-factor criteria, it decides every two-role matrix-algebra cost.
+The existing all-algebra question is false by #4763's polynomial examples.
+The finite predecessor censuses and #4789's low-rank classification are
+comparisons, not this contribution's deliverable. No predecessor verifier
+is imported or replayed.
+
+## Evidence
+
+The standard-library verifier implements the complement and graph construction
+directly. Every literal product matches its full target on all 65,536 binary
+4 by 4 matrices. Their rank histogram is [1,225,7350,37800,20160]. The ordered
+factors and free chart choices have SHA256
+`e71204a01c63133a328e47180e395a3563dd0c5266c6c44a3f20a710b2c7c504`.
+This is new constructive evidence for the universal upper bound, rather than
+a new claim about the already known binary optimum.
+
+There are 3,507 additional target executions: all scalar-block two-role
+matrices over F2,F3,F5,F7, plus 24 fixed-seed samples at every combination
+of those fields and m=1,2,3,4. Samples and scalar censuses can overlap;
+3,507 is an execution count, not a count of distinct targets. Twelve
+separate sharp witnesses cover those four fields and m=2,3,4. Each receives
+an attaining word, and the cited two-factor rank criterion rejects it.
+The binary m=2 witness also passes chronological execution on all 16 data
+inputs. Five controls cover inconsistent equations, the binary union-of-two-
+subspaces case, a free target, factor reversal and each factor omission.
+
+The universal statement rests on the written proof. The exhaustive census
+is only over F2,m=2, and the other stated domains are bounded corroboration.
+The replay writes no files. Its generated receipt binds all six package
+files, the two live predecessor documents and the executed results by SHA256.
+Checks remain active under optimized Python. No receipt is handwritten.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/matrix-algebra-three-factor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/matrix-algebra-three-factor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/matrix-algebra-three-factor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/matrix-algebra-three-factor --check-source-history
+```
+
+Any CPython 3.12 installation can replace the local path. Expected marker:
+`PASS_MATRIX_ALGEBRA_THREE_FACTOR binary_targets=65536 additional_targets=3507 sharp_witnesses=12 controls=5 no_new_kappa`.
+Both registered commands run the complete verifier with separate 120-second
+limits. [SOURCES.json](SOURCES.json) pins the exact source bytes.
+
+## Scope and engineering notes
+
+The historical card is connector-alphabet-change, explicitly changed to this
+algebraic side question. Its first working example passed with
+`PASS_UNIVERSAL_CONNECTOR_BOUNDARY pairings=945 max_coverage=31 queries=74 leaves=182`.
+The base is canonical main `624de9dc66858af0945e5f8a0942488d62280d43`,
+priority revision 7. [The advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132042)
+records the target. Live handoffs and PR bodies, main README terms and merged
+PR searches were checked. The overlap helper's sparse local-note coverage is
+incomplete; these searches are not a proof of novelty.
+
+Native coefficient preparation, overwrite ownership, reversible restoration,
+routing, frames, precision, stock and the complete supplier invoice remain
+unknown. More roles, singular radical extensions and simultaneous products
+are outside the theorem. No native supplier, selected-frontier change or
+complete multiplication theorem follows. Independent human and formal
+proof-kernel review are unclaimed. Lean, Docker and the selected operator
+replay were outside scope and were not run.
+
+The replay has no recursion or dynamic evaluation. All functions are below
+60 lines. Its target loops have explicit fixed bounds, with matrices of at
+most eight rows and columns, q in {2,3,5,7}, at most eight complement steps
+and at most eight source manifest entries. It streams the binary census
+without storing target matrices. Python's required dynamic allocation is a
+managed-runtime deviation from static allocation; these fixed matrix domains
+bound live memory. Package reads are capped at one MiB per file. Warning-strict
+normal and optimized replays and in-memory compilation provide diagnostics;
+no separate Python static analyzer is installed in the supplied environment.
+
+## Open next questions
+
+1. Which simultaneous complement conditions suffice for singular targets over
+   a product of full matrix algebras? One free chart must work in every
+   component. Start with two binary M2 components whose preferred swaps
+   conflict and test a common three-direction word. The componentwise rank
+   choices here need not coincide, so the present proof does not answer it.
+2. Can a literal native producer and consumer implement these algebra-valued
+   coefficients with a useful complete invoice? First specify and price
+   coefficient preparation, overwrite ownership, routing and restoration.
+   The unknown physical costs above block any supplier claim.
+
+Structured questions are in [TASK.json](TASK.json).
+
+## Credit
+
+This contribution was produced by Nick Petalas. Nick Petalas #4276 supplies
+the one/two-factor criteria; #4749 supplies the invertible semilocal comparison;
+#4265/#4243 supply the exact-cost question and free-map framework. ToikY #4334
+supplies the related field-product three-factor construction. Wentao Li #4099,
+following #2513, supplies the alphabet and column bound. The complement lemma,
+rank inequalities, linear sections and linear-map extension are classical
+linear algebra. The new claim is their stated all-target restricted-alphabet
+consequence and its literal constructor. Predecessor credit is unchanged.
+Apache-2.0.

research/matrix-algebra-three-factor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/right-vector-semilocal/README.md",
+      "usage": "input",
+      "git_blob": "66f8077f441f31d12685d83554a00c7d420773b5",
+      "sha256": "d0ffb0d8d5f469fb41602a82f76ec62683bd7ca33ef44a83a1170babfca3fea5"
+    },
+    {
+      "path": "research/right-vector-two-factor-criterion/PROOF.md",
+      "usage": "input",
+      "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c",
+      "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895"
+    }
+  ]
+}

research/matrix-algebra-three-factor/TASK.json

@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove a three-factor upper bound for every two-role target over M_m(K), including all singular ranks, and give a literal constructor.",
+  "scope_change_reason": "Self-contained algebraic side question from the right-vector alphabet lineage. It removes the invertible endpoint hypothesis of the semilocal theorem, rather than adding or pricing a native connector operation.",
+  "bottleneck_link": "The formal alphabet separates base-field right vectors from algebra-valued coefficients. A universal factor bound closes its two-role full-matrix target problem; native implementation and the complete recursive invoice remain unknown.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified universal upper bound or record its obstruction; do not extend to more roles or other algebras.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves cost<=3 for all fields and block sizes. verify.py checks the new constructor on all 65536 binary 4x4 targets, 3507 additional cases, 12 sharp witnesses and five controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Which simultaneous complement conditions suffice for singular targets over a product of full matrix algebras?",
+      "why_it_matters": "One common pair of free charts must work in every factor, unlike the single algebra here.",
+      "first_step": "Specify two binary M2 components whose preferred row or column swaps conflict, and test a common three-direction word.",
+      "blocked_by": "The componentwise maximal-rank chart choices in this proof need not coincide."
+    },
+    {
+      "question": "Can one literal native producer and consumer implement these algebra-valued coefficients with a favorable complete invoice?",
+      "why_it_matters": "Formal factor count does not provide a native supplier.",
+      "first_step": "State and price coefficient preparation, overwrite ownership, routing and restoration for one target.",
+      "blocked_by": "Native preparation, restoration, precision and stock costs remain unknown."
+    }
+  ]
+}