From d63d8848442acc0bdc7b62578e12726c530af3fa Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 09:14:34 -0500 Subject: [PATCH] Prove sharp graph-support inverse norm envelope --- research/sharp-banded-resolvent/README.md | 106 +++++++++++++++ research/sharp-banded-resolvent/SOURCES.json | 30 ++++ research/sharp-banded-resolvent/TASK.json | 82 +++++++++++ research/sharp-banded-resolvent/VERIFY.json | 33 +++++ research/sharp-banded-resolvent/verify.py | 136 +++++++++++++++++++ 5 files changed, 387 insertions(+) create mode 100644 research/sharp-banded-resolvent/README.md create mode 100644 research/sharp-banded-resolvent/SOURCES.json create mode 100644 research/sharp-banded-resolvent/TASK.json create mode 100644 research/sharp-banded-resolvent/VERIFY.json create mode 100644 research/sharp-banded-resolvent/verify.py diff --git a/research/sharp-banded-resolvent/README.md b/research/sharp-banded-resolvent/README.md new file mode 100644 index 0000000000..d68fc9625e --- /dev/null +++ b/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. diff --git a/research/sharp-banded-resolvent/SOURCES.json b/research/sharp-banded-resolvent/SOURCES.json new file mode 100644 index 0000000000..aaf6ad6c53 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/sharp-banded-resolvent/TASK.json b/research/sharp-banded-resolvent/TASK.json new file mode 100644 index 0000000000..610798b702 --- /dev/null +++ b/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." + } +} diff --git a/research/sharp-banded-resolvent/VERIFY.json b/research/sharp-banded-resolvent/VERIFY.json new file mode 100644 index 0000000000..8f7973cbf9 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/sharp-banded-resolvent/verify.py b/research/sharp-banded-resolvent/verify.py new file mode 100644 index 0000000000..44427db406 --- /dev/null +++ b/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()