Prove the sharp graph-support inverse norm envelope

research/sharp-banded-resolvent/README.md

@@ -0,0 +1,106 @@
+# Exact inverse norms from a directed support graph
+
+This is a scoped mathematical proof with exact finite checks. It gives the
+sharp inverse 1-norm allowed by the row-gap and support hypotheses in
+Cinna Davis's PR #4100 conditioning note. The complete kappa calculation
+and the selected frontier do not change.
+
+## The result
+
+Let G be a finite directed graph on n vertices. Allow every diagonal entry.
+An edge i to j permits the entry E[i,j]. Let 0 < rho < 1 and
+`sum_j |E[i,j]| <= rho` for each row. Write d(i,j) for directed distance,
+with `rho^infinity = 0`, and put delta = 1-rho. Then
+
+```text
+max_E ||(I-E)^-1||_1 = max_j sum_i rho^d(i,j) / delta.
+```
+
+This is a maximum over all complex matrices with that support and row
+budget. Nonnegative real matrices attain it. Diagonal permission is a
+hypothesis of attainment, not a condition needed for the upper bound.
+
+### Proof
+
+The Neumann series converges because `||E||_infinity <= rho < 1`.
+A length-k path cannot connect i to j when k < d(i,j). Also
+`|(E^k)[i,j]| <= ||E^k||_infinity <= rho^k`. Thus the absolute value of
+entry (i,j) of the inverse is at most `rho^d(i,j)/delta`. Sum each column
+and take the largest sum.
+
+Fix a maximizing root j. Give the root a diagonal entry rho. From each
+other vertex that can reach j, choose one edge that reduces its distance
+to j by one and put rho in that entry. Put zero in all other entries.
+A row that cannot reach j is zero. This matrix has the required support
+and row budget. Its k-th power has entry (i,j) equal to zero for k < d(i,j)
+and rho^k for k >= d(i,j). The root column of its inverse therefore
+attains every entry bound at once. This proves equality.
+
+### Banded lines and the conditioning consequence
+
+For the line with vertices `-mb,...,mb`, permit `|i-j| <= b`, where b,m
+are positive integers. Distance to zero is `ceil(|i|/b)`. The root-routing
+matrix above has column sum
+
+```text
+[1 + 2b sum_(k=1)^m rho^k] / delta.
+```
+
+The difference from the bound in INVERSE-CONDITIONING.md is exactly
+`2b rho^(m+1)/delta^2`. Consequently the dimension-independent ceiling
+`1/delta + 2b rho/delta^2` is the exact supremum over finite dimensions.
+Its constants cannot decrease using only these hypotheses. This does not
+state that a Gaussian matrix attains the ceiling.
+
+The squared Euclidean norm of the same column is
+`[1 + 2b sum_(k=1)^m rho^(2k)]/delta^2`. The operator 2-norm is at least
+that column norm. As m tends to infinity its square tends to
+`[1 + 2b rho^2/(1-rho^2)]/delta^2`. For fixed b and delta tending to zero,
+this is asymptotic to `b/delta^3`. The existing upper bound is asymptotic
+to `2b/delta^3`. Thus the power delta^(-3/2) in the operator 2-norm cannot
+improve uniformly in dimension. An exact operator 2-norm constant is not
+claimed.
+
+## Evidence and reproduction
+
+Use Python 3.12 or newer; the standard library is sufficient.
+
+```sh
+python3 -I -B research/sharp-banded-resolvent/verify.py
+python3 -I -O -B research/sharp-banded-resolvent/verify.py
+python3 -B scripts/research_package.py --package research/sharp-banded-resolvent
+```
+
+Expected marker: `PASS_SHARP_BANDED_RESOLVENT`. The checker uses rational
+Gauss-Jordan inverses, independently of the path formula. It exhausts every
+directed off-diagonal support through three vertices, two row budgets and
+every root: 402 attaining columns. It also checks 120 signed rational
+matrices and 24 banded instances. Six controls reject invalid budgets or
+diagonal permission and refute row-only inverse norm shortcuts. Checks
+remain active under Python -O. The universal theorem rests on the proof
+above; finite checks corroborate it.
+
+## Scope, sources and credit
+
+Cinna Davis supplies the original bound and Gaussian caller in
+[PR #4100](https://github.com/CrocSwap/integer-mult-bounds/pull/4100).
+James Reed supplies the periodic-section extension in
+[PR #4282](https://github.com/CrocSwap/integer-mult-bounds/pull/4282).
+Their source files are pinned in SOURCES.json at main
+`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. Neumann series, graph distance,
+and induced matrix norms are classical; no literature-priority claim is made.
+This package adds the exact support-dependent optimum and an attaining
+family. It does not rerun either predecessor's scientific suite.
+
+The Gaussian row gap, rounded coefficients, physical tape cost, complete
+supplier, outer recovery and unconditional multiplication theorem remain
+outside scope. No Lean, Docker or selected-frontier cold replay was run.
+Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+No independent human review or proof-kernel verification is claimed.
+
+## Open next questions
+
+Can the actual Gaussian caller supply a column budget or a reversible
+weighted measure that excludes this directed concentration? First bind such
+a condition to its rounded matrix. That source-specific condition is the
+blocker; the present row-only class cannot justify a smaller uniform order.

research/sharp-banded-resolvent/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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"
+    },
+    {
+      "path": "research/narrow-neumann-section/README.md",
+      "usage": "input",
+      "git_blob": "212a46e54e66e1581c7ddb0cc77951522ae28c94",
+      "sha256": "569954703531b826a3251fd0888dd1c78eca1a63e1e3238c3c07df3d8459b0d7"
+    },
+    {
+      "path": "research/unconditional-batched-crt/INVERSE-CONDITIONING.md",
+      "usage": "input",
+      "git_blob": "3853ffac91dfed5421b05533eb274a8646741071",
+      "sha256": "be3e4b729481b15a5ccc286b297908e4f9cef94c0c9144a28ee1cf58950d142a"
+    }
+  ]
+}

research/sharp-banded-resolvent/TASK.json

@@ -0,0 +1,82 @@
+{
+  "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": "Exact inverse 1-norm envelope for a finite directed support and row contraction; sharp banded specialization.",
+  "scope_change_reason": "Determine whether the source hypotheses permit a smaller uniform conditioning allowance.",
+  "bottleneck_link": "The Gaussian precision caller uses the row-gap estimate. Sharpness identifies needed extra structure.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the envelope, attaining family and spectral-order consequence.",
+  "outcome": "completed",
+  "evidence": "README.md proof and verify.py exact rational inverse checks.",
+  "author": "Ali Romman with OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance with proof, implementation, checks and publication.",
+  "open_questions": [
+    {
+      "question": "Does the rounded Gaussian caller have a useful column budget or reversible weighted measure?",
+      "why_it_matters": "Such structure could exclude the extremal concentration.",
+      "first_step": "Bind the condition to one pinned rounded matrix.",
+      "blocked_by": "No such caller-bound condition is supplied here."
+    }
+  ],
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147345",
+    "open_prs": 317,
+    "discussion_records": 4501,
+    "tracked_note_paths": 7091,
+    "checked_at": "2026-10-23T14:06:10Z",
+    "limits": "No arbitrary diffs or unpublished-work coverage."
+  }
+}

research/sharp-banded-resolvent/VERIFY.json

@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/narrow-neumann-section/README.md",
+    "research/unconditional-batched-crt/INVERSE-CONDITIONING.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact inverse envelope, attaining columns, signed controls and banded limits."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same checks with Python optimization enabled."
+    }
+  ]
+}

research/sharp-banded-resolvent/verify.py

@@ -0,0 +1,136 @@
+#!/usr/bin/env python3
+"""Check the support envelope. Ali Romman / OpenAI Codex. Apache-2.0."""
+from fractions import Fraction as F
+from itertools import product
+import json
+import random
+
+
+def require(value, message):
+    if not value:
+        raise ValueError(message)
+
+
+def inverse(a):
+    n = len(a)
+    t = [[F(x) for x in row] + [F(i == j) for j in range(n)] for i, row in enumerate(a)]
+    for j in range(n):
+        pivot = next(i for i in range(j, n) if t[i][j])
+        t[j], t[pivot] = t[pivot], t[j]
+        c = t[j][j]
+        t[j] = [x / c for x in t[j]]
+        for i in range(n):
+            if i != j:
+                c = t[i][j]
+                t[i] = [x - c*y for x, y in zip(t[i], t[j])]
+    return [row[n:] for row in t]
+
+
+def distances(edges, root):
+    n = len(edges)
+    d = [None] * n
+    d[root] = 0
+    queue = [root]
+    for j in queue:
+        for i in range(n):
+            if edges[i][j] and d[i] is None:
+                d[i] = d[j] + 1
+                queue.append(i)
+    return d
+
+
+def envelope(edges, rho):
+    require(F(0) < rho < F(1), "rho must be in (0,1)")
+    require(all(edges[i][i] for i in range(len(edges))), "diagonal support is required")
+    return [sum((rho**d for d in distances(edges, j) if d is not None), F(0)) / (1-rho)
+            for j in range(len(edges))]
+
+
+def route(edges, root, rho):
+    d = distances(edges, root)
+    n = len(edges)
+    e = [[F(0)] * n for _ in range(n)]
+    e[root][root] = rho
+    for i in range(n):
+        if i != root and d[i] is not None:
+            j = next(j for j in range(n) if edges[i][j] and d[j] == d[i] - 1)
+            e[i][j] = rho
+    return e
+
+
+def resolvent(e):
+    return inverse([[F(i == j)-x for j, x in enumerate(row)] for i, row in enumerate(e)])
+
+
+def check_matrix(edges, e, rho):
+    require(all(sum(map(abs, row)) <= rho for row in e), "row budget")
+    require(all(not e[i][j] or edges[i][j] for i in range(len(e)) for j in range(len(e))), "support")
+    r = resolvent(e)
+    for j, bound in enumerate(envelope(edges, rho)):
+        require(sum(abs(row[j]) for row in r) <= bound, "column bound")
+    return r
+
+
+def main():
+    graph_roots = 0
+    for n in range(1, 4):
+        off = [(i, j) for i in range(n) for j in range(n) if i != j]
+        for bits in product((0, 1), repeat=len(off)):
+            edges = [[i == j for j in range(n)] for i in range(n)]
+            for (i, j), bit in zip(off, bits):
+                edges[i][j] = bool(bit)
+            for rho in (F(1, 3), F(2, 3)):
+                for root, bound in enumerate(envelope(edges, rho)):
+                    r = check_matrix(edges, route(edges, root, rho), rho)
+                    require(sum(row[root] for row in r) == bound, "attainment")
+                    d = distances(edges, root)
+                    require(all(r[i][root] == (0 if d[i] is None else rho**d[i]/(1-rho))
+                                for i in range(n)), "individual entries")
+                    graph_roots += 1
+    rng = random.Random(104100)
+    for _ in range(120):
+        n = rng.randrange(2, 9)
+        edges = [[i == j or rng.choice((False, True)) for j in range(n)] for i in range(n)]
+        raw = [[F(rng.randrange(-3, 4) if edges[i][j] else 0) for j in range(n)] for i in range(n)]
+        rho = F(3, 4)
+        e = [[rho*x/max(F(1), sum(map(abs, row))) for x in row] for row in raw]
+        check_matrix(edges, e, rho)
+    banded = 0
+    for b, m, rho in product(range(1, 4), range(1, 5), (F(1, 2), F(3, 4))):
+        n = 2*b*m+1
+        edges = [[abs(i-j) <= b for j in range(n)] for i in range(n)]
+        r = check_matrix(edges, route(edges, b*m, rho), rho)
+        column = [row[b*m] for row in r]
+        finite = (1 + 2*b*sum((rho**k for k in range(1, m+1)), F(0)))/(1-rho)
+        require(sum(column) == finite, "finite line formula")
+        infinite = 1/(1-rho) + 2*b*rho/(1-rho)**2
+        require(infinite-finite == 2*b*rho**(m+1)/(1-rho)**2, "exact deficit")
+        require(sum(x*x for x in column) == (1+2*b*sum((rho**(2*k) for k in range(1,m+1)),F(0)))/(1-rho)**2,
+                "spectral lower certificate")
+        banded += 1
+    controls = 0
+    for rho in (F(0), F(1), F(-1)):
+        try:
+            envelope([[True]], rho)
+        except ValueError:
+            controls += 1
+        else:
+            raise ValueError("bad rho accepted")
+    try:
+        envelope([[False]], F(1, 2))
+    except ValueError:
+        controls += 1
+    else:
+        raise ValueError("missing loop accepted")
+    e = [[F(1, 2), F(0), F(0)], [F(1, 2), F(0), F(0)], [F(1, 2), F(0), F(0)]]
+    r = resolvent(e)
+    require(sum(row[0] for row in r) > 2, "row-only inverse-1 shortcut must fail")
+    require(sum(row[0]**2 for row in r) > 4, "row-only inverse-2 shortcut must fail")
+    controls += 2
+    print("PASS_SHARP_BANDED_RESOLVENT " + json.dumps({"directed_graph_roots": graph_roots,
+          "signed_matrices": 120, "banded_instances": banded, "controls": controls,
+          "kappa_changed": False}, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()