High-Order Singular-Series Averages, Random-Sieve Large Deviations, and Prime-Rich Intervals

Let \(MH,r\) be the average of the Hardy–Littlewood singular series over the \(r\)-element subsets of \([1,H]\), and put \(s=√log Hloglog H\). The manuscript proves unconditionally that \(MH,r=1+o(1)\) for \(r≤ exp(Σ_D(H)-q)\), where \(Σ_D(H)=(1+o(1))s\) and \(q\) tends to infinity, whereas \(MH,r\) tends to infinity uniformly for \(exp((√2+ε)s)≤ r≤ cH/log H\).For the normalized survivor count \(Q_H\) in the associated prime-modulus random sieve, the manuscript determines an exact branch of the survivor upper-tail rate function and a corresponding supercritical moment and free-energy limit. For actual primes, when \(H=λlog X\), it proves uniformly for \(λ≥1\) that\[#\{n≤ X:π(n+H)-π(n)≥ k\} Xexp(-k/(eλ))\]for \(1≤ k≤ c_0Hβ_*\), where \(β_*=0.313046…\). A density-dependent endpoint tends to \(exp(1-γ)/4\).The true singular-series transition constant, the optimal actual-prime endpoint, and the remainder of the survivor rate function remain open.The accompanying Python verification programs check finite identities, constants, and regression cases only. The Lean companion proves a limited collection of finite combinatorial and sieve statements. Neither the Python checks nor the Lean formalization prove the manuscript’s asymptotic analytic theorems or establish literature priority.This record contains the manuscript PDF, reproducible LaTeX source, bibliography, finite verification programs, verification receipts, and the limited Lean companion.