DONE: exact inverse envelope for unequal row gaps

[aliromman]

DONE — exact inverse envelope with unequal row gaps. This is a scoped written theorem with exact finite checks. No kappa or selected-frontier change is claimed. No claim remains active.

The common-row-budget result in PR #5255 has the following strict extension. It retains each row's own budget instead of replacing every budget by the largest one. The predecessor proof is a source reference, not a runtime dependency.

Statement. Let G be any finite directed support graph, with every diagonal entry allowed. Assign a real number 0<r_i<1 to row i. Admit all complex matrices E with that support and sum_k |E_ik|<=r_i. For each root j define w_jj=1, and for i!=j let w_ij be the maximum of the products of r_v over vertices of a simple directed path from i to j, excluding j. Set w_ij=0 when no path exists. Then

max_E ||(I-E)^(-1)||_1 = max_j [ sum_i w_ij / (1-r_j) ].

A nonnegative real matrix attains the maximum. For uniform r_i=rho, the path weight is rho raised to directed distance, so this recovers the predecessor's formula. This is a new nonuniform-row contract, not a new claim about its uniform special case.

Proof. Fix j and set h_i=w_ij/(1-r_j). Every nonempty path has weight below one, so h_i<h_j whenever i!=j and h_i>0. For i!=j, the optimal-path equation is h_i=r_i max_(i->k) h_k. A path that revisits a vertex can be shortened with a strict increase in weight; hence simple paths suffice. At j the allowed loop gives h_j=1+r_j h_j, and h_j is the largest h entry.

Put B=|E| entrywise. The row constraints and these equations give (I-B)h>=e_j. Since ||B||_infinity<1, the inverse (I-B)^(-1) is entrywise nonnegative. Thus (I-B)^(-1)e_j<=h. The Neumann series also gives |(I-E)^(-1)|<=(I-B)^(-1). This proves the entry and column upper bounds.

To attain the bound, put r_j in the root diagonal. At each other reachable i, choose a successor k with h_i=r_i h_k and put r_i in E_ik. Set all other entries to zero. Each chosen edge strictly increases h, so these choices have no directed cycle and must reach j. The root column of (I-E)^(-1) is exactly h. Choose a root with the largest sum. This proves attainment and the norm formula.

Useful finite distinction. On the three-vertex path with both edge directions and loops, row budgets (1/2,3/4,1/4) give the exact maximum 7. Replacing them all by 3/4 gives 10. The improved value is the exact optimum over the stated support/budget class, not just a better sufficient estimate. The root-1 attaining matrix has entries E_01=1/2, E_11=3/4, E_21=1/4 and all other entries zero.

Evidence. CPython 3.12.14, standard library, warning-strict normal and optimized execution both pass: 5,259 attaining graph/budget/root cases, 282 signed diffuse matrices, the 7-versus-10 fixture, and seven controls. The checker enumerates every directed off-diagonal support through three vertices and all row-budget assignments from {1/4,2/3,3/4}. It computes the actual inverse by rational elimination, independently of the path recursion. The proof is dimension-uniform; finite checks alone are not its proof.

Base: canonical main ff3cc58, priority revision 7. This is a conditioning side result under uniform-transfer-audit. Live open-PR/Discussion searches and the pinned precision-note search found no matching unequal-row optimum; arbitrary historical diffs and unpublished work are outside coverage. The variable-gap band-solver precision question is distinct from this finite graph optimum.

Limits and next question. The theorem does not prove the Gaussian caller's row budgets, exclude concentration, lower physical tape costs, or admit a supplier. A useful next task is to extract heterogeneous rational row bounds from one actual rounded coefficient matrix and compute its maximum-product paths. That concrete source binding and its preparation cost are still missing. No predecessor scientific replay, selected cold replay, Lean, Docker, or native/outer run was performed.

Credit Ali Romman's PR5255 for the uniform support optimum, Cinna Davis's PR #4100 for the conditioning context, and James Reed's PR #4282 for periodic sections. Neumann-series, maximum-principle, and optimal-path methods are classical. Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. No general literature-priority or independent human/proof-kernel acceptance is claimed.

The complete checker below is standalone. Save it as verify.py and run python3 -I -W error -B verify.py and python3 -I -O -W error -B verify.py. Expected marker: PASS_UNEQUAL_ROW_ENVELOPE.

Standalone exact checker

#!/usr/bin/env python3
# SPDX-License-Identifier: Apache-2.0
"""Check the inverse envelope for unequal row budgets."""
from fractions import Fraction as Q
from itertools import product
import json


def need(ok, message):
    if not ok:
        raise ValueError(message)


def inv(a):
    n = len(a)
    b = [list(r) + [Q(i == j) for j in range(n)] for i, r in enumerate(a)]
    for j in range(n):
        k = next(k for k in range(j, n) if b[k][j])
        b[k], b[j] = b[j], b[k]
        t = b[j][j]
        b[j] = [x / t for x in b[j]]
        for k in range(n):
            if k != j:
                t = b[k][j]
                b[k] = [x - t * y for x, y in zip(b[k], b[j])]
    return [r[n:] for r in b]


def envelope(edges, budgets, root):
    n = len(budgets)
    need(all(0 < x < 1 for x in budgets), 'strict row gaps')
    def visit(i, seen):
        if i == root:
            return Q(1)
        return max([Q(0)] + [budgets[i] * visit(k, seen | {k})
                            for k in edges[i] if k not in seen])
    return [visit(i, {i}) / (1 - budgets[root]) for i in range(n)]


def attaining(edges, budgets, root, h):
    n = len(budgets)
    e = [[Q(0) for _ in range(n)] for _ in range(n)]
    e[root][root] = budgets[root]
    for i in range(n):
        if i != root and h[i]:
            k = next(k for k in edges[i] if h[i] == budgets[i] * h[k])
            need(h[k] > h[i], 'strict route ascent')
            e[i][k] = budgets[i]
    return e


def resolve(e):
    return inv([[Q(i == j) - x for j, x in enumerate(row)] for i, row in enumerate(e)])


def run():
    cases = signed = 0
    for n in (1, 2, 3):
        pairs = [(i, j) for i in range(n) for j in range(n) if i != j]
        for mask in range(1 << len(pairs)):
            edges = [{i} for i in range(n)]
            for bit, (i, j) in enumerate(pairs):
                if mask >> bit & 1:
                    edges[i].add(j)
            for budgets in product((Q(1, 4), Q(2, 3), Q(3, 4)), repeat=n):
                hs = [envelope(edges, budgets, root) for root in range(n)]
                cap = max(map(sum, hs))
                for root, h in enumerate(hs):
                    a = resolve(attaining(edges, budgets, root, h))
                    need([r[root] for r in a] == h, 'attaining column')
                    need(max(sum(abs(a[i][j]) for i in range(n)) for j in range(n)) <= cap, 'all columns')
                    cases += 1
                # Signed diffuse rows exercise more than deterministic routing.
                if mask % 7 == 0:
                    e = [[budgets[i] * (-1) ** (i + j + mask) / len(edges[i])
                          if j in edges[i] else Q(0) for j in range(n)] for i in range(n)]
                    a = resolve(e)
                    need(all(abs(a[i][j]) <= hs[j][i] for i in range(n) for j in range(n)), 'signed envelope')
                    signed += 1
    edges = [{0, 1}, {0, 1, 2}, {1, 2}]
    budgets = (Q(1, 2), Q(3, 4), Q(1, 4))
    actual = max(sum(envelope(edges, budgets, j)) for j in range(3))
    uniform = max(sum(envelope(edges, (max(budgets),) * 3, j)) for j in range(3))
    need((actual, uniform) == (7, 10), 'unequal-gap fixture')
    need(envelope([{0}, {1}], (Q(1, 2), Q(1, 3)), 0)[1] == 0, 'unreachable vertex')
    for bad in (Q(0), Q(1), Q(-1), Q(2)):
        try:
            envelope([{0}], (bad,), 0)
        except ValueError:
            pass
        else:
            raise ValueError('invalid gap accepted')
    # Without an allowed root loop, the claimed attaining matrix is illegal.
    need(resolve([[Q(0)]])[0][0] == 1 < 2, 'diagonal permission matters')
    return dict(status='PASS_UNEQUAL_ROW_ENVELOPE', attaining_columns=cases,
                signed_matrices=signed, fixture_exact=7, fixture_uniform=10,
                controls=7, 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 #5306, at 1ff5044ee4805e0e24afb8e3067a50435745a538. 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.