23 Local Shadow Kernels and the Finite-Prime Weil Kernel
From a research-front directive proposing the route: celestial Cutkosky positivity \(\to \) local shadow kernels \(\to \) finite-prime Weil kernel \(\to \) Casimir compression \(\to \) global Weil positivity \(\to \) RH. The final logical step (finite Weil paired-form positivity on all nontrivial zeros \(\iff \) RH) is already proved unconditionally in the Cesàro Regularization and the Weil Positivity Criterion chapter (GppWeilCriterion.rh_iff_weil_pairedForm_nonneg) — but that criterion is an abstract pairing over finite subsets of the actual (unknown) zero set, not the classical Weil explicit-formula prime-sum quadratic form this chapter’s kernels feed into. Bridging the two needs the classical explicit formula itself (a separate, substantial, not-in-Mathlib undertaking) and is not attempted here.
For every real \(p{\gt}1\) and every real \(t\): the finite-place shadow kernel \(K_p(t):=(1-p^{-1})/(1-2p^{-1/2}\cos (t\log p)+p^{-1})\) is strictly positive. This is the value of the classical Poisson kernel on the circle (radius \(r=p^{-1/2}\)), whose Fourier-coefficient sequence \((r^{|n|})_n\) is termwise nonnegative.
With \(C(t):=t/(4\sinh (2\pi t))\) the already-derived celestial cut kernel and \(H(t):=(t^2+1/4)\, C(t)\) the Casimir-weighted Archimedean kernel: \(H(t)\geq 0\) for every real \(t\). Proof: \(t\) and \(\sinh (2\pi t)\) always share sign, so their ratio is nonnegative (the \(t=0\) case is Lean’s total-division junk value \(0/0=0\), itself \(\geq 0\)).
Self-correction. An earlier pass of this chapter claimed, as its central finding, that no positivity-preserving projection from \(K_p\) to \(K_p-1\) exists at the single-prime level, based on a Toeplitz matrix of Fourier coefficients (indices = frequencies) found indefinite. That claim was wrong: it tested the wrong object. The question that matters is whether the Gram matrix \(M_{jk}=(K_p-1)(\theta _j-\theta _k)\), built from point evaluations at arbitrary finite angle configurations, is positive semidefinite — and it is, trivially: convolution by \(K_p\) is diagonal in the Fourier basis with eigenvalues \(r^{|n|}\geq 0\); the vacuum subtraction only zeroes the \(n=0\) eigenvalue, which cannot make the rest negative.
For any finite point configuration \(x:\mathrm{Fin}\, N\to \mathbb {R}\), weights \(c:\mathrm{Fin}\, N\to \mathbb {C}\), and frequency \(n\in \mathbb {Z}\): \(\sum _{j,k}\bar c_jc_ke^{in(x_j-x_k)}=\bigl|\sum _jc_je^{-inx_j}\bigr|^2\). Pure finite algebra, generalizing the pre-existing gram_square_nonneg (Convolution Squares chapter) to complex amplitudes.
For a finite set of frequencies \(F\subset \mathbb {Z}\) and real weights \(a:\mathbb {Z}\to \mathbb {R}\): \(\sum _{j,k}\bar c_jc_k\sum _{n\in F}a_ne^{in(x_j-x_k)} =\sum _{n\in F}a_n\bigl|\sum _jc_je^{-inx_j}\bigr|^2\), derived from Theorem 23.3 by pure finite-sum reordering.
With \(K^0_{r,N}(\theta ):=\sum _{0{\lt}|n|\le N}r^{|n|}e^{in\theta }\) the truncated, vacuum-excluded finite-place kernel: \(\sum _{j,k}\bar c_jc_kK^0_{r,N}(x_j-x_k)\geq 0\) for every truncation \(N\), every finite point configuration, and every \(0\le r\). Follows from Theorem 23.4 plus Finset.sum_nonneg, via the intermediate corollary gram_square_freqSum_nonneg.
Corrected central finding. \(K_p-1\) IS a positive kernel, prime-by-prime, unconditionally, at every finite truncation (Theorem 23.5). This reverses the earlier (wrong) claim. It does not by itself establish global positivity of the assembled sum \(Q_{\mathrm{GPP}}=Q_\infty +\sum _p Q_p\) — single-prime kernel positivity was never going to answer that on its own (the classical Weil explicit formula’s local prime terms are individually sign-indefinite in their usual normalization even though local \(K_p\) positivity holds).
Proof-engineering note. A first attempt at the corrected result proved the untruncated two-sided HasSum over all of \(\mathbb {Z}\) and built PositiveType\((K_r-1)\) on top of it as one monolithic theorem; both repeatedly hit elaboration timeouts even at 20\(\times \) the default heartbeat budget. Restructured into the small, independently-fast layers above (each builds in under 4 seconds standalone) after bisecting via isolated scratch-file tests. See docs/FORMALIZATION_PLAN.md and discovery/cutkosky_weil/notes.md for the full diagnosis.
With cutKernelExt the continuous extension of cutKernel replacing Lean’s junk value \(0/0=0\) at \(t=0\) by the genuine limit \(C(0)=1/(8\pi )\) (proved from Real.sinh’s derivative at \(0\), , not asserted), and \(H_{\mathrm{ext}}(t):=(t^2+1/4)\, C_{\mathrm{ext}}(t)\): \(H_{\mathrm{ext}}(0) =1/(32\pi )\) () and \(H_{\mathrm{ext}}(t)\geq 0\) for every real \(t\).
For every \(0\le r{\lt}1\): \(K_r-1\) is positive-type in the sense of GppHaarPositivityWeil.PositiveType — for every finite point configuration and weights, \(\sum _{j,k}\bar c_jc_k(K_r-1)(x_j-x_k)\geq 0\) — for the genuine, untruncated kernel, not merely at finite truncation. Obtained from Theorem 23.5 by passing to the limit \(N\to \infty \): the two-sided Fourier series \(K_r(\theta )-1=\sum _{n\ne 0}r^{|n|}e^{in\theta }\) is established as a genuine HasSum () via Summable built from the geometric tail bound (not by tracking HasSum values through Int.rec, which is what had timed out); \(K^0_{r,N}\to K_r-1\) follows (); and positivity passes to the limit via ge_of_tendsto.
Fourth pass, following review: both items the third pass had deferred are now proved. The route for the \(N\to \infty \) passage separates convergence (built from the geometric tail bound via Summable.of_nat_of_neg) from the Gram-square algebra (already proved, unchanged, at finite truncation) — exactly as specified, rather than reviving the timed-out monolithic construction. 16 theorems total in CutkoskyWeilBridge.lean now, all kernel-clean.
On \(\mathrm{Ell2Z}:=\ell ^2(\mathbb {Z},\mathbb {C})\), the natural Fourier-coefficient model (Parseval-dual to the circle: convolution by a kernel becomes diagonal multiplication by its Fourier coefficients), let \(C_{K_r}\), \(P_0\), \(C_{K_r-1}\) be the bounded diagonal ContinuousLinearMaps with Fourier symbols \(r^{|n|}\); \(0\) at \(n=0\) and \(1\) elsewhere (the vacuum-deleting projection); and \(0\) at \(n=0\), \(r^{|n|}\) elsewhere, respectively. Then \(C_{K_r-1}=P_0\, C_{K_r}\, P_0\) as genuine bounded-operator composition (), for every \(0\le r{\lt}1\).
\(\langle x,C_{K_r-1}x\rangle \ge 0\) for every \(x\in \mathrm{Ell2Z}\) and every \(0\le r{\lt}1\), as a direct corollary of the general fact that a bounded diagonal operator with nonnegative-real-part Fourier symbol is positive semidefinite (), applied to \(C_{K_r-1}\)’s already-known eigenvalue signs (\(0\) at \(n=0\), \(r^{|n|}\ge 0\) elsewhere).
Fourth pass, following review: both items the third pass had deferred are now proved. The route for the \(N\to \infty \) passage separates convergence (built from the geometric tail bound via Summable.of_nat_of_neg) from the Gram-square algebra (already proved, unchanged, at finite truncation) — exactly as specified, rather than reviving the timed-out monolithic construction. 16 theorems total in CutkoskyWeilBridge.lean at that point, all kernel-clean.
Fifth pass, following a further review directive. Item 1 of a six-item program (the actual operator statement, not the finite Fourier identity again) is now DONE in full: Theorems 23.8 and 23.9 above, 8 new theorems, kernel-clean. Checking GppWeilCriterion.rh_iff_weil_pairedForm_nonneg’s actual statement found that theorem’s pairedForm is a zero-indexed reflection pairing over the (unknown) zero set itself — it carries no prime, Mellin, or Haar-measure content for a “finite-prime Weil kernel in this normalization” to mean, a mismatch this file’s own module doc had already flagged. The genuine classical target, GppHaarPositivityWeil.weil_criterion (\(D_k=\sum _\rho \hat\Omega (\rho )+\text{local terms}\)), remains a full True-stub, honestly blocked on Tate’s thesis and idèle class groups (neither in Mathlib). But the classical elementary (non-adelic) explicit formula’s finite-prime local term has a clean checked closed form: with \(\zeta _p(s):=(1-p^{-s})^{-1}\) the local Euler factor, \(W_p(t)=2\operatorname {Re}(-\zeta _p'/ \zeta _p(1/2+it))\) exactly — checked by hand, not yet formalized, the honest next Lean target. 24 theorems total in CutkoskyWeilBridge.lean now, all kernel-clean.
Sixth pass (2026-08-23). Attacking the bridge from the already-proved local kernel positivity to the classical Weil explicit formula’s finite-prime term directly.
With \(\zeta _p(s):=(1-\exp (-s\log p))^{-1}\) the local Euler factor as a genuine function of \(s\in \mathbb {C}\) (via Complex.exp, in EulerFactorLogDeriv.lean), \(\zeta _p\) has derivative \(-\bigl(\text{minusLogDerivZetaP}\, p\, s\bigr)\cdot \zeta _p(s)\) at every \(s\) with \(1-p^{-s}\ne 0\), where \(\text{minusLogDerivZetaP}\, p\, s:=\log (p)\cdot p^{-s}/(1-p^{-s})\) — i.e. this closed form genuinely is \(-\zeta _p'/\zeta _p\), from an actual HasDerivAt chain-rule computation through Complex.exp and HasDerivAt.inv, not asserted from the geometric-series shortcut.
Honest boundary, this pass. The connection back to \(W_p\) — \(W_p(p,t) = 2\operatorname {Re}(\text{minusLogDerivZetaP}\, p\, (1/2+it))\) — is checked by hand and numerically to 40 digits (four primes, three \(t\) values each) but not yet formalized: the Complex.cpow exponent-splitting algebra (\(p^{-(1/2+it)}=p^{-1/2}\cdot p^{-it}\)) needs more care than this pass affords without iterative feedback on this large a file.
Seventh pass (2026-08-23). The boundary above is now closed.
For every prime-like real \(p{\gt}1\) and real \(t\), \(W_p(p,t) = 2\operatorname {Re}(\text{minusLogDerivZetaP}\, p\, (1/2+it))\) exactly — i.e. \(W_p(p,t)=2\operatorname {Re}(-\zeta _p'/\zeta _p(1/2+it))\), genuinely proved rather than checked numerically. The proof computes both sides’ real and imaginary parts directly (Complex.exp_re/exp_im, Complex.div_re, Complex.normSq_apply) rather than manipulating cpow splittings, closing with the classical Poisson-kernel identity KrClosed_sub_one_eq_two_mul_re: for real \(r,\theta \) with \(0\le r{\lt}1\), \(K_r(\theta )-1 = 2\operatorname {Re}[re^{i\theta }/(1-re^{i\theta })]\). The \(r{\lt}1\) hypothesis is genuinely needed, not merely convenient: at \(r=1,\theta =0\) the denominator \(1-re^{i\theta }\) vanishes and Lean’s total division sends the two sides to different junk values, so the identity is false without it — this matches exactly the one case that ever arises (\(r=p^{-1/2}{\lt}1\) for \(p{\gt}1\)).
Together with Theorem 23.10, the full chain \(W_p(p,t) = 2\operatorname {Re}(-\zeta _p'/\zeta _p(1/2+it))\) is now proved end to end in Lean: the derivative computation is genuine complex analysis, and the connection to \(W_p\) is genuine real/imaginary-part algebra, not an asserted numerical coincidence. This does not touch the decisive-question finding below — the sign obstruction is unaffected by this formalization, since it concerns how \(W_p\) enters the classical explicit formula, not whether \(W_p\) equals this log-derivative expression.
The decisive question, answered. Does the already-proved positive-type property of \(W_p\)’s kernel help establish the sign the classical Weil explicit formula’s prime term actually needs? Verified by direct computation against real nontrivial zeta zeros (mpmath.zetazero, not from a half-remembered convention): with an even Gaussian test function \(h(r)=e^{-ar^2}\) and \(g(u)=\tfrac 1{2\pi }\int h(r)e^{-iru}\, dr\), Weil’s explicit formula
balances to \(\sim 10^{-10}\) against 60 real zeros, pinning the sign convention exactly: the prime sum enters with an overall minus sign. Its summand is exactly \(-2\sum _p\sum _m\log (p)p^{-m/2}g(m\log p)\) — literally minus a quantity built from the same Poisson-kernel structure \(W_p\) already proved positive-type. Local \(W_p\)/\(K_p-1\) positivity therefore does not make the prime sum’s contribution to the Weil quadratic form \(Q(f)\) nonnegative — it makes that contribution nonpositive. A real, checked, negative finding, recorded rather than glossed over: any actual RH-equivalent positivity of \(Q(f)\) must come from the Archimedean term dominating this genuinely negative prime pull, not from same-signed local pieces stacking up. This does not contradict anything already proved (Kp_pos, H_nonneg, and the positive-type kernel theorems all still hold exactly); it identifies precisely which direction that positivity pushes once correctly signed into the classical formula. See discovery/cutkosky_weil/notes.md and verify_weil_explicit_formula_sign.py for the full derivation and script.
Honest boundary (updated). Still not formalized in Lean: the exact Fourier pair \(H(t)\leftrightarrow G(x)=\tfrac {3}{512\pi }\operatorname {sech}^4(x/4)\) (confirmed numerically to \(\sim 10^{-51}\) relative error); the pole-cancellation/removable-singularity claim at \(t=\pm i/2\) (a different, complex-analytic singularity from the real-axis one at \(t=0\) closed in the fourth pass — confirmed via a shrinking-perturbation sequence); the representation-theoretic Casimir operator itself (the \(t^2+1/4\) eigenvalue is used only as a number, not derived from an operator — Mathlib has no \(SL(2,\mathbb {R})\) principal-series development); the \(W_p\leftrightarrow -\zeta _p'/\zeta _p\) connection is now CLOSED (Theorem 23.11, seventh pass); the classical explicit formula itself (contour integration of \(\zeta '/\zeta \), the argument principle) and the adelic Tate’s-thesis route, both large separate undertakings; and the \(Q_{\mathrm{GPP}}\) construction / global positivity factorization program — now known, per the decisive- question finding above, to need the Archimedean term to dominate a genuinely negative prime contribution, not to assemble from same-signed pieces. No axiom, no sorry, no RH claim, no global positivity claim, no Connes–Consani machinery imported.