From 720b7ecc76b605e4a3f9b90826f2544c6ba9e59e Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:32:33 -0500 Subject: [PATCH] Fund every returned residual in the physical inverse-pair error budget --- .../physical-pair-full-residuals/PROOF.md | 156 ++++++++++++++++++ .../physical-pair-full-residuals/README.md | 47 ++++++ .../physical-pair-full-residuals/RESULT.json | 17 ++ .../physical-pair-full-residuals/SOURCES.json | 54 ++++++ .../physical-pair-full-residuals/TASK.json | 74 +++++++++ .../physical-pair-full-residuals/VERIFY.json | 41 +++++ .../physical-pair-full-residuals/verify.py | 151 +++++++++++++++++ 7 files changed, 540 insertions(+) create mode 100644 research/physical-pair-full-residuals/PROOF.md create mode 100644 research/physical-pair-full-residuals/README.md create mode 100644 research/physical-pair-full-residuals/RESULT.json create mode 100644 research/physical-pair-full-residuals/SOURCES.json create mode 100644 research/physical-pair-full-residuals/TASK.json create mode 100644 research/physical-pair-full-residuals/VERIFY.json create mode 100644 research/physical-pair-full-residuals/verify.py diff --git a/research/physical-pair-full-residuals/PROOF.md b/research/physical-pair-full-residuals/PROOF.md new file mode 100644 index 0000000000..c53522e8d9 --- /dev/null +++ b/research/physical-pair-full-residuals/PROOF.md @@ -0,0 +1,156 @@ +# Full local residual transfer for the inverse-coded pair + +This enabling proof extends the inverse-only result in +[PR #5322](https://github.com/CrocSwap/integer-mult-bounds/pull/5322). +It allows errors at every stated operation in the local pair. It does not +prove provider accuracy or admit a complete caller. The complete paid +Gaussian profile and kappa are unchanged. + +Use the physical operators and order from JoyboyBrian's +[PR #5069](https://github.com/CrocSwap/integer-mult-bounds/pull/5069), +as retained at canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf. +D and Q commute, and C commutes with DQ. In general C does not commute +with D or Q separately. All operators act on 112 independent owners. +Errors use the maximum absolute real or imaginary component. + +## The chronological residual identity + +Each residual is the returned output minus the exact operator on its actual +computed input. Thus a residual can be nonlinear and depend on all earlier +errors. Define e0 after the entrance inverse, bX and bY after FULL, e1 after +the thin inverse, et after its Q^-1 and destination update, eQ after the exit +Q, eC after the exit C, and eL after the final Q^-1. Exact copies and monomial +wrappers are assumed. A defect in an update can be included in et, at the +same output site. The executed values satisfy these definitions: + +```text +y1 = C^-1 y + e0 +x2 = D(x-Q C y1) + bX +y2 = D y1 + bY +y3 = y2 + Q^-1(C^-1 x2+e1) + et +outY = Q^-1[C(Q y3+eQ)+eC] + eL. +``` + +Set S=Q^-1 C Q. Relative to the exact standard-pair outputs +`D(x-Qy)` and `DQ^-1 x`, the errors are exactly + +```text +Delta X = -DQ C e0 + bX +Delta Y = Q^-1 bX + S bY + Q^-1 C e1 + S et + + Q^-1 C eQ + Q^-1 eC + eL. +``` + +To prove this, substitute x2 in y3. The two terms involving the original y +cancel by `C^-1 DQ C=DQ`; the two terms involving e0 cancel by the same +identity. The exact part left in y3 is `Q^-1 C^-1 D x`. Its perturbation is +`Q^-1 C^-1 bX+bY+Q^-1 e1+et`. Apply the last line of the schedule and collect +terms. This proves the formula on every input and every residual vector. +There is no residual product and no assumption that a rounded map is linear. + +## Exact terminal norm + +Dillon's [PR #4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933) +gives the actual normalizers `K_i=Z_(z_i) P_(G_i)` and the four-point expansion +in its retained TERMINAL.md. For a nonzero code entry, put M=K_i^-1 K_j. +The source ports are distinct, so `G_i^-1 G_j e` is neither zero nor e. +In one digit column, each row of `Q^-1 M Q` therefore has four entries, +each equal to one of `+1/2,-1/2,+i/2,-i/2`. + +At positive fiber width f, the block is its f-fold tensor power. Each row has +4^f entries of magnitude 2^-f, and each entry is real or purely imaginary. +Thus each realified row has absolute sum 2^f. The owner coefficient A_ij is +applied once. Distinct input owners occupy disjoint columns, so there is no +cancellation between their row sums. Every row of A has absolute sum 26. +Consequently + +```text +||Q_f^-1 C_f Q_f||_(infinity,real) = 26 * 2^f. +``` + +This is an exact induced norm for arbitrary residuals. It improves the +product bound `26*2^(2 ceil(f/2))` by a factor two when f is odd. +It does not reduce the paid cost of the terminal operation. + +For comparison, let B1=2^ceil(f/2) and B9=2^ceil(9f/2). +The canonical Gaussian row formula gives `||Q^-1||=B1` and `||DQ||=B9`. +A real signed monomial preserves row absolute sums. Each block of Q^-1 C +is a Gaussian followed by a signed monomial, with total owner weight 26. +Hence `||Q^-1 C||=26 B1`; likewise `||DQ C||=26 B9`. + +## Budget with the actual inverse kernel + +The source finite kernel in [PR #5035](https://github.com/CrocSwap/integer-mult-bounds/pull/5035) +computes `x-M round(M^T x/52)` in integer grid units. Since +`A=I-MM^T/4` and `M^T M=56I`, its residual from A^-1 is `-M delta`, +where each mode rounding error delta has magnitude at most half a grid unit. +Each owner has four mode entries, so its error is at most two grid units. +Also `A M=-13 M`. Exact signed monomial wrappers therefore give `C e=-13 e` +for each of the two inverse residuals, even on perturbed valid inputs. +This is the error-shape premise already isolated by PR #5322. + +Let the eight residual bounds be epsilon0, epsilonX, epsilonY, epsilon1, +epsilont, epsilonQ, epsilonC and epsilonL in the order defined above. Then + +```text +||Delta X|| <= 13 B9 epsilon0 + epsilonX +||Delta Y|| <= B1 epsilonX + 26*2^f (epsilonY+epsilont) + + 13 B1 epsilon1 + 26 B1 epsilonQ + + B1 epsilonC + epsilonL. +``` + +These unequal allowances let a caller assign accuracy at each actual output +site. A useful common sufficient contract is, for u=2^-P, + +```text +epsilon0, epsilon1 <= 2u +all six other residual bounds <= u. +``` + +Under that contract, X error is at most `(26B9+1)u`, and Y error is at most +`(54B1+52*2^f+1)u`. For f>=1, B1<=2^f and B9>=16*2^f. Thus X is below +27B9 u and Y is at most 107*2^f u, below 7B9 u. It follows that + +```text +P = p + ceil(9f/2) + 5 => both output errors are strictly below 2^-p. +``` + +The inverse-only guard now funds the additional returned residuals under +explicit call contracts. It is not a proof that each physical provider meets +those contracts. If the inverse implementation does not preserve the error +subspace, replace the coefficients 13 by 26 in the two displayed bounds. + +## Evidence and limits + +The checker authenticates all six declared inputs. It checks all code entries, +the mode Gram identity, all 112 normalizers and all 5,824 terminal-block +independence premises. Three actual blocks have all 512 rows and columns +expanded with exact signed coefficients. A diagonal control loses four-point +support. Sixty-three exact rational chronological cases cover seven actual +Walsh fibers at widths 1, 2, 3 and 5, with each residual injected alone and +all injected together. Controls detect a missing FULL-Y residual, a missing +exit-Q residual, and reversed thin order. Twelve actual kernel calls verify +the inverse error subspace and paid scratch return. Five hundred widths check +the integer guard. The written operator, row and inequality proofs cover all +positive widths; the finite checks corroborate them. + +The second inverse range must include the perturbed x2. Provider input-domain +gates and their internal precision costs remain necessary. All Gaussian calls, +ordinary arithmetic, movement, workspace, copying and cleanup must retain +paid physical contracts. The error bound does not remove the unshared +boundary-call obstruction or supply a cheaper complete caller. It is a local +analytic result, not a full native, compiler, Lean or selected replay. + +## Credit and next question + +PR #5069 supplies the exact pair and its charged schedule. PR #4933 supplies +the real signed normalizers, mode code and four-point terminal formula. +PR #5035 supplies the finite rounded kernel. PR #5322 supplies the inverse-only +residual cancellation and error-shape guard. Those predecessors are not new +claims here. New result: all returned residual sites, the exact component +terminal norm and the resulting complete local accuracy contract. +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +The next question is whether a changed or shared-boundary caller can meet +these local provider bounds within its complete price and range budget. +Start by binding each epsilon above to a named provider contract. No +independent human or proof-kernel acceptance is claimed. diff --git a/research/physical-pair-full-residuals/README.md b/research/physical-pair-full-residuals/README.md new file mode 100644 index 0000000000..ac21b3115d --- /dev/null +++ b/research/physical-pair-full-residuals/README.md @@ -0,0 +1,47 @@ +# A complete local residual contract for the inverse-coded pair + +The guard `P=p+ceil(9f/2)+5` suffices for both pair outputs at every f>=1, +provided the two actual inverse kernels return at most two grid units of +error and each of the other six residual vectors has at most one. The new +proof includes FULL and Gaussian errors, which PR #5322 treated as zero. +It also proves `||Q^-1 C Q||_(infinity,real)=26*2^f` for the actual code. +The complete paid Gaussian profile and kappa do not change. + +[PROOF.md](PROOF.md) gives the chronological identity, unequal site budgets, +quantified proof, source credit and limits. [RESULT.json](RESULT.json) records +the exact checks. [SOURCES.json](SOURCES.json) pins canonical main +ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority 7. The scoped +[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19151016) +excludes the active native-history construction. + +## Reproduce + +Use CPython 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/physical-pair-full-residuals +python3.12 -I -O -W error -B research/physical-pair-full-residuals/verify.py +``` + +Expected marker: PASS_FULL_PAIR_RESIDUAL_TRANSFER. Both modes check 63 +chronological cases, all 5,824 block premises, 3,072 literal rows/columns, +12 actual source-kernel vectors and 500 guard widths. Source modules load +from authenticated source bytes. The written proof covers the all-width +result. No full physical caller, provider-accuracy, Lean, compiler or +selected-frontier replay ran. + +## Open next questions + +Bind each returned residual allowance to one physical provider and include +its input range, internal precision, movement and cost. A changed or shared +boundary caller still needs an affordable complete invoice. TASK.json states +the next check and blocker. + +## Credit + +JoyboyBrian's PR #5069 supplies the pair; PR #5035 supplies the finite kernel. +Dillon's PR #4933 supplies the normalizers and terminal formula. PR #5322 +supplies the inverse-only error transfer. PROOF.md links these predecessors. +The retained native, controller, precision and compiler authors keep their +credit. New all-site theorem and checks: Ali Romman with substantial OpenAI +Codex assistance. Apache-2.0. Author-checked, not independent acceptance. diff --git a/research/physical-pair-full-residuals/RESULT.json b/research/physical-pair-full-residuals/RESULT.json new file mode 100644 index 0000000000..3d51ca4c2f --- /dev/null +++ b/research/physical-pair-full-residuals/RESULT.json @@ -0,0 +1,17 @@ +{ + "status": "PASS_FULL_PAIR_RESIDUAL_TRANSFER", + "chronological_cases": 63, + "actual_terminal_blocks": 5824, + "literal_row_and_column_checks": 3072, + "source_kernel_vectors": 12, + "guard_widths": 500, + "controls": { + "omit_full_Y": true, + "omit_exit_Q": true, + "wrong_thin_order": true + }, + "terminal_component_norm": "26*2^f", + "guard": "P=p+ceil(9f/2)+5", + "provider_accuracy_verified": false, + "complete_caller_run": false +} diff --git a/research/physical-pair-full-residuals/SOURCES.json b/research/physical-pair-full-residuals/SOURCES.json new file mode 100644 index 0000000000..220641f6da --- /dev/null +++ b/research/physical-pair-full-residuals/SOURCES.json @@ -0,0 +1,54 @@ +{ + "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/coded-inverse-fixed-grid/kernel.py", + "usage": "input", + "git_blob": "70b5d65cae9a8f19cfda4a862c7ecc0bdc42c89b", + "sha256": "bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303" + }, + { + "path": "research/coded-native-caller/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + }, + { + "path": "research/coded-native-caller/PHYSICAL.md", + "usage": "input", + "git_blob": "da8837ba67423ef08ef1afb8e8297a8032aafe9f", + "sha256": "4321b159ff8d3fe705419adaaa1beef75606e869e34341bda553f17d598a6078" + }, + { + "path": "research/coded-native-caller/TERMINAL.md", + "usage": "input", + "git_blob": "213a1726761224d6f705b90affc52b6600c95676", + "sha256": "49e8f958e0a43f5d0b307dbef81c81076a55e83137563d7e620c608201d6dbcc" + }, + { + "path": "research/native-center-free-code/CODE.json", + "usage": "input", + "git_blob": "03170f4a31f7a8a3db7228f1cd5a6fdcb32720ae", + "sha256": "8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0" + }, + { + "path": "research/physical-inverse-pair/README.md", + "usage": "input", + "git_blob": "a4ed4756eaa2e2e1fe3d91f2d8c7f1d682d8185b", + "sha256": "32505039ae7289b6358de5ec9d83a8bb63b76140209b521c7e8c82e8e0000783" + } + ] +} diff --git a/research/physical-pair-full-residuals/TASK.json b/research/physical-pair-full-residuals/TASK.json new file mode 100644 index 0000000000..143b04ba1c --- /dev/null +++ b/research/physical-pair-full-residuals/TASK.json @@ -0,0 +1,74 @@ +{ + "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": "refined", + "actual_scope": "All-site local residual transfer and an exact terminal component norm for the physical inverse-coded pair.", + "scope_change_reason": "PR5322 assumes exact native and Gaussian calls. This follow-up assigns residuals to the actual remaining sites and derives their full local budget.", + "bottleneck_link": "A physical coded caller needs explicit numerical accuracy at every call site before admission.", + "budget_minutes": 60, + "stop_rule": "Stop after the local conditional theorem and source-bound checks; do not expand or admit a complete caller.", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json: quantified residual/norm proof, exact chronological cases, terminal rows and source-kernel checks.", + "author": "Ali Romman with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents or independent human acceptance.", + "open_questions": [ + { + "question": "Can an affordable changed caller meet every stated provider residual and input-range contract?", + "why_it_matters": "The analytic bound does not establish provider accuracy or physical cost.", + "first_step": "Bind each epsilon to one named provider and include its internal precision and movement cost.", + "blocked_by": "Complete caller allowance and provider domain/accuracy proofs." + } + ] +} diff --git a/research/physical-pair-full-residuals/VERIFY.json b/research/physical-pair-full-residuals/VERIFY.json new file mode 100644 index 0000000000..214d7f0c73 --- /dev/null +++ b/research/physical-pair-full-residuals/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coded-inverse-fixed-grid/kernel.py", + "research/coded-native-caller/NORMALIZERS.json", + "research/coded-native-caller/PHYSICAL.md", + "research/coded-native-caller/TERMINAL.md", + "research/native-center-free-code/CODE.json", + "research/physical-inverse-pair/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source pins, all-site chronological errors, exact terminal rows, actual inverse residual shape and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source pins, all-site chronological errors, exact terminal rows, actual inverse residual shape and semantic controls." + } + ] +} diff --git a/research/physical-pair-full-residuals/verify.py b/research/physical-pair-full-residuals/verify.py new file mode 100644 index 0000000000..3eec4692da --- /dev/null +++ b/research/physical-pair-full-residuals/verify.py @@ -0,0 +1,151 @@ +"""Check the full local residual transfer. Apache-2.0. +Ali Romman with substantial OpenAI Codex assistance. +Source identities retain JoyboyBrian and Dillon's credit. +""" +from fractions import Fraction as F +from pathlib import Path +from hashlib import sha256 +from collections import defaultdict +from types import SimpleNamespace +import argparse +import json + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + +def need(ok, why): + if not ok: + raise ValueError(why) + +for pin in json.loads((HERE/'SOURCES.json').read_text())['files']: + if pin['usage'] == 'input': + need(sha256((ROOT/pin['path']).read_bytes()).hexdigest() == pin['sha256'], 'Source pin') +a = [[F(v) for v in row] for row in json.loads((ROOT/'research/native-center-free-code/CODE.json').read_text())['A']] +normal = json.loads((ROOT/'research/coded-native-caller/NORMALIZERS.json').read_text()) +ports, modes = normal['ports'], normal['mode_columns'] +sparse = [[(j, v) for j, v in enumerate(row) if v] for row in a] +need(all(sum(abs(v) for _, v in row) == 26 for row in sparse), 'Code row norm') +need(all(a[i][j] == int(i == j)-F(sum(m[i]*m[j] for m in modes), 4) + for i in range(112) for j in range(112)), 'Actual mode factorization') +need(all(sum(x*y for x,y in zip(m,n)) == 56*(i == j) + for i,m in enumerate(modes) for j,n in enumerate(modes)), 'Mode Gram') + +def add(x, y, sign=1): + return [(r+sign*u, i+sign*v) for (r,i),(u,v) in zip(x,y)] + +def scale(x, c): + return [(c*r,c*i) for r,i in x] + +def phase(x, exponents): + return [((r,i),(-i,r),(-r,-i),(i,-r))[e%4] for (r,i),e in zip(x,exponents)] + +def code(x, inverse=False): + y = [(sum(v*x[j][0] for j,v in row),sum(v*x[j][1] for j,v in row)) for row in sparse] + return scale(add(y,scale(x,12)),F(1,13)) if inverse else y + +def mv(rows, u): + return sum(((r&u).bit_count()%2) << i for i,r in enumerate(rows)) + +def trans(rows): + return [sum(((r>>i)&1)<>1).bit_count() for v in row) for row in chart] + qi = [-v for v in q] + need(all((u+v-sum(w.bit_count() for w in us))%4 == 0 for u,v in zip(q,d)), 'Signed DQ phase') + def terminal(z): + return phase(code(phase(z,q)),qi) + for active in range(9): + e0,bx,by,e1,et,eQ,eC,eL = [v if active == 8 or j == active else zero for j,v in enumerate(fixtures[2:])] + y1 = add(code(y,True), e0) + x2 = add(phase(add(x,phase(code(y1),q),-1),d),bx) + y2 = add(phase(y1,d),by) + thin = add(phase(add(code(x2,True),e1),qi),et) + y3 = add(y2,thin) + out = add(phase(add(code(add(phase(y3,q),eQ)),eC),qi),eL) + idealx = phase(add(x,phase(y,q),-1),d) + idealy = phase(phase(x,qi),d) + dx = add(scale(phase(phase(code(e0),q),d),-1),bx) + dy = phase(bx,qi) + for term in (terminal(by), phase(code(e1),qi), terminal(et), phase(code(eQ),qi), phase(eC,qi), eL): + dy = add(dy,term) + need(x2 == add(idealx,dx) and out == add(idealy,dy), 'Chronological residual identity') + controls['omit_full_Y'] |= out != add(idealy,add(dy,terminal(by),-1)) + controls['omit_exit_Q'] |= out != add(idealy,add(dy,phase(code(eQ),qi),-1)) + wrong_thin = add(add(code(phase(x2,qi),True),phase(e1,qi)),et) + wrong = add(phase(add(code(add(phase(add(y2,wrong_thin),q),eQ)),eC),qi),eL) + controls['wrong_thin_order'] |= wrong != out + cases += 1 +need(all(controls.values()), 'Semantic controls') + +# All actual nonzero blocks satisfy the distinct-port premise. +need(len({p['q'] for p in ports}) == 112, 'Distinct source ports') +for p in ports: + g = p['G_rows'] + need(mv(g,1) == p['q'], 'Central source port') + need(all(((r&s).bit_count()%2) == int(i == j) for i,r in enumerate(g) for j,s in enumerate(g)), 'Orthogonal normalizer') +blocks = [(i,j) for i,row in enumerate(a) for j,v in enumerate(row) if v] +for i,j in blocks: + need(i != j and abs(a[i][j]) == F(1,2), 'Off-diagonal source coefficient') + need(mv(trans(ports[i]['G_rows']),ports[j]['q']) not in (0,1), 'Four distinct support points') + +# Expand the literal four-point formula, including signs, at every address. +def terminal_columns(i,j): + left,right = ports[i],ports[j] + out=[] + for x in range(512): + u=mv(right['G_rows'],x);v=mv(right['G_rows'],x^1) + gx=mv(trans(left['G_rows']),u);gy=mv(trans(left['G_rows']),v) + sign=lambda z: 1-2*(((left['Z_mask']^right['Z_mask'])&z).bit_count()%2) + sx,sy=sign(u),sign(v) + column=defaultdict(lambda:(0,0)) + for dst,value in [(gx,(sx,0)),(gy,(0,-sy)),(gx^1,(0,sx)),(gy^1,(sy,0))]: + old=column[dst];column[dst]=(old[0]+value[0],old[1]+value[1]) + out.append({k:v for k,v in column.items() if v != (0,0)}) + return out +for i,j in (blocks[0],blocks[len(blocks)//2],blocks[-1]): + columns=terminal_columns(i,j) + rows=[[] for _ in range(512)] + for x,col in enumerate(columns): + need(len(col)==4 and all(abs(r)+abs(v)==1 for r,v in col.values()), 'Literal column norm') + for dst,z in col.items():rows[dst].append(z) + need(all(len(row)==4 and sum(abs(r)+abs(v) for r,v in row)==4 for row in rows), 'Literal row norm') +need(all(len(c)==1 for c in terminal_columns(0,0)), 'Diagonal control loses four-point support') +for f in range(1,501): + B1,B9=2**((f+1)//2),2**((9*f+1)//2) + need(26*B9+1 < 32*B9, 'X guard') + need(54*B1+52*2**f+1 < 32*B9, 'Y guard') + need(2**f <= B9//16, 'All-width comparison control') + +# The actual source kernel returns the required error subspace. +path=ROOT/'research/coded-inverse-fixed-grid/kernel.py' +ns={'__name__':'source_kernel','__file__':str(path)} +exec(compile(path.read_bytes(),str(path),'exec'),ns) +kernel=SimpleNamespace(**ns) +for seed in range(1,13): + values=[((j*j+seed*11)%103)-51 for j in range(112)] + width=kernel.word_width(51) + words=[kernel.encode(v,width) for v in values] + scratch=[[1]*width for _ in range(9)] + kernel.recode(words,modes,51,scratch) + err=add([(F(kernel.decode(w)),F(0)) for w in words],code([(F(v),F(0)) for v in values],True),-1) + need(code(err)==scale(err,-13) and max(abs(r) for r,i in err)<=2, 'Actual inverse residual contract') + need(all(not any(w) for w in scratch), 'Source scratch return') +result={'status':'PASS_FULL_PAIR_RESIDUAL_TRANSFER','chronological_cases':cases, + 'actual_terminal_blocks':len(blocks),'literal_row_and_column_checks':3*512*2, + 'source_kernel_vectors':12,'guard_widths':500,'controls':controls, + 'terminal_component_norm':'26*2^f','guard':'P=p+ceil(9f/2)+5', + 'provider_accuracy_verified':False,'complete_caller_run':False} +parser=argparse.ArgumentParser();parser.add_argument('--write-result',action='store_true');args=parser.parse_args() +if args.write_result:(HERE/'RESULT.json').write_text(json.dumps(result,indent=2)+'\n') +else:need(json.loads((HERE/'RESULT.json').read_text())==result,'Receipt mismatch') +print(json.dumps(result,sort_keys=True))