Reduce Gaussian inverse locality degree from p^42 to p^22 (no new κ)

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.

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.

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"
+    }
+  ]
+}