Prove structure-dependent shear perturbation bounds (no new kappa)

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.

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"
+    }
+  ]
+}

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"
+  }
+}

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."
+    }
+  ]
+}

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))