Reduce the effective interval onset to 2^751000000 (no κ)

research/smaller-interval-onset/CODE-SAFETY.md

@@ -0,0 +1,44 @@
+# Verifier bounds and inspection
+
+The verifier only checks the new rational gates and hashes its own package.
+It does not implement, import, fetch or replay the cited probability law.
+
+- Control flow has no recursion. Failed gates raise `ValueError`; file errors
+  propagate after the context manager closes the file.
+- The Taylor sum has five terms. The gate loop has thirteen entries, the
+  rejecting-control loop has two inputs, and the file loop has seven paths.
+  There are no unbounded searches, queues, subprocesses or network calls.
+- The exponent is bounded by `10^12` and is never used as a power exponent.
+  Computed powers have exponents at most 80. The supplied rational numerators
+  and denominators stay below 256 bits. Every file read is capped at 65537
+  bytes and rejects lengths above 65536. Files close before the next read.
+- Every function is below 60 physical lines. `require` calls enforce the
+  arithmetic conditions in both ordinary and optimized execution. All mutable
+  collections are local, and returned gate results and file bytes are used.
+- No dynamic code, decorators, registration or callback chain is introduced.
+  `sum`, the context manager and JSON encoding use normal Python dispatch.
+  Imported calls have explicit standard-library targets.
+- Registered checks enable warnings as errors. Development mode is also run
+  locally. The repository's existing package workflow runs both registered
+  normal and optimized commands. No shared workflow or analyzer is changed.
+
+## Managed-runtime deviation
+
+Rule: 3, fix memory capacity before steady operation.
+
+Location: `verify.py`, rational arithmetic, dictionaries and JSON output.
+
+Reason: CPython and `Fraction` allocate objects during arithmetic; they do not
+provide an allocation-free execution mode.
+
+Scope: one bounded verifier invocation, including seven bounded file reads.
+
+Compensating control: fixed loop sizes, bounded exact integers, a 64 KiB cap
+per file and sequential file lifetimes. No retained probability distribution
+or enormous onset integer is allocated.
+
+Verification: the two registered commands, the local development-mode run,
+and static inspection of the bounded domains above.
+
+Follow-up: reassess these bounds before adding inputs, adjustable numerical
+domains or another package file to the receipt inventory.

research/smaller-interval-onset/PROOF.md

@@ -0,0 +1,165 @@
+# A smaller effective interval onset
+
+This scoped proof is produced by Nick Petalas. It uses alephnan's
+[PR #6713](https://github.com/CrocSwap/integer-mult-bounds/pull/6713),
+`LOCAL_LIMIT.md` at `cd666f05c4e9006025b634687cc493911c8371c8`,
+as a mathematical premise. No predecessor verifier or convolution is replayed.
+
+## Premise and conclusion
+
+Use the notation of that source. The centered sum is `Z_n`, the centered
+Gaussian `G_n` has variance `nv`, and `c_sigma = sqrt(2*pi*v)`.
+For every integer `n >= 1296`, every real `x`, and every interval `I` with
+endpoints `x,x+b`, the source proves
+
+\[
+\begin{aligned}
+ \sqrt n\,|\Pr(Z_n\in I)-\Pr(G_n\in I)|&\le A_n+bB_n,\\
+ \left|\sqrt n\,\Pr(Z_n\in I)
+       -\frac{b e^{-x^2/(2nv)}}{c_\sigma}\right|
+   &\le A_n+bB_n+\frac{b^2}{4\sqrt n},
+\end{aligned}
+\]
+
+where
+
+\[
+ B_n=3/\sqrt n+\sqrt n\log n\,e^{-\sqrt n/320},
+ \qquad A_n=(1+4B_n)/\log n.
+\]
+
+These are its equations (1) and (2). They include every endpoint convention,
+singletons when `b=0`, and the empty interval. Their six hypotheses H,
+including `2 <= v <= 3`, and their classical analytic dependencies remain
+premises here. In particular `c_sigma < 5` follows from `v <= 3, pi < 4`.
+
+**New conclusion.** Put `K = 751000000`. For every integer `n >= 2^K`,
+every real `x`, and `0 <= b <= 5000`, both
+
+\[
+ c_\sigma\sqrt n\,|\Pr(Z_n\in I)-\Pr(G_n\in I)| <10^{-8}
+\]
+
+and
+
+\[
+ \left|c_\sigma\sqrt n\,\Pr(Z_n\in I)
+       -b e^{-x^2/(2nv)}\right|<10^{-8}
+\]
+
+hold with the same endpoint conventions. The source used `n >= 2^(10^12)`
+for these guarantees. Only this local onset is improved. The proof below
+also yields the sharper intermediate remainder coefficient `1025/1024`
+in place of the source's simplification to `2`.
+
+## Uniform remainder bound
+
+Write `w = log n`, and first suppose `w >= 60`. The larger source bound is
+
+\[
+ E(n,b)=\frac1w+
+ (b+4/w)\left(3e^{-w/2}+w e^{w/2}e^{-e^{w/2}/320}\right)
+ +\frac{b^2}4e^{-w/2}.
+\]
+
+For `0 <= b <= 5000`, we have `b+4/w < 5001` and
+
+\[
+ 3\cdot5001+5000^2/4=6265003<2^{23}.
+\]
+
+Consequently
+
+\[
+ E(n,b)<\frac1w+2^{23}e^{-w/2}
+              +5001w e^{w/2}e^{-e^{w/2}/320}.                 \tag{A}
+\]
+
+Multiply the two remainder terms by `w`. The first,
+`R_1(w)=2^23 w e^(-w/2)`, decreases on `[60,infinity)` because its
+logarithmic derivative is `1/w-1/2 < 0`.
+The positive Taylor terms through degree four give
+
+\[
+ e^3>1+3+9/2+27/6+81/24=131/8>16,
+\]
+
+so `e^30 > 2^40`. Therefore
+
+\[
+ R_1(w)\le R_1(60)<60/2^{17}<1/2048.                         \tag{B}
+\]
+
+The second is `R_2(w)=5001w^2 e^(w/2) exp(-e^(w/2)/320)`.
+Its logarithmic derivative is
+
+\[
+ 2/w+1/2-e^{w/2}/640
+ \le 2/60+1/2-2^{40}/640<0.
+\]
+
+Thus `R_2` also decreases. The function `u exp(-u/320)` decreases for
+`u>320`. Since `e^30>2^40>320`,
+
+\[
+ \begin{aligned}
+ R_2(w)&\le R_2(60)
+ <5001\cdot60^2\cdot2^{40} e^{-2^{40}/320}\\
+ &<2^{65}e^{-2^{31}}
+ <2^{65-2^{31}}<1/2048.                                    \tag{C}
+ \end{aligned}
+\]
+
+Here `5001*60^2 < 2^25`, `2^40/320 > 2^31`, and `e>2`
+justify the successive strict inequalities. All of these are small exact
+integer or rational comparisons. Combining (A), (B), and (C) proves
+
+\[
+ \boxed{E(n,b)<\frac{1025}{1024\log n}}
+ \quad(w\ge60,\ 0\le b\le5000).                            \tag{D}
+\]
+
+The smaller Gaussian-integral error obeys the same bound. No atomic-mass
+estimate or change of endpoint convention is introduced.
+
+## The new onset
+
+The positive series
+`log 2 = 2 sum_(j>=0) (1/3)^(2j+1)/(2j+1)` gives `log 2 > 2/3`.
+For `n >= 2^K`, therefore, `w > 2K/3 > 60` and `n > 1296`.
+Multiplying (D) by `c_sigma < 5` yields
+
+\[
+ c_\sigma E(n,b)
+ <\frac{5\cdot1025}{1024w}
+ <\frac{15375}{2048K}
+ <\frac1{10^8},
+\]
+
+because, exactly,
+
+\[
+ 2048\cdot751000000-15375\cdot10^8=548000000>0.
+\]
+
+This proves both stated conclusions. The old and new onset exponents obey
+`10^12 > 1331*K`; this compares exponents of symbolic integers, not runtime
+or measured practical performance. No power with either enormous exponent
+is constructed.
+
+## Scope and credit
+
+Alephnan retains credit for the effective interval inequalities, their
+Fourier argument and application to the complete historical flow. CubeJerry
+retains the fixed-height exponent result in PR #6329. The raw-p7 law and
+analytic lineage retain the credit recorded there, including zxv,
+Ryanson Jonathan / pinterbanget, DLamdata, Cinna Davis / 1337isnot1337,
+Jacob Alan Sussman, and Nick Petalas's earlier leaf results. Beurling,
+Selberg, Vaaler and Shou retain the classical approximation credit.
+
+The new contribution is the strict rational remainder budget and its smaller
+sufficient local onset. The original hypotheses and interval inequalities
+are cited, not independently proved or certified here. This written proof
+has not been checked by a proof kernel. It does not substitute the new onset
+into the full mixed-layer flow proof, improve its exponent, price a physical
+implementation, or discharge any selected framework assumption.

research/smaller-interval-onset/README.md

@@ -0,0 +1,68 @@
+# A smaller effective interval-local-limit onset
+
+Scoped proof produced by Nick Petalas. Assuming the interval error inequalities
+of alephnan's [PR #6713](https://github.com/CrocSwap/integer-mult-bounds/pull/6713)
+at `cd666f05c4e9006025b634687cc493911c8371c8`, the same uniform `10^-8`
+local-limit guarantee holds for
+
+```text
+n >= 2^751000000   instead of   n >= 2^(10^12).
+```
+
+This covers every interval of length at most 5000, every real location and
+every endpoint convention, for both the exact Gaussian integral and the
+left-endpoint Gaussian approximation. The exponents decrease by a factor
+greater than 1331. Neither enormous integer is materialized.
+
+[PROOF.md](PROOF.md) proves the new intermediate bound
+`E(n,b) < 1025/(1024 log n)` whenever `log n >= 60` and `0 <= b <= 5000`.
+The improvement comes from retaining a smaller bound for the two decaying
+remainders. It uses the predecessor's analytic inequalities as premises;
+no predecessor program, certificate or probability convolution executes.
+The source and exact hash are in [SOURCES.json](SOURCES.json).
+
+## Reproduction and evidence
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/smaller-interval-onset/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/smaller-interval-onset/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/smaller-interval-onset
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/smaller-interval-onset --check-source-history
+```
+
+Other hosts may substitute their CPython 3.12 executable. The verifier checks
+the exact rational gates in the new proof, rejects two insufficient onset
+certificates, and emits a generated receipt bound to every package file.
+Those rejecting controls concern this sufficient estimate; they are not
+counterexamples to the local-limit theorem at smaller depths. The universal
+conclusion rests on the written monotonicity argument and cited premises.
+
+## Limitations
+
+The onset remains impractical. This is a historical analytic side result,
+not a new kappa or a complete multiplication theorem. The six H hypotheses,
+source interval inequalities and classical analytic approximation remain
+mathematical inputs. No predecessor replay or independent audit is claimed.
+The complete flow majorant has not been rederived with this onset. No
+physical supplier, compiler, precision, ownership, tape or recovery obligation
+is discharged. The selected record and all five assumptions remain unchanged.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Propagate this smaller local onset through the complete fixed-height flow
+  proof. Begin by identifying every use of its original local-limit cutoff;
+  retain all mixed layers, boundary exits and terminal leaves.
+- Improve the error rate or remainder constant using the actual characteristic
+  function. A sharper spectral estimate could reduce the still enormous
+  sufficient onset much further.
+
+## Credit
+
+The new remainder estimate and onset are produced by Nick Petalas.
+Alephnan retains the effective interval-bound credit in PR #6713, and
+CubeJerry retains the fixed-height exponent theorem in PR #6329. The law,
+flow and analytic lineage, and the classical approximation credit, are
+listed in [PROOF.md](PROOF.md). Apache-2.0.

research/smaller-interval-onset/SOURCES.json

@@ -0,0 +1,29 @@
+{
+  "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"
+    }
+  ],
+  "external_mathematical_dependencies": [
+    {
+      "author": "alephnan",
+      "pr": 6713,
+      "commit": "cd666f05c4e9006025b634687cc493911c8371c8",
+      "path": "research/effective-direct-flow/LOCAL_LIMIT.md",
+      "url": "https://github.com/alephnan/integer-mult-bounds/blob/cd666f05c4e9006025b634687cc493911c8371c8/research/effective-direct-flow/LOCAL_LIMIT.md",
+      "sha256": "07702eabadefa4e2c435d6ea7e60c781aaa786fa875cab773a5962d8d2a2efe3",
+      "used": "Equations (1) and (2), the six H hypotheses and c_sigma < 5. These are cited premises. The verifier does not fetch, import or authenticate the external source; the hash identifies the inspected bytes. No foreign Git-history availability is asserted."
+    }
+  ]
+}