Prove exact fixed-rank Gaussian inverse error (no κ)

research/gaussian-inverse-rank-error/PROOF.md

@@ -0,0 +1,176 @@
+# Exact fixed-rank compression error of the full Gaussian inverse
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Claim and exact predecessor premise
+
+Fix alpha>0, put b=pi/alpha^2, and take 0<theta<1. Write
+rho=1+theta, N=floor(1/theta), c=1/(2rho), and
+
+    K_theta[k,i] = alpha^(-1) exp(-b (i-k/rho-c)^2),  0<=k,i<N.
+
+No entry is truncated. For a bounded operator X define
+
+    d_r(X) = inf { ||X-R||_op : rank R <= r },  r=0,1,2,... .
+
+For every FIXED nonnegative integer r, the new conclusion is
+
+    lim_(theta -> 0) d_r(K_theta^(-1)) / ||K_theta^(-1)||_op
+      = 1 / sqrt(2 floor(r/2)+1).                         (1)
+
+In particular, a rank-one approximation has asymptotically the same
+operator-norm error as the zero approximation. Rank two first lowers the
+relative limiting error to 1/sqrt(3). This statement allows arbitrary
+linear approximants, including those mixing the two ends of the cell.
+It is an analytic optimum, not a method for preparing or applying modes.
+
+The cited premise is JoyboyBrian's [PR5183](https://github.com/CrocSwap/integer-mult-bounds/pull/5183),
+retained at base 7c49fe32c55de02c2c873655c804b16e4c3fef0a in
+[PROOF.md](../gaussian-half-line-operator-limit/PROOF.md). Its theorem gives
+an isometric embedding U_theta into H=L2(0,infinity) direct-sum L2(0,infinity)
+and the checkerboard sign matrix S=diag((-1)^i) such that
+
+    X_theta = U_theta [sqrt(theta) S K_theta^(-1) S] U_theta*
+    ||X_theta - a (T_b direct-sum T_b)||_op -> 0,
+    a = alpha exp(b/4) / P(b)^3,
+    P(b) = product_(j>=1) (1-exp(-2bj)),
+    (T_b f)(x) = integral_(x to infinity) exp(-b(y^2-x^2)) f(y) dy. (2)
+
+We use (2) as a credited mathematical premise. We do not re-prove or
+replay the source finite Gaussian matrices, source exponents, q-LDU sum,
+embedding estimates or boundary-layer convergence. The new argument
+calculates every singular value of T_b and transfers the resulting
+approximation law through (2). No uniform growing-alpha result is used.
+
+## Complete half-line singular system
+
+Let H_n be the physicists' Hermite polynomial. Define the normalized
+full-line Hermite functions, scaled to b, by
+
+    phi_n(x) = (2b)^(1/4) H_n(sqrt(2b)x) exp(-bx^2)
+               / [pi^(1/4) sqrt(2^n n!)].
+
+Their orthonormality, completeness and parity are classical; see
+[NIST DLMF 1.18.42-43](https://dlmf.nist.gov/1.18#E42).
+Let psi_n be sqrt(2) times the restriction of phi_n to x>0.
+Each of the two sequences
+
+    e_k = psi_(2k),    o_k = psi_(2k+1),    k>=0,
+
+is an orthonormal basis of the SAME half-line Hilbert space. To see
+completeness, extend a half-line function evenly or oddly to the full
+line, use the full-line basis, and restrict back. The two sequences are
+not asserted to be mutually orthogonal to each other.
+
+The classical weighted derivative identity is
+
+    d/dz [exp(-z^2) H_n(z)] = -exp(-z^2) H_(n+1)(z).
+
+See [NIST DLMF 18.9.26](https://dlmf.nist.gov/18.9#E26).
+The polynomial times Gaussian vanishes at infinity. With z=sqrt(2b)y,
+integrating this identity gives
+
+    T_b [H_(2k+1)(sqrt(2b)y) exp(-by^2)](x)
+       = H_(2k)(sqrt(2b)x) exp(-bx^2) / sqrt(2b).
+
+Taking account of the different normalization constants yields
+
+    T_b o_k = s_k e_k,
+    s_k = 1 / [2 sqrt(b(2k+1))].                          (3)
+
+There is no extra boundary condition imposed on either input or output.
+The integral itself determines (3).
+
+For completeness T_b is bounded independently of the spectral conclusion.
+For 0<=x<=y one has y^2-x^2 >= (y-x)^2. Both integrals of its nonnegative
+kernel, in either variable with the other fixed, are at most
+integral_0^infinity exp(-bt^2)dt=sqrt(pi)/(2sqrt(b)). The Schur test
+therefore bounds its operator norm. Equality (3) on the input basis
+extends by continuity to every L2 input. Since the output sequence is
+also a basis, this is a complete singular-value expansion. Its adjoint
+maps e_k to s_k o_k. Truncating after m terms has norm error s_m -> 0,
+so T_b is compact. Its singular values, indexed from zero, are exactly
+the strictly decreasing numbers s_k in (3).
+
+The Hermite facts and diagonal-operator argument are classical. The new
+source-specific consequence is the full spectrum and fixed-rank law for
+(2), rather than another estimate of its top norm.
+
+## Optimal rank error and doubled modes
+
+Put B=a(T_b direct-sum T_b). Each s_k occurs twice in the singular
+spectrum of B, multiplied by a. Thus
+
+    d_r(B) = a / [2 sqrt(b(2 floor(r/2)+1))].              (4)
+
+Here is a direct minimax proof, including arbitrary approximants. The
+upper bound retains the r largest singular modes. For the lower bound,
+restrict any rank-at-most-r operator R to the span of the first r+1
+right singular vectors. Rank-nullity supplies a nonzero vector v in
+that span with Rv=0. Orthogonality of their images implies
+||Bv|| >= sigma_(r+1)(B)||v||, with singular values now indexed from one.
+Consequently ||B-R|| >= sigma_(r+1)(B), which is (4). A rank mixing the
+two edges cannot escape this argument.
+
+For any bounded X,Y on the same spaces,
+
+    |d_r(X)-d_r(Y)| <= ||X-Y||.                           (5)
+
+Indeed, for every rank-at-most-r R, the triangle inequality gives
+||X-R|| <= ||X-Y||+||Y-R||; take infima and exchange X,Y.
+Applying (5) to (2) and (4) gives the absolute limit
+
+    sqrt(theta) d_r(K_theta^(-1))
+       -> a / [2 sqrt(b(2 floor(r/2)+1))].                (6)
+
+An isometric embedding followed by zero on its orthogonal complement
+does not change nonzero singular values or rank approximation errors.
+One may also prove this directly: embed a finite approximant for the
+upper bound and compress any Hilbert-space approximant by U_theta*
+and U_theta for the lower bound. Compression does not increase rank
+or norm. Multiplication by S on either side preserves both. These facts
+justify the left side of (6) without changing the permitted approximants.
+For r=0, (6) has the positive limit a/(2sqrt(b)). Dividing proves (1).
+
+Equivalently, for every fixed j>=1,
+
+    sqrt(theta) sigma_j(K_theta^(-1))
+       -> a / [2 sqrt(b(2 floor((j-1)/2)+1))].            (7)
+
+The order of limits is fixed j or r first, then theta tending to zero.
+
+## Exact compression threshold in the limiting operator
+
+For 0<epsilon<=1, the least rank attaining relative error at most epsilon
+for B itself is
+
+    r_min(epsilon) = 2 ceil((epsilon^(-2)-1)/2).         (8)
+
+This follows by solving (4), since the first rank in every equal-error
+pair is even. For epsilon=1/2 the least rank is four; for epsilon=1/10
+it is 100. Formula (8) concerns the limiting operator. At an exact equality
+threshold it does not establish the eventual least rank of every finite
+K_theta. Likewise, (1) alone does not apply to an unbounded r(theta).
+
+## Evidence, credit and limits
+
+The bounded verifier proves polynomial identities and exact Gaussian
+integrals on finite Hermite spans and checks the doubled spectral and
+threshold arithmetic. These calculations corroborate (3)-(8); they do
+not prove infinite-dimensional completeness or the source limit by
+sampling. The universal claim rests on the written argument and the
+explicit classical and predecessor premises.
+
+Credit JoyboyBrian / PR5183 for (2), including its full coefficient and
+endpoint embedding, and its predecessors Jose Manuel / PR4193, Vlado
+Vojdanovski / PR1673, Ryanson Jonathan / PR4435, Nick Petalas / PR5150,
+Cinna Davis and the retained Gaussian lineage. Their files are unchanged.
+No global literature priority is claimed for Hermite singular systems,
+minimax approximation or the inequalities used here.
+
+This exact-real theorem supplies no rounded prefix analysis, mode
+preparation or application algorithm, bit/tape/storage/movement tariff,
+native/compiler/stock admission, exact integer recovery, new kappa or
+complete multiplication theorem. The selected frontier and its five
+framework assumptions are unchanged. Independent human and formal
+proof-kernel review are unclaimed.

research/gaussian-inverse-rank-error/README.md

@@ -0,0 +1,140 @@
+# Exact rank-error asymptote for the full Gaussian inverse
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For the original **untruncated varying-phase full cell** of JoyboyBrian's
+[PR5183](https://github.com/CrocSwap/integer-mult-bounds/pull/5183), fix alpha>0
+and let theta tend to zero. For every fixed nonnegative integer r,
+
+```text
+best rank-at-most-r approximation error / inverse operator norm
+    -> 1 / sqrt(2 floor(r/2)+1).
+```
+
+This is a scoped written mathematical proof with exact finite corroboration.
+The new result determines the complete limiting singular spectrum and the
+optimal fixed-rank error, beyond the predecessor's top-norm result.
+The two boundary layers duplicate every singular value. Consequently rank
+one cannot lower the limiting relative error, and the limiting operator
+needs rank four to reach relative error at most one half. These are analytic
+rank counts, not physical recursive bills. No new kappa is claimed.
+
+[PROOF.md](PROOF.md) defines the exact finite matrix and proves the result.
+It constructs odd/even half-line Hermite bases and derives
+`s_k(T_b)=1/(2 sqrt(b(2k+1)))`. Rank-nullity proves optimality even for
+approximants mixing the two edges. The source operator-norm limit and the
+Lipschitz property of rank approximation errors transfer the result to the
+finite Gaussian inverse. The source theorem is a credited premise; no
+predecessor scientific replay is included.
+
+## Reproduction
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-inverse-rank-error/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/gaussian-inverse-rank-error/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-inverse-rank-error
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-inverse-rank-error --check-source-history
+```
+
+On another host, substitute its Python 3.12 path. The final command requires
+a commit containing this package and full source history. The direct commands
+print `PASS_GAUSSIAN_INVERSE_RANK_ERROR` inside a generated JSON receipt bound
+to the package and source-proof hashes. Optional `--receipt /absolute/path.json`
+creates that receipt exclusively outside the checkout. No replay writes
+artifacts into the checkout.
+
+The exact verifier compares explicit factorial and recurrence definitions of
+Hermite polynomials, evaluates their Gaussian Gram integrals, and solves
+weighted antiderivatives by descending coefficients. Coherent polynomial
+mixtures test the integral map and normalization. Finite doubled diagonal
+truncations check rank indexing, and rank-one matrices mixing the first two
+edge modes have explicit kernel witnesses. Rational tolerance checks exercise
+the least-rank threshold, including its equality cases. Invalid contracts and
+one-edge, parity and dilation controls remain active under optimized Python.
+These are finite corroboration, not a substitute for the written proof or
+classical Hermite completeness.
+
+Local CPython 3.12.15 on macOS passed both registered commands. Individually
+timed direct runs took 0.137 and 0.146 seconds, with identical JSON receipts.
+They enumerate 34 polynomial definitions, 33 derivative identities, 512
+Gram entries, 16 antiderivatives and normalizations, 81 coherent mixtures,
+1,275 coordinate truncations, 324 rational tolerances, 33 mixed-edge
+rank-one matrices and 15 rejection/semantic controls. These are check
+durations and finite counts, not a runtime speedup claim.
+
+## Scope and limits
+
+The order of limits is fixed r or fixed singular index first, then theta
+shrinking at fixed alpha. The exact limiting-operator least rank is
+`2 ceil((epsilon^(-2)-1)/2)` for `0<epsilon<=1`. At equality thresholds this
+is not an eventual finite-matrix least-rank assertion. No growing-rank or
+growing-alpha uniformity is proved.
+
+No coefficient or mode preparation, inverse application, rounded execution,
+precision/tape/storage/movement tariff, dirty restoration, stock, native or
+compiler admission, integer recovery or complete multiplication theorem is
+supplied. The selected PR6030 frontier and all five framework assumptions
+remain unchanged. Independent human and formal proof-kernel review are
+unclaimed. Lean, Docker and the selected scientific cold replay are outside
+this analytic contribution.
+
+## Open next questions
+
+Can the rank-error asymptote hold uniformly for a specified growing rank
+r(theta)? This matters when the requested relative error vanishes. Start
+with the source operator-norm remainder and compare it to the next predicted
+singular value for one rank schedule. A useful uniform remainder and the
+complete physical cost of preparing and applying those modes remain missing.
+No wider construction search is included.
+
+## Sources and overlap
+
+Credit JoyboyBrian / PR5183 for the two-edge limit and its full coefficient;
+Jose Manuel / PR4193, Vlado Vojdanovski / PR1673, Ryanson Jonathan / PR4435,
+Nick Petalas / PR5150, Cinna Davis and the retained Gaussian lineage.
+Classical Hermite completeness and the weighted derivative identity are
+cited to [NIST DLMF 1.18.42](https://dlmf.nist.gov/1.18#E42) and
+[18.9.26](https://dlmf.nist.gov/18.9#E26). Hermite singular systems,
+minimax approximation and operator-norm perturbation are classical; no
+general literature priority is claimed for them. The contribution is their
+explicit full-cell inverse rank-error consequence. Predecessor files and
+credit are unchanged.
+
+The base is canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`,
+priority revision 8, selected PR6030. [TASK.json](TASK.json) records the
+changed card scope; [SOURCES.json](SOURCES.json) pins the source proof.
+The advance [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363381)
+followed live claims, reservations, current-main formula/object searches,
+open/merged searches and recent account-work checks. Sparse historical
+notes, arbitrary historical diffs and unpublished work remain limits.
+
+Related open work includes PR3910 on forward row-norm transfer, PR371 on
+final-grid rounding, PR6413 on finite encoded setup, PR6459 on constant-shift
+finite-cap inverse bounds, and PR6404/6405 on truncated Gaussian Schur
+boundaries. Their objects or quantities differ from this full-cell inverse
+singular spectrum; no shared computed number is compared. PR5986 concerns
+polynomial locality under norm hypotheses rather than rank compression.
+
+## Implementation bounds
+
+Build the Lever led to a standalone exact verifier; Prove It Works led to
+separate polynomial constructors, literal antiderivatives and Gram integrals.
+Power of Ten inspection is confined to verify.py. There is no recursion,
+network, subprocess, dynamic code loading or predecessor executable import.
+Polynomial degrees are at most 33, Gram blocks have sixteen modes per parity,
+the mixing enumeration has 81 four-coefficient vectors, and every truncation
+subset lies in an eight-mode space. Rank-one controls enumerate 81 integer
+matrices. Tolerances have denominators at most 32. Functions fit sixty lines.
+Explicit exceptions preserve checks under optimization.
+
+Power of Ten rule 3 has a managed-runtime deviation for Python integers,
+Fractions, tuples and lists. Fixed finite domains bound all live collections;
+there is no steady service. Rule 9 retains standard-library iterator and
+argument-parser dispatch with fixed visible targets. Package hashing admits
+at most sixteen regular files of at most 1 MiB each and one source proof of
+at most 1 MiB. The receipt file is scoped and closed on every exit. A fixed
+memory native checker would be required to remove those runtime deviations.
+Warning-strict normal and optimized execution and in-memory AST/compilation
+checks supply local diagnostics; no shared configuration changes are made.

research/gaussian-inverse-rank-error/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/gaussian-half-line-operator-limit/PROOF.md",
+      "usage": "input",
+      "git_blob": "794842c1155fe826742a98e6107256b040a39b9d",
+      "sha256": "2bf0e36ecd0c3647888e78bc0b8ae30614f5daf07511a4424d69cb3efc29c904"
+    }
+  ]
+}