Exact inverse envelope for unequal row contraction budgets

research/unequal-row-resolvent/README.md

@@ -0,0 +1,41 @@
+# Exact inverse envelope for unequal row contraction budgets
+
+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](https://github.com/CrocSwap/integer-mult-bounds/pull/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](https://github.com/aliromman/integer-mult-bounds/blob/d63d8848442acc0bdc7b62578e12726c530af3fa/research/sharp-banded-resolvent/README.md) 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
+
+```text
+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 ff3cc58e370d0f678e529246f8c73e8094e18fcf, 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](https://github.com/CrocSwap/integer-mult-bounds/pull/4100) for the conditioning context, and James Reed's [PR #4282](https://github.com/CrocSwap/integer-mult-bounds/pull/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.
+
+## Reproduce
+
+```sh
+python3 -B scripts/research_package.py --package research/unequal-row-resolvent
+```
+
+Use Python 3.12 with the standard library. The normal and optimized commands must print `PASS_UNEQUAL_ROW_ENVELOPE`. The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The checker has no external runtime inputs.
+
+## Open next questions
+
+Extract unequal rational row budgets from one emitted coefficient matrix and charge their preparation. The source binding and physical cost model are not supplied by this package. See `TASK.json` for the structured scope.

research/unequal-row-resolvent/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/unequal-row-resolvent/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 gives the exact worst column norm of an inverse under unequal row contraction budgets and a fixed directed support. Maximum-product paths give an attaining matrix for every column. It extends the uniform-budget result without imposing a common worst row gap.",
+  "scope_change_reason": "This is a scoped interface theorem. It does not complete the original supplier or uniform-transfer task.",
+  "bottleneck_link": "Extract unequal rational row budgets from one emitted coefficient matrix and charge their preparation.",
+  "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": "5,259 attaining columns, 282 signed matrices and seven controls",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or proof-kernel acceptance is claimed.",
+  "open_questions": [
+    {
+      "question": "Extract unequal rational row budgets from one emitted coefficient matrix and charge their preparation.",
+      "why_it_matters": "The abstract result needs an actual caller and a complete cost model.",
+      "first_step": "Extract unequal rational row budgets from one emitted coefficient matrix and charge their preparation.",
+      "blocked_by": "No production caller or physical cost model is supplied."
+    }
+  ],
+  "upstream_checkpoint": {
+    "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+    "priority_revision": 7,
+    "checked_at": "2026-10-23T16:46:30.808561+00:00"
+  }
+}

research/unequal-row-resolvent/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": "5,259 attaining columns, 282 signed matrices and seven controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "5,259 attaining columns, 282 signed matrices and seven controls"
+    }
+  ]
+}

research/unequal-row-resolvent/verify.py

@@ -0,0 +1,101 @@
+#!/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))