Prove exact rank-one matrix-algebra cost at every role count (no new κ)

research/right-vector-rank-one/PROOF.md

@@ -0,0 +1,87 @@
+# Exact cost of an ordinary rank-one target
+
+Let K be any field, R=M_m(K), m>=2, and n>=1. A paid factor is
+P(u,y)=I_n+u y^T, where u belongs to R^n and y belongs to K^n. Free maps
+are GL_n(K), acting as S tensor I_m. Cost counts paid factors in an arbitrary
+word of paid and free maps. The target M is an nm by nm matrix, partitioned
+into n by n blocks of size m. Rank in this note always means ordinary K-rank
+on K^(nm), rather than the predecessor's column-image dimension on K^n.
+
+**Theorem.** If rank_K(M)=1, then cost(M)=n. There is an attaining word with
+n paid factors and one free input-block permutation, without scratch roles.
+
+The ordinary rank inequalities below are classical. The contribution is their
+application to this restricted-right-vector alphabet and the attaining word
+for every ordinary rank-one matrix-algebra target at every role count. The
+alphabet and exact-cost questions are inherited from #4099/#4243/#4265/#4276.
+
+## Lower bound, including arbitrary free maps
+
+For y nonzero, P(u,y) fixes (ker y^T) tensor K^m pointwise. That subspace has
+dimension (n-1)m, so rank P(u,y)>=(n-1)m. If y=0 the factor is the identity.
+Thus each paid factor has nullity at most m. Each free map has nullity zero.
+
+For square matrices of common size N, Sylvester's inequality gives
+
+    nullity(A B) <= nullity(A) + nullity(B).
+
+Induction along any word with k paid factors, allowing any number and position
+of free maps, therefore gives rank M >= nm-km. If k<=n-1, rank M>=m>=2,
+which contradicts rank M=1. Hence cost(M)>=n. In fact this proves the same
+lower bound for every target with ordinary rank strictly below m.
+
+## Attaining word
+
+Write M=a b, where a is a nonzero column of length nm and b is a nonzero row
+of length nm. Write a_i and b_j for their length-m blocks, so M_ij=a_i b_j.
+Choose a nonzero block b_j. A free permutation of the input blocks moves it
+to b_1. In this paragraph M denotes that permuted target; undo the permutation
+at the right endpoint at no paid cost.
+
+Choose an internal coordinate h with b_1[h]!=0. For j=2,...,n, define the
+m by m matrix
+
+    C_j = e_h b_j / b_1[h].
+
+Then b_1 C_j=b_j. Define F_1 to equal I_n with its first block column
+replaced by (a_1 b_1,...,a_n b_1)^T. This is the allowed paid factor
+
+    F_1 = I_n + u_1 e_1^T,
+    (u_1)_i = a_i b_1 - delta_(i,1) I_m.
+
+For each j>=2 define F_j to equal I_n with its j-th block column replaced
+by e_1 C_j. Equivalently,
+
+    F_j = I_n + u_j e_j^T,
+    (u_j)_1=C_j, (u_j)_j=-I_m, all other blocks zero.
+
+Right multiplication by F_j replaces block column j by block column 1
+times C_j, and preserves every other block column. Starting from F_1,
+successive right multiplication by F_2,...,F_n therefore gives columns
+
+    a b_1, a b_1 C_2, ..., a b_1 C_n
+    = a b_1, a b_2, ..., a b_n.
+
+Consequently F_1 F_2 ... F_n=M. The displayed product is a matrix product;
+on column data its chronological execution is F_n,...,F_1, after the free
+input permutation at the right endpoint. All right vectors e_j are over K.
+The left coefficients belong to R, as permitted. The formula also covers
+n=1 with only F_1. This proves cost(M)<=n and completes the theorem.
+
+## Boundary controls and scope
+
+The zero target also has cost n, by the same rank bound and n coordinate
+zeroing factors. This zero-target fact is already a case of #4243's diagonal
+theorem and is not claimed as new.
+
+The assumption m>=2 matters. At m=1 every nonzero rank-one target has cost
+n-1: free left/right field basis changes reduce it to diag(1,0,...,0),
+and ordinary nullity gives the matching lower bound. This also follows from
+the predecessor diagonal theorem. Free maps of the theorem are always
+S tensor I_m. Its lower bound also survives arbitrary invertible maps on
+K^(nm), since such maps have nullity zero.
+
+These are singular formal targets. Their overwrite behavior discards data.
+No reversible dirty-helper restoration, native coefficient preparation,
+physical routing, precision, stock or complete supplier invoice is supplied.
+No multiplication theorem or exponent improvement follows.

research/right-vector-rank-one/README.md

@@ -0,0 +1,128 @@
+# Exact right-vector cost of ordinary rank-one matrix targets
+
+Scoped proof with finite corroboration. For every field K, every matrix size
+m>=2 and every role count n>=1, every target M in M_n(M_m(K)) of ordinary
+K-rank one has exact paid cost
+
+```text
+cost(M) = n.
+```
+
+Paid factors are I+u y^T with u in M_m(K)^n and y in K^n. Free GL_n(K) maps
+may occur anywhere. Rank here means rank on K^(nm). It is not the
+column-image dimension on K^n used in the earlier delta invariant. There is
+no new kappa or selected-frontier change.
+
+[PROOF.md](PROOF.md) gives the proof and explicit factors. Each paid factor
+has nullity at most m, so n-1 paid factors cannot reach rank below m.
+Conversely, write M=a b. After moving one nonzero block b_1 to the first
+position, replace column 1 by a b_1 and then replace each column j by column
+1 times C_j, where b_1 C_j=b_j. All n replacements are legal paid factors.
+This is a singular family for arbitrary role counts, extending the
+noncommutative exact-cost questions of #4265 and #4276. The classical rank
+inequality and rank-one matrix count are not claimed as new.
+
+## Exact finite evidence
+
+The standard-library verifier enumerates each rank-one target exactly once:
+normalize the first nonzero coordinate of a to one and take every nonzero b.
+The classical count is (q^(nm)-1)^2/(q-1). It checks the literal flattened
+matrix product, each factor's rank bound and a separate chronological
+block-vector interpreter on every standard basis input. Linearity then
+covers every data input for each enumerated target.
+
+| Field | Roles n | Block size m | Enumerated targets | Exact paid cost |
+|---|---:|---:|---:|---:|
+| F2 | 1 | 2 | 9 | 1 |
+| F2 | 2 | 2 | 225 | 2 |
+| F3 | 2 | 2 | 3,200 | 2 |
+| F4 | 2 | 2 | 21,675 | 2 |
+| F2 | 3 | 2 | 3,969 | 3 |
+| F2 | 2 | 3 | 3,969 | 2 |
+
+There are 33,047 targets across the six domains. F4 is implemented in the
+polynomial basis F2[t]/(t^2+t+1), with complete finite field-law checks.
+Nine discriminating controls check a dropped factor, reversed order, the
+odd-characteristic sign, multiplication on the wrong side, the omitted
+input permutation, each of two n-1-factor deletions, the predecessor zero
+target and the scalar-block boundary. At m=1 a nonzero rank-one target has
+cost n-1, as already follows from the predecessor diagonal theorem.
+
+The verifier writes nothing. It generates a receipt from the six package
+file hashes and computed results. Warning-strict normal and optimized runs
+execute the same explicit checks; no check depends on Python assertions.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library only:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-rank-one/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-rank-one/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-rank-one
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-rank-one --check-source-history
+```
+
+Any CPython 3.12 installation can replace the local interpreter path. Expected
+marker: `PASS_RIGHT_VECTOR_RANK_ONE targets=33047 controls=9`, followed by a
+generated receipt digest and `no_new_kappa`. The package runner ends with
+`PASS_REGISTERED_RESEARCH_PACKAGE`.
+
+## Provenance and scope
+
+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 package base is canonical main 1f87c3578ae546c8f903f7f4d83dc2e2fb99650b,
+priority revision 7. [SOURCES.json](SOURCES.json) pins that
+base, the full card, selected provenance and two predecessor documents.
+Neither predecessor verifier is imported or replayed as this contribution.
+
+[The advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131172)
+reserves this question. Live open PR bodies, recent handoffs, main READMEs
+and distinctive merged searches were checked. The initial overlap helper
+reported complete pagination for 426 open PRs and 3,684 Discussion records;
+sparse local coverage was 49 records of 6,061 HEAD candidates. This is search
+coverage, not a proof of novelty.
+
+This is a formal alphabet with singular, data-discarding factors. Native
+coefficient preparation, reversible dirty-state restoration, frames, routing,
+precision, stock and the complete recursive invoice are unknown. It does
+not produce a native supplier or complete multiplication theorem. No Lean,
+Docker or selected-construction replay is required or claimed. Independent
+human and formal proof-kernel review are unclaimed.
+
+The finite verifier is bounded to q in {2,3,4}, n<=4, m<=3 and nm<=8, with
+at most 4,096 stored vectors. The six actual census domains have nm<=6.
+All calls are direct and nonrecursive; functions stay below 60 lines.
+Python allocates bounded temporary lists during replay, a managed-runtime
+deviation from fixed preallocation. It holds one target and word at a time,
+rather than all target matrices. Explicit checks remain enabled under -O.
+No language-specific static analyzer is required by this package; the
+registered warning-strict replays are its executable diagnostics.
+
+## Open next questions
+
+1. Which targets of ordinary rank 2 through m-1 still cost n? This would
+   locate the first obstruction to a higher-rank singular extension. Start
+   with m=3, n=2 and the block-restriction rank criterion of #4276. A higher
+   dimensional row space need not have one block retaining its whole rank.
+2. Can a literal native producer and consumer implement these column
+   replacements with a favorable full invoice? First specify one matrix
+   coefficient's preparation, overwrite, routing and restoration contract.
+   All physical costs remain unknown; this note does not justify a supplier
+   construction campaign.
+
+The structured questions and blockers are in [TASK.json](TASK.json).
+
+## Credit
+
+This contribution was produced by Nick Petalas. Nick Petalas's #4276 and
+#4265 supply the exact-cost questions, and #4243 supplies the free-map normal
+form and diagonal boundary. Wentao Li's #4099 supplies the right-vector
+alphabet and column bound, following #2513. ToikY's #4334 supplies the
+commutative-product comparison. The current invertible matrix-block
+extension is Nick Petalas's #4749; this note concerns singular targets.
+Ordinary matrix rank inequalities, rank-one decomposition and finite-field
+rank-one counts are classical. All predecessor credit remains unchanged.
+Apache-2.0.

research/right-vector-rank-one/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b",
+  "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-general-target/README.md",
+      "usage": "input",
+      "git_blob": "3134451a6d39f116801b8ad6a965115e6c923ced",
+      "sha256": "deffed632430c26e65872ee972b7eaa78e0bd2f3c0f0ab8c772f44e447b536c8"
+    },
+    {
+      "path": "research/right-vector-two-factor-criterion/PROOF.md",
+      "usage": "input",
+      "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c",
+      "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895"
+    }
+  ]
+}

research/right-vector-rank-one/TASK.json

@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b",
+  "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 exact paid cost n for every ordinary rank-one target in M_n(M_m(K)), m>=2, for every field K and every positive role count n.",
+  "scope_change_reason": "This takes the arbitrary-role noncommutative cost question of PR4276 and PR4265 as a singular matrix-algebra side result. It does not add an operation to the original connector alphabet or claim a complete physical budget.",
+  "bottleneck_link": "A formal exact-cost family in the relaxed algebra-valued alphabet. It identifies the full n-call cost of low ordinary-rank singular targets; it supplies no native coefficient preparation or recursive supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first written exact family and a bounded literal-word verification; leave higher-rank and native questions open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives an all-field rank-loss lower bound and n-factor construction. verify.py enumerates rank-one targets over F2, F3 and F4, checks literal factors, block-matrix products and independent vector action, plus rejection and sharpness controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Which targets of ordinary rank 2 through m-1 have paid cost n over M_m(K)?",
+      "why_it_matters": "This would locate the first obstruction to extending the singular exact-cost family beyond rank one.",
+      "first_step": "For m=3 and n=2, test whether an ordinary rank-two target has an input block restriction retaining its complete row-space rank, using PR4276 Corollary C.",
+      "blocked_by": "A rank-one row always has a nonzero block; the higher-rank simultaneous block condition is not automatic."
+    },
+    {
+      "question": "Can one literal native producer and consumer realize these algebra-valued column replacements at their charged cost?",
+      "why_it_matters": "A formal word does not price a recursive supplier.",
+      "first_step": "Choose one actual matrix coefficient and record its preparation, overwrite, routing and restoration contract before any construction expansion.",
+      "blocked_by": "All native implementation and complete invoice costs are unknown."
+    }
+  ]
+}

research/right-vector-rank-one/VERIFY.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/right-vector-general-target/README.md",
+    "research/right-vector-two-factor-criterion/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "All enumerated literal words, independent arbitrary-input basis actions, exact rank-one counts and meaningful negative controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Repeat every check with assertions disabled; explicit contracts must still enforce all evidence."
+    }
+  ]
+}