From 1ff5044ee4805e0e24afb8e3067a50435745a538 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 11:47:56 -0500 Subject: [PATCH] Exact inverse envelope for unequal row contraction budgets --- research/unequal-row-resolvent/README.md | 41 ++++++++ research/unequal-row-resolvent/SOURCES.json | 18 ++++ research/unequal-row-resolvent/TASK.json | 79 +++++++++++++++ research/unequal-row-resolvent/VERIFY.json | 34 +++++++ research/unequal-row-resolvent/verify.py | 101 ++++++++++++++++++++ 5 files changed, 273 insertions(+) create mode 100644 research/unequal-row-resolvent/README.md create mode 100644 research/unequal-row-resolvent/SOURCES.json create mode 100644 research/unequal-row-resolvent/TASK.json create mode 100644 research/unequal-row-resolvent/VERIFY.json create mode 100644 research/unequal-row-resolvent/verify.py diff --git a/research/unequal-row-resolvent/README.md b/research/unequal-row-resolvent/README.md new file mode 100644 index 0000000000..5ef2cafa9b --- /dev/null +++ b/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 00. 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. diff --git a/research/unequal-row-resolvent/SOURCES.json b/research/unequal-row-resolvent/SOURCES.json new file mode 100644 index 0000000000..277ad46954 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/unequal-row-resolvent/TASK.json b/research/unequal-row-resolvent/TASK.json new file mode 100644 index 0000000000..012513786f --- /dev/null +++ b/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" + } +} diff --git a/research/unequal-row-resolvent/VERIFY.json b/research/unequal-row-resolvent/VERIFY.json new file mode 100644 index 0000000000..28e2f8c922 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/unequal-row-resolvent/verify.py b/research/unequal-row-resolvent/verify.py new file mode 100644 index 0000000000..fb8c4feafd --- /dev/null +++ b/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))