From 5c72ad1fef28cdb5f07d4585bc4e859dbeb02760 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 10:44:43 +0000 Subject: [PATCH] feat(research): prove anticommuting query additivity --- .../anticommuting-query-additivity/PROOF.md | 156 +++++++++ .../anticommuting-query-additivity/README.md | 126 +++++++ .../SOURCES.json | 18 + .../anticommuting-query-additivity/TASK.json | 92 +++++ .../VERIFY.json | 34 ++ .../anticommuting-query-additivity/verify.py | 327 ++++++++++++++++++ 6 files changed, 753 insertions(+) create mode 100644 research/anticommuting-query-additivity/PROOF.md create mode 100644 research/anticommuting-query-additivity/README.md create mode 100644 research/anticommuting-query-additivity/SOURCES.json create mode 100644 research/anticommuting-query-additivity/TASK.json create mode 100644 research/anticommuting-query-additivity/VERIFY.json create mode 100644 research/anticommuting-query-additivity/verify.py diff --git a/research/anticommuting-query-additivity/PROOF.md b/research/anticommuting-query-additivity/PROOF.md new file mode 100644 index 0000000000..3e941d535f --- /dev/null +++ b/research/anticommuting-query-additivity/PROOF.md @@ -0,0 +1,156 @@ +# Exact additivity for two anticommuting query types + +This is a scoped algebraic proof. All fields, role counts and matrix sizes below +are finite. No physical Gaussian realization or complete multiplication theorem +is asserted. + +## Model and theorem + +Let K be any field of characteristic different from two. Fix a nonempty finite +list of positive integers d_c and the ordinary coefficient algebra + + A = product_c Mat_(d_c)(K). + +The payload operator algebra is H = A tensor_K Mat_2(K). Write + + Q = I tensor [[0,1],[1,0]], R = I tensor [[1,0],[0,-1]]. + +Thus Q^2 = R^2 = I, RQ = -QR, and H is the direct sum of the four left +A-modules A, AQ, AR, AQR. The result also holds in any faithful realization +of this algebra. Faithfulness means equality on all payloads distinguishes +these four A-coefficients. It is a hypothesis, not a finite-width inference. + +A program has arbitrary independent source fields x_1,...,x_n and arbitrary +independent receivers y_1,...,y_m. Borrowed fields are arbitrary and must be +restored. Owned fields start at zero and must return zero. The allowed ordinary +instructions are finite A-linear maps on the fields, including accumulation +and clearing owned fields. One paid query applies Q or R to one whole field. +Each inverse has the same price, since both queries are involutions. Arbitrary +linear feedback, overwriting, retention and interleaving are allowed. The +ordinary algebra excludes Q and R and excludes choosing a different query type +in different components of one paid call. + +For matrices A0,B,C in Mat_(m by n)(A), require the full endpoint + + x stays x, y becomes y + (A0 + BQ + CR)x, + +with every borrowed field restored and every owned field zero. There is no QR +coefficient in this target. Expand B and C in component c to scalar matrices +B_c,C_c of size (m d_c) by (n d_c), and define + + k_B = max_c ceil(rank_K(B_c)/d_c), + k_C = max_c ceil(rank_K(C_c)/d_c). + +**Theorem.** Every admissible program uses at least k_B queries of type Q and +at least k_C queries of type R. One program attains both bounds at once. Hence +the exact minimum total is k_B+k_C. For positive prices w_Q,w_R the exact +minimum charge is w_Q k_B + w_R k_C. + +## 1. One-query rank lemma + +Let E be a unital ordinary algebra and suppose the represented operator algebra +is the direct sum E + ET, with T^2=I and T e = sigma(e) T for an automorphism +sigma of E. Initially the ET-coefficient row of every arbitrary original input +and every zero owned field is zero. Ordinary E-linear instructions only combine +existing ET-coefficient rows. A T query creates one new such row, regardless of +whether it overwrites a field or uses a retained field. + +Record the new row at each of the q query occurrences for this proof only. +Induction over instructions puts every final ET row in their E-linear span. +Therefore the final ET matrix factors through q E-rows. Restricting its columns +to the original source fields preserves that factorization. This argument +includes arbitrary receiver and borrowed inputs; it never assumes they vanish +in the actual program. Clearing is an E-linear map and preserves the span +statement. No runtime bank retaining all q rows is assumed. + +For E = product_j Mat_(e_j)(K), any factorization through q E-rows expands to a +factorization through q e_j scalar coordinates in component j. Its component +rank is at most q e_j. Conversely, scalar rank factorizations, padded to q e_j +middle coordinates and assembled into e_j by e_j blocks, attain + + inner_rank_E(D) = max_j ceil(rank_K(D_j)/e_j). + +This is ordinary finite-dimensional rank factorization. The proof of the +present theorem does not require replaying any predecessor implementation. + +## 2. Count Q even when R is free + +Enlarge the ordinary algebra, solely for a lower bound, to + + E_R = A + AR. + +Its projectors (I+R)/2 and (I-R)/2 give the explicit isomorphism +E_R -> A times A, a+bR -> (a+b,a-b). Every original ordinary instruction and +every R query is E_R-linear. Q normalizes E_R by a+bR -> a-bR. Moreover +H = E_R + E_R Q is a direct sum. The one-query lemma thus applies to the +number q_Q of Q queries in the original program, with all R queries granted +for free in this relaxation. + +The target's E_R Q coefficient is exactly B. Its two components are (B,B), +so its expanded ranks in both copies of component c equal rank_K(B_c). +Consequently q_Q >= k_B. The receiver identity and the A0+CR part are E_R-even +and create no extra odd coefficient. Restoration requirements remain in the +full endpoint. + +## 3. Count R even when Q is free + +Use E_Q = A + AQ and its projectors (I+Q)/2 and (I-Q)/2. Now H = E_Q + E_Q R, +and R normalizes E_Q by a+bQ -> a-bQ. The target's E_Q R coefficient is C, +embedded as (C,C). The same argument gives q_R >= k_C. These are simultaneous +inequalities for each original program, so their sum is a valid lower bound. +They are not alternatives between which a program may choose. + +## 4. Attain both bounds with one owned query field + +Choose component rank factorizations B_c=L_c V_c, padding each middle dimension +to k_B d_c. Reassemble the blocks to get B=L V through k_B A-rows. For row j: + +1. In a zero owned field h, accumulate h = sum_a V_(j,a) x_a. +2. Apply Q once to h. Since Q commutes with A, h = sum_a V_(j,a) Q x_a. +3. For each receiver i, add L_(i,j) h to y_i. +4. Clear h to zero. + +Repeat for every row, then do the same for a k_C-row factorization of C using +R. Accumulate A0x ordinarily. The original source bank never changes, receiver +values remain arbitrary, and borrowed fields are untouched. All owned storage +returns zero. The sequence uses exactly k_B Q queries and k_C R queries, and +only one owned query field at a time. Its routing operations still have cost; +only the query count is optimized here. If actual A coefficients require an +evaluator, its workspace and literal words must be charged separately. + +## 5. A sharp sector accounting gap + +Take A=K times K and n=m=1, B=(1,0), C=(0,1), A0=0. In the first component +only Q is needed, and in the second only R is needed. Each component alone has +query total one, but the complete contract needs two calls. Thus + + max_c (ceil(rank(B_c)/d_c) + ceil(rank(C_c)/d_c)) = 1 + +is not the correct global answer. The sum of the two maxima is two. A paid +operation that conditionally chooses Q in one component and R in the other +would change the alphabet and defeat this example. It is expressly excluded. + +For a noncommutative packing example, take A=Mat_2(K), n=m=2 and +B=C=diag(E_11,E_11). Both expanded ranks are two, so the minimum is two calls, +one of each type. Matrix units pack the two same-type demands into one field; +they do not turn the two different query types into one call. + +## Scope, novelty and remaining obligations + +This answers the faithful anticommuting-involution specialization of RQ09 in +David Ganz's PR5803, at head 0acda5ab421d28b98fdf916968696c8f9453376f. +R03-R06 there supply the single-query inner-rank framework and noncommutative +matrix-block motivation. Ali Romman's PR5626 supplies the earlier faithful +ordinary-sector query compiler. Their algebraic methods and the classical +matrix-rank ingredients retain credit. The new step is the simultaneous +opposite-type relaxation, exact two-type tariff and sharp sector conflict +example. No worldwide novelty claim is made for classical Clifford algebra. + +The theorem does not cover a nonzero QR target coefficient, characteristic two, +a nonfaithful payload action, ordinary maps outside A, nonlinear instructions, +selectable per-component query types, or queries on several fields at once. +It does not assert that actual Gaussian queries anticommute. Finding a lawful +native realization, physical coefficient words, input/output matchers, paid +movement, precision, restoration, stock, productive targets and a complete +signed invoice remains a separate task. The proof is informal; finite checks +corroborate it and do not discharge its universal quantifiers in a proof kernel. diff --git a/research/anticommuting-query-additivity/README.md b/research/anticommuting-query-additivity/README.md new file mode 100644 index 0000000000..7a27ab16fb --- /dev/null +++ b/research/anticommuting-query-additivity/README.md @@ -0,0 +1,126 @@ +# Two anticommuting query types have an additive exact tariff + +This contribution was produced by Nick Petalas. Claim type: scoped algebraic +proof with exact finite corroboration. No new κ or physical supplier is claimed. + +For a faithful algebra with Q²=R²=I, RQ=-QR and ordinary coefficients +A=product_c Mat_(d_c)(K), char(K)≠2, the input-preserving shear + + y += (A0 + BQ + CR)x + +has the exact query count + + max_c ceil(rank(B_c)/d_c) + max_c ceil(rank(C_c)/d_c). + +Every word needs the first summand in Q calls and the second in R calls, even +with arbitrary linear feedback, retention, overwriting and restored borrowed +dirty fields. One source-preserving word attains both bounds and streams its +queries through one zero-return owned field. Positive unequal type prices give +the corresponding weighted sum. Ordinary routing is still charged separately. + +[PROOF.md](PROOF.md) gives the complete model and argument. To lower-bound Q, +grant every R call for free, split the enlarged ordinary algebra into R's two +eigenspaces and factor the final Q coefficient through the Q outputs. Reverse +the roles for R. The two inequalities hold for the same original word. + +The distinction matters even for A=K×K. Demands B=(1,0), C=(0,1) need two +queries globally, although each component needs only one. Taking the maximum +of each component's total would undercount. Noncommutative matrix blocks can +still pack several same-type demands; the explicit Mat_2 example needs one Q +and one R rather than four separately acquired responses. + +## Reproduce + +From the repository root, using standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/anticommuting-query-additivity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/anticommuting-query-additivity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/anticommuting-query-additivity --check-source-history +``` + +Use the last command after committing. On another machine substitute its +CPython 3.12 path. Both registered commands must finish with +`PASS_ANTICOMMUTING_QUERY_ADDITIVITY`; the launcher then reports +`PASS_REGISTERED_RESEARCH_PACKAGE`. + +The checker runs independently written formal-coefficient and literal-payload +interpreters on every original source, receiver and borrowed input column: + +- All 6,561 pairs of scalar 2×2 response matrices over F_3. +- All 6,561 pairs of one-role Mat_2(F_3) response matrices. +- 216 rectangular/product-algebra fixtures over F_3,F_5,F_7, with nonzero + ordinary response terms and dimensions up to three source/receiver fields. +- The explicit packed Mat_2 example and the two-component sector-conflict + example, including arbitrary receiver/borrowed inputs and scratch restoration. +- All 1,555 words of length at most four in a six-instruction, two-role + feedback alphabet. Their complete mixed coefficients satisfy both type cuts. +- Eight rejection controls for query deletion, wrong query type, dirty-owned + leakage, borrowed-field corruption and invalid finite-model parameters. + +The interpreters enumerate 149,742 input columns across the first three +fixture families. These are basis-column comparisons, not that many input +assignments. Their formal circuits contain 213,064 instructions in total. +The feedback enumeration corroborates lower bounds and is not an exhaustive +search over the theorem's arbitrary programs. Each run emits its counts and +SHA256 hashes of the six package files as a generated receipt to stdout; it +writes no files. No receipt is handwritten or retained as a frozen result. + +## Scope and provenance + +The target is the anticommuting-involution specialization of RQ09 in David +Ganz's [PR5803](https://github.com/CrocSwap/integer-mult-bounds/pull/5803), exact +head `0acda5ab421d28b98fdf916968696c8f9453376f`, +[volume-algebra.md](https://github.com/CrocSwap/integer-mult-bounds/blob/0acda5ab421d28b98fdf916968696c8f9453376f/research/frontier-mathematical-atlas/volume-algebra.md). +Credit its R03-R06 single-query inner-rank framework and explicit two-type +question, Ali Romman's [PR5626](https://github.com/CrocSwap/integer-mult-bounds/pull/5626) +faithful-sector compiler, Dugongue's PR5578 T6/T7, and the retained native, +phase, ownership, controller and compiler lineage, including Cao Yifan, +Cinna Davis, Ryanson Jonathan, zxv and Jacob Alan Sussman. Classical rank +factorization and Clifford algebra are not claimed as globally new. + +The proof is self-contained. No predecessor verifier or numerical result is +replayed, and no pending source object or network service is needed to run the +checker. The cited atlas is bibliographic context, not a runtime input. +[SOURCES.json](SOURCES.json) pins the original catalogue and selected record +as historical provenance. [TASK.json](TASK.json) explicitly records the change +from the source-bound decoder card to this algebraic side result. + +Live overlap checking included open PR metadata, this account's earlier PRs, +recent handoffs, active Discussions, merged-PR searches and all-main README +searches for the distinctive algebra and tariff. The overlap snapshot covered +426 open PRs and 5,328 Discussion records. Its sparse local search covered only +225 notes out of 7,845; the all-main Git searches cover omitted README paths, +not every package file or historical wording. These checks are not proof of +novelty. + +The theorem excludes mixed QR target terms, characteristic two, nonfaithful +representations, extra ordinary operators, nonlinear instructions, queries on +multiple fields and choosing query type per component. Actual native Gaussian +realization, physical coefficient words, complete routing/precision/stock and +signed-moment funding remain unproved. No selected source or frontier changes. +Independent human and formal proof-kernel review are unclaimed. + +## Verification design + +The retained checker has no recursion, subprocesses, network access, external +dependencies or writes. Its fixed enumeration bounds, at most two components, +block size two, three source/receiver fields and 57 instructions bound all +work. Each matrix operation checks its dimensions; mathematical checks raise +explicit exceptions and survive optimized Python. Functions remain under 60 +lines. Managed Python allocations are a Power of Ten deviation: these bounded +finite matrices allocate during evaluation; there is no fixed-memory runtime +claim. Warning-strict normal and optimized execution supplies the available +interpreter diagnostics. No separate static analyzer is installed. + +## Open next questions + +- Determine the exact minimum when a QR output coefficient is present. First + compare the two type-specific projected ranks with explicit mixed words. + The present proof supplies no attaining general constructor for that domain. +- Instantiate one faithful native caller with both query types and ordinary + spectator matrix units. First pin the operators, phases and four-coefficient + independence, then price the full producer/consumer. Its physical contract + and complete paid/productive invoice are still missing. + +New work is Apache-2.0. The predecessor notices remain with their sources. diff --git a/research/anticommuting-query-additivity/SOURCES.json b/research/anticommuting-query-additivity/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/research/anticommuting-query-additivity/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/anticommuting-query-additivity/TASK.json b/research/anticommuting-query-additivity/TASK.json new file mode 100644 index 0000000000..317b7a3a39 --- /dev/null +++ b/research/anticommuting-query-additivity/TASK.json @@ -0,0 +1,92 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact type-specific and total query minima for a faithful two-anticommuting-involution shear over a finite product of full matrix algebras.", + "scope_change_reason": "The chosen decoder card leads to a source-independent algebraic side result answering RQ09 of David Ganz PR5803. This supplies a sharp typed-interface obstruction, not a physical coframe or complete-invoice improvement.", + "bottleneck_link": "A query bundle must count each nonordinary query type in its actual alphabet. The sum of componentwise maxima can exceed the maximum component total; ordinary spectator mixing cannot erase this typed charge. No complete supplier gain is asserted.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact scoped theorem, attaining word and bounded independent literal/formal checks pass.", + "outcome": "completed", + "evidence": "PROOF.md proves the universal algebraic statement. verify.py checks 13,338 complete shear fixtures in two operator representations, 1,555 feedback words, the packed example and eight rejection controls. It emits a generated source-hash-bound receipt to stdout.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What exact tariff holds when the endpoint includes a nonzero QR coefficient?", + "why_it_matters": "The present two odd coefficients have no mixed contribution. Mixed endpoints can exploit sequential queries and require fresh simultaneous bounds.", + "first_step": "Compare the two opposite-type projected ranks B plus/minus D and C plus/minus D against explicit small attaining words.", + "blocked_by": "No matching general constructor or lower-bound theorem is supplied here." + }, + { + "question": "Does one actual native caller realize this faithful anticommuting algebra with ordinary spectator matrix units?", + "why_it_matters": "The abstract tariff can constrain a physical bundle only after its exact algebra and full endpoint are established.", + "first_step": "Pin one source window, exhibit both query operators and the four-coefficient independence, then emit all ordinary coefficients.", + "blocked_by": "Native realization, phase matchers, dirty restoration, movement, precision, stock and complete paid/productive invoice remain unproved." + } + ], + "question_source": { + "pr": 5803, + "head": "0acda5ab421d28b98fdf916968696c8f9453376f", + "section": "volume-algebra.md RQ09", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5803" + }, + "environment": { + "python": "CPython 3.12.15", + "dependencies": "standard library only", + "platform": "macOS arm64" + } +} diff --git a/research/anticommuting-query-additivity/VERIFY.json b/research/anticommuting-query-additivity/VERIFY.json new file mode 100644 index 0000000000..aa2e13c8c6 --- /dev/null +++ b/research/anticommuting-query-additivity/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact attaining shears in formal Clifford coefficients and independent literal payload matrices; feedback type cuts; model and corruption controls; generated source-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Repeat the same mathematical comparisons with language assertions disabled. All proof-relevant checks use explicit exceptions." + } + ] +} diff --git a/research/anticommuting-query-additivity/verify.py b/research/anticommuting-query-additivity/verify.py new file mode 100644 index 0000000000..a85658581a --- /dev/null +++ b/research/anticommuting-query-additivity/verify.py @@ -0,0 +1,327 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the two-type theorem. Nick Petalas, Apache-2.0.""" +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +class VerificationError(Exception): + """A mathematical comparison or bounded input contract failed.""" + + +def require(condition, message): + if not condition: + raise VerificationError(message) + + +def zero(rows, cols): + return [[0] * cols for _ in range(rows)] + + +def mm(left, right, p): + rows, inner, cols = len(left), len(right), len(right[0]) + require(all(len(row) == inner for row in left), "matrix dimensions") + return [[sum(left[i][k] * right[k][j] for k in range(inner)) % p + for j in range(cols)] for i in range(rows)] + + +def rref(matrix, p): + work = [row[:] for row in matrix] + rows, cols, pivots = len(work), len(work[0]), [] + for col in range(cols): + candidates = [i for i in range(len(pivots), rows) if work[i][col] % p] + if not candidates: + continue + row, found = len(pivots), candidates[0] + work[row], work[found] = work[found], work[row] + inv = pow(work[row][col], -1, p) + work[row] = [(v * inv) % p for v in work[row]] + for i in range(rows): + if i != row: + scale = work[i][col] + work[i] = [(a - scale * b) % p + for a, b in zip(work[i], work[row], strict=True)] + pivots.append(col) + return work, pivots + + +def rank(matrix, p): + return len(rref(matrix, p)[1]) + + +def factor(matrix, middle, p): + reduced, pivots = rref(matrix, p) + require(len(pivots) <= middle, "insufficient factor capacity") + left, right = zero(len(matrix), middle), zero(middle, len(matrix[0])) + for j, col in enumerate(pivots): + for i in range(len(matrix)): + left[i][j] = matrix[i][col] + right[j] = reduced[j][:] + if middle: + require(mm(left, right, p) == matrix, "rank factorization") + else: + require(not any(any(row) for row in matrix), "zero rank matrix") + return left, right + + +def block(matrix, row, col, d): + return [line[col*d:(col+1)*d] for line in matrix[row*d:(row+1)*d]] + + +def tariff(matrices, dimensions, p): + return max((rank(a, p) + d - 1) // d + for a, d in zip(matrices, dimensions, strict=True)) + + +def validate_case(p, dimensions, n, m, a0, b, c): + require(p in (3, 5, 7), "unsupported finite control field") + require(1 <= len(dimensions) <= 2, "component capacity") + require(all(d in (1, 2) for d in dimensions), "block capacity") + require(1 <= n <= 3 and 1 <= m <= 3, "role capacity") + for matrices in (a0, b, c): + require(len(matrices) == len(dimensions), "component mismatch") + for a, d in zip(matrices, dimensions, strict=True): + require(len(a) == m*d and all(len(row) == n*d for row in a), + "response dimensions") + require(all(type(v) is int and 0 <= v < p for row in a for v in row), + "noncanonical coefficient") + + +def emit(p, dimensions, n, m, a0, b, c): + validate_case(p, dimensions, n, m, a0, b, c) + scratch, word = n+m+1, [] + for i in range(m): + for a in range(n): + coeff = [block(v, i, a, d) for v, d in zip(a0, dimensions, strict=True)] + word.append(("add", n+i, a, coeff)) + for label, matrices in (("Q", b), ("R", c)): + count = tariff(matrices, dimensions, p) + factors = [factor(v, count*d, p) + for v, d in zip(matrices, dimensions, strict=True)] + for j in range(count): + for a in range(n): + coeff = [block(v, j, a, d) + for (_, v), d in zip(factors, dimensions, strict=True)] + word.append(("add", scratch, a, coeff)) + word.append((label, scratch, -1, [])) + for i in range(m): + coeff = [block(l, i, j, d) + for (l, _), d in zip(factors, dimensions, strict=True)] + word.append(("add", n+i, scratch, coeff)) + word.append(("clear", scratch, -1, [])) + require(len(word) <= 57, "word capacity") + return word + + +def formal_run(word, component, d, originals, fields, p): + bank = [[zero(d, originals*d) for _ in range(4)] for _ in range(fields)] + for slot in range(originals): + for i in range(d): + bank[slot][0][i][slot*d+i] = 1 + for op, dest, src, coeff in word: + if op == "add": + for t in range(4): + delta = mm(coeff[component], bank[src][t], p) + bank[dest][t] = [[(a+b) % p for a, b in zip(x, y, strict=True)] + for x, y in zip(bank[dest][t], delta, strict=True)] + elif op == "clear": + bank[dest] = [zero(d, originals*d) for _ in range(4)] + else: + require(op in ("Q", "R"), "unknown query") + order = (1, 0, 3, 2) if op == "Q" else (2, 3, 0, 1) + signs = (1, 1, 1, 1) if op == "Q" else (1, -1, 1, -1) + old = bank[dest] + bank[dest] = [[[(signs[t]*v) % p for v in row] for row in old[order[t]]] + for t in range(4)] + return bank + + +def kron_query(coeff, label): + small = {"I": ((1, 0), (0, 1)), "Q": ((0, 1), (1, 0)), + "R": ((1, 0), (0, -1))}[label] + return [[coeff[i//2][j//2] * small[i % 2][j % 2] + for j in range(2*len(coeff[0]))] for i in range(2*len(coeff))] + + +def literal_run(word, component, d, originals, fields, p): + size = 2*d + bank = [zero(size, originals*size) for _ in range(fields)] + ident = [[int(i == j) for j in range(d)] for i in range(d)] + for slot in range(originals): + for i in range(size): + bank[slot][i][slot*size+i] = 1 + for op, dest, src, coeff in word: + if op == "clear": + bank[dest] = zero(size, originals*size) + elif op == "add": + delta = mm(kron_query(coeff[component], "I"), bank[src], p) + bank[dest] = [[(a+b) % p for a, b in zip(x, y, strict=True)] + for x, y in zip(bank[dest], delta, strict=True)] + else: + bank[dest] = mm(kron_query(ident, op), bank[dest], p) + return bank + + +def expected_formal(d, n, m, a0, b, c): + originals, fields = n+m+1, n+m+2 + bank = [[zero(d, originals*d) for _ in range(4)] for _ in range(fields)] + for slot in range(originals): + for i in range(d): + bank[slot][0][i][slot*d+i] = 1 + for i in range(m): + for t, matrix in enumerate((a0, b, c)): + for u in range(d): + for v in range(n*d): + bank[n+i][t][u][v] = matrix[i*d+u][v] + return bank + + +def expected_literal(d, n, m, a0, b, c, p): + size, originals, fields = 2*d, n+m+1, n+m+2 + bank = [zero(size, originals*size) for _ in range(fields)] + for slot in range(originals): + for i in range(size): + bank[slot][i][slot*size+i] = 1 + for i in range(m): + for a in range(n): + terms = [kron_query(block(v, i, a, d), label) + for v, label in ((a0, "I"), (b, "Q"), (c, "R"))] + for u in range(size): + for v in range(size): + bank[n+i][u][a*size+v] = sum(t[u][v] for t in terms) % p + return bank + + +def endpoints(word, p, dimensions, n, m, a0, b, c): + for j, d in enumerate(dimensions): + got = formal_run(word, j, d, n+m+1, n+m+2, p) + require(got == expected_formal(d, n, m, a0[j], b[j], c[j]), "formal endpoint") + literal = literal_run(word, j, d, n+m+1, n+m+2, p) + require(literal == expected_literal(d, n, m, a0[j], b[j], c[j], p), + "literal arbitrary-input endpoint") + + +def check_case(p, dimensions, n, m, a0, b, c): + word = emit(p, dimensions, n, m, a0, b, c) + require(sum(op == "Q" for op, *_ in word) == tariff(b, dimensions, p), "Q count") + require(sum(op == "R" for op, *_ in word) == tariff(c, dimensions, p), "R count") + endpoints(word, p, dimensions, n, m, a0, b, c) + return len(word), sum((n+m+1)*2*d for d in dimensions) + + +def scalar_exhaustive(): + matrices = [[list(v[:2]), list(v[2:])] for v in product(range(3), repeat=4)] + counts = [0, 0, 0] + for b, c in product(matrices, repeat=2): + steps, columns = check_case(3, (1,), 2, 2, [zero(2, 2)], [b], [c]) + counts = [counts[0]+1, counts[1]+steps, counts[2]+columns] + return counts + + +def block_exhaustive(): + matrices = [[list(v[:2]), list(v[2:])] for v in product(range(3), repeat=4)] + counts = [0, 0, 0] + for b, c in product(matrices, repeat=2): + steps, columns = check_case(3, (2,), 1, 1, [zero(2, 2)], [b], [c]) + counts = [counts[0]+1, counts[1]+steps, counts[2]+columns] + return counts + + +def rectangular_cases(): + counts = [0, 0, 0] + for p, dims, n, m, seed in product((3, 5, 7), ((1, 2), (2,)), + range(1, 4), range(1, 4), range(4)): + matrices = [] + for family in range(3): + parts = [] + for component, d in enumerate(dims): + parts.append([[(i*i+3*i*j+7*j+seed*(i+1)+family*(j+2) + +component+family*seed) % p for j in range(n*d)] + for i in range(m*d)]) + matrices.append(parts) + steps, columns = check_case(p, dims, n, m, *matrices) + counts = [counts[0]+1, counts[1]+steps, counts[2]+columns] + return counts + + +def feedback_controls(): + ident = [[1]] + alphabet = [("add", 0, 1, [ident]), ("add", 1, 0, [ident])] + alphabet += [(label, slot, -1, []) for label in ("Q", "R") for slot in (0, 1)] + checked = 0 + for length in range(5): + for word in product(alphabet, repeat=length): + bank = formal_run(word, 0, 1, 2, 2, 3) + for label, t in (("Q", 1), ("R", 2)): + count = sum(op == label for op, *_ in word) + for sign in (1, -1): + projected = [[(bank[i][t][0][j]+sign*bank[i][3][0][j]) % 3 + for j in range(2)] for i in range(2)] + require(rank(projected, 3) <= count, "mixed feedback type cut") + checked += 1 + return checked + + +def packed_example(): + matrix = zero(4, 4) + matrix[0][0] = matrix[2][2] = 1 + word = emit(3, (2,), 2, 2, [zero(4, 4)], [matrix], [matrix]) + endpoints(word, 3, (2,), 2, 2, [zero(4, 4)], [matrix], [matrix]) + require(sum(op in ("Q", "R") for op, *_ in word) == 2, "packed example") + return 1 + + +def rejection_controls(): + dims, a0, b, c = (1, 1), [[[0]], [[0]]], [[[1]], [[0]]], [[[0]], [[1]]] + word = emit(3, dims, 1, 1, a0, b, c) + endpoints(word, 3, dims, 1, 1, a0, b, c) + require(tariff(b, dims, 3)+tariff(c, dims, 3) == 2, "sector conflict total") + require(max(rank(x, 3)+rank(y, 3) for x, y in zip(b, c, strict=True)) == 1, + "sector conflict comparison") + queries = [i for i, step in enumerate(word) if step[0] in ("Q", "R")] + mutants = [word[:queries[0]]+word[queries[0]+1:]] + wrong_type = word[:] + wrong_type[queries[0]] = ("R", word[queries[0]][1], -1, []) + mutants.append(wrong_type) + mutants.append(word[:-1]) + mutants.append(word+[("add", 2, 0, [[[1]], [[1]]])]) + for changed in mutants: + failed = False + try: + endpoints(changed, 3, dims, 1, 1, a0, b, c) + except VerificationError: + failed = True + require(failed, "endpoint mutant escaped") + bad_args = [(2, dims, 1, 1, a0, b, c), (3, (0,), 1, 1, a0, b, c), + (3, dims, 4, 1, a0, b, c), (3, dims, 1, 1, a0, [], c)] + for args in bad_args: + failed = False + try: + emit(*args) + except VerificationError: + failed = True + require(failed, "invalid model accepted") + return len(mutants)+len(bad_args) + + +def main(): + result = {"scalar_exhaustive": scalar_exhaustive(), + "matrix_block_exhaustive": block_exhaustive(), + "rectangular_product_cases": rectangular_cases(), + "feedback_words": feedback_controls(), + "packed_example": packed_example(), + "rejection_controls": rejection_controls()} + root = Path(__file__).resolve().parent + hashes = {} + for name in ("verify.py", "PROOF.md", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json"): + payload = (root / name).read_bytes() + require(len(payload) <= 65536, "receipt source capacity") + hashes[name] = sha256(payload).hexdigest() + result["source_sha256"] = hashes + print("PASS_ANTICOMMUTING_QUERY_ADDITIVITY") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()