Joint safety criterion and least-barrier update for coefficient changes

research/coupled-comparison-barrier/README.md

@@ -0,0 +1,79 @@
+# Joint safety criterion and least-barrier update for coefficient changes
+
+DONE — a joint safety test and exact least-barrier update for several coefficient changes. Scoped proof with exact finite checks; no new kappa. No claim remains active.
+
+The rank-one result in [Discussion #5263](https://github.com/CrocSwap/integer-mult-bounds/discussions/5263) does not permit separate tests to be composed without checking their interaction. The following criterion handles all nonnegative low-rank deteriorations at once and gives a strict counterexample to that shortcut on the same retained source fixture.
+
+**Statement.** Let M be a real Z-matrix: its off-diagonal entries are nonpositive. Suppose some w>0 satisfies Mw>0. Let U,V be nonnegative n-by-k matrices, and define
+
+```text
+M_new = M - U V^T,
+X = M^(-1) U,
+C = V^T X.
+```
+
+Then M_new has a positive dominance witness if and only if the spectral radius rho(C)<1. When this holds, for every residual envelope r>=0 the componentwise least supersolution of M_new d>=r is
+
+```text
+h_new = h + X (I-C)^(-1) V^T h,    h=M^(-1)r.
+```
+
+At rho(C)=1 the comparison matrix is singular. For a common multiplier tau on the whole update, the exact witness domain is tau rho(C)<1. If rho(C)=0, every finite nonnegative tau is allowed. A large allowed update can still produce a large, unhelpful error barrier.
+
+**Proof.** The source positive-witness argument gives M^(-1)>=0: scale columns by w and normalize the positive diagonal to obtain a strictly row-substochastic nonnegative Neumann remainder. In particular, M^(-1)1>0. This same argument applies to any Z-matrix with a positive dominance witness.
+
+If rho(C)<1, the Neumann series gives (I-C)^(-1)>=0. Direct multiplication gives the Woodbury inverse
+
+```text
+M_new^(-1) = M^(-1) + X (I-C)^(-1) V^T M^(-1) >= 0.
+```
+
+Applying this inverse to 1 supplies a positive dominance witness; applying it to r supplies h_new. Multiplication of any supersolution inequality by the nonnegative inverse proves minimality.
+
+For necessity, suppose rho(C)>=1. Perron-Frobenius theory gives a nonzero v>=0 with Cv=rho(C)v. Put x=Xv. It is nonzero, since otherwise Cv=0. It is also nonnegative, and
+
+```text
+M_new x = (1-rho(C)) Uv <= 0.
+```
+
+A positive dominance witness for M_new would give a nonnegative inverse, hence x<=0, a contradiction. At equality the same nonzero x is a null vector. Scaling U by tau scales C by tau and proves the threshold statement.
+
+**Principal windows.** For any complex source whose comparison matrix is componentwise at least M_new, the predecessor maximum principle gives the residual bound h_new on every principal window. Indeed, nonpositive off-diagonal entries and h_new>=0 imply (M_new)_J (h_new)_J>=r_J. The same updated vector therefore covers every ordered sequence of windows from the changed source. Losing this witness is not proof that every signed or complex source in the comparison class is singular.
+
+**A source-bound failure of separate tests.** The [retained setup fixture](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/sliding-window-inverse/inputs/gaussian_check_setup.py) has comparison matrix
+
+```text
+M = [[4,-1,0],[-1/3,5,-1/2],[0,-1/4,3]].
+```
+
+Change the magnitudes at positions (0,1) and (1,0) by s,t>=0. The exact joint safety condition is
+
+```text
+(1+s)(1+3t) < 119/2.
+```
+
+Eliminating the unchanged third row leaves the positive-diagonal two-by-two Z-matrix with diagonal (4,119/24) and off-diagonal entries -(1+s), -(1/3+t). Its determinant proves the condition. Equivalently, det(M_new)=119/2-(1+s)(1+3t).
+
+The separate tests allow s<117/2 and t<39/2. Nevertheless s=8,t=2 fails jointly: 9*7=63>119/2. Both single changes are far below their individual thresholds. The coupled pair s=t=3 is safe. For k=2 the general spectral condition can also be tested exactly as C_11<1, C_22<1 and (1-C_11)(1-C_22)>C_12 C_21; no floating eigenvalue computation is required.
+
+**Prepared-update cost.** With fixed directions U,V and retained factors of M, preparing X uses k solves and forming C costs O(n k^2) field operations. For later nonnegative diagonal amplitude changes U diag(t), retain X, C, h and V^T h. Each barrier update then needs a k-by-k solve plus O(nk) operations, after the relevant joint safety test. Factorization, exact coefficient growth, source reads and physical storage/movement remain paid. These are arithmetic counts, not a bit-complexity claim.
+
+**Evidence.** Both warning-strict normal and optimized CPython 3.12.14 checks pass all 375 tested pairs of source positions and update sizes: 312 safe and 63 unsafe. They compare the coupling criterion with all principal minors of the changed matrix, compare prepared updates with a separate permutation-determinant Cramer solve, check 8,112 principal-window residual vertices, and check four exact singular boundaries and the separate-test counterexample. All computations are rational.
+
+Base: canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7. Main and live open-PR/Discussion overlap were refreshed. This numerical-recovery side result changes the `uniform-transfer-audit` scope to simultaneous updates. It does not repeat the predecessor's rank-one result or supply a production caller.
+
+Credit Nick Petalas's [PR #5119](https://github.com/CrocSwap/integer-mult-bounds/pull/5119) and [least-barrier proof](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/window-comparison-barrier/README.md), Ali Romman's Discussion5263 rank-one update, David Ganz / Dugongue's [PR #3872](https://github.com/CrocSwap/integer-mult-bounds/pull/3872), and Jose Manuel's [PR #3851](https://github.com/CrocSwap/integer-mult-bounds/pull/3851) setup fixture. Woodbury, M-matrix and Perron-Frobenius theory are classical; no general priority claim is made.
+
+**Remaining task.** Bind one actual multi-coefficient update to fixed nonnegative directions and retained factors, then charge the full update path. Native/outer admission, a production Gaussian page, source preparation and tape costs remain open. No predecessor scientific suite, selected cold replay, Lean or Docker build was run. Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. No independent human or proof-kernel acceptance is claimed.
+
+## Reproduce
+
+```sh
+python3 -B scripts/research_package.py --package research/coupled-comparison-barrier
+```
+
+Use Python 3.12 with the standard library. The normal and optimized commands must print `PASS_COUPLED_BARRIER`. The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The checker has no external runtime inputs.
+
+## Open next questions
+
+Bind a real multi-coefficient update to fixed nonnegative directions and price the complete update. The source binding and physical cost model are not supplied by this package. See `TASK.json` for the structured scope.

research/coupled-comparison-barrier/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "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"
+    }
+  ]
+}

research/coupled-comparison-barrier/TASK.json

@@ -0,0 +1,79 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "This scoped proof replaces separate coefficient checks with one exact joint condition. For a nonnegative rank-k subtraction from a retained comparison matrix, the updated matrix has a positive barrier exactly when the small feedback matrix has spectral radius below one. A rational example passes each separate test but fails jointly.",
+  "scope_change_reason": "This is a scoped interface theorem. It does not complete the original supplier or uniform-transfer task.",
+  "bottleneck_link": "Bind a real multi-coefficient update to fixed nonnegative directions and price the complete update.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the scoped proof, exact controls and bounded registered replay; do not expand to physical lowering.",
+  "outcome": "completed",
+  "evidence": "375 updates, 8,112 principal-window residual vertices and four singular boundaries",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or proof-kernel acceptance is claimed.",
+  "open_questions": [
+    {
+      "question": "Bind a real multi-coefficient update to fixed nonnegative directions and price the complete update.",
+      "why_it_matters": "The abstract result needs an actual caller and a complete cost model.",
+      "first_step": "Bind a real multi-coefficient update to fixed nonnegative directions and price the complete update.",
+      "blocked_by": "No production caller or physical cost model is supplied."
+    }
+  ],
+  "upstream_checkpoint": {
+    "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+    "priority_revision": 7,
+    "checked_at": "2026-10-23T16:51:42.319588+00:00"
+  }
+}

research/coupled-comparison-barrier/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": "375 updates, 8,112 principal-window residual vertices and four singular boundaries"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "375 updates, 8,112 principal-window residual vertices and four singular boundaries"
+    }
+  ]
+}

research/coupled-comparison-barrier/verify.py

@@ -0,0 +1,90 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Check coupled comparison-barrier updates with exact independent solves."""
+from fractions import Fraction as Q
+from itertools import permutations, product, combinations
+import json
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def det(a):
+    n = len(a); total = Q(0)
+    for p in permutations(range(n)):
+        term = Q((-1)**sum(p[i] > p[j] for i in range(n) for j in range(i+1, n)))
+        for i in range(n):
+            term *= a[i][p[i]]
+        total += term
+    return total
+
+
+def cramer(a, b):
+    d = det(a); need(d != 0, 'singular matrix')
+    return [det([[b[i] if j == k else a[i][j] for j in range(len(a))]
+                 for i in range(len(a))])/d for k in range(len(a))]
+
+
+def solve(a, b):
+    n = len(a); rows = [list(r) + [b[i]] for i, r in enumerate(a)]
+    for j in range(n):
+        k = next(k for k in range(j, n) if rows[k][j])
+        rows[j], rows[k] = rows[k], rows[j]
+        d = rows[j][j]; rows[j] = [x/d for x in rows[j]]
+        for k in range(n):
+            if k != j:
+                d = rows[k][j]; rows[k] = [x-d*y for x, y in zip(rows[k], rows[j])]
+    return [r[-1] for r in rows]
+
+
+M = [[Q(4), Q(-1), Q(0)], [Q(-1, 3), Q(5), Q(-1, 2)], [Q(0), Q(-1, 4), Q(3)]]
+
+
+def run():
+    directions = [(i, j) for i in range(3) for j in range(3) if i != j]
+    h = solve(M, [Q(1)]*3)
+    need(h == [Q(49,156), Q(10,39), Q(83,234)], 'retained source fixture')
+    prepared = [solve(M, [Q(k == i) for k in range(3)]) for i in range(3)]
+    safe = unsafe = windows = 0
+    for d0, d1 in combinations(directions, 2):
+        for s, t in product((Q(0), Q(1,2), Q(2), Q(8), Q(20)), repeat=2):
+            ds = (d0, d1); ts = (s, t)
+            x = [[prepared[ds[j][0]][i]*ts[j] for j in range(2)] for i in range(3)]
+            c = [[x[ds[i][1]][j] for j in range(2)] for i in range(2)]
+            small = [[Q(i == j)-c[i][j] for j in range(2)] for i in range(2)]
+            admissible = c[0][0] < 1 and c[1][1] < 1 and det(small) > 0
+            a = [r[:] for r in M]
+            for (i,j), tau in zip(ds, ts):
+                a[i][j] -= tau
+            principal_positive = all(det([[a[i][j] for j in J] for i in J]) > 0
+                                     for k in range(1,4) for J in combinations(range(3),k))
+            need(admissible == principal_positive, 'coupling criterion versus all principal minors')
+            if not admissible:
+                unsafe += 1
+                continue
+            y = solve(small, [h[d0[1]], h[d1[1]]])
+            updated = [h[i]+sum(x[i][j]*y[j] for j in range(2)) for i in range(3)]
+            need(updated == cramer(a, [Q(1)]*3), 'prepared update versus fresh Cramer solve')
+            for k in range(1, 4):
+                for J in combinations(range(3), k):
+                    block = [[a[i][j] for j in J] for i in J]
+                    for signs in product((-1,1), repeat=k):
+                        e = cramer(block, list(map(Q,signs)))
+                        need(all(abs(v) <= updated[i] for i,v in zip(J,e)), 'principal-window residual')
+                        windows += 1
+            safe += 1
+    for s in (Q(0), Q(1), Q(8), Q(20)):
+        t = (Q(119,2)/(1+s)-1)/3
+        a = [r[:] for r in M];a[0][1]-=s;a[1][0]-=t
+        need(det(a) == 0, 'exact coupled threshold')
+    need(8 < Q(117,2) and 2 < Q(39,2) and (1+8)*(1+3*2) > Q(119,2), 'separate checks miss coupling')
+    need((1+3)*(1+3*3) < Q(119,2), 'safe joint fixture')
+    return dict(status='PASS_COUPLED_BARRIER', safe_updates=safe, unsafe_updates=unsafe,
+                window_vertices=windows, singular_thresholds=4,
+                independent_safety_foil=True, no_new_kappa=True)
+
+
+if __name__ == '__main__':
+    print(json.dumps(run(), sort_keys=True))