From cd33c723408bb98875211ee3145582c507881f29 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 11:01:30 -0500 Subject: [PATCH] Prove structure-dependent shear perturbation bounds --- .../shear-structure-perturbation/README.md | 131 ++++++++++++++++++ .../shear-structure-perturbation/SOURCES.json | 24 ++++ .../shear-structure-perturbation/TASK.json | 80 +++++++++++ .../shear-structure-perturbation/VERIFY.json | 34 +++++ .../shear-structure-perturbation/verify.py | 114 +++++++++++++++ 5 files changed, 383 insertions(+) create mode 100644 research/shear-structure-perturbation/README.md create mode 100644 research/shear-structure-perturbation/SOURCES.json create mode 100644 research/shear-structure-perturbation/TASK.json create mode 100644 research/shear-structure-perturbation/VERIFY.json create mode 100644 research/shear-structure-perturbation/verify.py diff --git a/research/shear-structure-perturbation/README.md b/research/shear-structure-perturbation/README.md new file mode 100644 index 0000000000..badc068ab1 --- /dev/null +++ b/research/shear-structure-perturbation/README.md @@ -0,0 +1,131 @@ +# Shear structure removes the small-error invertibility restriction + +**Scoped written proof with exact finite checks; no new kappa.** +If coefficient errors preserve each elementary shear, every changed linear +prefix remains invertible for every finite error size. The product bounds +below replace the small-total-error admission used for general gate errors in +[ywz65's PR #2701](https://github.com/CrocSwap/integer-mult-bounds/pull/2701). +They control forward prefixes, inverse prefixes, both operator defects, and +additive arithmetic noise. They do not assert that a rounded instruction +sequence is an invertible map of a finite grid. + +The exact scientific base is `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, +priority revision 7. The selected conditional kappa is 0.00302015 and is +unchanged. This changes the `uniform-transfer-audit` card to one numerical +interface lemma; no complete PR4100 caller is discharged. + +## Theorem + +Use an induced matrix norm and its compatible vector norm. Over R or C, let + +```text +N_i^2 = 0, +A_i = I + a_i N_i, Ahat_i = I + (a_i + e_i) N_i, +F_0 = Q_0 = I, +F_j = A_j ... A_1, Q_j = Ahat_j ... Ahat_1, +D_i = e_i F_(i-1)^(-1) N_i F_(i-1), +d_i = ||D_i||, P_j = product_(i=1..j) (1+d_i), +B >= max_j (||F_j||, ||F_j^(-1)||). +``` + +The coefficient errors are fixed. They need not be small, independent, +unbiased, or of one sign. The N_i need not commute. All Q_j are invertible, +and for every j, + +```text +||Q_j||, ||Q_j^(-1)|| <= B P_j, +||Q_j-F_j||, ||Q_j^(-1)-F_j^(-1)|| <= B (P_j-1). +``` + +In particular, P_j <= exp(sum_(i<=j) d_i) is valid with no restriction on +that sum. The finite product can be evaluated with rational arithmetic when +the chosen norm data are rational. + +For an arithmetic trajectory with arbitrary bounded or data-dependent noise, + +```text +y_0 = x, +y_i = Ahat_i y_(i-1) + u_i, +||y_j-F_j x|| <= B [ (P_j-1)||x|| + + sum_(i=1..j) (P_j/P_i)||F_i^(-1)u_i|| ]. +``` + +One may replace each transformed noise norm by B||u_i||. Noise is evaluated +on the actual trajectory; no probabilistic cancellation is assumed. + +## Proof + +Since N_i^2=0, the exact and changed inverse gates are I-a_i N_i and +I-(a_i+e_i)N_i. Thus no finite coefficient error makes a gate singular. +Also A_i^(-1)N_i=N_i. With R_j=F_j^(-1)Q_j, multiplication in the given +order gives R_j=(I+D_j)R_(j-1). Conjugation preserves D_i^2=0, so +(I+D_i)^(-1)=I-D_i. + +Submultiplicativity bounds both the forward ordered product and its reverse +inverse product by P_j. Expand either finite product and subtract its +constant term. The sum of the norms of all remaining ordered terms is at +most P_j-1. Multiplication by F_j or F_j^(-1) proves the four inequalities. +The exponential bound follows from 1+t <= exp(t) for t>=0. + +For arithmetic noise, set z_j=F_j^(-1)y_j. Then +z_j=(I+D_j)z_(j-1)+F_j^(-1)u_j. An error inserted after step i is multiplied +only by later factors. Their norm product is P_j/P_i. Expand this recurrence, +subtract x, and multiply by F_j. This proves the trajectory bound. + +The same proof applies to any square-zero N_i, including a block shear. +An elementary shear is the case N_i=E_(r,c), r!=c. If structural zeros or +diagonal ones may also change, the conclusion fails: perturbing I by +diag(-1,0) produces a singular matrix. The structure premise is essential. + +## Exact evidence + +The standalone checker uses Fraction arithmetic and Gaussian elimination for +the actual inverse matrices. It does not use the displayed inverse formula +to compute the tested inverses. It checks 24 noncommuting two- and three-row +circuits, 192 prefixes, 192 noisy steps, and 16 circuits with sum d_i>=1. +Five controls distinguish large supported errors, unsupported singular +errors, omitted higher-order terms, changed order, and an endpoint-only norm +bound. Finite checks support the written proof; they are not a formal proof. + +With CPython 3.12 or later and no external packages: + +```sh +python3 -I -W error -B research/shear-structure-perturbation/verify.py +python3 -I -O -W error -B research/shear-structure-perturbation/verify.py +python3 -B scripts/research_package.py --package research/shear-structure-perturbation +``` + +Both direct modes report `PASS_SHEAR_PERTURBATION`, 24 circuits, 192 prefixes, +192 noise steps, 16 large-budget circuits, and five controls. No selected +cold replay, native replay, compiler build, Lean build, or Docker run was used. + +## Limits + +The bound is sufficient and need not be sharp. Large P_j can make an error +estimate useless even though invertibility survives. This is not a numerical +accuracy guarantee at arbitrary precision. Gate coefficients and exact +prefixes are mathematical inputs. Overflow, integer bits, coefficient +generation, physical reads, movement, restoration, and the full outer bill +remain unpriced. + +## Open next questions + +The next useful task is to bind a production shear word and its actual +coefficient storage policy to N_i, e_i and the prefix norms, then compare +its finite error budget with the general bound. Start with one emitted local +tile. A specified arithmetic kernel and physical cost model are required. + +## Credit + +ywz65's PR2701 supplies the simultaneous-error interaction coordinates and +the general prefix/noise contract. Vlado Vojdanovski's +[PR #1673](https://github.com/CrocSwap/integer-mult-bounds/pull/1673) supplies +the Toeplitz circuit and precision context. Nick Petalas's +[PR #5153](https://github.com/CrocSwap/integer-mult-bounds/pull/5153) supplies +the separate endpoint-norm refinement and sharp B-power examples; that +refinement is not a result of this package. Nilpotent inverse formulas and +ordered-product estimates are classical. The contribution here is their +explicit structure-dependent contract at the retained rounding interface. + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +No independent human or proof-kernel acceptance is claimed. diff --git a/research/shear-structure-perturbation/SOURCES.json b/research/shear-structure-perturbation/SOURCES.json new file mode 100644 index 0000000000..af244a01ab --- /dev/null +++ b/research/shear-structure-perturbation/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/simultaneous-gate-rounding/README.md", + "usage": "provenance", + "git_blob": "eaad013627f7ded744f032eea77fed6f121fc01c", + "sha256": "4bd564aa762f07d67127cba668b370bab3c1407c733f873c756cf2f62e906f2a" + } + ] +} diff --git a/research/shear-structure-perturbation/TASK.json b/research/shear-structure-perturbation/TASK.json new file mode 100644 index 0000000000..8f94dd6be5 --- /dev/null +++ b/research/shear-structure-perturbation/TASK.json @@ -0,0 +1,80 @@ +{ + "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": "Prove a structure-dependent simultaneous-error contract for fixed square-zero shear gates.", + "scope_change_reason": "This numerical interface side theorem replaces a small-error invertibility premise; it does not close a complete PR4100 caller.", + "bottleneck_link": "The contract separates structural invertibility from accuracy in rounded elementary-shear circuits.", + "budget_minutes": 60, + "stop_rule": "Stop after the universal ordered-product proof and exact controls; physical lowering is separate.", + "outcome": "completed", + "evidence": "README.md gives the proof; verify.py checks 24 circuits, 192 prefixes and five controls.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance; no human or proof-kernel acceptance claimed.", + "open_questions": [ + { + "question": "Can a production shear word use this bound with its actual storage policy?", + "why_it_matters": "A finite guard needs coefficients, prefix norms and an arithmetic kernel.", + "first_step": "Bind one emitted local tile and compare its complete error budget.", + "blocked_by": "Production coefficients, arithmetic behavior and physical costs are external." + } + ], + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4202#discussioncomment-19149211", + "upstream_checkpoint": { + "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "priority_revision": 7, + "checked_at": "2026-10-23T15:58:00Z" + } +} diff --git a/research/shear-structure-perturbation/VERIFY.json b/research/shear-structure-perturbation/VERIFY.json new file mode 100644 index 0000000000..772ba95428 --- /dev/null +++ b/research/shear-structure-perturbation/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": 60, + "checks": "Exact ordered shear products, independent matrix inverses, noise propagation and five premise controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact ordered shear products, independent matrix inverses, noise propagation and five premise controls." + } + ] +} diff --git a/research/shear-structure-perturbation/verify.py b/research/shear-structure-perturbation/verify.py new file mode 100644 index 0000000000..25980b1736 --- /dev/null +++ b/research/shear-structure-perturbation/verify.py @@ -0,0 +1,114 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Check ordered shear perturbation bounds with exact rational matrices.""" +from fractions import Fraction as F +from itertools import product +import json + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def eye(n): + return [[F(i == j) for j in range(n)] for i in range(n)] + + +def add(a, b): + return [[x + y for x, y in zip(r, s)] for r, s in zip(a, b)] + + +def scale(a, t): + return [[t * x for x in r] for r in a] + + +def mul(a, b): + return [[sum(x * y for x, y in zip(r, c)) for c in zip(*b)] for r in a] + + +def norm(a): + return max(sum(abs(x) for x in r) for r in a) + + +def inv(a): + n = len(a) + rows = [list(r) + s for r, s in zip(a, eye(n))] + for j in range(n): + k = next((k for k in range(j, n) if rows[k][j]), None) + need(k is not None, 'singular matrix') + rows[j], rows[k] = rows[k], rows[j] + pivot = rows[j][j] + rows[j] = [x / pivot for x in rows[j]] + for k in range(n): + if k != j: + t = rows[k][j] + rows[k] = [x - t * y for x, y in zip(rows[k], rows[j])] + return [r[n:] for r in rows] + + +def run(): + counts = dict(circuits=0, prefixes=0, noise_steps=0, large_budget=0) + for n, repeats, error in product((2, 3), (1, 2, 3), (F(0), F(1, 8), F(1), F(3))): + data = [] + for i in range(4 * repeats): + r, c = (i % n, (i + 1) % n) + nil = [[F(0) for _ in range(n)] for _ in range(n)] + nil[r][c] = 1 + a = F((-1) ** i * (i + 1), 3) + e = (-1) ** (i // 2) * error + data.append((nil, a, e)) + exact = [eye(n)] + changed = [eye(n)] + ds = [] + ps = [F(1)] + for nil, a, e in data: + ds.append(scale(mul(mul(inv(exact[-1]), nil), exact[-1]), e)) + exact.append(mul(add(eye(n), scale(nil, a)), exact[-1])) + changed.append(mul(add(eye(n), scale(nil, a + e)), changed[-1])) + ps.append(ps[-1] * (1 + norm(ds[-1]))) + bound = max(norm(z) for p in exact for z in (p, inv(p))) + rel = eye(n) + initial = [[F((-1) ** i, i + 1)] for i in range(n)] + y = initial + noise_terms = [] + for j, ((nil, a, e), d) in enumerate(zip(data, ds), 1): + need(norm(mul(d, d)) == 0, 'nilpotent interaction error') + rel = mul(add(eye(n), d), rel) + need(changed[j] == mul(exact[j], rel), 'ordered interaction identity') + need(norm(changed[j]) <= bound * ps[j], 'forward prefix') + need(norm(inv(changed[j])) <= bound * ps[j], 'inverse prefix') + need(norm(add(changed[j], scale(exact[j], -1))) <= bound * (ps[j] - 1), 'forward defect') + need(norm(add(inv(changed[j]), scale(inv(exact[j]), -1))) <= bound * (ps[j] - 1), 'inverse defect') + noise = [[F((-1) ** (i + j), 7 + j)] for i in range(n)] + y = add(mul(add(eye(n), scale(nil, a + e)), y), noise) + noise_terms.append(norm(mul(inv(exact[j]), noise))) + allowance = bound * ((ps[j] - 1) * norm(initial) + sum(ps[j] / ps[i] * v for i, v in enumerate(noise_terms, 1))) + need(norm(add(y, scale(mul(exact[j], initial), -1))) <= allowance, 'noise propagation') + counts['prefixes'] += 1 + counts['noise_steps'] += 1 + counts['circuits'] += 1 + counts['large_budget'] += sum(map(norm, ds)) >= 1 + # These fixtures distinguish the hypotheses from stronger false claims. + n = [[F(0), F(1)], [F(0), F(0)]] + need(inv(add(eye(2), scale(n, 100))) == add(eye(2), scale(n, -100)), 'large error stays invertible') + singular = [[F(0), F(0)], [F(0), F(1)]] + try: + inv(singular) + except ValueError: + pass + else: + raise ValueError('arbitrary-entry singular control') + m = [[F(0), F(0)], [F(1), F(0)]] + need(mul(add(eye(2), n), add(eye(2), m)) != add(eye(2), add(n, m)), 'higher order cannot be dropped') + need(mul(add(eye(2), n), add(eye(2), m)) != mul(add(eye(2), m), add(eye(2), n)), 'order matters') + # The exact endpoint is I but its intermediate scale is large. + u = add(eye(2), scale(n, 100)) + v = add(eye(2), m) + need(norm(mul(mul(inv(u), v), u)) > norm(v), 'endpoint bound does not bound prefixes') + counts['controls'] = 5 + return dict(status='PASS_SHEAR_PERTURBATION', **counts, no_new_kappa=True) + + +if __name__ == '__main__': + print(json.dumps(run(), sort_keys=True))