Research audit: tighter Gaussian correction-power endpoint bound (no new kappa)

research/gaussian-endpoint-potential-audit/CLAIM.md

@@ -0,0 +1,29 @@
+# Local sprint claim
+
+- Track: adversarial mathematical audit; OS-random seed: 62 (cryptographic byte rejection at 200, then modulo 100).
+- Base: f567884aeb8851b6e794af1184119a3bfbe1e631.
+- Object: notes/fast-gaussian-resampling.tex, lem:correction-powers; retain the correlated endpoint squares in the existing potential argument.
+- Hypothesis: combining the endpoint terms gives beta_end^2/theta - beta_start^2/theta, reducing the exponential prefactor; derive certified residual counts without confusing a power residual with the inverse tail.
+- Method: written universal algebra; exact rational path enumeration, a separate integer-scaled oracle, rational constant bounds and adversarial sign/tie/carry controls. Seed 62 fixes supplemental path samples.
+- Deliverable: one scoped proof/audit package with a deterministic certificate and offline verification command. No new kappa; no selected-frontier change.
+- Expected finish: 2026-10-13 12:00 UTC (14:00 Europe/Paris).
+- Three candidates considered: packed-bit exceptional repair (already addressed by #735/#763/#773); signed coefficient extraction (already addressed by #690/#693); Gaussian correction-power endpoint accounting (chosen).
+- Overlap: current open PR titles through #898; targeted all-state searches for selected-bit, signed packing, resampling, Neumann and correction powers. #5 supplies the original potential; #684 audits chirp windows and explicitly excludes Neumann evaluation. No duplicate endpoint-power refinement found in these searches. This is a bounded metadata inspection, not an exhaustive review of every PR's source.
+- Coordination: the open-issue query returned only #650, a request to enable Discussions, not a pinned sprint issue. Claim recorded locally; no reservation issue opened.
+- Budget: scope now frozen; reserve the final quarter of implementation/verification effort for adversarial checks and handoff.
+
+## Result (single completion update)
+
+Completed: the combined endpoint potential removes the additive `1/2` from
+the old burn-in exponent and gives the exact odd/even denominator refinement.
+The same-decay term count improves on 1,876 of 3,296 declared parameter cases.
+Eight new test groups pass normally and under optimized Python; isolated
+reproduction and the existing selected-record checks pass. No new kappa.
+
+Review: https://github.com/CrocSwap/integer-mult-bounds/pull/902
+
+The final overlap refresh covered arrivals through #901 and the targeted
+Gaussian/potential search. The remote main still equals the recorded base.
+The base ledger records #5 as partially reviewed and #371 as unreviewed;
+these wider predecessor reviews are not completed by this narrow audit.
+All scientific changes are confined to this package; see VALIDATION.md.

research/gaussian-endpoint-potential-audit/README.md

@@ -0,0 +1,204 @@
+# Gaussian correction powers: keep the endpoint squares together
+
+**Research audit / analytic refinement; no new kappa.** The existing
+`lem:correction-powers` in `notes/fast-gaussian-resampling.tex` is valid but
+separately bounds two correlated endpoint terms. Keeping them together gives
+
+\[
+ \|E^n\|_\infty\le
+ \exp\left(\frac{\pi\alpha^2}{\theta}
+                \frac{\lfloor s/2\rfloor^2}{s^2}\right)
+ \left(\sum_{h\ne0}e^{-\pi\alpha^2\sigma h^2}\right)^n
+ <\exp\left(\frac{\pi\alpha^2}{\theta}
+                \frac{\lfloor s/2\rfloor^2}{s^2}\right)
+ (2.01e^{-\pi\alpha^2\sigma})^n.
+\]
+
+Here `2 <= s < t` are coprime integers, `sigma=t/s`, `theta=sigma-1`,
+`alpha >= 2`, and `n >= 1`. The old exponential prefactor uses
+`1/(4 theta) + 1/2`; the new one uses at most `1/(4 theta)`, and less
+when `s` is odd. This is a deduction from eumemic's existing potential,
+not a new Gaussian algorithm. There is no contradiction to the old bound.
+No optimality of the new prefactor or truncation count is claimed.
+
+## Precise object and proof
+
+Use the correction operator from the pinned note, on `s`-periodic vectors:
+
+\[
+ (Eu)_j=\sum_{h\in\mathbb Z\setminus\{0\}}
+ e^{-A X_{j,h}}u_{j+h},\quad
+ A=\pi\alpha^2,\quad
+ X_{j,h}=(\sigma h+\beta_j)^2-\beta_{j+h}^2,
+\]
+
+where `q_j=floor(tj/s+1/2)` and `beta_j=tj/s-q_j` for every integer `j`.
+Thus `-1/2 <= beta_j < 1/2`; ties round upward. In particular **nonzero
+multiples of s remain in the sum**, even though they address the same
+coordinate. Periodicity is not a reason to discard them.
+
+Put `y=beta_j+theta h` and `w=q_(j+h)-q_j-h`. Then `w` is integral and
+`beta_(j+h)=y-w`. Direct expansion gives the sharper one-step identity
+
+\[
+ X_{j,h}=\sigma h^2+
+ \frac{\beta_{j+h}^2-\beta_j^2}{\theta}
+ +\frac{\sigma}{\theta}w(2y-w).                 \tag{1}
+\]
+
+The last term is nonnegative: writing `z=y-w` gives
+`w(2y-w)=w^2+2wz >= w^2-|w| >= 0`. This uses only `theta>0`,
+not `theta<1`. Equivalently, in the predecessor's proof combine
+`Phi(end)-Phi(start)` with `beta_start^2-beta_end^2` **before** bounding
+them: since `sigma/theta-1=1/theta`, their sum is exactly the middle
+term in (1).
+
+For a path `j_i=j_(i-1)+h_i`, sum (1):
+
+\[
+ \sum_i X_{j_{i-1},h_i}\ge
+ \sigma\sum_i h_i^2+
+ (\beta_{j_n}^2-\beta_{j_0}^2)/\theta.        \tag{2}
+\]
+
+This holds for every finite path of nonzero integer increments, including
+negative increments, repeated coordinates and arbitrary winding. Coprimality
+implies the residues `tj mod s` visit every residue. Hence
+
+\[
+ \min_j\beta_j^2=0,\qquad
+ \max_j\beta_j^2=\lfloor s/2\rfloor^2/s^2=:b_s^2.
+\]
+
+Apply (2) to every term in the path expansion of `E^n`. The positive
+Gaussian sums converge absolutely (quadratic decay in each increment), so
+Tonelli permits summing the inequalities. The sum of the majorants factors
+into the nth power of the one-dimensional Gaussian sum. Every row sum is
+bounded by `exp(A beta_j^2/theta)` times that power; taking the maximum
+proves the first displayed bound. Equivalently, conjugation by
+`D_jj=exp(A beta_j^2/theta)` makes every row sum of `D^-1 E D` at most
+the Gaussian sum. No diagonalization or eigenvalue assumption is used.
+
+For `a=A sigma>4 pi>12`, the inequality `h^2 >= 1+3(h-1)` for `h>=1`
+gives
+
+\[
+ \sum_{h\ne0}e^{-a h^2}\le 2e^{-a}/(1-e^{-3a})<2.01e^{-a}.
+\]
+
+For the last strict comparison it suffices that `e>2` and `a>12`, so
+`e^-3a < 4096^-3`; the remaining comparison is rational and checked.
+
+## Certified counts and what they do not mean
+
+Let `L=(333/106)/(6932/10000)` and `U=(355/113)/(693/1000)`.
+Then `L < pi/log(2) < U`, and `log2(2.01)<101/100`. Define
+
+\[
+ d=L\alpha^2\sigma-101/100>0,\qquad
+ B=U\alpha^2 b_s^2/\theta,\qquad
+ n_p=\left\lceil(p+B)/d\right\rceil.
+\]
+
+The bound above implies **`||E^n_p|| < 2^-p`**. The verifier encloses
+pi by Machin's identity with alternating rational arctangent sums and
+log(2) by the positive series `2 atanh(1/3)`, including its tail. It
+does not use floating-point evaluations of a logarithm or exponential.
+
+For the inverse partial sum `S_n=sum_{k=0}^{n-1}(-E)^k`,
+`(I+E)S_n=I-(-E)^n`. Thus `n_p` certifies its **residual**, not by
+itself the same absolute inverse error. If the separately established
+`||E||<1/2` holds, then
+
+\[
+ \|(I+E)^{-1}-S_n\|\le2\|E^n\|.
+\]
+
+Use `n_(p+1)` to certify inverse error below `2^-p`. We retain this
+extra bit explicitly. Neither bound prices rounded evaluations of `E`,
+storage, setup, source access, restoration or tape movement. No modified
+resampling implementation, end-to-end running time or multiplication
+exponent is claimed. The algebraic operator bound holds for all `theta>0`;
+it does **not** enlarge the implemented chirp domain.
+
+`RESULT.json` separates three counts: the original corollary's simplified
+count, the old endpoint bound priced with the **same** rational decay `d`,
+and the new endpoint bound. Only the last comparison isolates the gain
+from this contribution. The original count is compared only within its
+stated `alpha^2 theta>=1, theta<1` domain.
+
+Exact examples from the receipt:
+
+| p | alpha | s,t | Old endpoint, same decay | New residual | New inverse, if norm < 1/2 |
+|---:|---:|---|---:|---:|---:|
+| 128 | 4 | 15,16 | 6 | 5 | 5 |
+| 1024 | 8 | 63,64 | 20 | 19 | 19 |
+| 4096 | 16 | 255,256 | 68 | 67 | 67 |
+
+## Counterexamples and finite evidence
+
+The prefactor cannot simply be deleted. At `s=4,t=5,j=2,h=1`, (1) has
+`X=1/2`, `sigma h^2=5/4`, endpoint contribution `-3/4`, and zero
+remainder. At `alpha=2`, this one positive term in row 2 of E exceeds
+`2.01 exp(-A sigma)`, because `exp(3A/4)>exp(9)>2.01`.
+This also refutes the claimed prefactor-free operator bound, not merely
+one intermediate inequality. The tuple has `theta=1/4` and
+`alpha^2 theta=1`, inside the implemented Gaussian parameter restriction.
+
+The residual/inverse distinction has a separate scalar counterexample:
+`E=-1/4`, `n=2`, gives residual `1/16` but inverse error `1/12`.
+It refutes the general inference from residual alone; this signed scalar
+is not asserted to be one of the positive Gaussian matrices.
+
+The finite audit enumerates all coprime `2<=s<=32, s<t<=3s`, all starting
+residues and nonzero steps in `[-4,4]`. A second path calculation uses only
+integer phase numerators and cross multiplication; it imports no predecessor
+routine and does not call the rational step identity. All increment words
+over `{-2,-1,1,2}` of lengths 1 through 4 are checked for six listed pairs,
+with 620 supplemental seed-62 paths of lengths up to 16. The finite count
+screen uses `p in {101,128,256,1024}`, integer `2<=alpha<=16`,
+`alpha^2<p`, and `alpha^-2<=theta<=1/4` on those coprime pairs.
+This fixed coverage is the stopping rule; it is not an exhaustive search
+over all Gaussian parameters. Universal claims rest on the proof above.
+
+## Reproduction, scope and credit
+
+From the repository root, Python 3.10+ with the standard library:
+
+```sh
+python -B research/gaussian-endpoint-potential-audit/verify.py
+python -B -m unittest discover -s research/gaussian-endpoint-potential-audit -p test_verify.py -v
+```
+
+The first command must print `PASS_GAUSSIAN_ENDPOINT_POTENTIAL` and match
+every field and JSON type of `RESULT.json`. Source drift fails before
+arithmetic. `--write NEW_PATH` creates a fresh receipt without overwriting
+an existing file. `SOURCES.json` pins the exact base, SHA256 and Git blob
+identities of all four inputs. `CLAIM.md` records the seed, alternatives,
+bounded overlap search and result. `VALIDATION.md` records executed checks.
+
+Base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. Selected conditional
+kappa: `1661634653669567/10^18`, unchanged. The selected PR799 construction,
+PR589 bit supplier and their all-size/compiler, common-label/mutable-source,
+hosting, precision/tape and analytic obligations are not independently
+replayed or discharged here. No formal proof-assistant result is claimed.
+
+Credit eumemic's PR5 (`d3d370c34937503bd3fa63c83d505a05e8e50893`) for the
+correction operator and potential argument, icekylinx for the retained
+shifted chirp error enclosure, and Harvey and van der Hoeven for the
+underlying Gaussian resampling algorithms. The exact audited derivative
+is the base's note, rather than an assertion that PR5 bytes are unchanged.
+Effy Elden's concurrent PR684 identifies the implemented Gaussian domain
+and audits windows/precision; it explicitly leaves Neumann evaluation
+outside its scope. Its PR description informed this scope comparison;
+no pending-PR source or certificate is imported. Packed-repair audits
+PR735/763/773 and signed-packing audits PR690/693 motivated choosing a
+different obligation. See the repository's existing NOTICE and LICENSE.
+
+The base ledger marks PR5 partially reviewed and PR371's separate
+final-grid-rounding proposal unreviewed. This package does not change
+either disposition or audit the rounded chirp implementation.
+
+Prepared for **Alan Grillo (@bg-grillo-alan)**, with substantial **OpenAI Codex assistance**
+in the derivation, code, verification and writing. One AI agent; no
+independent human review is claimed. New material is Apache-2.0.

research/gaussian-endpoint-potential-audit/RESULT.json

@@ -0,0 +1,61 @@
+{
+  "assignment_seed": 62,
+  "controls": 10,
+  "coprime_pairs": 646,
+  "count_cases": 3296,
+  "exact_paths": 9460,
+  "exact_steps": 112672,
+  "examples": [
+    {
+      "alpha": 2,
+      "burn": "1420000/78309",
+      "decay": "198848251/9184900",
+      "inverse_count_if_norm_below_half": 6,
+      "old_endpoint_same_decay_count": 6,
+      "original_corollary_count": 11,
+      "p": 101,
+      "residual_count": 6,
+      "s": 4,
+      "t": 5
+    },
+    {
+      "alpha": 4,
+      "burn": "7952000/33561",
+      "decay": "701123251/9184900",
+      "inverse_count_if_norm_below_half": 5,
+      "old_endpoint_same_decay_count": 6,
+      "original_corollary_count": 18,
+      "p": 128,
+      "residual_count": 5,
+      "s": 15,
+      "t": 16
+    },
+    {
+      "alpha": 8,
+      "burn": "21833920000/4933467",
+      "decay": "18879062757/64294300",
+      "inverse_count_if_norm_below_half": 19,
+      "old_endpoint_same_decay_count": 20,
+      "original_corollary_count": 68,
+      "p": 1024,
+      "residual_count": 19,
+      "s": 63,
+      "t": 64
+    },
+    {
+      "alpha": 16,
+      "burn": "293160704000/3993759",
+      "decay": "181704695267/156143300",
+      "inverse_count_if_norm_below_half": 67,
+      "old_endpoint_same_decay_count": 68,
+      "original_corollary_count": 260,
+      "p": 4096,
+      "residual_count": 67,
+      "s": 255,
+      "t": 256
+    }
+  ],
+  "pinned_files": 4,
+  "status": "SCOPED_EXACT_AUDIT_NO_NEW_KAPPA",
+  "strict_endpoint_only_count_savings": 1876
+}

research/gaussian-endpoint-potential-audit/SOURCES.json

@@ -0,0 +1,27 @@
+{
+  "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631",
+  "original_fast_gaussian_pr5": "d3d370c34937503bd3fa63c83d505a05e8e50893",
+  "upstream_openai_math": "adc7f1241b42e322a6451854ab7e4b4c146bf78a",
+  "files": [
+    {
+      "path": "notes/fast-gaussian-resampling.tex",
+      "sha256": "1a81e6b7f9228adace139ef891684db3a894e2a8b6f41b5234275627d25fe455",
+      "git_blob": "a102d214280181fe10fdbcd6343326e40b7849fa"
+    },
+    {
+      "path": "scripts/fast_gaussian.py",
+      "sha256": "11430c2df0783b933dc91080595bb7514bb052b8c7b12107e27a1ef701e31e43",
+      "git_blob": "f534b9e894381ddf301d8dda9d4a0f3cb9a2e249"
+    },
+    {
+      "path": "upstream/build/sections/07-resampling.tex",
+      "sha256": "8a6b91670f9163afb54892489fa2210c77fe1b058f0325ec7d18b44b94be6e2c",
+      "git_blob": "256243bf9416baefb82bf9203f80215b9ebe28f2"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "sha256": "9873519224e2db72d6a8c926f51e3e75129671e467948c6f6b03744f8bcfc699",
+      "git_blob": "1f107b55a2f045fa66d9c35d658b3b79549f5ba6"
+    }
+  ]
+}

research/gaussian-endpoint-potential-audit/VALIDATION.md

@@ -0,0 +1,67 @@
+# Verification handoff
+
+Status: scoped mathematical audit / analytic bound refinement, no new kappa.
+Base: `f567884aeb8851b6e794af1184119a3bfbe1e631`.
+Environment: Windows, CPython 3.14.5, standard library only.
+Executed 2026-10-13. No wall-time speedup or Linux/hosted-CI pass is claimed.
+
+## Completed checks
+
+- `python -B research/gaussian-endpoint-potential-audit/verify.py --write NEW_PATH`:
+  initial exact receipt generation passes. Four source files match both the
+  SHA256 manifest and their Git blobs at the exact base.
+- `python -O -B research/gaussian-endpoint-potential-audit/verify.py`:
+  exact receipt equality passes with assertions disabled. Code uses explicit
+  rejection checks rather than assertions.
+- `python -B -m unittest discover -s research/gaussian-endpoint-potential-audit -p test_verify.py -v`:
+  all eight test groups pass; the same command with `-O` also passes.
+- A minimal copy containing just this package and the four pinned source
+  files passes `python -I -B .../verify.py`, outside the repository in a
+  temporary path containing spaces. It reproduces the complete receipt.
+- `python -B scripts/verify_selected_result.py`: passes, selected conditional
+  kappa `1661634653669567/10^18` unchanged.
+- `python -B -m unittest discover -s tests -p test_selected_result.py -v`:
+  all five existing tests pass.
+- `git diff --cached --check`: passes. The only changed paths are the seven
+  files in this research package; the selected record and `upstream/` have
+  no diff. Remote main was rechecked before submission and still equals
+  the exact base above.
+
+The scientific receipt contains 646 coprime pairs, 112,672 exact single-step
+checks, 9,460 longer/supplemental path checks, and 3,296 parameter-count
+cases. In 1,876 count cases, the new endpoint bound needs strictly fewer
+terms than the old endpoint bound priced with the same decay estimate.
+This finite census does not claim a uniform frequency or an optimal count.
+
+Ten in-verifier controls comprise four mathematical rejection witnesses,
+one positive source tie-convention check and five rejected domain inputs.
+The unit tests additionally check exact formal matrix squares with wrapped
+nonzero steps, signed phase periodicity, corrupted independent arithmetic,
+changed/missing source files, receipt field removal/value/type corruption,
+and preservation of an existing output file. The polynomial matrix tests
+do not numerically approximate an infinite Gaussian sum.
+
+## Review and limits
+
+The written proof establishes the all-path inequality by an exact
+nonnegative remainder and a telescoping endpoint; it then bounds the
+positive infinite Gaussian sums. The finite interpreter and integer oracle
+provide independent implementation evidence, not proof-assistant verification.
+The inverse-tail guarantee explicitly requires `||E||<1/2` and one extra
+residual bit. The count refinement has no new supplier or complete rounded
+cost recurrence, so it does not support a new multiplication exponent.
+
+Full `make verify`, selected-supplier cold reconstruction and Lean were not
+run for these isolated additions. No generator, existing certificate,
+selected frontier or `upstream/` file is changed. The pending rounding
+proposal PR371 is outside this package; its ledger disposition is retained.
+
+Initial metadata checks covered open titles through PR898 and targeted
+all-state searches for the three candidate obligations. Final refresh
+covered arrivals through PR901 and an all-state Gaussian/potential search;
+no duplicate endpoint refinement was found in that bounded inspection.
+PR684's window/domain audit and PR5's original potential are explicitly
+credited. No pinned sprint coordination issue was available.
+
+Attribution: Alan Grillo (@bg-grillo-alan), with substantial OpenAI Codex
+assistance; see README for predecessors, licenses and exact source pins.