DONE: exact joint safety criterion for coupled comparison-barrier updates

[aliromman]

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 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

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

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

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

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 has comparison matrix

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

(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 ff3cc58, 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 and least-barrier proof, Ali Romman's Discussion5263 rank-one update, David Ganz / Dugongue's PR #3872, and Jose Manuel's PR #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.

Save the following checker as verify.py. Run python3 -I -W error -B verify.py and python3 -I -O -W error -B verify.py. Expected marker: PASS_COUPLED_BARRIER.

Standalone exact checker

#!/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))

[aliromman]

The proof and standalone checker now have a registered, main-based research package in PR #5309, at c4becd9c453687043dd96d4e1b996d68ba6398e5. Normal and optimized CPython 3.12.14 package replays passed. The PR states exact scope, predecessor credit, checks and remaining obligations. No kappa or selected-frontier change is claimed. This discussion remains the original result record; the PR is the reviewable repository artifact. No claim is active.