Certify uniform operator error for fixed physical transfer tables

research/transfer-metric-error-bound/README.md

@@ -0,0 +1,135 @@
+# Uniform operator error from a physical transfer metric
+
+This package gives a finite exact certificate for a uniform operator-norm bound
+on the complete fixed-transfer endpoint of PR5441. It checks the full local
+input/output block operator. It has no factor from the growing payload dimension.
+It is a sufficient contract, not a characterization of all bounded families.
+The complete kappa calculation is unchanged.
+
+## Contract and theorem
+
+Use the predecessor's fixed table T[y,x], D virtual states, local dimension d,
+left boundary F with p output roles and right boundary B with q input roles.
+The complete physical endpoint E_f has entries
+
+```
+E_f[i,y_1...y_f ; j,x_1...x_f] = (F T[y_1,x_1] ... T[y_f,x_f] B)[i,j].
+```
+
+Let P be positive definite. Supply nonnegative real a,b,c with c<=1 and prove
+
+```
+F* F <= a P,
+B* P B <= b I_q,
+[sum_y T[y,x]* P T[y,x']]_(x,x') <= c (I_d tensor P).
+```
+
+The order is the positive-semidefinite order, and star is conjugate transpose.
+The third inequality includes all off-diagonal x,x' blocks. Then, for every
+positive integer f,
+
+```
+||E_f||_op^2 <= a b c^f <= a b c.
+```
+
+Here the norm is the full physical operator norm, with all input and output
+roles. The bound applies to an error if the supplied table represents the
+complete residual between an implementation and its exact target. It does not
+follow from separately bounded entries or a few tested widths.
+
+## Proof
+
+Give the virtual space the norm from P. The local operator maps
+`virtual tensor input-column` to `virtual tensor output-column`; its block
+from x to y is T[y,x]. The third inequality bounds its squared norm by c.
+First apply B to the input role, with squared norm at most b. Apply the local
+operator to columns f,f-1,...,1, with identities on all other columns. This
+order gives exactly T[y_1,x_1] ... T[y_f,x_f]. Tensoring by identities preserves
+operator norm. Finally apply F, with squared norm at most a. Submultiplicativity
+proves the displayed result. This reasoning sums coherently over the virtual
+state and physical inputs; it never replaces operator norm by entrywise or
+Frobenius norm. Thus it has no dimension factor. All p and q role blocks remain
+in the two boundary inequalities.
+
+The checker supports rational real tables and metrics. Rational Schur elimination
+checks positive definiteness of P and positive semidefiniteness of the three
+residual matrices. At a zero pivot, a nonzero remaining off-diagonal entry
+rejects the matrix. Otherwise it removes the zero row or takes the exact Schur
+complement. This is the standard PSD criterion; no eigenvalue tolerance is used.
+The proof also holds over C, but complex certificate parsing is not implemented.
+
+## Examples and limits
+
+A two-state table with T[0,0]=I, T[1,1]=diag(1,-1), and other blocks zero has
+F=(epsilon/2,-epsilon/2), B=(1,1)^T and P=I. Take a=epsilon squared/2,
+b=2 and c=1. Its endpoint is epsilon times the odd-parity projector. Its norm
+is exactly |epsilon| at every positive width. This gives a sharp certificate
+without paying a factor 2 to the width from a Frobenius estimate.
+
+Noncommuting rational virtual rotations and reflections give further exact
+examples. A nonidentity metric checks invariance under a rational similarity
+change; scaling each local operator by r gives the exact decay r to the width.
+The source's slow-phase example is also checked in its real two-coordinate
+representation. It has the safe uniform error bound two. Small early errors do
+not make that bound small. No improved native recovery tolerance is inferred.
+
+Per-input or per-entry checks are insufficient. The one-state local matrix
+[[1,1],[0,0]] has unit-norm columns but operator norm sqrt(2). The full block
+certificate rejects c=1. The transpose gives a second rejected coherent sum.
+Singular/indefinite metrics, understated boundaries, understated rates, floats
+and incomplete tables also reject.
+
+A stable family can fail this certificate for the supplied representation.
+Failure is not an instability proof. Finding P is a separate search. A change
+of layout, varying table, unrepresented width schedule, or omitted dirty role
+needs a new contract. Physical synthesis, bit precision, input conditioning,
+tape access, recursive stock and exact recovery remain separate obligations.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/transfer-metric-error-bound
+python3.12 -B research/transfer-metric-error-bound/certificate.py /path/to/certificate.json
+```
+
+Use the standard library. The JSON keys are `transfer_dimension`, `local_dimension`,
+`metric`, `left`, `right`, `transitions`, `left_bound`, `right_bound` and
+`squared_rate`. Integers and rational strings are accepted. The table is a full
+d by d array of D by D matrices, including explicit zero blocks.
+
+Registered normal and optimized checks use explicit exceptions. Literal complete
+endpoint matrices corroborate the parity, noncommuting and slow-phase examples.
+A separate determinant routine checks all principal minors for 125 symmetric
+2-by-2 matrices and agrees with the PSD routine. The finite checks do not replace
+the written all-width proof or establish independent human acceptance.
+
+## Source and distinction
+
+This answers Open next question 4 of zxv's
+[PR #5441](https://github.com/CrocSwap/integer-mult-bounds/pull/5441), using its
+[exact physical-table contract](https://github.com/zxv/integer-mult-bounds/blob/11fedb46fa199283f78282187c10aea432d8b0bb/research/finite-memory-lifting/PROOF.md).
+Its exact endpoint theorem and slow-phase counterexample remain intact. The
+new contribution is an exact sufficient approximation certificate in that same
+contract. No predecessor executable is imported. The repository's Perron weight
+work concerns recursive cost systems; this certificate concerns the physical
+operator norm of a transfer table and includes coherent cross-input blocks.
+Canonical base and proof-source objects are recorded in SOURCES.json. The overlap
+search covered current open PRs, Discussions and all tracked in-scope notes;
+unposted work and arbitrary historical diffs remain outside coverage.
+
+## Open next questions
+
+Extract a complete residual table from one real consumer and find a rational
+metric that passes this test. Start with a numerical metric proposal, then
+verify the rational inequalities exactly. Table size, a suitable metric, and
+the source's complete role/version binding are the blockers. The resulting
+operator bound must still fit a separately proved exact-recovery budget.
+
+## Credit
+
+zxv supplies the finite-memory physical contract, examples and approximation
+handoff. The source retains the weighted-automata, matrix-product, native and
+phase predecessors. Weighted operator norms, Schur complements and contractive
+composition are classical. Ali Romman with substantial OpenAI Codex assistance;
+Apache-2.0. No new general stability algorithm, physical supplier or kappa is
+claimed. No independent human or proof-kernel acceptance is claimed.

research/transfer-metric-error-bound/SOURCES.json

@@ -0,0 +1,27 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    }
+  ],
+  "external_provenance": [
+    {
+      "repository": "zxv/integer-mult-bounds",
+      "commit": "11fedb46fa199283f78282187c10aea432d8b0bb",
+      "path": "research/finite-memory-lifting/PROOF.md",
+      "git_blob": "36152f9e31555a88ce3636ae59abf07a8058d78d",
+      "usage": "Read-only contract and open question; no runtime import."
+    }
+  ]
+}

research/transfer-metric-error-bound/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "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 rational weighted-metric certificate for the complete physical transfer endpoint at every width.",
+  "scope_change_reason": "Take PR5441 open question 4 on uniform approximation rather than the historical CRT audit.",
+  "bottleneck_link": "Finite tolerance checks do not imply a uniform recovery-safe operator error.",
+  "budget_minutes": 60,
+  "stop_rule": "Prove and check the sufficient contraction contract; do not claim a physical consumer binding.",
+  "outcome": "completed",
+  "evidence": "README.md theorem; certificate.py exact PSD checker; verify.py literal endpoints and controls.",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance.",
+  "open_questions": [
+    {
+      "question": "Does one actual complete consumer residual admit a useful rational metric?",
+      "why_it_matters": "It could certify a uniform operator error for its precision budget.",
+      "first_step": "Extract its complete fixed table and verify a proposed metric exactly.",
+      "blocked_by": "No source-bound consumer table or recovery budget is supplied."
+    }
+  ]
+}

research/transfer-metric-error-bound/VERIFY.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete physical endpoints, independent principal minors and semantic rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "-O",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete physical endpoints, independent principal minors and semantic rejection controls."
+    }
+  ]
+}

research/transfer-metric-error-bound/certificate.py

@@ -0,0 +1,83 @@
+#!/usr/bin/env python3
+"""Check a rational uniform operator bound for a physical transfer family.
+
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import argparse
+from fractions import Fraction as Q
+import json
+from pathlib import Path
+
+
+def scalar(x):
+    if type(x) not in (int,str): raise ValueError('use exact rational values')
+    return Q(x)
+
+
+def matrix(a,n,m):
+    if not isinstance(a,list) or len(a)!=n or any(not isinstance(r,list) or len(r)!=m for r in a):
+        raise ValueError('matrix shape mismatch')
+    return [[scalar(x) for x in r] for r in a]
+
+
+def eye(n): return [[Q(i==j) for j in range(n)] for i in range(n)]
+def transpose(a): return list(map(list,zip(*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 sub(a,b): return [[x-y for x,y in zip(r,s)] for r,s in zip(a,b)]
+def scale(c,a): return [[c*x for x in r] for r in a]
+
+
+def psd(a,strict=False):
+    if a!=transpose(a): return False
+    a=[list(r) for r in a]
+    for k in range(len(a)):
+        pivot=a[k][k]
+        if pivot<0: return False
+        if pivot==0:
+            if strict or any(a[k][j] for j in range(k+1,len(a))): return False
+        else:
+            for i in range(k+1,len(a)):
+                for j in range(k+1,len(a)):
+                    a[i][j]-=a[i][k]*a[k][j]/pivot
+    return True
+
+
+def check(data):
+    D,d=data['transfer_dimension'],data['local_dimension']
+    if type(D) is not int or type(d) is not int or min(D,d)<1:
+        raise ValueError('dimensions must be positive integers')
+    P=matrix(data['metric'],D,D)
+    F=matrix(data['left'],len(data['left']),D)
+    if not F: raise ValueError('empty output roles')
+    B=matrix(data['right'],D,len(data['right'][0]))
+    if not B[0]: raise ValueError('empty input roles')
+    raw=data['transitions']
+    if len(raw)!=d or any(len(row)!=d for row in raw): raise ValueError('incomplete physical table')
+    T=[[matrix(raw[y][x],D,D) for x in range(d)] for y in range(d)]
+    a,b,c=[scalar(data[k]) for k in ('left_bound','right_bound','squared_rate')]
+    if min(a,b,c)<0 or c>1: raise ValueError('invalid uniform-bound scalar')
+    if not psd(P,strict=True): raise ValueError('metric is not positive definite')
+    if not psd(sub(scale(a,P),mul(transpose(F),F))): raise ValueError('left boundary bound fails')
+    if not psd(sub(scale(b,eye(len(B[0]))),mul(transpose(B),mul(P,B)))):
+        raise ValueError('right boundary bound fails')
+    gram=[[Q(0) for _ in range(d*D)] for _ in range(d*D)]
+    for x in range(d):
+        for xp in range(d):
+            block=scale(c,P) if x==xp else scale(Q(0),P)
+            for y in range(d): block=sub(block,mul(transpose(T[y][x]),mul(P,T[y][xp])))
+            for i in range(D):
+                for j in range(D): gram[x*D+i][xp*D+j]=block[i][j]
+    if not psd(gram): raise ValueError('full physical block contraction fails')
+    return {'status':'PASS_UNIFORM_TRANSFER_METRIC','squared_boundary_factor':str(a*b),
+            'squared_rate':str(c),'all_positive_width_squared_bound':'boundary_factor * squared_rate ** width',
+            'uniform_positive_width_squared_bound':str(a*b*c)}
+
+
+def main():
+    parser=argparse.ArgumentParser(description=__doc__); parser.add_argument('input',type=Path); args=parser.parse_args()
+    try: result=check(json.loads(args.input.read_text()))
+    except (ValueError,KeyError,TypeError,IndexError,ZeroDivisionError) as error: parser.error(str(error))
+    print(json.dumps(result,sort_keys=True))
+
+
+if __name__=='__main__': main()