From 116992ef72c8aa9f8994137b04395584d3b350e8 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:27:58 +0100 Subject: [PATCH] feat(research): prove rank-one matrix target costs at every role count --- research/right-vector-rank-one/PROOF.md | 87 +++++++ research/right-vector-rank-one/README.md | 128 +++++++++++ research/right-vector-rank-one/SOURCES.json | 30 +++ research/right-vector-rank-one/TASK.json | 68 ++++++ research/right-vector-rank-one/VERIFY.json | 35 +++ research/right-vector-rank-one/verify.py | 237 ++++++++++++++++++++ 6 files changed, 585 insertions(+) create mode 100644 research/right-vector-rank-one/PROOF.md create mode 100644 research/right-vector-rank-one/README.md create mode 100644 research/right-vector-rank-one/SOURCES.json create mode 100644 research/right-vector-rank-one/TASK.json create mode 100644 research/right-vector-rank-one/VERIFY.json create mode 100644 research/right-vector-rank-one/verify.py diff --git a/research/right-vector-rank-one/PROOF.md b/research/right-vector-rank-one/PROOF.md new file mode 100644 index 0000000000..6ac032094c --- /dev/null +++ b/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. diff --git a/research/right-vector-rank-one/README.md b/research/right-vector-rank-one/README.md new file mode 100644 index 0000000000..ae921032dc --- /dev/null +++ b/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. diff --git a/research/right-vector-rank-one/SOURCES.json b/research/right-vector-rank-one/SOURCES.json new file mode 100644 index 0000000000..712d5bf0b7 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/right-vector-rank-one/TASK.json b/research/right-vector-rank-one/TASK.json new file mode 100644 index 0000000000..b8c682d3ab --- /dev/null +++ b/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." + } + ] +} diff --git a/research/right-vector-rank-one/VERIFY.json b/research/right-vector-rank-one/VERIFY.json new file mode 100644 index 0000000000..32153a9ccd --- /dev/null +++ b/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." + } + ] +} diff --git a/research/right-vector-rank-one/verify.py b/research/right-vector-rank-one/verify.py new file mode 100644 index 0000000000..27a9ab5230 --- /dev/null +++ b/research/right-vector-rank-one/verify.py @@ -0,0 +1,237 @@ +#!/usr/bin/env python3 +"""Literal finite corroboration of the rank-one matrix-algebra cost theorem. + +Produced by Nick Petalas. Apache-2.0. No predecessor verifier is imported. +""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def field(q): + need(q in (2, 3, 4), "unsupported finite control field") + add = [[(x + y) % q for y in range(q)] for x in range(q)] + mul = [[(x * y) % q for y in range(q)] for x in range(q)] + if q == 4: + # Polynomial basis F2[t]/(t^2+t+1), encoded as two bits. + add = [[x ^ y for y in range(q)] for x in range(q)] + for x, y in product(range(q), repeat=2): + raw = (x if y & 1 else 0) ^ (x << 1 if y & 2 else 0) + mul[x][y] = raw ^ (7 if raw & 4 else 0) + neg = [next(y for y in range(q) if add[x][y] == 0) for x in range(q)] + inv = [0] + [next(y for y in range(1, q) if mul[x][y] == 1) + for x in range(1, q)] + for x, y in product(range(q), repeat=2): + need(add[x][y] == add[y][x] and mul[x][y] == mul[y][x], "field commutativity") + need(add[x][0] == x and mul[x][1] == x and mul[x][0] == 0, "field identities") + for x, y, z in product(range(q), repeat=3): + need(add[add[x][y]][z] == add[x][add[y][z]], "addition associativity") + need(mul[mul[x][y]][z] == mul[x][mul[y][z]], "multiplication associativity") + need(mul[x][add[y][z]] == add[mul[x][y]][mul[x][z]], "distributivity") + return add, mul, neg, inv + + +def identity(size): + return [[int(i == j) for j in range(size)] for i in range(size)] + + +def mm(left, right, f): + add, mul, _, _ = f + size = len(left) + out = [[0] * size for _ in range(size)] + for i, k in product(range(size), repeat=2): + if left[i][k]: + for j in range(size): + out[i][j] = add[out[i][j]][mul[left[i][k]][right[k][j]]] + return out + + +def mv(matrix, vector, f): + add, mul, _, _ = f + out = [0] * len(vector) + for i, j in product(range(len(vector)), repeat=2): + out[i] = add[out[i]][mul[matrix[i][j]][vector[j]]] + return out + + +def rank(matrix, f): + add, mul, neg, inv = f + rows = [row[:] for row in matrix] + height, width = len(rows), len(rows[0]) + pivot = 0 + for col in range(width): + candidates = [r for r in range(pivot, height) if rows[r][col]] + if not candidates: + continue + r = candidates[0] + rows[pivot], rows[r] = rows[r], rows[pivot] + scale = inv[rows[pivot][col]] + rows[pivot] = [mul[scale][x] for x in rows[pivot]] + for r in range(pivot + 1, height): + scale = rows[r][col] + rows[r] = [add[x][neg[mul[scale][y]]] + for x, y in zip(rows[r], rows[pivot])] + pivot += 1 + if pivot == height: + break + return pivot + + +def factor(left, right, n, m, f): + need(len(left) == n * m and len(right) == n, "factor dimensions") + need(all(len(row) == m for row in left), "left block dimensions") + add, mul, _, _ = f + out = identity(n * m) + for i, j, k in product(range(n * m), range(n), range(m)): + out[i][j * m + k] = add[out[i][j * m + k]][mul[left[i][k]][right[j]]] + return out + + +def outer(a, b, f): + return [[f[1][x][y] for y in b] for x in a] + + +def construction(a, b, n, m, f): + need(1 <= n <= 4 and 1 <= m <= 3 and n * m <= 8, "finite control bounds") + need(len(a) == len(b) == n * m and any(a) and any(b), "rank-one input") + add, mul, neg, inv = f + first = next(j for j in range(n) if any(b[j * m:(j + 1) * m])) + permuted = list(b) + permuted[:m], permuted[first * m:(first + 1) * m] = ( + b[first * m:(first + 1) * m], b[:m]) + h = next(k for k in range(m) if permuted[k]) + left = outer(a, permuted[:m], f) + for k in range(m): + left[k][k] = add[left[k][k]][neg[1]] + words = [(left, [1] + [0] * (n - 1))] + for j in range(1, n): + left = [[0] * m for _ in range(n * m)] + left[h] = [mul[inv[permuted[h]]][x] + for x in permuted[j * m:(j + 1) * m]] + for k in range(m): + left[j * m + k][k] = neg[1] + words.append((left, [int(k == j) for k in range(n)])) + free = identity(n * m) + for k in range(m): + free[k], free[first * m + k] = free[first * m + k], free[k] + return words, free + + +def matrix_word(words, free, n, m, f): + out = identity(n * m) + for left, right in words: + out = mm(out, factor(left, right, n, m, f), f) + return mm(out, free, f) + + +def data_word(words, free, vector, n, m, f): + # Execute the mathematical product on column data in reverse factor order. + add, mul, _, _ = f + state = mv(free, vector, f) + for left, right in reversed(words): + selected = [0] * m + for j, k in product(range(n), range(m)): + selected[k] = add[selected[k]][mul[right[j]][state[j * m + k]]] + change = [0] * (n * m) + for i, k in product(range(n * m), range(m)): + change[i] = add[change[i]][mul[left[i][k]][selected[k]]] + state = [add[x][y] for x, y in zip(state, change)] + return state + + +def check_target(a, b, q, n, m, f): + target = outer(a, b, f) + words, free = construction(a, b, n, m, f) + need(len(words) == n, "unpaid column replacement") + need(matrix_word(words, free, n, m, f) == target, "literal matrix product") + need(rank(target, f) == 1, "ordinary target rank") + need(rank(free, f) == n * m, "free map invertibility") + for left, right in words: + need(all(0 <= x < q for row in left for x in row), "coefficient field") + need(rank(factor(left, right, n, m, f), f) >= (n - 1) * m, + "paid factor nullity exceeds m") + for vector in identity(n * m): + need(data_word(words, free, vector, n, m, f) == mv(target, vector, f), + "independent basis-data execution") + + +def census(q, n, m): + f = field(q) + size = n * m + need(1 <= n <= 4 and 1 <= m <= 3 and q ** size <= 4096, "finite vector capacity") + vectors = tuple(product(range(q), repeat=size)) + normalized = [a for a in vectors if any(a) and next(x for x in a if x) == 1] + count = 0 + for a in normalized: + for b in vectors[1:]: + check_target(a, b, q, n, m, f) + count += 1 + expected = (q ** size - 1) ** 2 // (q - 1) + need(count == expected, "rank-one enumeration count") + return {"q": q, "n": n, "m": m, "rank_one_targets": count, "exact_cost": n} + + +def controls(): + n, m, f = 2, 2, field(3) + a, b = (1, 0, 0, 1), (1, 0, 0, 1) + words, free = construction(a, b, n, m, f) + target = outer(a, b, f) + need(matrix_word(words[:-1], free, n, m, f) != target, "dropped-factor control") + need(matrix_word(words[::-1], free, n, m, f) != target, "reversed-word control") + left, right = words[1] + changed = [row[:] for row in left] + changed[2][0] = changed[3][1] = 1 + need(matrix_word([words[0], (changed, right)], free, n, m, f) != target, + "odd-field sign control") + changed = [row[:] for row in left] + changed[0][:], changed[1][:] = [0, 0], [1, 0] + need(matrix_word([words[0], (changed, right)], free, n, m, f) != target, + "wrong right-ideal multiplication control") + b = (0, 0, 1, 1) + words, free = construction(a, b, n, m, f) + need(matrix_word(words, identity(4), n, m, f) != outer(a, b, f), + "missing free input permutation control") + for omitted in range(n): + remaining = words[:omitted] + words[omitted + 1:] + need(rank(matrix_word(remaining, free, n, m, f), f) >= m, + "n-minus-one rank-loss control") + zero_words = [] + for j in range(n): + left = [[0] * m for _ in range(n * m)] + for k in range(m): + left[j * m + k][k] = f[2][1] + zero_words.append((left, [int(k == j) for k in range(n)])) + need(matrix_word(zero_words, identity(4), n, m, f) == [[0] * 4 for _ in range(4)], + "predecessor zero-target boundary") + scalar = [[1, 0], [0, 0]] + need(rank(scalar, f) == 1 and scalar == factor([[0], [2]], [0, 1], 2, 1, f), + "m-equals-one has cost n-minus-one") + return 9 + + +def main(): + cases = [(2, 1, 2), (2, 2, 2), (3, 2, 2), (4, 2, 2), (2, 3, 2), (2, 2, 3)] + results = [census(q, n, m) for q, n, m in cases] + boundary_controls = controls() + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + receipt = {"results": results, "controls": boundary_controls, + "files": {name: sha256((package / name).read_bytes()).hexdigest() + for name in names}} + encoded = json.dumps(receipt, sort_keys=True, separators=(",", ":")).encode() + print(json.dumps(receipt, sort_keys=True)) + print("PASS_RIGHT_VECTOR_RANK_ONE", + "targets=" + str(sum(row["rank_one_targets"] for row in results)), + "controls=" + str(boundary_controls), "receipt=" + sha256(encoded).hexdigest(), + "no_new_kappa") + + +if __name__ == "__main__": + main()