diff --git a/research/chebyshev-inverse-locality/PROOF.md b/research/chebyshev-inverse-locality/PROOF.md
new file mode 100644
index 0000000000..de1c06206a
--- /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, W<p, and H and each section used for an inverse
+have both norms at most p^10. Set
+
+    K=p^10,    d=p^22.
+
+Then
+
+    ||B_d(H)-H^-1||_2 <= 2p^10 exp(-2p^2) < p^10 exp(-p^2),
+
+because exp(p^2)>2 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 while retaining the input matrix
+class and conditioning contract.
+
+## 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<L^2, the recurrence bounds the next norm by
+
+    2L(3L)^j + L^2(3L)^(j-1) = (7/9)(3L)^(j+1).
+
+Thus coefficient numerator and denominator bit lengths are O(d log K).
+With d=p^22 and K=p^10 this is polynomial in p. Naive exact recurrence and
+local polynomial evaluation therefore give polynomial offline setup, as
+required of a locality witness. This is not a practical runtime benchmark
+or a charged physical coefficient-page implementation.
+
+## Scope
+
+This proves one conditional approximation and locality improvement. It
+supplies no optimized global core geometry, complete tape/precision bill,
+rounded implementation, native supplier admission, new kappa, or complete
+multiplication theorem. The selected record and all five assumptions remain
+unchanged. Coefficient rounding and finite-precision recurrence stability
+require their own analysis before replacing a physical implementation.
+
+The finite verifier corroborates identities on bounded rational matrices.
+The universal quantifiers above rest on this written proof. Independent
+human and formal proof-kernel review are unclaimed.
diff --git a/research/chebyshev-inverse-locality/README.md b/research/chebyshev-inverse-locality/README.md
new file mode 100644
index 0000000000..f8c5885da2
--- /dev/null
+++ b/research/chebyshev-inverse-locality/README.md
@@ -0,0 +1,118 @@
+# A smaller exact locality polynomial for the Gaussian inverse
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written mathematical proof with exact finite corroboration.
+Under the historical Gaussian caller's unchanged assumptions
+`||H||_2, ||H^-1||_2 <= p^10` and physical bandwidth `W<p`, an explicit
+Chebyshev inverse polynomial replaces the Neumann locality witness:
+
+```text
+                            historical witness      new witness
+residual degree             p^42                    p^22
+conservative halo           p^48                    p^24
+inverse error bound         p^10 exp(-p^2)           2p^10 exp(-2p^2)
+```
+
+The new error is strictly smaller than the old majorant for every integer
+`p>=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 while retaining
+the input matrix class and conditioning contract.
+The exact finite verifier is new and imports no predecessor implementation.
+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.
+
+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()