Prove the sharp Gaussian concentration threshold (no new κ)

research/gaussian-concentration-threshold/PROOF.md

@@ -0,0 +1,164 @@
+# The sharp concentration threshold for nearest-grid Gaussian dominance
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+## Model and statement
+
+Let \(s,t\) be integers with \(s<t<2s\), \(\rho=t/s=1+\theta\),
+and use the physical Gaussian source's half-up convention
+
+\[
+q_j=\lfloor\rho j+1/2\rfloor,\qquad \beta_j=\rho j-q_j\in[-1/2,1/2).
+\]
+
+For real \(a>0\), define the original-coordinate coefficient at displacement
+\(h\ne0\) by
+
+\[
+k_{i,h}(a)=\exp\{-a[(\rho h+\beta_i)^2-\beta_{i+h}^2]\}.
+\]
+
+The cyclic matrix \(N_{s,t,w}(a)\), for integer \(1\le w<s/2\), has diagonal
+one and coefficient \(k_{i,h}\) at column \(i+h\pmod s\) for
+\(0<|h|\le w\); all other entries vanish. Since \(\beta_{j+s}=\beta_j\),
+this agrees with the source's signed cyclic displacement, including physical
+period seams. It is an ideal matrix, before numerical coefficient errors.
+The production concentration is \(a=\pi u\); here \(a\) is allowed to vary.
+
+Write \(R_i(a)=\sum_{0<|h|\le w}k_{i,h}(a)\). For every \(a\ge1\),
+
+\[
+\boxed{R_i(a)\le e^{-2a\theta}+2e^{-2a}
+                   +\frac{2e^{-6a}}{1-e^{-6a}}.}                 \tag{1}
+\]
+
+For even \(s\ge6\), \(t=s+1\), and \(2\le w<s/2\), the half-tie row
+\(i=s/2\) also satisfies
+
+\[
+\boxed{R_{s/2}(a)\ge e^{-2a/s}+e^{-a(2+4/s)}+e^{-a(2+8/s)}.}  \tag{2}
+\]
+
+For this family there is a unique threshold \(A_{s,w}>0\) such that every
+row is strictly diagonally dominant exactly when \(a>A_{s,w}\). Uniformly
+over every allowed \(w\ge2\), as even \(s\to\infty\),
+
+\[
+\boxed{A_{s,w}=\tfrac12(\log s-\log\log s+\log2)+o(1).}        \tag{3}
+\]
+
+All logarithms are natural. In particular the leading concentration
+coefficient \(1/2\), the subtractive log-log term, and the additive
+\(\log2/2\) are necessary for a uniform continuous-concentration guarantee.
+For integer \(u\), the least admitted value is
+\(\lfloor A_{s,w}/\pi\rfloor+1\); its corresponding expansion has
+\(O(1)\), rather than \(o(1)\), rounding uncertainty.
+
+## Upper bound
+
+The retained LOG-A-PHASE-SCHUR-AUDIT, section 1, already proves
+
+\[
+k_{i,-1}+k_{i,1}\le e^{-2a\theta}+e^{-2a(1+\theta)}.           \tag{4}
+\]
+
+We use that result as a premise. The new estimate concerns the farther
+tail. Since \(\beta_{i+h}^2\le1/4\), for each positive \(h\ge2\),
+
+\[
+k_{i,h}+k_{i,-h}\le
+e^{-a((\rho h+\beta_i)^2-1/4)}+
+e^{-a((\rho h-\beta_i)^2-1/4)}.
+\]
+
+The right side is an even convex function of \(\beta_i\) on
+\([-1/2,1/2]\). Indeed each summand's second derivative has the sign of
+\(2a(\rho h\pm\beta_i)^2-1\), which is positive for \(a\ge1,h\ge2\).
+Its maximum is therefore at an endpoint. Since \(\rho>1\), this gives
+
+\[
+k_{i,h}+k_{i,-h}\le e^{-ah(h-1)}+e^{-ah(h+1)}.
+\]
+
+Summing the positive convergent series and shifting the first index yields
+
+\[
+\sum_{|h|\ge2}k_{i,h}\le e^{-2a}
+           +2\sum_{r\ge2}e^{-ar(r+1)}
+\le e^{-2a}+\frac{2e^{-6a}}{1-e^{-6a}}.                        \tag{5}
+\]
+
+For the last inequality, successive exponents \(r(r+1)\) differ by at least
+six for \(r\ge2\). Combine (4), (5), and
+\(e^{-2a(1+\theta)}\le e^{-2a}\). A finite band only removes positive terms,
+so (1) follows without an infinite-period identification or a tail-admission
+assumption. The earlier \(5e^{-2a}\) tail coefficient is sufficient but
+does not locate the additive transition constant.
+
+## Lower bound
+
+For \(t=s+1\), even \(s\), and \(i=s/2\), the actual nearest convention gives
+
+\[
+\beta_i=-1/2,\quad
+\beta_{i+1}=-1/2+1/s,\quad
+\beta_{i-1}=1/2-1/s,\quad
+\beta_{i+2}=-1/2+2/s.
+\]
+
+Substitution into the coefficient definition gives exponents
+\(2/s\), \(2+4/s\), and \(2+8/s\) at displacements \(+1,-1,+2\).
+All three are retained for every \(w\ge2\). Dropping the other nonnegative
+entries proves (2). The second farther entry matters: retaining only one
+\(e^{-2a}\) contribution predicts an incorrect additive threshold.
+
+## Threshold and its uniform asymptotics
+
+Every off-diagonal exponent is positive because
+\(|\rho h+\beta_i|\ge\rho|h|-1/2>1/2\ge|\beta_{i+h}|\).
+Thus \(\max_i R_i(a)\) is continuous and strictly decreasing. At zero it is
+\(2w>1\), and it tends to zero at infinity. This proves existence and
+uniqueness of \(A_{s,w}\), including the strict endpoint convention.
+
+Set \(L=\log s\) and, for any fixed real \(b\),
+
+\[
+a_s(b)=\tfrac12(L-\log L+b),\qquad e^{-2a_s(b)}=s^{-1}Le^{-b}.
+\]
+
+As \(s\to\infty\), \(a_s(b)\to\infty\), \(a_s(b)/s\to0\), and
+
+\[
+\frac{1-e^{-2a_s(b)/s}}{s^{-1}L}\longrightarrow1.
+\]
+
+In (1) the other leading contribution, divided by \(s^{-1}L\), is
+\(2e^{-b}\); the remaining geometric tail divided by that scale tends
+to zero. In (2), the two farther terms have sum
+
+\[
+s^{-1}Le^{-b}(e^{-4a_s(b)/s}+e^{-8a_s(b)/s}),
+\]
+
+whose normalized limit is also \(2e^{-b}\). Consequently (1) proves
+dominance eventually whenever \(b>\log2\), and (2) proves failure
+eventually whenever \(b<\log2\). Neither estimate depends on \(w\).
+Sandwiching the threshold between these two concentrations, with \(b\)
+arbitrarily close to \(\log2\), proves (3) uniformly in \(w\).
+No sign at the exact choice \(b=\log2\) is asserted.
+
+## Scope and predecessor credit
+
+The matrix convention comes from Jose Manuel's PR3851 physical Gaussian
+core. The nearest-neighbor estimate (4) comes from Vlado Vojdanovski's
+retained phase-cell audit in the PR1673 lineage and its RaD/hipotures
+predecessors. The new result is the matching concentration threshold,
+using (5) and the three-entry obstruction. No predecessor computation is
+replayed as a contribution.
+
+This theorem varies concentration outside the unchanged production guard.
+It does not prove a changed production caller, coefficient-error bound,
+inverse implementation, complete signed invoice, or new multiplication
+theorem or kappa. The selected frontier and all five assumptions remain.
+The universal result is this written proof; the accompanying exact finite
+checks corroborate its new formulas and detect missing-tail admissions.

research/gaussian-concentration-threshold/README.md

@@ -0,0 +1,111 @@
+# A sharp Gaussian concentration threshold
+
+Scoped proof with exact finite controls. This contribution was produced by
+Nick Petalas. Apache-2.0. No new kappa is claimed.
+
+For the nearest-grid Gaussian matrix with expansion ratio \(1+1/s\), even
+\(s\), and any retained bandwidth \(2\le w<s/2\), let \(A_{s,w}\) be the
+continuous concentration at which the largest off-diagonal row sum equals
+one. [PROOF.md](PROOF.md) establishes
+
+\[
+A_{s,w}=\frac{\log s-\log\log s+\log2}{2}+o(1),
+\]
+
+uniformly in the bandwidth. Every row is strictly dominant exactly above
+that threshold. The result determines both the log-log correction and the
+additive constant. Integer concentration \(u\), with \(a=\pi u\), has the
+corresponding bounded rounding uncertainty.
+
+The new proof sharpens the farther-tail estimate to obtain
+
+\[
+R_i(a)\le e^{-2a\theta}+2e^{-2a}
+                    +\frac{2e^{-6a}}{1-e^{-6a}},\qquad a\ge1.
+\]
+
+Three literal entries at the half-tie row give the matching obstruction.
+At \(a=k\log2\) and \(s=2^{20}\), the exact controls certify failure for
+\(k=8\) and dominance for \(k=9\). A separate \(s=2^{19},k=8\) control
+shows that deleting one of the two leading tail contributions falsely
+certifies dominance. These finite examples are supporting certificates;
+the asymptotic statement follows from the written proof.
+
+## Reproduction and evidence
+
+From the repository root, using CPython 3.12 and only its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-concentration-threshold
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-concentration-threshold --check-source-history --check-modes
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/gaussian-concentration-threshold/verify.py
+```
+
+Use another CPython 3.12 executable on other machines. The registered commands
+run both normal and optimized modes. Each prints
+`PASS_GAUSSIAN_CONCENTRATION_THRESHOLD` and a generated report bound to the
+package and live-source SHA256 hashes. No receipt is handwritten.
+
+The finite checks enumerate 522 geometry equalities, 336 complete band rows
+and their 4,368 retained off-diagonal entries. They also classify all 231
+declared dyadic concentration/period pairs through \(s=2^{24}\), with 136
+certified dominant and 95 certified nondominant cases, none unresolved.
+Four malformed arithmetic-domain cases are rejected. All interval endpoints
+are integers on a 192-bit dyadic grid, using outward integer multiplication,
+integer square roots and bounded exponentiation. No floating point,
+transcendental implementation or predecessor verifier is used.
+
+The retained sources have exact main-commit, Git-blob and SHA256 pins in
+[SOURCES.json](SOURCES.json). Their mathematical conventions are inputs;
+their prior scientific results are cited rather than re-audited. The source
+checker authenticates both live files before the new finite calculations.
+
+## Scope and relation to existing work
+
+The [original question](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241969)
+changes concentration outside the unchanged production guard. It asks for
+a matching obstruction and sufficient condition at that changed guard.
+
+Jose Manuel's [PR3851](https://github.com/CrocSwap/integer-mult-bounds/pull/3851)
+supplies the physical matrix convention. The retained PR1673 phase-cell
+audit by Vlado Vojdanovski, with its RaD/hipotures predecessors, supplies
+the nearest-neighbor majorant. Its farther-tail estimate has coefficient
+five; the new estimate and half-tie obstruction determine the threshold.
+Gaussian convexity and geometric-series arguments are standard.
+
+[PR6099](https://github.com/CrocSwap/integer-mult-bounds/pull/6099) concerns
+coefficient perturbation and leaves production row dominance open.
+[PR6126](https://github.com/CrocSwap/integer-mult-bounds/pull/6126) improves
+the inverse bound under unchanged production guards. Neither is a theorem
+dependency here. The present result varies the guard and supplies a matching
+failure family, rather than computing that production inverse bound.
+
+No complete physical caller at reduced concentration is supplied. The theorem
+does not bound numerical coefficient errors, infinite periodization error,
+LU growth, physical preparation, tensor assembly or the full recursive bill.
+No selected cold replay, proof kernel or independent human review ran.
+The selected frontier and all five inherited assumptions remain unchanged.
+There is no sign claim at the exact critical asymptotic offset.
+
+## Open next questions
+
+1. Can a reduced-concentration physical caller pay its coefficient errors and
+   retain a sufficient inverse allowance? This could reduce normalization
+   charges. Start with the explicit sufficient bound above at one complete
+   production parameter tuple; physical geometry and the full error/cost
+   invoice remain blockers.
+2. What is the first vanishing correction to the continuous threshold? Start
+   with the same three half-tie entries and a sharper uniform remainder.
+   Identifying an exact maximizing row is the remaining obstacle. This is
+   separate from the proved additive \(\log2/2\) constant.
+
+## Verifier bounds
+
+The verifier has fixed finite fixture sets, at most 24 root or exponent-bit
+iterations per arithmetic call, and at most 256 indices in a geometry loop.
+Its matrix fixtures have at most 32 rows. It uses no recursion or indirect
+code execution. Python allocates managed integers and dictionaries during
+execution, a documented deviation from static allocation; their sizes are
+bounded by these fixtures and the fixed grid. Runtime contracts remain
+enabled under optimization. The universal mathematical claim rests on the
+proof, not on expanding those finite bounds.

research/gaussian-concentration-threshold/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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/capped-phase-fusion/evidence/gaussian_fast_ultra/LOG-A-PHASE-SCHUR-AUDIT.md",
+      "usage": "input",
+      "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73",
+      "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_axis.py",
+      "usage": "input",
+      "git_blob": "edc443a7281e83536a00e9f9fa950d7d854705a3",
+      "sha256": "d416918d7442c5033e43fba94ccc5ed33badc3aebe90ddd479b0b6c020de9724"
+    }
+  ]
+}