From d53754b5c7211442aa9df762396c00fe1d84f587 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 10:43:47 +0100 Subject: [PATCH] feat(research): sharpen principal-window residual bounds --- research/window-comparison-barrier/PROOF.md | 158 +++++++++++ research/window-comparison-barrier/README.md | 110 ++++++++ .../window-comparison-barrier/SOURCES.json | 36 +++ research/window-comparison-barrier/TASK.json | 91 ++++++ .../window-comparison-barrier/VERIFY.json | 38 +++ research/window-comparison-barrier/verify.py | 262 ++++++++++++++++++ 6 files changed, 695 insertions(+) create mode 100644 research/window-comparison-barrier/PROOF.md create mode 100644 research/window-comparison-barrier/README.md create mode 100644 research/window-comparison-barrier/SOURCES.json create mode 100644 research/window-comparison-barrier/TASK.json create mode 100644 research/window-comparison-barrier/VERIFY.json create mode 100644 research/window-comparison-barrier/verify.py diff --git a/research/window-comparison-barrier/PROOF.md b/research/window-comparison-barrier/PROOF.md new file mode 100644 index 0000000000..09eb053e21 --- /dev/null +++ b/research/window-comparison-barrier/PROOF.md @@ -0,0 +1,158 @@ +# A reusable optimal comparison barrier + +The dimension-uniform statements below are informal proofs. The verifier supplies +exact finite corroboration. Neither is a complete multiplication theorem. + +## 1. Comparison and every principal restriction + +Let H be an N-by-N complex matrix with nonzero diagonal. Its real comparison +matrix M has entries + + M_ii = |H_ii|, M_ij = -|H_ij| for i != j. + +Assume there is w > 0 with Mw > 0, componentwise. For example, the weighted +strict diagonal dominance in Dugongue's #3872 supplies such a w. This assumption +is essential; invertibility of H alone does not imply it. + +Write M=S(I-B), where S=diag(|H_ii|) and B is nonnegative with zero diagonal. +For W=diag(w), the row sums of W^-1 B W are strictly below one, since Mw > 0. +Thus its geometric series converges in the infinity norm. Consequently + + M^-1 = (I-B)^-1 S^-1 >= 0. + +Every principal restriction M_J has the same property, using w restricted to J. +In particular, if M_J v >= 0 then v >= 0. Here inequalities are componentwise. + +For any complex vector e on J, the triangle inequality gives + + M_J |e| <= |H_J e|. + +Therefore, for a nonnegative residual envelope r_J, + + |H_J e| <= r_J implies |e| <= M_J^-1 r_J. (1) + +This also proves H_J is invertible, by applying (1) with r_J=0 to its kernel. +No inverse cache or numerical experiment is a premise of this argument. + +## 2. One source barrier covers all ordered windows + +Fix a full-source envelope r >= 0 and set h=M^-1 r. Then h >= 0. For every +principal index set J, + + M_J h_J = r_J + sum_(k outside J) |H_ik| h_k >= r_J. (2) + +Multiplication by M_J^-1 proves + + M_J^-1 r_J <= h_J. + +Combining with (1), the restriction of one precomputed source barrier certifies +the physical error after every principal-window solve. Simultaneous row/column +permutations simply reorder (1) and (2), so any legal ordered slide sequence is +covered, independently of its length. This is a residual certificate at each +current solve; it does not sum or cancel errors across a product of solves. + +If y approximates the exact solution x of H_J x=b and +`|H_J y-b| <= r_J`, then `|y-x| <= h_J`. In particular, if x is independently +known to be integral, `max_i h_i < 1/2` guarantees unique nearest-integer +recovery. Integral output remains an explicit premise. + +## 3. Optimality in the declared comparison method + +The barrier h is the componentwise least full-source supersolution: if Md >= r, +then `d-h=M^-1(Md-r) >= 0`. It is attained, with Mh=r. When r>0, h>0, since the +diagonal term S^-1 in the nonnegative inverse series is strictly positive. + +For the uniform envelope r=1, a positive test vector d with Md>0 gives the +scalar maximum-principle certificate + + ||H_J^-1||_infinity <= max_i d_i / min_i (Md)_i (3) + +for every J. To see this, divide d by t=min_i(Md)_i and apply section 2's +supersolution reasoning. Its restriction satisfies M_J(d_J/t)>=1. + +Conversely d/t is a supersolution for the full source, so d/t>=h. Hence + + min_(d>0, Md>0) max_i d_i / min_i(Md)_i + = ||M^-1 1||_infinity, + +and d=h attains the minimum. When the unweighted choice d=1 is feasible, it +recovers the familiar inverse minimum-row-gap bound. Optimizing this certificate +cannot do worse than that feasible choice. + +This does not say that ||H^-1||_infinity equals ||M^-1||_infinity. Comparison +discards signs and phases. It is sharp over the class with the same diagonal +magnitudes and off-diagonal magnitudes: take H=M and residual vector 1. Then +the error is exactly h. This identifies the sharpness model without asserting +optimality of a physical decoder, precision scheme or paid implementation. + +## 4. The retained setup fixture + +Jose Manuel's exact setup fixture, retained unchanged in #3872, is + + H = [ 4 -1 0 ] + [ 1/3 5 -1/2 ] + [ 0 1/4 3 ]. + +It is a rational setup fixture, not a production Gaussian window. Its minimum +unweighted row gap is 11/4, giving the previous certificate 4/11. Direct rational +multiplication gives + + h = (49/156, 10/39, 83/234), Mh = (1,1,1). + +All coordinates are positive, so this equation alone also supplies the required +positive dominance witness. The improved all-window error constant is + + C = 83/234 = 4/11 - 23/2574. + +For `||H_J y-b||_infinity <= t`, the new componentwise bound is `|y-x|<=t h_J`. +Known-integer recovery follows whenever + + t < 1/(2C) = 117/83, + +instead of the old sufficient `t < 11/8`. At t=7/5 the new error bound is +581/1170<1/2, whereas the old one is 28/55>1/2 and gives no conclusion. +There is no claim that the old method produces an incorrect answer there. + +For the comparison matrix itself, residual `(117/83)1` has an error coordinate +exactly 1/2. Thus the new threshold must remain strict for the same-magnitude +comparison class. This boundary witness is not a failure claim about H itself. + +## 5. Cost and scope + +When M and r are rational, as in the retained fixture, preparing h uses one +rational solve in M, O(N^3) field operations with ordinary dense elimination +and its O(N^2) workspace, plus O(N) retained barrier rationals. Testing a +proposed rational barrier uses O(N^2) field operations. The general complex +theorem is an exact mathematical statement; it makes no rational-arithmetic +claim for irrational magnitudes. A window can reuse the restricted h without another +solve. Residual formation, comparison, coefficient creation, protected-page +emission, ownership, scaling and clearing remain paid work. No fixed-tape or +bit-cost improvement follows just from this arithmetic preparation component. + +The exact M-matrix comparison and maximum-principle arguments are classical. +The contribution is the least reusable residual-barrier contract for this +sliding-window boundary and its new exact fixture constant and recovery margin. +The predecessor's inverse-update algorithms and replay counts are cited, not +re-audited. No selected frontier, supplier, kappa or full Gaussian guard changes. + +## 6. Verifier constraints + +The verifier has no recursion or dynamic code execution. Rational matrix inputs +are bounded to dimension eight and 128-bit source coefficients; the actual +enumeration is the fixed three-coordinate fixture. Its separate determinant +oracle is bounded to dimension four. The largest enumeration has 16 sign +variants, 15 ordered windows and eight residual vertices per window. Source +bytes are authenticated before AST-only literal extraction; source modules are +never imported. All mathematical gates use explicit exceptions, including under +`-O`. Functions remain below 60 physical lines. Normal runs are read-only; +receipt output is optional, exclusive-create and outside the checkout. + +Power-of-Ten rule 3 has a managed-runtime deviation in verify.py: CPython and +Fraction allocate during arithmetic, so fixed post-initialization allocation +is unavailable. This is confined to a terminating finite verifier with the +explicit dimension, coefficient, source-size and enumeration bounds above. +Live matrix storage is quadratic and case comparisons stream into one digest. +The normal/optimized replay exercises these bounds and rejection controls. +Any change to larger fixture dimensions must revisit the resource bound. +Rule 10 uses warning-as-error normal/optimized execution and AST inspection; +no new repository-wide static-analysis configuration or native build is added. diff --git a/research/window-comparison-barrier/README.md b/research/window-comparison-barrier/README.md new file mode 100644 index 0000000000..d2a5cea4ba --- /dev/null +++ b/research/window-comparison-barrier/README.md @@ -0,0 +1,110 @@ +# A smaller reusable residual bound for principal windows + +One positive source barrier improves the retained #3851/#3872 setup fixture's +all-principal-window inverse-error constant from **4/11 to 83/234**. The exact +decrease is 23/2574. Its sufficient known-integer recovery threshold increases +from residual infinity norm `<11/8` to `<117/83`. + +At residual `7/5`, the improved certificate gives error at most +`581/1170 < 1/2`, while the older row-gap certificate gives `28/55 > 1/2` and +does not decide recovery. Integral exact output is an explicit premise. + +The claim type is a scoped proof with exact finite corroboration. This is a +new numerical certificate at Dugongue's fixed-source sliding-window boundary, +taking [#3872](https://github.com/CrocSwap/integer-mult-bounds/pull/3872) Open +next question 3. It does not re-audit its inverse cache or reproduce its slide +census. The matrix is an actual retained rational setup fixture, not a +production Gaussian window. No production guard or selected frontier changes. + +## Result and optimality boundary + +For a complex matrix H, let `M_ii=|H_ii|` and `M_ij=-|H_ij|` off the diagonal. +Assume a positive vector w satisfies `Mw>0`. For any nonnegative full-source +residual envelope r, set `h=M^-1 r`. Then every principal window J satisfies + +```text +|H_J y-b| <= r_J implies |y-H_J^-1 b| <= h_J. +``` + +The same h covers every ordered slide sequence, regardless of length. It is +the componentwise least full-source supersolution `Md>=r`. For r=1 it also +attains the best scalar certificate `max(d)/min(Md)` over positive d with Md>0. +For the retained fixture, + +```text +h = (49/156, 10/39, 83/234), Mh = (1,1,1). +``` + +[PROOF.md](PROOF.md) gives the dimension-uniform maximum-principle argument, +principal-restriction implication, optimality and recovery corollary. The +comparison matrix itself attains the bound. This proves sharpness over the +same-magnitude comparison class, not the exact inverse norm of the signed +source H or the optimal cost of a physical decoder. + +For rational M and r, including this fixture, preparing h costs one dense +rational solve, O(N^3) field operations, with O(N) stored barrier rationals in +addition to solve workspace and source access. The complex theorem does not +assert rational arithmetic for irrational magnitudes. +All residual formation, coefficient preparation, comparisons, scaling, page +emission and cleanup remain paid. A physical saving is not inferred from the +smaller sufficient error constant. + +## Evidence and reproduction + +CPython 3.12, standard library only, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/window-comparison-barrier +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/window-comparison-barrier/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/window-comparison-barrier/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/window-comparison-barrier --check-source-history +``` + +The marker is `PASS_WINDOW_COMPARISON_BARRIER`. Every run constructs the new +barrier by rational elimination and checks it with a separate permutation-sum +determinant oracle. It enumerates all 15 ordered nonempty principal windows, +all 16 sign choices at the four nonzero off-diagonal positions and all residual +box vertices, giving 1,248 direct error comparisons. It also checks 78 literal +known-integer recoveries at residual 7/5, the sharp comparison-class half-unit +boundary and 12 rejected malformed or insufficient certificates. No predecessor +module is imported or executed. + +Source hashes are checked before AST-only extraction of the retained fixture. +The [source manifest](SOURCES.json) binds the source README, proof and immutable +setup file to canonical main `81e9bd69e4a5b00ba9c713a1620e36d576d5522e`. +All three are declared replay inputs. Catalogue and selected-record pins are +provenance only. The [task record](TASK.json) states the changed card scope. + +An optional `--receipt /absolute/new/path.json` writes a generated result and +package-file SHA256 manifest outside the checkout. Ordinary runs write nothing. +Receipts are not hand-written. Normal and optimized registered replays run the +same explicit checks; correctness does not depend on Python assertions. + +The universal result rests on the written proof. Finite cases corroborate the +fixture and verifier. Independent human and formal proof-kernel review are +unclaimed. No full Gaussian page integration, native or fixed-tape execution, +selected cold replay, complete supplier admission or new kappa is claimed. + +## Open next questions + +- Bind the barrier to an actual rounded production factor page. First freeze + its global H, format, incoming-grid bound and exact residual envelope, then + compare complete old/new guards. The missing physical preparation, emission + and cleanup bill blocks an operational saving claim. +- If the global source changes, can its least comparison barrier be updated + without a new dense solve? First specify one exact source update and its + comparison-matrix change. A preserved positive dominance witness is required; + the present theorem assumes one fixed source. + +## Credit + +This result was produced by Nick Petalas. David Ganz / Dugongue's #3872 supplies +the fixed-source sliding-window boundary, weighted recovery question and retained +fixture. Jose Manuel / jmbarrancoml's #3851 at +`7ab67b4a84d28cd562b9711aa315ca5b47822b37` supplies that exact setup fixture and +physical preparation context. Credit Chafik Boukhalfa's #489/#481/#486, +RaD / hipotures, Jose Manuel's #3787 and the retained Gaussian/FFT lineage for +the predecessor framework. Classical M-matrix and maximum-principle reasoning +retain their mathematical credit. The new step is this reusable least-barrier +contract and its exact fixture improvement, not invention of comparison theory. +No predecessor source or credit line is changed. New work is Apache-2.0. diff --git a/research/window-comparison-barrier/SOURCES.json b/research/window-comparison-barrier/SOURCES.json new file mode 100644 index 0000000000..2c00df3ffe --- /dev/null +++ b/research/window-comparison-barrier/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "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/sliding-window-inverse/PROOF.md", + "usage": "input", + "git_blob": "c95bef030bf13ee7ee836a9f81e38e26f720907d", + "sha256": "e087c64dee82b541cf563245a5c59dc5bd5236072fc96b094ead15ee848bfb3e" + }, + { + "path": "research/sliding-window-inverse/README.md", + "usage": "input", + "git_blob": "cca049dfc1981fd92f53715a067d52ee6345eb18", + "sha256": "846561df84d5dd049fa174d6b25fde8964216cdac5fb9cf6988b02e3c9c2e375" + }, + { + "path": "research/sliding-window-inverse/inputs/gaussian_check_setup.py", + "usage": "input", + "git_blob": "529c2e7fe3c6dafc28c23346622bca97a09d1b25", + "sha256": "46e234fbadbbf934cb02f609d7aa14355789c42f82e384cf624d31e57bd05a3a" + } + ] +} diff --git a/research/window-comparison-barrier/TASK.json b/research/window-comparison-barrier/TASK.json new file mode 100644 index 0000000000..4cd0d65612 --- /dev/null +++ b/research/window-comparison-barrier/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "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 least reusable comparison-residual barrier for all principal windows and improve the retained PR3851/PR3872 fixture bound from 4/11 to 83/234.", + "scope_change_reason": "The original card asks for an audit of a quantified PR4100 step. This contribution instead takes PR3872 Open next question 3 and supplies a new numerical-recovery bound; predecessor audits are not its deliverable.", + "bottleneck_link": "Scoped side result for the actual fixed-source principal-window preparation boundary. It sharpens a sufficient physical residual tolerance, but does not integrate or price production Gaussian pages or admit a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified constant improvement; retain physical integration and further refinements as open questions.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-dimension argument and exact barrier. verify.py enumerates the finite fixture windows, residual vertices, same-magnitude sign class, recovery examples and rejected certificates.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a barrier certificate reduce the actual rounded factor-page guard at one production Gaussian window?", + "why_it_matters": "The new constant concerns a retained setup fixture; production integration is necessary before changing an operational precision bill.", + "first_step": "Freeze one actual global H, page format, incoming-grid magnitude and exact residual envelope, then compare its barrier and the complete old guard.", + "blocked_by": "An actual caller residual and the separately paid preparation, comparison, page emission and cleanup costs." + }, + { + "question": "Can the least barrier be updated cheaply after the global source itself changes?", + "why_it_matters": "The present reuse theorem assumes one fixed global source; repeated full comparison solves could repay any local saving.", + "first_step": "Specify one exact source update and determine whether its comparison-matrix change has a controlled low-rank formula.", + "blocked_by": "A source-update contract preserving a positive dominance witness; arbitrary sign changes do not have a fixed low-rank comparison update." + } + ], + "claim_type": "scoped proof with finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19142783", + "overlap": { + "checked_at_utc": "2026-10-23T09:33:00Z", + "canonical_main": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "open_pr_records": 323, + "discussion_records": 4243, + "local_note_records": 150, + "local_head_note_records": 6824, + "limitations": "Sparse local notes, arbitrary diffs and unpublished work are not exhaustively covered. Main-tree formula and object searches, merged PR searches and current local claims were also checked." + } +} diff --git a/research/window-comparison-barrier/VERIFY.json b/research/window-comparison-barrier/VERIFY.json new file mode 100644 index 0000000000..0f62637b8d --- /dev/null +++ b/research/window-comparison-barrier/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/sliding-window-inverse/PROOF.md", + "research/sliding-window-inverse/README.md", + "research/sliding-window-inverse/inputs/gaussian_check_setup.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact barrier, 15 ordered windows, 16 off-diagonal sign variants, 1248 residual vertices, 78 recovery cases, sharp comparison boundary and 12 rejected certificates." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat every proof-relevant finite check with Python assertions disabled; all gates use explicit exceptions." + } + ] +} diff --git a/research/window-comparison-barrier/verify.py b/research/window-comparison-barrier/verify.py new file mode 100644 index 0000000000..e182686f68 --- /dev/null +++ b/research/window-comparison-barrier/verify.py @@ -0,0 +1,262 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact finite evidence for the comparison-barrier proof; standard library only.""" + +import argparse +import ast +from fractions import Fraction as F +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rational_matrix(matrix): + n = len(matrix) + require(1 <= n <= 8, "matrix dimension must lie in 1..8") + require(all(len(row) == n for row in matrix), "square matrix required") + require(all(type(x) in (int, F) for row in matrix for x in row), + "exact rational matrix required") + result = tuple(tuple(F(x) for x in row) for row in matrix) + require(all(max(abs(x.numerator).bit_length(), x.denominator.bit_length()) + <= 128 for row in result for x in row), "input height limit") + return result + + +def matvec(matrix, vector): + return tuple(sum((a * b for a, b in zip(row, vector)), F(0)) + for row in matrix) + + +def solve(matrix, rhs): + """Small rational elimination used only to construct the new barrier.""" + matrix = rational_matrix(matrix) + n = len(matrix) + require(len(rhs) == n, "right-hand side dimension") + rows = [list(row) + [F(rhs[i])] for i, row in enumerate(matrix)] + for k in range(n): + pivots = [i for i in range(k, n) if rows[i][k]] + require(bool(pivots), "singular matrix") + pivot = pivots[0] + rows[k], rows[pivot] = rows[pivot], rows[k] + value = rows[k][k] + rows[k] = [x / value for x in rows[k]] + for i in range(n): + if i != k: + value = rows[i][k] + rows[i] = [x - value * y for x, y in zip(rows[i], rows[k])] + answer = tuple(row[-1] for row in rows) + require(matvec(matrix, answer) == tuple(map(F, rhs)), "solve residual") + return answer + + +def comparison(matrix): + matrix = rational_matrix(matrix) + return tuple(tuple(abs(x) if i == j else -abs(x) + for j, x in enumerate(row)) + for i, row in enumerate(matrix)) + + +def certify(matrix, barrier, envelope): + matrix = rational_matrix(matrix) + n = len(matrix) + require(len(barrier) == len(envelope) == n, "certificate dimension") + require(all(type(x) in (int, F) for x in (*barrier, *envelope)), + "exact rational certificate required") + require(all(x > 0 for x in barrier), "positive barrier required") + require(all(x > 0 for x in envelope), "positive residual envelope required") + image = matvec(comparison(matrix), barrier) + require(all(a >= b for a, b in zip(image, envelope)), + "comparison supersolution required") + return max(barrier) + + +def determinant(matrix): + """Independent Leibniz oracle, bounded to dimension four; no elimination.""" + n = len(matrix) + require(n <= 4 and all(len(row) == n for row in matrix), "oracle dimension") + total = F(0) + for order in permutations(range(n)): + inversions = sum(order[i] > order[j] for i in range(n) for j in range(i+1, n)) + term = F(-1 if inversions % 2 else 1) + for i, j in enumerate(order): + term *= matrix[i][j] + total += term + return total + + +def cofactor_solve(matrix, rhs): + denominator = determinant(matrix) + require(denominator != 0, "oracle nonsingularity") + answer = [] + for j in range(len(matrix)): + replaced = [[rhs[i] if k == j else x for k, x in enumerate(row)] + for i, row in enumerate(matrix)] + answer.append(determinant(replaced) / denominator) + return tuple(answer) + + +def literal_number(node): + if isinstance(node, ast.Constant) and type(node.value) is int: + return F(node.value) + require(isinstance(node, ast.Call) and isinstance(node.func, ast.Name) + and node.func.id == "Fraction" and not node.keywords + and 1 <= len(node.args) <= 2, "rational fixture literal") + values = [] + for arg in node.args: + sign = 1 + if isinstance(arg, ast.UnaryOp) and isinstance(arg.op, ast.USub): + sign, arg = -1, arg.operand + require(isinstance(arg, ast.Constant) and type(arg.value) is int, + "integer Fraction argument") + values.append(sign * arg.value) + return F(*values) + + +def source_fixture(root, package): + sources = json.loads((package / "SOURCES.json").read_text()) + for entry in sources["files"]: + if entry["usage"] == "input": + data = (root / entry["path"]).read_bytes() + require(len(data) <= 1_048_576, "source size limit") + require(sha256(data).hexdigest() == entry["sha256"], "source hash mismatch") + path = root / "research/sliding-window-inverse/inputs/gaussian_check_setup.py" + tree = ast.parse(path.read_text()) + nodes = tuple(ast.walk(tree)) + require(len(nodes) <= 20_000, "source syntax size limit") + candidates = [] + for node in nodes: + if not isinstance(node, ast.Assign): + continue + named = any(isinstance(t, ast.Name) and t.id == "source" for t in node.targets) + if named and isinstance(node.value, ast.List) and len(node.value.elts) == 3: + rows = node.value.elts + require(all(isinstance(row, ast.List) and len(row.elts) == 3 for row in rows), + "three-by-three source fixture") + candidates.append(tuple(tuple(literal_number(x) for x in row.elts) for row in rows)) + require(len(candidates) == 1, "unique source fixture") + return rational_matrix(candidates[0]) + + +def principal(matrix, labels): + return tuple(tuple(matrix[i][j] for j in labels) for i in labels) + + +def window_checks(matrix, barrier): + """Every ordered principal window, every residual-box vertex, every sign.""" + n = len(matrix) + sites = tuple((i, j) for i in range(n) for j in range(n) if i != j and matrix[i][j]) + require(len(sites) <= 6, "finite sign enumeration limit") + windows = tuple(labels for width in range(1, n+1) + for labels in permutations(range(n), width)) + cases = 0 + digest = sha256() + for signs in product((-1, 1), repeat=len(sites)): + variant = [list(row) for row in matrix] + for (i, j), sign in zip(sites, signs): + variant[i][j] = sign * abs(matrix[i][j]) + for labels in windows: + block = principal(variant, labels) + bound = tuple(barrier[i] for i in labels) + certify(block, bound, (F(1),) * len(labels)) + for rhs in product((-1, 1), repeat=len(labels)): + actual = cofactor_solve(block, rhs) + require(all(abs(x) <= h for x, h in zip(actual, bound)), "window bound") + digest.update((str((signs, labels, rhs, actual)) + "\n").encode()) + cases += 1 + return len(windows), 2 ** len(sites), cases, digest.hexdigest() + + +def recovery_checks(matrix, barrier): + cases = 0 + residual = F(7, 5) + require(residual * max(barrier) == F(581, 1170) < F(1, 2), "new recovery margin") + require(residual * F(4, 11) == F(28, 55) > F(1, 2), "old certificate inconclusive") + for width in range(1, len(matrix)+1): + for labels in permutations(range(len(matrix)), width): + block = principal(matrix, labels) + exact = tuple(F(2*i-3) for i in labels) + for signs in product((-1, 1), repeat=width): + rhs = tuple(residual * sign for sign in signs) + error = cofactor_solve(block, rhs) + approximate = tuple(a+b for a, b in zip(exact, error)) + recovered = tuple((x+F(1, 2)).numerator // (x+F(1, 2)).denominator + for x in approximate) + require(recovered == exact, "literal known-integer recovery") + require(matvec(block, error) == rhs, "physical residual identity") + cases += 1 + return cases + + +def rejection_checks(matrix, barrier): + rejected = 0 + controls = [([], (), ()), ([[1, 2]], (1,), (1,)), + ([[1.0]], (1,), (1,)), ([[1]], (0,), (1,)), + ([[1]], (1,), (0,)), ([[1]], (1,), (1.0,)), + ([[1]], (F(1, 2),), (1,)), ([[1, 2], [2, 1]], (1, 1), (1, 1)), + (matrix, (F(1, 4), F(1, 5), F(1, 3)), (1, 1, 1))] + for k in range(len(barrier)): + lowered = tuple(x-F(i == k, 1000) for i, x in enumerate(barrier)) + controls.append((matrix, lowered, (1, 1, 1))) + for args in controls: + try: + certify(*args) + except ValueError: + rejected += 1 + else: + raise ValueError("negative certificate accepted") + return rejected + + +def evidence(root, package): + matrix = source_fixture(root, package) + ones = (F(1),) * len(matrix) + comp = comparison(matrix) + barrier = solve(comp, ones) + require(barrier == (F(49, 156), F(10, 39), F(83, 234)), "new barrier value") + bound = certify(matrix, barrier, ones) + require(bound == F(83, 234), "improved constant") + old_gap = min(matvec(comp, ones)) + require(old_gap == F(11, 4) and 1/old_gap-bound == F(23, 2574), "exact gain") + require(cofactor_solve(comp, ones) == barrier, "independent sharpness witness") + threshold = F(1, 2)/bound + error = cofactor_solve(comp, (threshold,) * len(matrix)) + require(max(error) == F(1, 2), "strict threshold boundary") + windows, signs, vertices, digest = window_checks(matrix, barrier) + recovered = recovery_checks(matrix, barrier) + rejected = rejection_checks(matrix, barrier) + return {"claim_type": "scoped proof with finite corroboration", + "barrier": list(map(str, barrier)), "bound": str(bound), + "old_bound": str(1/old_gap), "gain": str(1/old_gap-bound), + "recovery_threshold": str(threshold), "ordered_windows": windows, + "sign_variants": signs, "residual_vertices": vertices, + "known_integer_recoveries": recovered, "rejected_controls": rejected, + "case_sha256": digest} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write a new receipt outside the checkout") + args = parser.parse_args() + package = Path(__file__).resolve().parent + root = package.parent.parent + result = evidence(root, package) + print(json.dumps(result, sort_keys=True)) + if args.receipt is not None: + output = args.receipt.expanduser().resolve() + require(not output.is_relative_to(root), "receipt must be outside checkout") + hashes = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file()} + receipt = {"result": result, "package_sha256": hashes} + with output.open("x", encoding="utf-8") as handle: + handle.write(json.dumps(receipt, indent=2, sort_keys=True) + "\n") + print("PASS_WINDOW_COMPARISON_BARRIER") + + +if __name__ == "__main__": + main()