GPPVerify: Lean 4 Formalization of the Shadow Framework

21 Local-Field Shadow Kernels

From Daniel Toupin’s “Local-field shadow kernels, celestial unitarity, and the adelic principal series” (2026) — a new research front investigating whether celestial Cutkosky unitarity, 1D Mellin/shadow harmonic analysis, and adelic PGL(2) harmonic analysis share a common rank-one local-to-global structure. Not an RH proof; not evidence toward RH. Full honest boundary, including the paper’s own open research problems, in discovery/local_field_shadow/local_shadow_kernel_notes.md.

Theorem 21.1 Archimedean Shadow Reflection
#

For the Archimedean shadow kernel \(K_{\infty ,d}(a) := \Gamma (a)\Gamma (d-a)/\Gamma (d)\): \(K_{\infty ,d}(a) = K_{\infty ,d}(d-a)\).

Theorem 21.2 Principal-Series Positivity

On the principal series \(a=d/2+it\): \(K_{\infty ,d}(a) = |\Gamma (d/2+it)|^2/\Gamma (d)\), positive whenever \(d{\gt}0\). Shadow reflection becomes Hermitian conjugation exactly on this line, via \(d-a=\overline{a}\).

Theorem 21.3 Diagonal Conformal Lift
#

The diagonal lift \(D(s):=(s,s)\) of a scalar 1D weight has \(\Delta (D(s))=2s\) and spin \(J(D(s))=0\).

Theorem 21.4 Shadow Compatibility
#

\(D(1-s) = \mathrm{Shadow}_2(D(s))\): the 1D shadow \(s\mapsto 1-s\) and the 2D celestial shadow \((h,\bar h)\mapsto (1-h,1-\bar h)\) intertwine exactly under the diagonal lift.

21.1 The \(d=2\) Cut vs. the Spherical Weyl Coefficient

The naive conjecture that a single local factor \(a_\infty (s)\) gives both the physical kernel \(C_\infty =a_\infty (s)a_\infty (1-s)\) and the normalized Weyl/Gindikin–Karpelevich intertwiner \(M_\infty =a_\infty (1-s)/a_\infty (s)\) is false — confirmed numerically not proportional at the Archimedean place and not equal at finite places (2026-08-22 resolution). The failure is informative: the physical kernel and the Weyl coefficient are distinct canonical objects on the same rank-one principal series. What is true is the exact decomposition below.

Theorem 21.5 Legendre Duplication for the Archimedean Factors

With \(\Gamma _R(s):=\pi ^{-s/2}\Gamma (s/2)\) and \(\Gamma _C(s):=2(2\pi )^{-s}\Gamma (s)\): \(\Gamma _C(s) = \Gamma _R(s)\Gamma _R(s+1)\), for every complex \(s\).

Theorem 21.6 The Celestial Cut as Two Archimedean Sectors

\(K_{\infty ,2}(\Delta ) = \pi ^2\Gamma _C(\Delta )\Gamma _C(2-\Delta ) = \pi ^2\cdot \Gamma _R(\Delta )\Gamma _R(\Delta +1)\cdot \Gamma _R(2-\Delta )\Gamma _R(3-\Delta )\) — the celestial \(d=2\) cut decomposes exactly into two shadow-paired real Archimedean Gamma sectors, \((\Gamma _R(\Delta ),\Gamma _R(2-\Delta ))\) and its shift \((\Gamma _R(\Delta +1),\Gamma _R(3-\Delta ))\).

21.2 The Global Eisenstein Coefficient

Theorem 21.7 Celestial-Shadow Form of the Eisenstein Coefficient

With \(\Lambda \) the completed Riemann zeta function and \(\varphi (\Delta ):=\Lambda (\Delta -1)/\Lambda (\Delta )\): \(\varphi (\Delta ) = \Lambda (2-\Delta )/\Lambda (\Delta )\) — immediate from \(\Lambda (1-w)=\Lambda (w)\).

Theorem 21.8 Eisenstein Reflection
#

\(\varphi (2-\Delta )\varphi (\Delta ) = 1\) wherever \(\Lambda (\Delta )\neq 0\) and \(\Lambda (2-\Delta )\neq 0\). This is not evidence toward RH: Eisenstein scattering already contains \(\zeta (s)\) in its functional-equation normalization without that proving anything about its zeros.

Honest boundary. The integral representation of \(K_{\infty ,d}\) is taken as a definition (verified numerically against direct quadrature, not derived from Mathlib’s \([0,1]\)-Beta integral). Not formalized at all: the non-Archimedean kernel \(K_{q,d}\) (Mathlib has no \(p\)-adic multiplicative Haar measure infrastructure), the deeper representation- theoretic reason the physical kernel and Weyl intertwiner are distinct (beyond the numerical confirmation that they are), the Cutkosky-vs-Rankin-Selberg local bridge, the \(\mathbb {R}_+\) dilation/Mellin principal-series skeleton as an actual Lean object, and \(|\varphi (1+i\lambda )|=1\) (needs \(\Lambda \)’s conjugation symmetry, not directly in Mathlib). All are the paper’s own genuinely open research targets, not bookkeeping — see the notes file for the precise statement of each.