From fbf2bd033f2d3ae1605a3cad690e1fc2fbf477e7 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 21:20:25 +0100 Subject: [PATCH] feat(research): bound every matrix-algebra target by three factors --- research/matrix-algebra-three-factor/PROOF.md | 159 ++++++++++ .../matrix-algebra-three-factor/README.md | 128 ++++++++ .../matrix-algebra-three-factor/SOURCES.json | 30 ++ .../matrix-algebra-three-factor/TASK.json | 68 +++++ .../matrix-algebra-three-factor/VERIFY.json | 35 +++ .../matrix-algebra-three-factor/verify.py | 281 ++++++++++++++++++ 6 files changed, 701 insertions(+) create mode 100644 research/matrix-algebra-three-factor/PROOF.md create mode 100644 research/matrix-algebra-three-factor/README.md create mode 100644 research/matrix-algebra-three-factor/SOURCES.json create mode 100644 research/matrix-algebra-three-factor/TASK.json create mode 100644 research/matrix-algebra-three-factor/VERIFY.json create mode 100644 research/matrix-algebra-three-factor/verify.py diff --git a/research/matrix-algebra-three-factor/PROOF.md b/research/matrix-algebra-three-factor/PROOF.md new file mode 100644 index 0000000000..b134eed43d --- /dev/null +++ b/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) 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. diff --git a/research/matrix-algebra-three-factor/README.md b/research/matrix-algebra-three-factor/README.md new file mode 100644 index 0000000000..9106fc5d0f --- /dev/null +++ b/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. diff --git a/research/matrix-algebra-three-factor/SOURCES.json b/research/matrix-algebra-three-factor/SOURCES.json new file mode 100644 index 0000000000..519ba3a5df --- /dev/null +++ b/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" + } + ] +} diff --git a/research/matrix-algebra-three-factor/TASK.json b/research/matrix-algebra-three-factor/TASK.json new file mode 100644 index 0000000000..34166cca02 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/matrix-algebra-three-factor/VERIFY.json b/research/matrix-algebra-three-factor/VERIFY.json new file mode 100644 index 0000000000..583fb3feca --- /dev/null +++ b/research/matrix-algebra-three-factor/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/right-vector-semilocal/README.md", + "research/right-vector-two-factor-criterion/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal three-factor construction on all 65536 binary 4x4 targets, further prime-field cases, sharp witnesses, order/omission/solver/complement/free controls and generated file-bound receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same full corroboration and controls with Python assertions disabled." + } + ] +} diff --git a/research/matrix-algebra-three-factor/verify.py b/research/matrix-algebra-three-factor/verify.py new file mode 100644 index 0000000000..e9dfe58a3e --- /dev/null +++ b/research/matrix-algebra-three-factor/verify.py @@ -0,0 +1,281 @@ +#!/usr/bin/env python3 +"""Bounded constructive corroboration of the all-target three-factor theorem.""" + +import hashlib +import itertools +import json +from pathlib import Path +import random + + +def check(condition, message): + if not condition: + raise RuntimeError(message) + + +def add(a, b, q): + return tuple((x + y) % q for x, y in zip(a, b, strict=True)) + + +def scale(c, a, q): + return tuple(c * x % q for x in a) + + +def basis(vectors, q): + """Reduced row basis, also used for column spaces represented as vectors.""" + rows = [] + pivots = [] + for vector in vectors: + v = vector + for p, row in zip(pivots, rows, strict=True): + v = add(v, scale(-v[p], row, q), q) + p = next((i for i, x in enumerate(v) if x), None) + if p is None: + continue + v = scale(pow(v[p], -1, q), v, q) + for i, row in enumerate(rows): + rows[i] = add(row, scale(-row[p], v, q), q) + at = sum(old < p for old in pivots) + pivots.insert(at, p) + rows.insert(at, v) + return rows + + +def inside(v, space, q): + return len(basis([*space, v], q)) == len(space) + + +def columns(a): + return list(zip(*a, strict=True)) + + +def transpose(a): + return tuple(columns(a)) + + +def matmul(a, b, q): + return tuple(tuple(sum(x * y for x, y in zip(row, col, strict=True)) % q + for col in columns(b)) for row in a) + + +def identity(n): + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def solve(a, rhs, q): + """Return one solution with free coordinates zero, or None.""" + n = len(a[0]) + rows = basis([(*row, y) for row, y in zip(a, rhs, strict=True)], q) + if any(not any(row[:n]) and row[n] for row in rows): + return None + answer = [0] * n + for row in rows: + p = next((i for i in range(n) if row[i]), None) + if p is not None: + answer[p] = row[n] + check(matmul(a, transpose([answer]), q) == tuple((x,) for x in rhs), + "linear solver returned a false solution") + return tuple(answer) + + +def kernel(a, q): + n = len(a[0]) + rows = basis(a, q) + pivots = [next(i for i, x in enumerate(row) if x) for row in rows] + result = [] + for free in range(n): + if free in pivots: + continue + v = [int(i == free) for i in range(n)] + for p, row in zip(pivots, rows, strict=True): + v[p] = -row[free] % q + result.append(tuple(v)) + return result + + +def common_complement(w, v, k, q): + """Complement v inside w while avoiding k, where dim(k)<=dim(v).""" + check(len(k) <= len(v) <= len(w), "bad complement dimensions") + u = [] + for _ in range(len(w) - len(v)): + av, ak = basis([*v, *u], q), basis([*k, *u], q) + x = next(z for z in w if not inside(z, av, q)) + if inside(x, ak, q): + y = next(z for z in w if not inside(z, ak, q)) + x = add(x, y, q) if inside(y, av, q) else y + check(not inside(x, av, q) and not inside(x, ak, q), + "common-complement step failed") + u.append(x) + check(len(basis([*v, *u], q)) == len(w), "not a complement") + check(len(basis([*k, *u], q)) == len(k) + len(u), "kernel intersection") + return u + + +def chart(a, row_swap, col_swap): + m = len(a) // 2 + rows = list(range(m, 2*m)) + list(range(m)) if row_swap else list(range(2*m)) + cols = list(range(m, 2*m)) + list(range(m)) if col_swap else list(range(2*m)) + return tuple(tuple(a[i][j] for j in cols) for i in rows) + + +def join(x, y): + return tuple((*r, *s) for r, s in zip(x, y, strict=True)) + + +def construct(a, q): + """Choose ranks, construct the graph, then return three legal factors.""" + m = len(a) // 2 + check(q in (2, 3, 5, 7) and 1 <= m <= 4 and len(a) == 2*m, + "verifier domain exceeded") + check(all(len(row) == 2*m and all(0 <= x < q for x in row) for row in a), + "invalid field matrix") + row_ranks = [len(basis(a[i*m:(i+1)*m], q)) for i in range(2)] + col_ranks = [len(basis([v[i*m:(i+1)*m] for v in a], q)) for i in range(2)] + rs, cs = row_ranks[1] > row_ranks[0], col_ranks[0] > col_ranks[1] + n = chart(a, rs, cs) + w = basis(columns(n), q) + v = basis(columns(n)[m:], q) + if not w: + f = tuple((0,) * m for _ in range(m)) + else: + wm = transpose(w) + k = [tuple(z[0] for z in matmul(wm, transpose([c]), q)) + for c in kernel(wm[:m], q)] + u = common_complement(w, v, k, q) + system = transpose([*columns(n)[m:], *u]) + solutions = [solve(system, c, q) for c in columns(n)[:m]] + check(all(s is not None for s in solutions), "graph lift unsolvable") + f = transpose([s[:m] for s in solutions]) + first, second = transpose(columns(n)[:m]), transpose(columns(n)[m:]) + graph_image = tuple(add(x, scale(-1, y, q), q) + for x, y in zip(first, matmul(second, f, q), strict=True)) + e, lower = graph_image[:m], graph_image[m:] + b = [solve(transpose(e), row, q) for row in lower] + check(all(row is not None for row in b), "row projection not injective") + b = tuple(b) + upper_right, bottom_right = second[:m], second[m:] + d = tuple(add(x, scale(-1, y, q), q) + for x, y in zip(bottom_right, matmul(b, upper_right, q), strict=True)) + one, zero = identity(m), tuple((0,) * m for _ in range(m)) + p = (*join(one, zero), *join(b, one)) + r = (*join(one, upper_right), *join(zero, d)) + s = (*join(e, zero), *join(f, one)) + return (p, r, s), (rs, cs) + + +def verify_target(a, q, data=False): + factors, (rs, cs) = construct(a, q) + m = len(a) // 2 + product = identity(2*m) + for i, factor in enumerate(factors): + fixed = range(m, 2*m) if i % 2 == 0 else range(m) + check(all(columns(factor)[j] == columns(identity(2*m))[j] for j in fixed), + "factor violates its base-field right-vector alphabet") + product = matmul(product, factor, q) + check(chart(product, rs, cs) == a, "three-factor product differs from target") + if data: + for x in itertools.product(range(q), repeat=2*m): + state = transpose([x]) + for factor in reversed(factors): + state = matmul(factor, state, q) + check(state == matmul(chart(a, rs, cs), transpose([x]), q), + "chronological data action differs") + return factors, (rs, cs) + + +def exhaustive_binary(): + digest = hashlib.sha256() + ranks = [0] * 5 + for entries in itertools.product(range(2), repeat=16): + a = tuple(tuple(entries[i:i+4]) for i in range(0, 16, 4)) + factors, charts = verify_target(a, 2) + ranks[len(basis(a, 2))] += 1 + digest.update(bytes(x for f in factors for row in f for x in row)) + digest.update(bytes(charts)) + check(ranks == [1, 225, 7350, 37800, 20160], "binary rank coverage changed") + return {"targets": 65536, "rank_histogram": ranks, "word_sha256": digest.hexdigest()} + + +def sharp_target(m): + a = [list(row) for row in identity(2*m)] + a[0], a[m+1] = a[m+1], a[0] + return tuple(tuple(row) for row in a) + + +def two_factor(a, q): + m = len(a) // 2 + lines = [(1, x) for x in range(q)] + [(0, 1)] + for s, t in lines: + row = tuple(add(scale(s, x, q), scale(t, y, q), q) + for x, y in zip(a[:m], a[m:], strict=True)) + full_rank = len(basis(row, q)) + for x, y in lines: + block = [add(scale(x, r[:m], q), scale(y, r[m:], q), q) for r in row] + if len(basis(block, q)) == full_rank: + return True + return False + + +def examples_and_controls(): + rng = random.Random(831049) + count = 0 + sharp = 0 + order_controls = 0 + for q in (2, 3, 5, 7): + for m in (1, 2, 3, 4): + for _ in range(24): + a = tuple(tuple(rng.randrange(q) for _ in range(2*m)) for _ in range(2*m)) + factors, charts = verify_target(a, q) + rev = matmul(matmul(factors[2], factors[1], q), factors[0], q) + order_controls += chart(rev, *charts) != a + count += 1 + if m >= 2: + a = sharp_target(m) + verify_target(a, q, data=(q == 2 and m == 2)) + check(not two_factor(a, q), "sharp witness admits two factors") + sharp += 1 + check(solve(((0,),), (1,), 2) is None, "inconsistent solver control") + check(common_complement([(1, 0), (0, 1)], [(1, 0)], [(0, 1)], 2) + == [(1, 1)], "binary union-of-two-subspaces control") + check(two_factor(identity(4), 2), "free target control") + check(order_controls > 0, "reversal control failed to discriminate") + a = sharp_target(2) + factors, charts = verify_target(a, 2) + check(all(chart(matmul(factors[i], factors[j], 2), *charts) != a + for i, j in ((0, 1), (0, 2), (1, 2))), "omission control") + for q in (2, 3, 5, 7): + for entries in itertools.product(range(q), repeat=4): + verify_target((entries[:2], entries[2:]), q) + count += 1 + return {"additional_targets": count, "sharp_witnesses": sharp, "controls": 5, + "reversed_words_differing": order_controls} + + +def receipt(results): + package = Path(__file__).resolve().parent + root = package.parent.parent + hashes = {} + for name in ("README.md", "PROOF.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py"): + path = package / name + check(path.stat().st_size <= 1024*1024, "oversize package file") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + manifest = json.loads((package / "SOURCES.json").read_text()) + check(len(manifest["files"]) <= 8, "source manifest exceeds replay bound") + for row in manifest["files"]: + if row["usage"] == "input": + payload = (root / row["path"]).read_bytes() + check(hashlib.sha256(payload).hexdigest() == row["sha256"], "source pin drift") + hashes[row["path"]] = row["sha256"] + return {"files": hashes, "results": results} + + +def main(): + results = {"binary": exhaustive_binary(), "other": examples_and_controls()} + print(json.dumps(receipt(results), sort_keys=True)) + print("PASS_MATRIX_ALGEBRA_THREE_FACTOR binary_targets=65536 " + f"additional_targets={results['other']['additional_targets']} " + "sharp_witnesses=12 controls=5 no_new_kappa") + + +if __name__ == "__main__": + main()