From 3893f896c445c7b77d91ccd6912d8ddd3fbcef18 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 19:35:47 +0000 Subject: [PATCH 1/2] feat(research): shrink Gaussian inverse locality with Chebyshev --- research/chebyshev-inverse-locality/PROOF.md | 156 +++++++++++ research/chebyshev-inverse-locality/README.md | 118 +++++++++ .../chebyshev-inverse-locality/SOURCES.json | 36 +++ research/chebyshev-inverse-locality/TASK.json | 83 ++++++ .../chebyshev-inverse-locality/VERIFY.json | 42 +++ research/chebyshev-inverse-locality/verify.py | 248 ++++++++++++++++++ 6 files changed, 683 insertions(+) create mode 100644 research/chebyshev-inverse-locality/PROOF.md create mode 100644 research/chebyshev-inverse-locality/README.md create mode 100644 research/chebyshev-inverse-locality/SOURCES.json create mode 100644 research/chebyshev-inverse-locality/TASK.json create mode 100644 research/chebyshev-inverse-locality/VERIFY.json create mode 100644 research/chebyshev-inverse-locality/verify.py diff --git a/research/chebyshev-inverse-locality/PROOF.md b/research/chebyshev-inverse-locality/PROOF.md new file mode 100644 index 0000000000..f247b428e7 --- /dev/null +++ b/research/chebyshev-inverse-locality/PROOF.md @@ -0,0 +1,156 @@ +# Chebyshev inverse locality under the retained conditioning contract + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written mathematical proof. The Chebyshev identities and +normal-equation approximation method are classical. The new contribution is +the explicit replacement of the Gaussian caller's locality parameters under +its existing conditioning hypotheses. No global literature priority is claimed. + +The general approximation-based inverse-decay method also predates this +application. Credit Stephen Demko, William F. Moss and Philip W. Smith, +[Decay rates for inverses of band matrices, 1984](https://doi.org/10.1090/S0025-5718-1984-0758197-9). +The argument below gives the explicit residual and exact section-row interface +needed here; it does not claim a new general inverse-decay theorem. + +## The polynomial + +Let H be an invertible finite complex square matrix with + + ||H||_2 <= K, ||H^-1||_2 <= K, K > 1. + +Write A=H*H. Its eigenvalues lie in [K^-2,K^2]. For any integer d>=1 put + + c = (K^4+1)/(K^4-1), + t(x) = (K^4+1-2K^2 x)/(K^4-1), + R_d(x) = T_d(t(x))/T_d(c), + q_(d-1)(x) = (1-R_d(x))/x, + B_d(H) = q_(d-1)(H*H) H*. + +Here T_d is the Chebyshev polynomial of the first kind. Since t(0)=c, +R_d(0)=1. Thus q_(d-1) is a polynomial of degree at most d-1, with no pole +at zero. In particular this definition does not require a matrix inverse. + +The classical identity + + T_d((z+z^-1)/2) = (z^d+z^-d)/2 + +and |T_d(t)|<=1 on [-1,1] follow from the recurrence T_0=1, T_1=t, +T_(j+1)=2t T_j-T_(j-1). They are also recorded in +[NIST DLMF, equation 18.5.1](https://dlmf.nist.gov/18.5.E1). +These identities are premises from classical polynomial theory, not new claims. + +## Error for arbitrary nonnormal matrices + +The identity x q_(d-1)(x)=1-R_d(x) gives, in the indicated order, + + B_d(H)-H^-1 = -R_d(H*H) H^-1. + +Indeed A^-1 H*=H^-1. The spectral theorem applies to the Hermitian A, +regardless of whether H is normal. Since t maps [K^-2,K^2] to [-1,1], + + ||B_d(H)-H^-1||_2 <= K/T_d(c). + +Take z=(K^2+1)/(K^2-1)>1. Then c=(z+z^-1)/2, so + + 1/T_d(c) = 2/(z^d+z^-d) <= 2 z^-d + <= 2 exp(-2d/K^2). + +For the last inequality put u=K^-2 in (0,1). Integrating +2/(1-u^2)>=2 from 0 to u gives +log((1+u)/(1-u))>=2u. Therefore log z>=2/K^2. This proves + + ||B_d(H)-H^-1||_2 <= 2K exp(-2d/K^2). + +No row or column dominance, symmetry of H, Gaussian entry formula or +translation invariance is used in this implication. + +## Exact locality and principal sections + +Let the indices carry the linear or circular physical distance used by the +caller. Suppose H_ij=0 when the distance between i and j exceeds W. +The same is true of H*. A monomial (H*H)^j H* contains 2j+1 factors, +and each step moves at most W. Hence B_d(H) has physical bandwidth at most + + r = (2d-1)W. + +Let S be any principal index set, H_S the corresponding principal matrix, +and i in S. If the distance from i to every omitted index is greater than r, +then the row of B_d(H_S), extended by zero outside S, equals row i of B_d(H) +exactly. Every path contributing to a monomial stays in S: an exit would +reach an omitted index in at most 2d-1 steps of length at most W. The same +coefficients are used in both polynomials, including the same K and d. + +This is equality of polynomial rows, not equality of exact inverse rows. +For an inverse-error assertion on H_S, that section must itself satisfy +the norm and inverse-norm hypotheses with the same K. The locality assertion +alone does not require H_S to be invertible. A separately rerounded section, +different K, or a Schur complement is not covered by this row identity. + +## Substitution at the Gaussian caller + +Use the precise hypotheses of Cinna Davis's +[HALO.md](../unconditional-batched-crt/HALO.md), pinned in SOURCES.json: +p is an integer at least two, W2 for p>=2. Furthermore + + r <= (2p^22-1)(p-1) < 2p^23 <= p^24. + +Thus a row at distance at least p^24 from every omitted index has exact +polynomial agreement. This replaces the historical Neumann degree p^42 +by p^22 and permits the conservative halo p^24 in place of p^48, with a +strictly smaller error than the old p^10 exp(-p^2) majorant. Both the global +matrix and every actual inverted section retain their original assumptions. +The argument does not establish those assumptions for a new matrix. + +The predecessor locality work, including Nick Petalas's #4217 and Mihir +Srivastava's #4501, supplies the distinction between polynomial locality, +section inverses and ordered nonnormal error identities. Their Neumann +polynomials and finite examples are not audited or replayed here. The new +polynomial changes the approximation method, rather than a group, target, +or truncation constant in a recent account contribution. + +## Exact coefficient construction + +For integer K>=2 put D=K^4-1 and L=(K^2+1)^2. Define integer polynomials + + N_0(x)=1, + N_1(x)=K^4+1-2K^2 x, + N_(j+1)(x)=2(K^4+1-2K^2 x)N_j(x)-D^2 N_(j-1)(x). + +Induction gives N_d(x)=D^d T_d(t(x)), so R_d(x)=N_d(x)/N_d(0). +N_d(0)>0. If N_d(x)=sum a_j x^j, the inverse polynomial's coefficients +are exactly -a_(j+1)/a_0. No numerical root, transcendental coefficient or +unknown inverse entry is needed to construct them. + +For completeness, ||N_j||_(coefficient 1-norm) <= (3L)^j. The initial cases +hold since ||N_1||=L. Since D^2=2`. A section polynomial row agrees exactly with its global row when +its distance to omitted indices exceeds `(2p^22-1)W`. Each section used +for an inverse estimate must retain the same conditioning assumptions. + +[PROOF.md](PROOF.md) gives the polynomial, the ordered error identity for +nonnormal matrices, exact row locality and a rational coefficient recurrence +with polynomial bit lengths. Chebyshev approximation is classical, with +[DLMF equation 18.5.1](https://dlmf.nist.gov/18.5.E1) cited explicitly. +The new step is the source-compatible parameter replacement. No claim of +global literature priority is made. The general approximation-based +inverse-decay method is credited to +[Demko, Moss and Smith](https://doi.org/10.1090/S0025-5718-1984-0758197-9). + +## Reproduction and evidence + +From the repository root, use CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -X dev -I -B research/chebyshev-inverse-locality/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -X dev -I -O -B research/chebyshev-inverse-locality/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/chebyshev-inverse-locality +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/chebyshev-inverse-locality --check-source-history +``` + +Another CPython 3.12 installation can replace the shown interpreter. Direct +replay prints `PASS_CHEBYSHEV_INVERSE_LOCALITY` in generated JSON, binding +all six package files by SHA256. It writes no files. The finite checks cover: + +- 3,696 exact scalar samples for `K=2..8`, degrees `1..16`, and 33 rational + points across the complete spectral interval. Integer coefficient + construction agrees with an independent scalar Chebyshev recurrence; + normalizations agree with the closed-form identity. +- 45 nonnormal operator fixtures, checking the exact ordered inverse-error + identity and its operator-norm bound by rational LDL positivity. Moving + the residual to the wrong side or reversing its sign fails on each fixture. +- 33 full section rows on a 21-point circle, for degrees 1,2,3, with exact + global/section agreement beyond the proved radius. Six rows at the radius + reject the smaller-halo extension. All bandwidth entries are checked. +- 127 integer parameter substitutions `p=2..128`, and six rejected invalid + coefficient-constructor inputs. Checks remain active under optimized Python. + +These reduced fixtures do not construct a degree-`p^22` production matrix. +The universal statement follows from the written proof, not a finite census. +No predecessor verifier, fixture or mathematical result is rechecked. + +## Scope and obligations + +The `uniform-transfer-audit` card is changed to an original component +construction for the `precision_tape` locality interface. This supplies a +smaller exact polynomial under explicit assumptions. It does not discharge +that entire selected assumption or provide a new supplier. + +No optimized core geometry, complete physical coefficient-page cost, +finite-precision recurrence stability, native execution, rounded multiplier, +new kappa or complete multiplication theorem is supplied. No selected-source +cold replay, Lean or Docker build is run. Independent human and formal +proof-kernel review are unclaimed. The selected frontier and its five +assumptions remain unchanged. + +The verifier has no recursion, subprocesses or external runtime inputs. +All loops run over fixed finite collections, with matrices at most 21 by 21 +and coefficient degree at most 16. Its largest function is below 60 lines. +Python's required dynamic allocation is a Power of Ten deviation, bounded +here by those fixed domains and one active matrix fixture. Exact fractions +have bounded sizes because both dimensions and rational inputs are fixed. +The checks use explicit exceptions under normal and optimized Python, with +warnings treated as errors. No shared build settings are changed. +Ruff is unavailable in the supplied interpreter; no separate static analyzer +is claimed. Static AST inspection finds a maximum function length of 28 lines. + +## Credit and overlap + +Cinna Davis's PR #4100 supplies the historical Gaussian caller, its +conditioning/section contract and Neumann locality witness. Credit the +retained capped-Gaussian and multiplication-framework predecessors in its +NOTICE.md. Nick Petalas's #4217 separates polynomial locality from inverse +row equality, and Mihir Srivastava's #4501 retains the ordered nonnormal +identity and a stronger cross-cell conditioning contract. These are cited +predecessor results, not new outputs. SOURCES.json pins their retained +texts at main `19fdb086ea96af9a9f87936a2b888e10af4ed810`. + +The new construction changes the approximation polynomial, rather than +extending a recent account result by changing only a group or target. +The exact finite verifier is new and imports no predecessor implementation. +Live open PRs, recent account work, handoff claims, main README searches and +merged-PR searches were checked. Cached overlap has complete remote +pagination but incomplete sparse local-note coverage. These bounded checks +are not a novelty certificate. + +Advance claim: +https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226112 + +## Open next questions + +Can a complete coefficient-page producer realize this smaller polynomial +with a favorable rounding and physical setup bill? The first step is a +bounded, exact coefficient page at one named caller section, with every +coefficient width, recurrence intermediate and output error charged. This +matters because exact locality alone does not lower the physical invoice. +The missing rounding, coefficient-page and consumer contracts are blockers. +No further construction or search is included here. diff --git a/research/chebyshev-inverse-locality/SOURCES.json b/research/chebyshev-inverse-locality/SOURCES.json new file mode 100644 index 0000000000..abf0d56175 --- /dev/null +++ b/research/chebyshev-inverse-locality/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/delta-cross-cell-independent-audit/README.md", + "usage": "input", + "git_blob": "3c068271779d0176ded1a954b0017d844a90698d", + "sha256": "77a08e97abcff4fcec527e84b5e8e1340cf3742c58afc0417c69d9ceb00268b6" + }, + { + "path": "research/halo-locality-witness-audit/README.md", + "usage": "input", + "git_blob": "03b244baf61b427edbccd29698a05583b5405dd6", + "sha256": "fc87657cb3e89a74b9462483cc15713f0122256a623fefa65c887e2118f81276" + }, + { + "path": "research/unconditional-batched-crt/HALO.md", + "usage": "input", + "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b", + "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" + } + ] +} diff --git a/research/chebyshev-inverse-locality/TASK.json b/research/chebyshev-inverse-locality/TASK.json new file mode 100644 index 0000000000..79fee21cc5 --- /dev/null +++ b/research/chebyshev-inverse-locality/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct a Chebyshev inverse-locality polynomial under the historical Gaussian caller conditioning contract, reducing the residual degree from p^42 to p^22 and the conservative halo from p^48 to p^24.", + "scope_change_reason": "The card requests discharge of a selected assumption. This original component construction changes the approximation method at a historical precision_tape locality interface and retains its conditioning premises; it does not discharge the full assumption.", + "bottleneck_link": "A smaller exact locality witness can reduce required halo extent under the same analytic interface. Complete coefficient-page, rounding and physical caller costs remain unknown; no new kappa is claimed.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified polynomial/locality improvement. Do not optimize core geometry, search another polynomial, or implement a physical caller.", + "outcome": "completed", + "evidence": "PROOF.md and the standalone normal/optimized exact verifier: 3696 scalar samples, 45 nonnormal operator fixtures, 33 exact section rows, six too-small-halo controls, six invalid-input controls and 127 parameter substitutions.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a complete coefficient-page producer realize this smaller polynomial with a favorable rounding and physical setup bill?", + "why_it_matters": "Exact locality alone does not lower the physical invoice.", + "first_step": "Construct one exact coefficient page at a named caller section and charge coefficient widths, recurrence intermediates and output error.", + "blocked_by": "A rounding analysis, a physical coefficient-page implementation and its complete consumer bill are missing." + } + ] +} diff --git a/research/chebyshev-inverse-locality/VERIFY.json b/research/chebyshev-inverse-locality/VERIFY.json new file mode 100644 index 0000000000..b64e451f3c --- /dev/null +++ b/research/chebyshev-inverse-locality/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/delta-cross-cell-independent-audit/README.md", + "research/halo-locality-witness-audit/README.md", + "research/unconditional-batched-crt/HALO.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-X", + "dev", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact scalar recurrence, ordered nonnormal error, LDL operator bound, section locality, coefficient and invalid-input controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-X", + "dev", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete exact checks under optimized Python." + } + ] +} diff --git a/research/chebyshev-inverse-locality/verify.py b/research/chebyshev-inverse-locality/verify.py new file mode 100644 index 0000000000..2e833131d6 --- /dev/null +++ b/research/chebyshev-inverse-locality/verify.py @@ -0,0 +1,248 @@ +"""Exact finite corroboration of the new inverse-locality polynomial. + +Produced by Nick Petalas. Apache-2.0. No predecessor verifier is imported. +""" + +from fractions import Fraction as F +from hashlib import sha256 +import json +from pathlib import Path +import platform + + +def need(condition, message): + if not condition: + raise RuntimeError(message) + + +def coefficients(k, degree): + """Return integer N_d, its scale denominator, and inverse coefficients.""" + if type(k) is not int or not 2 <= k <= 16: + raise ValueError("the finite checker requires integer 2 <= K <= 16") + if type(degree) is not int or not 1 <= degree <= 16: + raise ValueError("the finite checker requires integer 1 <= degree <= 16") + a, b, denominator = k**4 + 1, 2 * k**2, k**4 - 1 + previous, current = [1], [a, -b] + for _ in range(1, degree): + following = [0] * (len(current) + 1) + for j, value in enumerate(current): + following[j] += 2 * a * value + following[j + 1] -= 2 * b * value + for j, value in enumerate(previous): + following[j] -= denominator**2 * value + previous, current = current, following + need(current[0] > 0, "positive normalization") + inverse = tuple(F(-value, current[0]) for value in current[1:]) + return tuple(current), denominator**degree, inverse + + +def evaluate(poly, value): + result = F(0) + for coefficient in reversed(poly): + result = result * value + coefficient + return result + + +def chebyshev(value, degree): + previous, current = F(1), value + for _ in range(1, degree): + previous, current = current, 2 * value * current - previous + return current + + +def eye(n): + return tuple(tuple(F(i == j) for j in range(n)) for i in range(n)) + + +def transpose(a): + return tuple(zip(*a, strict=True)) + + +def combine(a, b, alpha=F(1), beta=F(1)): + return tuple(tuple(alpha * x + beta * y for x, y in zip(u, v, strict=True)) + for u, v in zip(a, b, strict=True)) + + +def multiply(a, b): + columns = transpose(b) + return tuple(tuple(sum(x * y for x, y in zip(row, col, strict=True)) + for col in columns) for row in a) + + +def matrix_poly(poly, a): + identity = eye(len(a)) + result = combine(identity, identity, F(0), F(0)) + for coefficient in reversed(poly): + result = combine(multiply(result, a), identity, F(1), coefficient) + return result + + +def inverse(a): + n = len(a) + rows = [list(row) + list(unit) for row, unit in zip(a, eye(n), strict=True)] + for col in range(n): + pivot = next((r for r in range(col, n) if rows[r][col]), None) + if pivot is None: + raise ValueError("singular fixture") + rows[col], rows[pivot] = rows[pivot], rows[col] + divisor = rows[col][col] + rows[col] = [value / divisor for value in rows[col]] + for r in range(n): + if r != col: + factor = rows[r][col] + rows[r] = [x - factor * y for x, y in + zip(rows[r], rows[col], strict=True)] + result = tuple(tuple(row[n:]) for row in rows) + need(multiply(a, result) == eye(n), "inverse identity") + return result + + +def positive_definite(a): + """Exact unpivoted LDL test, used only on real symmetric fixtures.""" + n = len(a) + if transpose(a) != a: + return False + lower = [[F(i == j) for j in range(n)] for i in range(n)] + diagonal = [F(0)] * n + for j in range(n): + diagonal[j] = a[j][j] - sum(lower[j][r]**2 * diagonal[r] + for r in range(j)) + if diagonal[j] <= 0: + return False + for i in range(j + 1, n): + lower[i][j] = (a[i][j] - sum(lower[i][r] * lower[j][r] * diagonal[r] + for r in range(j))) / diagonal[j] + return True + + +def approximation(h, k, degree): + numerator, denominator, poly = coefficients(k, degree) + gram = multiply(transpose(h), h) + result = multiply(matrix_poly(poly, gram), transpose(h)) + residual = matrix_poly(tuple(F(c, numerator[0]) for c in numerator), gram) + normalization = F(numerator[0], denominator) + return result, residual, normalization, gram + + +def scalar_checks(): + samples = 0 + for k in range(2, 9): + for degree in range(1, 17): + numerator, denominator, poly = coefficients(k, degree) + c = F(k**4 + 1, k**4 - 1) + need(F(numerator[0], denominator) == chebyshev(c, degree), + "independent normalization recurrence") + z = F(k**2 + 1, k**2 - 1) + need(chebyshev(c, degree) == (z**degree + z**(-degree)) / 2, + "closed-form normalization") + need(sum(abs(x) for x in numerator) <= (3 * (k**2 + 1)**2)**degree, + "integer coefficient bound") + for j in range(33): + x = F(1, k**2) + F(j, 32) * (k**2 - F(1, k**2)) + t = (k**4 + 1 - 2 * k**2 * x) / (k**4 - 1) + r = evaluate(numerator, x) / numerator[0] + need(r == chebyshev(t, degree) / chebyshev(c, degree), + "independent scalar recurrence") + need(abs(r) <= F(denominator, numerator[0]), "residual envelope") + need(x * evaluate(poly, x) == 1 - r, "divisible residual") + samples += 1 + return samples + + +def operator_checks(): + fixtures = ( + ((F(1), F(1)), (F(0), F(1))), + ((F(1), F(1, 3), F(0)), (F(0), F(1), F(-1, 4)), + (F(1, 5), F(0), F(1))), + ((F(3, 4), F(1, 5)), (F(-1, 7), F(5, 4))), + ) + count = 0 + for h in fixtures: + h_inverse, identity = inverse(h), eye(len(h)) + for k in (2, 3, 5): + for degree in (1, 2, 3, 4, 6): + result, residual, normalization, gram = approximation(h, k, degree) + need(positive_definite(combine(gram, identity, F(1), F(-1, k**2))), + "lower singular-value hypothesis") + need(positive_definite(combine(identity, gram, F(k**2), F(-1))), + "upper singular-value hypothesis") + error = combine(result, h_inverse, F(1), F(-1)) + expected = combine(multiply(residual, h_inverse), identity, F(-1), F(0)) + need(error == expected, "ordered error identity") + ceiling = F(k**2) / normalization**2 + need(positive_definite(combine(identity, multiply(transpose(error), error), + ceiling, F(-1))), "operator norm bound") + wrong_order = combine(multiply(h_inverse, residual), identity, F(-1), F(0)) + need(error != wrong_order, "wrong residual order control") + need(error != multiply(residual, h_inverse), "wrong residual sign control") + count += 1 + return count + + +def cyclic_fixture(n): + return tuple(tuple(F(i == j) + F(1, 8) * ((i - j) % n == 1) + + F(1, 10) * ((j - i) % n == 1) + for j in range(n)) for i in range(n)) + + +def locality_checks(): + checked, different = 0, 0 + for degree in (1, 2, 3): + n, radius = 21, 2 * degree - 1 + h = cyclic_fixture(n) + selected = tuple(range(2, n - 2)) + section = tuple(tuple(h[i][j] for j in selected) for i in selected) + full = approximation(h, 2, degree)[0] + local = approximation(section, 2, degree)[0] + omitted = tuple(i for i in range(n) if i not in selected) + for r, i in enumerate(selected): + distance = min(min((i - j) % n, (j - i) % n) for j in omitted) + embedded = tuple(local[r][selected.index(j)] if j in selected else F(0) + for j in range(n)) + if distance > radius: + need(embedded == full[i], "section row equality") + checked += 1 + elif distance == radius: + need(embedded != full[i], "too-small halo control") + different += 1 + for i in range(n): + for j in range(n): + if min((i - j) % n, (j - i) % n) > radius: + need(full[i][j] == 0, "physical bandwidth") + return checked, different + + +def controls_and_parameters(): + rejected = 0 + for k, degree in ((1, 1), (0, 1), (17, 1), (2.0, 1), (2, 0), (2, 17)): + try: + coefficients(k, degree) + except ValueError: + rejected += 1 + need(rejected == 6, "finite-domain rejection controls") + for p in range(2, 129): + degree = p**22 + need((2 * degree - 1) * (p - 1) < p**24, "new halo") + need(degree < p**42 and p**24 < p**48, "strict parameter improvement") + return rejected, 127 + + +def main(): + scalar = scalar_checks() + operators = operator_checks() + rows, halo_controls = locality_checks() + invalid, parameters = controls_and_parameters() + root = Path(__file__).resolve().parent + files = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + receipt = { + "status": "PASS_CHEBYSHEV_INVERSE_LOCALITY", "python": platform.python_version(), + "scalar_samples": scalar, "operator_fixtures": operators, + "exact_section_rows": rows, "too_small_halo_rejections": halo_controls, + "invalid_inputs_rejected": invalid, "parameter_instances": parameters, + "sha256": {name: sha256((root / name).read_bytes()).hexdigest() for name in files}, + } + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main() From 31bbc7b22ea697437660a0af4c006e114b90710b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 19:36:33 +0000 Subject: [PATCH 2/2] docs(research): clarify the Chebyshev contribution boundary --- research/chebyshev-inverse-locality/PROOF.md | 4 ++-- research/chebyshev-inverse-locality/README.md | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/research/chebyshev-inverse-locality/PROOF.md b/research/chebyshev-inverse-locality/PROOF.md index f247b428e7..de1c06206a 100644 --- a/research/chebyshev-inverse-locality/PROOF.md +++ b/research/chebyshev-inverse-locality/PROOF.md @@ -115,8 +115,8 @@ The predecessor locality work, including Nick Petalas's #4217 and Mihir Srivastava's #4501, supplies the distinction between polynomial locality, section inverses and ordered nonnormal error identities. Their Neumann polynomials and finite examples are not audited or replayed here. The new -polynomial changes the approximation method, rather than a group, target, -or truncation constant in a recent account contribution. +polynomial changes the approximation method while retaining the input matrix +class and conditioning contract. ## Exact coefficient construction diff --git a/research/chebyshev-inverse-locality/README.md b/research/chebyshev-inverse-locality/README.md index d0c59564f5..f8c5885da2 100644 --- a/research/chebyshev-inverse-locality/README.md +++ b/research/chebyshev-inverse-locality/README.md @@ -96,10 +96,10 @@ identity and a stronger cross-cell conditioning contract. These are cited predecessor results, not new outputs. SOURCES.json pins their retained texts at main `19fdb086ea96af9a9f87936a2b888e10af4ed810`. -The new construction changes the approximation polynomial, rather than -extending a recent account result by changing only a group or target. +The new construction changes the approximation polynomial while retaining +the input matrix class and conditioning contract. The exact finite verifier is new and imports no predecessor implementation. -Live open PRs, recent account work, handoff claims, main README searches and +Live open PRs, handoff claims, main README searches and merged-PR searches were checked. Cached overlap has complete remote pagination but incomplete sparse local-note coverage. These bounded checks are not a novelty certificate.