19 Thread HT — Prime–Archimedean Heat Trace (Elementary Layer)
From arithmetic_principal_series_RH_program34.tex (the BPY prime–Archimedean spectral program). That paper reformulates RH as a zero-independent statement: with \(m_*(u) = \tfrac {1}{2\sqrt{1+u}}(\xi '/\xi )(\tfrac 12+\sqrt{1+u})\), \(\mathcal{W}=\nu _\infty -\nu _p\) the completed prime–Archimedean boundary distribution, and \(\mathcal{K}(t)=(4\pi t)^{-1/2}\langle \mathcal{W},e^{-(\cdot )^2/(4t)}\rangle \), subordination of the massive resolvent gives \(m_*(u)=\int _0^\infty e^{-(1+u)t}\mathcal{K}(t)\, dt\), and the paper’s heat-trace criterion states \(\mathrm{RH} \iff \mathcal{K}\) is completely monotone on \((0,\infty )\).
This chapter covers the elementary, kernel-checkable layer of that chain: the arithmetic and Laplace-transform bookkeeping. Two genuinely hard inputs (Bernstein/Hausdorff–Widder for the criterion itself, and the digamma piece of the Archimedean Laplace transform) are named and not claimed here — see the honest-boundary note at the end of this chapter.
19.1 Complete Monotonicity and Laplace Bookkeeping
\(f\) is completely monotone on \((0,\infty )\) if \((-1)^n f^{(n)}(t) \geq 0\) for all \(n\) and all \(t{\gt}0\). Absent from Mathlib at the pinned commit c44e0c8 — no Bernstein/Hausdorff–Widder theory exists upstream.
\(t \mapsto e^{-at}\) is completely monotone for \(a \geq 0\). In the paper’s notation this is one term of \(\mathcal{K}(t)=\sum _{\gamma {\gt}0} m_\gamma e^{-\gamma ^2 t}\).
\(\int _0^\infty e^{-ct}\, dt = 1/c\) for \(c{\gt}0\).
\(\int _0^\infty e^{-(1+u)t}e^{-\gamma ^2 t}\, dt = 1/(u+1+\gamma ^2)\). The paper’s displayed step converting the Hadamard partial-fraction sum into the heat expansion, by uniqueness of the Laplace transform.
19.2 Subordination
\(\int _0^\infty e^{-r^2t}(4\pi t)^{-1/2}\, dt = 1/(2r)\) for \(r{\gt}0\). The \(x=0\) case of the paper’s boxed identity \(e^{-rx}/(2r) = \int _0^\infty e^{-r^2t}(4\pi t)^{-1/2}e^{-x^2/(4t)}\, dt\).
For \(a,b{\gt}0\): \(\int _0^\infty t^{-1/2}e^{-at-b/t}\, dt = \sqrt{\pi /a}\, e^{-2\sqrt{ab}}\). This is a genuine \(K_{1/2}\) Bessel evaluation, confirmed absent from Mathlib entirely at the pin, proved here without any Bessel-function machinery: the substitution \(t=(\sqrt{b}/\sqrt{a})w^2\) reduces it to an auxiliary integral \(\kappa (c) := \int _0^\infty e^{-c(w^2+w^{-2})}\, dw\); the \(w\mapsto 1/w\) symmetry of the integrand doubles it to \(2\kappa (c)=\int _0^\infty (1+w^{-2})e^{-c(w^2+w^{-2})}\, dw\); the substitution \(p=w-1/w\) — a bijection \((0,\infty )\to \mathbb {R}\) whose derivative is exactly the weight \(1+w^{-2}\) — turns this into a two-sided Gaussian integral, closed by Real.integral_gaussian. This is the general-\(x\) instance of the paper’s boxed subordination formula, in full.
19.3 Bridge to Thread L, and the Archimedean Laplace Transform
\(\sum _{n\geq 2}\Lambda (n)n^{-1/2}e^{-(\log n)^2/(4t)}\) is exactly one half of GppWeilLadder.primeSide evaluated at the heat Gaussian \(x\mapsto e^{-x^2/(4t)}\), since that test function is even. Consequence: the whole support-ladder toolkit of WeilSupportLadder.lean applies verbatim to the heat trace’s prime side — the two threads are the same object.
For \(r{\gt}-1/2\): \(\int _0^\infty (e^{-rx}-e^{-x})e^{-x/2}\, dx = 1/(r+1/2)-2/3\).
For \(r{\gt}1/2\): \(\int _0^\infty (e^{-rx}-e^{-x})e^{x/2}\, dx = 1/(r-1/2)-2\). Together with Lemma 19.8, these are the two purely elementary pieces of the paper’s Archimedean Laplace transform \(A_\infty (r)\); the remaining digamma piece is not formalized here. (Mathlib now supports a real digamma function \(\psi =\Gamma '/\Gamma \) via GppDigamma.digamma — see the QG-Blackbody chapter — but the specific Gauss integral representation of \(\psi \) at general \(r\) this lemma would need is a further step not yet established, distinct from the special values and functional equation already proved.) \(A_\infty \) itself is not assembled in this file.
19.4 Honest Boundary
Not claimed in this chapter: Bernstein’s theorem / the Hausdorff–Widder characterization of completely monotone functions as Laplace transforms of positive measures (needed for the heat-trace criterion itself, still absent from Mathlib at the pin), the digamma integral representation at general \(r\) (needed to assemble the full Archimedean Laplace transform \(A_\infty \) — see the QG-Blackbody chapter for what is now available), and the heat-trace criterion RH \(\iff \mathcal{K}\) completely monotone, as a single theorem. Nothing in this chapter proves or assumes RH.