diff --git a/research/transfer-metric-error-bound/README.md b/research/transfer-metric-error-bound/README.md new file mode 100644 index 0000000000..d0642b7857 --- /dev/null +++ b/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. diff --git a/research/transfer-metric-error-bound/SOURCES.json b/research/transfer-metric-error-bound/SOURCES.json new file mode 100644 index 0000000000..2187fcc8d0 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/transfer-metric-error-bound/TASK.json b/research/transfer-metric-error-bound/TASK.json new file mode 100644 index 0000000000..e2bd23fdbc --- /dev/null +++ b/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." + } + ] +} diff --git a/research/transfer-metric-error-bound/VERIFY.json b/research/transfer-metric-error-bound/VERIFY.json new file mode 100644 index 0000000000..4771b493f3 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/transfer-metric-error-bound/certificate.py b/research/transfer-metric-error-bound/certificate.py new file mode 100644 index 0000000000..55eadcba13 --- /dev/null +++ b/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() diff --git a/research/transfer-metric-error-bound/verify.py b/research/transfer-metric-error-bound/verify.py new file mode 100644 index 0000000000..9abec392e4 --- /dev/null +++ b/research/transfer-metric-error-bound/verify.py @@ -0,0 +1,116 @@ +#!/usr/bin/env python3 +"""Check transfer certificates against literal endpoint matrices and controls.""" +from copy import deepcopy +from fractions import Fraction as Q +from itertools import product,combinations +import json +from pathlib import Path +import sys +sys.path.insert(0,str(Path(__file__).resolve().parent)) +from certificate import check,eye,mul,sub,scale,transpose,psd + + +def require(value,message): + if not value: raise ValueError(message) + + +def encode(x): + if isinstance(x,dict): return {k:encode(v) for k,v in x.items()} + if isinstance(x,list): return [encode(y) for y in x] + if isinstance(x,Q): return str(x) + return x + + +def det(a): + a=[list(r) for r in a]; out=Q(1) + for k in range(len(a)): + pivot=next((i for i in range(k,len(a)) if a[i][k]),None) + if pivot is None: return Q(0) + if pivot!=k: a[pivot],a[k]=a[k],a[pivot]; out=-out + out*=a[k][k] + for i in range(k+1,len(a)): + factor=a[i][k]/a[k][k] + for j in range(k+1,len(a)): a[i][j]-=factor*a[k][j] + return out + + +def principal_psd(a): + return all(det([[a[i][j] for j in ids] for i in ids])>=0 + for k in range(1,len(a)+1) for ids in combinations(range(len(a)),k)) + + +def endpoint(T,F,B,f): + d=len(T); words=list(product(range(d),repeat=f)); p=len(F); q=len(B[0]) + out=[[Q(0) for _ in range(q*len(words))] for _ in range(p*len(words))] + for yi,y in enumerate(words): + for xi,x in enumerate(words): + a=F + for yy,xx in zip(y,x): a=mul(a,T[yy][xx]) + a=mul(a,B) + for i in range(p): + for j in range(q): out[i*len(words)+yi][j*len(words)+xi]=a[i][j] + return out + + +def fixture(T,F,B,P,a,b,c): + return encode(dict(transfer_dimension=len(P),local_dimension=len(T),transitions=T, + left=F,right=B,metric=P,left_bound=a,right_bound=b,squared_rate=c)) + + +def main(): + certificates=endpoints=psd_controls=0 + zero=scale(Q(0),eye(2)); Z=[[Q(1),Q(0)],[Q(0),Q(-1)]] + for epsilon in (Q(1),Q(1,3),Q(1,16)): + T=[[eye(2),zero],[zero,Z]]; F=[[epsilon/2,-epsilon/2]]; B=[[Q(1)],[Q(1)]] + data=fixture(T,F,B,eye(2),epsilon**2/2,Q(2),Q(1)); check(data); certificates+=1 + for f in range(1,6): + E=endpoint(T,F,B,f); n=len(E) + expected=[[epsilon if i==j and i.bit_count()%2 else Q(0) for j in range(n)] for i in range(n)] + require(E==expected,'literal parity endpoint') + require(mul(E,E)==scale(epsilon,E),'attaining projector') + endpoints+=1 + R=[[Q(3,5),Q(-4,5)],[Q(4,5),Q(3,5)]] + S=[[Q(2),Q(0)],[Q(0),Q(1)]]; Si=[[Q(1,2),Q(0)],[Q(0),Q(1)]] + for rate in (Q(1),Q(1,2),Q(2,3)): + T=[[scale(rate,mul(Si,mul(R,S))),zero],[zero,scale(rate,Z)]] + data=fixture(T,S,Si,mul(transpose(S),S),Q(1),Q(1),rate**2); check(data); certificates+=1 + for f in range(1,5): + E=endpoint(T,S,Si,f) + require(mul(transpose(E),E)==scale(rate**(2*f),eye(len(E))),'literal noncommuting unitary lift') + endpoints+=1 + # The source slow-phase example has a uniform bound of two. + for N in (1,7,101): + c=Q(N*N-1,N*N+1); s=Q(2*N,N*N+1) + rotation=[[c,-s],[s,c]] + local=[[Q(0) for _ in range(4)] for _ in range(4)] + for i in range(2): + for j in range(2): local[i][j]=rotation[i][j]; local[i+2][j+2]=Q(i==j) + F=[[Q(1),Q(0),Q(-1),Q(0)],[Q(0),Q(1),Q(0),Q(-1)]] + B=transpose([[Q(1),Q(0),Q(1),Q(0)],[Q(0),Q(1),Q(0),Q(1)]]) + check(fixture([[local]],F,B,eye(4),Q(2),Q(2),Q(1))); certificates+=1 + for f in range(1,10): + E=endpoint([[local]],F,B,f); gap=sub(scale(Q(4),eye(2)),mul(transpose(E),E)) + require(principal_psd(gap),'slow-phase uniform bound') + endpoints+=1 + for a,b,c in product(range(-2,3),repeat=3): + m=[[Q(a),Q(b)],[Q(b),Q(c)]] + require(psd(m)==principal_psd(m),'independent principal minors') + psd_controls+=1 + good=fixture([[eye(2),zero],[zero,Z]],[[Q(1),Q(0)]],[[Q(1)],[Q(0)]],eye(2),Q(1),Q(1),Q(1)) + mutants=[] + for key,value in [('squared_rate','1/4'),('metric',[[1,0],[0,0]]), + ('metric',[[1,0],[0,-1]]),('left',[[2,0]]),('right',[[2],[0]]), + ('squared_rate','2'),('left_bound',1.0),('transitions',[])]: + bad=deepcopy(good); bad[key]=value; mutants.append(bad) + for values in ([[1,1],[0,0]],[[1,0],[1,0]]): + T=[[[[Q(values[y][x])]] for x in range(2)] for y in range(2)] + mutants.append(fixture(T,[[Q(1)]],[[Q(1)]],[[Q(1)]],Q(1),Q(1),Q(1))) + for bad in mutants: + try: check(bad) + except (ValueError,IndexError): pass + else: raise ValueError('invalid certificate accepted') + print('PASS_TRANSFER_METRIC_ERROR_BOUND '+json.dumps(dict(certificates=certificates, + literal_endpoints=endpoints,independent_psd_cases=psd_controls,rejecting_controls=len(mutants)),sort_keys=True)) + + +if __name__=='__main__': main()