Prove exact common-pairing capacity under coordinate uncertainty (no κ)

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.

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.

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"
+    }
+  ]
+}