From 0a49cfa436fc2ad9cd8fffa84ebb35fb376b06a1 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 12 Nov 2026 18:27:45 +0000 Subject: [PATCH] feat(research): prove robust coordinate-pairing capacity --- research/robust-coordinate-pairing/PROOF.md | 128 +++++++ research/robust-coordinate-pairing/README.md | 146 ++++++++ .../robust-coordinate-pairing/SOURCES.json | 18 + research/robust-coordinate-pairing/TASK.json | 104 ++++++ .../robust-coordinate-pairing/VERIFY.json | 34 ++ research/robust-coordinate-pairing/verify.py | 313 ++++++++++++++++++ 6 files changed, 743 insertions(+) create mode 100644 research/robust-coordinate-pairing/PROOF.md create mode 100644 research/robust-coordinate-pairing/README.md create mode 100644 research/robust-coordinate-pairing/SOURCES.json create mode 100644 research/robust-coordinate-pairing/TASK.json create mode 100644 research/robust-coordinate-pairing/VERIFY.json create mode 100644 research/robust-coordinate-pairing/verify.py diff --git a/research/robust-coordinate-pairing/PROOF.md b/research/robust-coordinate-pairing/PROOF.md new file mode 100644 index 0000000000..b9d112078c --- /dev/null +++ b/research/robust-coordinate-pairing/PROOF.md @@ -0,0 +1,128 @@ +# Exact common pairings under coordinate uncertainty + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written algebraic proof with exact finite corroboration. +The argument uses classical matrix rank, rank factorization and outer products. +No claim of general literature priority is made for those tools. + +## 1. Contract and theorem + +Let F be any field, B an m by n matrix over F, and E a subset of +{1,...,m} times {1,...,n}. The uncertainty family is + + B(t) = B + sum_{(i,j) in E} t_ij e_i e_j^T, t_ij in F. + +For r >= 0, a common identity pairing consists of fixed matrices X of size +r by m and Y of size n by r such that + + X B(t) Y = I_r (1) + +for every parameter choice. X and Y cannot depend on t. Empty matrices give +the r=0 convention. Write B[A,C] for the submatrix with row set A and column +set C. A rectangle A times C is clean when it is disjoint from E. + +**Theorem.** The largest r satisfying (1) is exactly + + c(B,E) = max_{A,C: (A times C) intersect E = empty} rank B[A,C]. (2) + +Empty rectangles have rank zero. The same answer holds if (1) is requested +only for the nominal B and the single-entry alternatives B+e_i e_j^T, one +for each (i,j) in E. No large or infinite field hypothesis is needed. + +**Upper bound.** Subtract the nominal equation from each single-entry +alternative. For every (i,j) in E this gives + + (X e_i)(e_j^T Y) = 0. (3) + +An outer product over a field is zero only if one factor is zero. Let A be +the indices of nonzero columns of X and C the indices of nonzero rows of Y. +Equation (3) says that A times C is clean. Consequently + + r = rank(X B Y) = rank(X[:,A] B[A,C] Y[C,:]) + <= rank B[A,C] <= c(B,E). + +**Attainment.** A rank-d clean submatrix has a nonsingular d by d minor +B[A',C']=M. Let S select rows A' and let T embed into coordinates C', in the +corresponding orders. Then X=M^{-1}S and Y=T satisfy XBY=I_d. For every +(i,j) in E, either i is outside A' or j is outside C'. Thus Xe_i e_j^T Y=0, +so the same X,Y satisfy (1). Restricting this identity pairing attains every +r<=d. For d=0 use empty matrices. This proves (2). + +Necessity used only the nominal and single-entry alternatives. Sufficiency +uses linearity. This proves the assertion for the smaller finite family too. +The finite oracle directly enumerates the single-entry alternatives; it does +not assume the outer-product factorization when computing its answer. + +## 2. Identity nominal pairing and its error graph + +For B=I_n, construct a graph on n coordinates. An error (i,j) forbids an +independent set from containing both i and j. A loop (i,i) forbids i itself. +Direction has no effect on independence; one directed edge suffices. + +**Corollary.** c(I_n,E) equals the independence number alpha(E), with this +loop convention. Arbitrary dense X,Y cannot improve on coordinate selection. + +Indeed rank I_n[A,C]=|A intersect C|. If A times C is clean, A intersect C is +independent, so (2) is at most alpha(E). Conversely an independent set S gives +the clean rectangle S times S, with submatrix I_|S|. Coordinate selection +therefore attains alpha(E) over every field. + +For the directed cycle E={(1,2),(2,3),...,(n-1,n),(n,1)}, n>=3, the sharp +value is floor(n/2). Summing the n inequalities +1_S(i)+1_S(i+1)<=1 gives 2|S|<=n, and alternating vertices attain the bound. +In particular the five-cycle admits exactly two common channels. Yet each +individual alternative I_n+e_i e_j^T in this cycle is invertible, with inverse +I_n-e_i e_j^T since i!=j. Thus the loss already occurs for a finite family of +n+1 entirely invertible maps. It is not caused by including a singular +simultaneous perturbation. + +Replacing each single-entry alternative by B+a_ij e_i e_j^T, for any nonzero +fixed a_ij, leaves the answer unchanged. Divide (3) by a_ij for necessity. +Arbitrarily small nonzero errors over R or C therefore have the same exact +obstruction. Approximate output contracts require a different theorem. + +## 3. Boundary witnesses + +Independent coordinate uncertainty cannot be replaced by support alone when +coefficients are correlated. Over Q, put + + B = I_3, + D = [[0,1,1],[-1,0,1],[-1,-1,0]], + Y = [[1,1],[-1,0],[1,0]], + X = [[0,-1/2,1/2],[1,1/2,-1/2]]. + +Direct multiplication gives XY=I_2 and XDY=0, hence X(I_3+tD)Y=I_2 for +every t. The nonzero-entry support of D is the complete loopless graph, +whose independent-coordinate capacity is only one. Correlation changes the +uncertainty space and escapes the theorem. This is a boundary witness. + +The identity-graph corollary also cannot replace (2) for arbitrary B. For +B=[[0,1],[1,0]] with uncertain diagonal entries, the graph has a loop on +every vertex. Nevertheless X=[1,0] and Y=[0,1]^T give one common channel. +Formula (2) finds the clean off-diagonal minor and gives exactly one. + +## 4. Helper relevance and limitations + +The new premise requires a proposed helper interface to use the same two +linear maps for the nominal pairing and specified coordinate alternatives. +Equation (1) is necessary for every stronger interface requiring that +identity block. Formula (2) exactly solves this optimistic algebraic +relaxation. A failed capacity test excludes that common-pairing contract. +No selected supplier is asserted to have this uncertainty family. + +For square B, every solution of positive size has full row rank X and full +column rank Y, since XBY=I_r. They extend to separate invertible output and +input bases over F. This does not force either off-diagonal block of the +transformed B(t) to vanish. Arbitrary dirty spectator independence, +restoration, chronological delivery and invertible dyadic completion require +additional conditions. Extra workspace, adaptive bases, correlated errors, +nonlinear decoders, approximate recovery and coefficients in rings with zero +divisors are outside this statement. Over rings, (3) need not kill a factor. + +No producer, native word, scalar schedule, paid/target histogram, precision +policy, physical hosting, storage or tape implementation is supplied. Their +costs are unknown and are not zero. This side result changes no selected +frontier and proves no complete multiplication theorem. All five selected +framework assumptions remain. The universal statement rests on the written +proof. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/robust-coordinate-pairing/README.md b/research/robust-coordinate-pairing/README.md new file mode 100644 index 0000000000..d35f9f3cd0 --- /dev/null +++ b/research/robust-coordinate-pairing/README.md @@ -0,0 +1,146 @@ +# Exact helper-pairing capacity under coordinate uncertainty + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped written algebraic proof with exact finite corroboration. +No new kappa is claimed. + +For any field, nominal matrix B and set E of independently uncertain entries, +the largest identity block recoverable by one fixed left/right pairing is + +```text +max { r : X (B + sum_E t_ij E_ij) Y = I_r for every t } + = max { rank B[A,C] : the rectangle A times C contains no entry of E }. +``` + +The theorem grants arbitrary dense field-valued X,Y. It supplies attaining +maps from a clean nonsingular minor. Testing just the nominal map and each +single-entry alternative gives the same capacity as the entire uncertainty +family. The proof works over small fields as well as R or C. + +For B=I, the capacity is exactly the independence number of the directed +error-support graph; loops forbid their vertices. Dense mixing gives no gain +over selecting independent coordinates. A directed n-cycle has sharp capacity +floor(n/2), even though the nominal and every single-entry alternative are +invertible. Five such uncertain entries therefore reduce five pointwise +recoverable channels to exactly two common channels. [PROOF.md](PROOF.md) +gives the quantified statements, proof and explicit boundary witnesses. + +This is an original contract obstruction for the optimistic identity-pairing +relaxation. It can reject a common helper contract when its uncertain pairing +has too little capacity. No selected supplier is asserted to have that +uncertainty model, and passing this test supplies no physical implementation. + +## Reproduce + +From the repository root with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/robust-coordinate-pairing/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/robust-coordinate-pairing/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/robust-coordinate-pairing +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/robust-coordinate-pairing --check-source-history +``` + +Substitute another absolute CPython 3.12 path elsewhere. Direct replay prints +`PASS_ROBUST_COORDINATE_PAIRING` in a generated JSON receipt bound to the six +package files by SHA256. It writes nothing and needs no Git, network, solver +or predecessor executable. Normal and optimized modes enforce the same checks. + +The exhaustive oracle considers every left/right matrix, not just coordinate +selectors. It compares the exact maximum against the clean-rectangle formula +on 10,266 support cases from 231 nominal matrices, examining 943,861 sandwiches +and finding 7,869 nominal identity sandwiches. The nominal domains are all +1-by-1 and 2-by-2 matrices over F2 and F3, all 2-by-3 and 3-by-2 matrices over +F2, and I3 over F2. Every possible uncertainty support is included in each +case. All 8,400 positive-capacity cases also receive a constructed attaining +pairing, checked against the nominal and every permitted single-entry change. + +Additional checks cover all 530 directed graphs with loops on one through +three vertices; fifteen cycle instances of lengths three through five over +Q, F2, F3, F5 and F7; and 112 rational nominal/support cases. Eight boundary +equalities and four rejecting omitted-error controls distinguish independent +uncertainty, correlated uncertainty, the identity nominal assumption, empty +and full uncertainty, singular nominal matrices and exact recovery. + +These are finite corroborations of the written theorem. They do not exhaust +all fields or dimensions and are not a proof-kernel certificate. + +## Scope, provenance and credit + +The complex-new-helper-inventory card changes scope to a common-pairing +interface lemma. This settles an explicitly changed algebraic premise rather +than delivering the card's physical supplier or complete signed moment. Work +stopped at the first proved result. The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19571898) +records the question before the proof and exhaustive computation. + +The base is canonical main e54523517d0f03e58352e647c403a5af3e525a57, priority +revision 8. The selected record gives conditional kappa 0.00363005817 and +`make frontier7000-verify`; the older priority prose describes an earlier +checkpoint. The selected binding-only orientation passed. The selected +scientific construction was not replayed. SOURCES pins the selected record +and original card as historical provenance; there are no live source inputs. + +The proof builds on classical rank inequalities, nonsingular minors and the +zero-outer-product property over fields. No contributor construction, word, +identity, invoice or numerical result is used as a premise. Ali Romman's +[#5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615) supplies the +surrounding dyadic helper-pairing context. Nick Petalas's +[#7269](https://github.com/CrocSwap/integer-mult-bounds/pull/7269) concerns odd +denominator budgets for a fixed pairing; his +[#6585](https://github.com/CrocSwap/integer-mult-bounds/pull/6585) requires +common-chart isolation with both cross blocks zero. Those results are +background and are neither extended nor audited here. No general literature +priority is claimed for elementary rank-factorization methods. + +Live open/account PR lists, recent handoff comments, active Discussions, +local reservations, the cached card search, targeted merged/open PR searches +and direct main-tree formula/object searches were inspected. Their text +coverage does not prove novelty or cover all diffs and unpublished work. + +## Limitations + +Only the retained identity block is constrained. Both spectator cross blocks, +arbitrary dirty restoration, chronology, extra workspace, adaptive charts, +correlated errors, approximation and coefficients in rings with zero divisors +require different arguments. Field-valued attaining maps need not be dyadic. +No actual cut, producer, consumer, scalar schedule, native realization, +precision/storage policy, physical hosting, paid/target invoice or complete +multiplication theorem is supplied. All five selected framework assumptions +remain. Independent human and formal proof-kernel review are unclaimed. +Lean, Docker and the selected scientific cold replay are unrun. + +## Open next questions + +- Does one actual helper cut require common pairings across a specified + independently varying coordinate family? Bind the producer's alternatives + and permitted charts first. Without that contract, this theorem does not + exclude the cut or imply a new supplier cost. +- What is the capacity for a supplied correlated error space? Begin with two + specified error generators. The skew-symmetric boundary witness shows why + replacing the space by the union of its entry supports can lose channels. + Physical delivery and complete invoices remain separate obligations. + +## Implementation bounds + +Build the Lever led to the rerunnable verifier. Prove It Works led to the +complete small-field sandwich oracle and explicit attaining maps. The +engineering playbook is autonomous local run, with a stop at the first proved +result. No shared code or frozen predecessor package is changed. + +All functions are below 60 physical lines. There is no recursion, subprocess, +network or dynamic code execution. The verifier has no external mathematical +input. Matrix dimensions are at most five; field enumerations store at most +512 matrices with nine entries each, and support tables have at most 512 +entries. Each exhaustive loop is bounded by these fixed finite domains. +The five-dimensional cycle check considers at most 1,024 rectangles. Explicit +exceptions retain mathematical checks under optimized execution. + +Power of Ten rule 3 has a managed-runtime deviation in verify.py: CPython +allocates bounded tuples, lists, integers and Fractions during this offline +calculation. The finite domains above bound live state; no fixed-pool or +steady-service claim is made. A fixed-storage implementation would need a +separate port. Rule 9 uses one fixed local sorting key for a finite rectangle +list and ordinary standard-library iterators; there is no user-supplied call +target. Warning-strict normal/optimized replay and in-memory compilation are +the available interpreter diagnostics. No separate static type analysis is +claimed. No production implementation is admitted by these checks. diff --git a/research/robust-coordinate-pairing/SOURCES.json b/research/robust-coordinate-pairing/SOURCES.json new file mode 100644 index 0000000000..5335fa97d9 --- /dev/null +++ b/research/robust-coordinate-pairing/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/robust-coordinate-pairing/TASK.json b/research/robust-coordinate-pairing/TASK.json new file mode 100644 index 0000000000..bcdaa9aeeb --- /dev/null +++ b/research/robust-coordinate-pairing/TASK.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?", + "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" + ], + "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": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.", + "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": [ + "productive helper", + "target refinement", + "5599", + "5614" + ], + "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 all-field common identity-pairing capacity under independent coordinate uncertainty, with sharp clean-submatrix and identity-graph formulas.", + "scope_change_reason": "Replace a physical helper inventory search by an original algebraic obstruction for one explicit changed common-pairing contract. No supplier or full signed invoice is delivered.", + "bottleneck_link": "Side result: a necessary identity-block capacity test for a proposed robust common helper interface. No selected supplier is asserted to require this uncertainty model; physical realization and complete costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved exact capacity theorem with finite independent-algorithm corroboration; package it without extending to correlated errors or actual supplier searches.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py: 10266 exhaustive nominal/support cases, 943861 sandwiches, 8400 attaining pairings, 530 graph cases, 15 cycle instances, 112 rational cases and four rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does an actual helper cut require this independent-coordinate common-pairing contract?", + "why_it_matters": "Only a source-bound contract allows applying the obstruction to a physical supplier.", + "first_step": "Pin its nominal matrix, exact alternatives and permitted charts.", + "blocked_by": "No actual producer or consumer has been assigned this uncertainty law." + }, + { + "question": "What is the capacity for two specified correlated error generators?", + "why_it_matters": "The skew example proves a union-of-supports replacement can undercount channels.", + "first_step": "Specify two matrices and solve their common sandwich equations.", + "blocked_by": "Independent-entry factorization does not apply; physical cost remains separate." + } + ], + "claim_type": "scoped written algebraic proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19571898", + "selected_orientation": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; selected kappa 0.00363005817; no selected scientific replay", + "engineering_playbook": "autonomous-run", + "environment": { + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "version": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "overlap": { + "open_pr_bodies": 760, + "discussion_records": 7345, + "remote_pagination_complete": true, + "open_pr_timestamp": "2026-11-12T18:19:39.779475+00:00", + "discussion_timestamp": "2026-11-12T18:21:50.339330+00:00", + "supplements": "Live handoffs and claims, main-tree distinctive formula/object terms, targeted all-state and merged PR searches; refreshed before commit. No exhaustive diff or unpublished-work coverage." + }, + "upstream_checkpoint": { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "priority_revision": 8, + "checked_utc": "2026-11-12T18:27:22.867837+00:00", + "changed_since_start": false + } +} diff --git a/research/robust-coordinate-pairing/VERIFY.json b/research/robust-coordinate-pairing/VERIFY.json new file mode 100644 index 0000000000..f9611a2bdb --- /dev/null +++ b/research/robust-coordinate-pairing/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": 120, + "checks": "Exhaustive literal sandwiches against clean-rectangle capacity, attaining maps, graph and rational cases, and hypothesis controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact mathematical checks with optimized execution; exceptions remain active." + } + ] +} diff --git a/research/robust-coordinate-pairing/verify.py b/research/robust-coordinate-pairing/verify.py new file mode 100644 index 0000000000..962ad62bbb --- /dev/null +++ b/research/robust-coordinate-pairing/verify.py @@ -0,0 +1,313 @@ +#!/usr/bin/env python3 +"""Exact clean-rectangle predictions versus complete small-field sandwiches.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def norm(value, prime): + return value % prime if prime else Fraction(value) + + +def eye(size): + return tuple(tuple(int(i == j) for j in range(size)) for i in range(size)) + + +def matrices(rows, columns, prime): + need(1 <= rows <= 3 and 1 <= columns <= 3, "enumeration shape") + need(prime in (2, 3) and prime ** (rows * columns) <= 512, "enumeration cap") + return tuple(tuple(tuple(flat[i * columns:(i + 1) * columns]) + for i in range(rows)) + for flat in product(range(prime), repeat=rows * columns)) + + +def multiply(left, right, prime): + need(left and right and len(left[0]) == len(right), "product shape") + need(max(len(left), len(right), len(right[0])) <= 5, "matrix cap") + return tuple(tuple(norm(sum(left[i][k] * right[k][j] + for k in range(len(right))), prime) + for j in range(len(right[0]))) + for i in range(len(left))) + + +def rank(matrix, prime): + if not matrix or not matrix[0]: + return 0 + work = [list(row) for row in matrix] + rows, columns = len(work), len(work[0]) + need(rows <= 5 and columns <= 5, "rank shape cap") + pivot = 0 + for column in range(columns): + candidates = [i for i in range(pivot, rows) if work[i][column]] + if not candidates: + continue + chosen = candidates[0] + work[pivot], work[chosen] = work[chosen], work[pivot] + value = work[pivot][column] + reciprocal = pow(value, -1, prime) if prime else 1 / Fraction(value) + work[pivot] = [norm(x * reciprocal, prime) for x in work[pivot]] + for i in range(rows): + if i != pivot: + factor = work[i][column] + work[i] = [norm(a - factor * b, prime) + for a, b in zip(work[i], work[pivot], strict=True)] + pivot += 1 + if pivot == rows: + break + return pivot + + +def inverse(matrix, prime): + size = len(matrix) + need(1 <= size <= 5 and all(len(row) == size for row in matrix), "inverse shape") + work = [list(row) + list(unit) + for row, unit in zip(matrix, eye(size), strict=True)] + for column in range(size): + candidates = [i for i in range(column, size) if work[i][column]] + need(candidates, "singular minor") + chosen = candidates[0] + work[column], work[chosen] = work[chosen], work[column] + value = work[column][column] + reciprocal = pow(value, -1, prime) if prime else 1 / Fraction(value) + work[column] = [norm(x * reciprocal, prime) for x in work[column]] + for i in range(size): + if i != column: + factor = work[i][column] + work[i] = [norm(a - factor * b, prime) + for a, b in zip(work[i], work[column], strict=True)] + result = tuple(tuple(row[size:]) for row in work) + need(multiply(matrix, result, prime) == eye(size), "inverse endpoint") + return result + + +def submatrix(matrix, rows, columns): + return tuple(tuple(matrix[i][j] for j in columns) for i in rows) + + +def rectangles(matrix, prime): + rows, columns = len(matrix), len(matrix[0]) + need(1 <= rows <= 5 and 1 <= columns <= 5, "rectangle cap") + records = [] + for row_mask in range(1 << rows): + chosen_rows = tuple(i for i in range(rows) if row_mask >> i & 1) + for column_mask in range(1 << columns): + chosen_columns = tuple(j for j in range(columns) if column_mask >> j & 1) + mask = sum(1 << (i * columns + j) + for i in chosen_rows for j in chosen_columns) + dimension = rank(submatrix(matrix, chosen_rows, chosen_columns), prime) + records.append((dimension, mask, chosen_rows, chosen_columns)) + return tuple(records) + + +def prediction(records, errors): + return max((row for row in records if not row[1] & errors), key=lambda row: row[0]) + + +def witness(matrix, record, prime): + dimension, _, rows, columns = record + if dimension == 0: + return (), tuple(() for _ in matrix[0]) + for chosen_rows in combinations(rows, dimension): + for chosen_columns in combinations(columns, dimension): + minor = submatrix(matrix, chosen_rows, chosen_columns) + if rank(minor, prime) != dimension: + continue + inv = inverse(minor, prime) + left = tuple(tuple(inv[a][chosen_rows.index(i)] if i in chosen_rows else 0 + for i in range(len(matrix))) + for a in range(dimension)) + right = tuple(tuple(int(j == chosen_columns[b]) for b in range(dimension)) + for j in range(len(matrix[0]))) + return left, right + raise ValueError("missing full-rank minor") + + +def changed(matrix, index, prime): + columns = len(matrix[0]) + return tuple(tuple(norm(value + int(i * columns + j == index), prime) + for j, value in enumerate(row)) + for i, row in enumerate(matrix)) + + +def check_pairing(matrix, left, right, errors, prime): + if not left: + return + dimension = len(left) + need(multiply(multiply(left, matrix, prime), right, prime) == eye(dimension), + "nominal pairing") + for index in range(len(matrix) * len(matrix[0])): + if errors >> index & 1: + alternative = changed(matrix, index, prime) + need(multiply(multiply(left, alternative, prime), right, prime) == eye(dimension), + "single-entry pairing") + + +def literal_sandwich(left, middle_right, prime): + """Separate oracle arithmetic: reject at the first nonidentity entry.""" + size = len(left) + for a in range(size): + for b in range(size): + value = 0 + for k in range(len(middle_right)): + value += left[a][k] * middle_right[k][b] + if value % prime != int(a == b): + return False + return True + + +def oracle(matrix, prime): + """Enumerate every X,Y; directly test every single-entry alternative.""" + rows, columns = len(matrix), len(matrix[0]) + capacities = [0] * (1 << (rows * columns)) + accepted, examined = 0, 0 + alternatives = tuple(changed(matrix, index, prime) for index in range(rows * columns)) + for dimension in range(1, min(rows, columns) + 1): + all_right = matrices(columns, dimension, prime) + right_products = tuple(multiply(matrix, right, prime) for right in all_right) + for left in matrices(dimension, rows, prime): + for right, middle_right in zip(all_right, right_products, strict=True): + examined += 1 + if not literal_sandwich(left, middle_right, prime): + continue + accepted += 1 + legal = 0 + for index, alternative in enumerate(alternatives): + alt_product = multiply(alternative, right, prime) + if literal_sandwich(left, alt_product, prime): + legal |= 1 << index + for errors in range(1 << (rows * columns)): + if not errors & ~legal: + capacities[errors] = max(capacities[errors], dimension) + return capacities, accepted, examined + + +def exhaustive_families(): + digest = sha256() + counts = {"nominal_matrices": 0, "support_cases": 0, "sandwiches_examined": 0, + "nominal_identity_sandwiches": 0, "attaining_pairings": 0} + domains = ((1, 1, 2), (1, 1, 3), (2, 2, 2), (2, 2, 3), + (2, 3, 2), (3, 2, 2), (3, 3, 2)) + for rows, columns, prime in domains: + samples = (eye(3),) if rows == columns == 3 else matrices(rows, columns, prime) + for matrix in samples: + capacities, accepted, examined = oracle(matrix, prime) + records = rectangles(matrix, prime) + counts["nominal_matrices"] += 1 + counts["sandwiches_examined"] += examined + counts["nominal_identity_sandwiches"] += accepted + for errors, capacity in enumerate(capacities): + record = prediction(records, errors) + need(record[0] == capacity, "rectangle/oracle disagreement") + left, right = witness(matrix, record, prime) + check_pairing(matrix, left, right, errors, prime) + counts["attaining_pairings"] += int(capacity > 0) + counts["support_cases"] += 1 + digest.update(json.dumps([prime, matrix, errors, capacity], separators=(",", ":")).encode()) + counts["capacity_table_sha256"] = digest.hexdigest() + return counts + + +def independent_set_size(size, errors): + maximum = 0 + for subset in range(1 << size): + valid = True + for i in range(size): + for j in range(size): + if subset >> i & 1 and subset >> j & 1 and errors >> (i * size + j) & 1: + valid = False + if valid: + maximum = max(maximum, subset.bit_count()) + return maximum + + +def graph_cases(): + counts = {"graphs": 0, "cycle_instances": 0} + for size in range(1, 4): + records = rectangles(eye(size), 2) + for errors in range(1 << (size * size)): + need(prediction(records, errors)[0] == independent_set_size(size, errors), + "graph capacity") + counts["graphs"] += 1 + for size in range(3, 6): + errors = sum(1 << (i * size + (i + 1) % size) for i in range(size)) + for prime in (0, 2, 3, 5, 7): + record = prediction(rectangles(eye(size), prime), errors) + need(record[0] == size // 2, "cycle floor") + check_pairing(eye(size), *witness(eye(size), record, prime), errors, prime) + for i in range(size): + alternative = changed(eye(size), i * size + (i + 1) % size, prime) + need(rank(alternative, prime) == size, "invertible cycle alternative") + counts["cycle_instances"] += 1 + return counts + + +def rational_cases(): + fixtures = (((Fraction(3, 2), 0), (0, Fraction(5, 8))), + ((0, 1), (1, 0)), ((1, 1), (1, 1)), + ((1, Fraction(1, 2), 0), (0, 1, Fraction(-3, 4)))) + checked = 0 + for matrix in fixtures: + records = rectangles(matrix, 0) + for errors in range(1 << (len(matrix) * len(matrix[0]))): + record = prediction(records, errors) + check_pairing(matrix, *witness(matrix, record, 0), errors, 0) + checked += 1 + return {"rational_support_cases": checked} + + +def controls(): + left = ((0, Fraction(-1, 2), Fraction(1, 2)), + (1, Fraction(1, 2), Fraction(-1, 2))) + right = ((1, 1), (-1, 0), (1, 0)) + skew = ((0, 1, 1), (-1, 0, 1), (-1, -1, 0)) + need(multiply(left, right, 0) == eye(2), "correlated nominal") + need(multiply(multiply(left, skew, 0), right, 0) == ((0, 0), (0, 0)), "correlated error") + complete = sum(1 << (i * 3 + j) for i in range(3) for j in range(3) if i != j) + need(prediction(rectangles(eye(3), 0), complete)[0] == 1, "independent/correlated gap") + swap = ((0, 1), (1, 0)) + need(prediction(rectangles(swap, 0), 9)[0] == 1, "nonidentity nominal") + need(independent_set_size(2, 9) == 0, "graph corollary nominal boundary") + rejected = 0 + for errors in (1, 2, 4, 8): + try: + check_pairing(eye(2), eye(2), eye(2), errors, 2) + except ValueError as error: + need(str(error) == "single-entry pairing", "wrong rejection") + rejected += 1 + else: + raise ValueError("omitted-error mutation accepted") + need(rank(((1, 0), (0, 0)), 2) == 1, "singular baseline rank") + need(prediction(rectangles(eye(2), 2), 0)[0] == 2, "empty uncertainty") + need(prediction(rectangles(eye(2), 2), 15)[0] == 0, "full uncertainty") + return {"boundary_equalities": 8, "omitted_error_rejections": rejected} + + +def source_hashes(): + root = Path(__file__).resolve().parent + names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + result = {} + for name in names: + data = (root / name).read_bytes() + need(len(data) <= 256 * 1024, "package-file size cap") + result[name] = sha256(data).hexdigest() + return result + + +def main(): + result = {"status": "PASS_ROBUST_COORDINATE_PAIRING", "claim_type": "scoped written proof", + "exhaustive": exhaustive_families(), "graph": graph_cases(), + "rational": rational_cases(), "controls": controls(), + "source_sha256": source_hashes()} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()