7 Celestial Holography
7.1 Shadow Discontinuity = Loop Integrand
The discontinuity of a celestial amplitude across the shadow cut \(z \mapsto \bar{z}\) (i.e., \(\Delta \mapsto 2-\bar\Delta \)) equals the loop integrand, replacing Feynman diagrams with analytic continuation.
Correction, re-audited 2026-08-15: the cited declaration GppShadowDisc.shadow_discontinuity is a theorem foo : True := trivial stub, not a proof of the statement above. The four “proved clean” facts below it are real, kernel-checked theorems in ShadowDiscontinuity.lean — but they are elementary complex-analysis/algebra lemmas the main claim would use as ingredients, not a proof of the claim itself. See Section 7.2 for the concrete topology-level advance on this thread and the precise remaining analytic gap.
Proved clean (as standalone lemmas, not as a proof of the boxed claim above):
\(\mathrm{Disc}\, f(x) = 2i\, \mathrm{Im}\, f(x)\) (basic complex analysis).
Shadow is an involution: \(2-(2-s)=s\).
Shadow equals conjugate on principal series \(\Delta = 1+i\lambda \).
Residue at simple pole: algebraic identity.
Gap: celestial amplitude theory, unitarity cut equations, celestial OPE (not in Mathlib 4.19.0). Tracked honestly as three named stubs, celestial_amplitude_has_cut, disc_equals_loop_integrand, shadow_disc_mellin_density — none discharged by this chapter.
7.2 Tree-to-Loop Topology (Shadow-Pair Sewing)
From Toupin, Loop Integrands Hidden in Trees: Explicit Extraction by Double Shadow Discontinuities (Aug. 2026). The paper’s central claim: a higher-point tree celestial correlator’s shadow-pole analytic structure already encodes a lower-point loop integrand, extractable by a double shadow discontinuity. This section covers the graph-theoretic layer of that claim, formalized in GppTreeLoopSewing.lean — unconditional, no axiom, no sorry — and states precisely what remains open.
For a connected cubic tree with \(n = 4+2L\) external leaves (\(V_T = n-2\) trivalent vertices, \(I_T = n-3\) internal edges), sewing \(L\) disjoint pairs among the designated \(2L\) extra leaves leaves \(4\) external legs and \(I = I_T + L = 3L+1\) internal edges, with cycle rank \(\beta _1 = I - V_T + 1 = L\). Proved for all \(L\) by direct computation on the vertex/edge counts (omega); no combinatorial machinery beyond arithmetic is needed since only the counts, not an explicit graph object, are formalized here.
At \(L=1\): the open six-point cubic tree (4 vertices, 3 internal edges) with one pair sewing gives 4 external legs, 4 internal edges, cycle rank 1 — the one-loop box topology.
With \(D(x) := Q(x)\) the propagator-denominator function, the closed box denominator \(Q(\ell )\, Q(\ell -p_1)\, Q(\ell -p_1-p_2)\, Q(\ell +p_4)\) is literally the missing closure edge \(Q(\ell )\) times the three denominators already present in the open six-point chain. A definitional identity once the open-chain object is named.
A structure with fields doubleDisc (tree \(\to \) pair shadow discontinuity), inverseMellin, closePair (the same closure described directly in momentum space), and a field sewing_identity asserting inverseMellin(doubleDisc T a b) = closePair T a b. This is the paper’s own boxed “remaining analytic theorem” (\(\mathcal M^{-1}_{5,6}[\mathrm{dDisc}_{\rm sh}^{(56)}\widetilde T_6] = \tfrac {i}{\ell ^2+i0}T_6(\ell ,p_1,\dots ,-\ell )\)), stated here as a local hypothesis rather than a global axiom or an unnamed gap. Nothing in this file proves sewing_identity for an explicit six-point celestial amplitude, and it is not claimed to be proved. ShadowPairSewing.tree_to_loop_extraction is the (structurally trivial) corollary that the extraction pipeline commutes, conditional on this one named hypothesis.
Fix a celestial null 4-vector \(q(x,y) = (1+x^2+y^2,\, 2x,\, 2y,\, 1-x^2-y^2)\) (the real Lorentzian slice \(\bar z = z^*\), \(z=x+iy\)) and the frame legs \(p_1=(-E,0,0,E)\), \(p_2=(-E,0,0,-E)\), \(p_4=(E,-E\sin \theta ,0,-E\cos \theta )\). Writing \(A := 2q{\cdot }p_1\), \(A' := 2q{\cdot }p_2\), \(B := 2q{\cdot }(p_1{+}p_2)\), \(C := 2q{\cdot }p_4\): \(A = -4E\) identically (no \(z\)-dependence), \(A' = -4E|z|^2 \le 0\), \(B = -4E(1+|z|^2) {\lt} 0\) for \(E{\gt}0\), and \(C\) clears its \((1-\cos \theta )\) factor to an exact sum of two squares, hence \(C \ge 0\) for \(\cos \theta {\lt} 1\) (i.e. \(t \ne 0\)). Consequently, for any physical t-channel threshold \(B''{\gt}0\) and any point with \(C \ne 0\) (away from the collinear point), the two tied-leg sewing coefficients \(-1/(2ACB)\) and \(-1/(2A'CB'')\) have a nonpositive product — they are never both nonnegative and never both nonpositive. This is the exact algebraic content behind the numerical finding (checked at 39/39 structured and 666/666 random kinematic points, zero exceptions, in discovery/shadow_ope/sign_opposition_sweep.py) that the tied-leg discontinuities \(\mathrm{Sewn}_s\), \(\mathrm{Sewn}_t\) always carry opposite-sign imaginary parts. Pure real algebra and elementary geometry: no Mellin transforms, no complex analysis, no Legendre functions.
Honest boundary. What is proved: the graph-combinatorial topology count (Theorem 7.2), its one-loop specialization (Corollary 7.3), the denominator bookkeeping (Lemma 7.4), and the sewing sign-opposition fact (Theorem 7.6) — all unconditional. What is not proved, and is isolated rather than hidden: the analytic celestial-sewing identity (Definition 7.5), which requires an explicit six-point celestial tree amplitude computation the paper itself states has not yet been carried out, and the Sokhotski-Plemelj discontinuity construction itself (the actual \(\mathrm{Sewn}_s\), \(\mathrm{Sewn}_t\), their \(\lambda \)-integral closed forms, and any comparison to the box integral), which remains exploratory Python in discovery/, not formalized. This section does not discharge, and does not claim to discharge, disc_equals_loop_integrand or the other two stubs in Theorem 7.1.
7.3 Loops from Cuts (canonical replacement series)
Daniel has designated Loops_from_Cuts_in_Celestial_Holography.tex et al. as the canonical replacement for the shadow-discontinuity framing above: loop integrands arise from an ordinary two-particle unitarity cut on the celestial sphere, not a residue at a shadow pole. See the Quantum Gravity — Blackbody Law chapter for the spectral-weight theorems already landed from this series; this section covers the loop paper’s own most novel link, the cut geometry itself.
For the null celestial momentum direction \(q(x,y) = (1{+}x^2{+}y^2,\, 2x,\, 2y,\, 1{-}x^2{-}y^2)\) (metric \((+,-,-,-)\); \(\langle q(x,y),q(x,y)\rangle =0\) identically, for every \(x,y\)) and every \((x_5,y_5)\ne (0,0)\), \(M\in \R \), writing \(r^2:=x_5^2+y_5^2\),
the resulting momenta satisfy \(\omega _5\, q(x_5,y_5) + \omega _6\, q(x_6,y_6) = (M,0,0,0)\) componentwise. Proved clean: ‘Loops_from_Cuts_in_Celestial_Holography.tex‘, Theorem "Cut geometry: antipodal pairing and uniform measure" (‘thm:measure‘) — the algebraic core of the paper’s own claimed solution, verified here by direct vector computation (‘field_simp‘/‘ring‘ on each of the four components after ‘fin_cases‘), independent of and prior to any measure-theoretic argument. Not attempted: uniqueness of this solution (a separate fact about the orbit structure of null directions on the two-sphere), and the phase-space measure reduction itself, \(\dd \Pi _2 = \dd ^2z/[8\pi ^2(1{+}|z|^2)^2]\), \(\int \dd \Pi _2=1/(8\pi )\) — this needs genuine \(\delta ^4\)-constrained pushforward-measure and Jacobian machinery this repository has not built, and is left open as the natural next step of this thread.
For \(0{\lt}s{\lt}1\),
Proved clean: the Beta-reflection integral underlying Loops_from_Cuts_in_Celestial_Holography.tex’s dispersion-relation reconstruction (thm:disp, thm:celdisp), whose Mellin kernel \(\int _0^\infty S^{\sigma -1}/(s'{+}S)\, \dd S = s'^{\sigma -1}\pi /\sin (\pi \sigma )\) reduces, via \(S=s'u\), to the base case \(\int _0^\infty u^{\sigma -1}/(1{+}u)\, \dd u=\pi /\sin (\pi \sigma )\) — a “second Euler Beta integral” on \((0,\infty )\) confirmed absent from Mathlib v4.19.0 by direct grep (only the \((0,1)\) form, Complex.betaIntegral, exists). This theorem is Complex.betaIntegral s (1-s) unfolded to its defining real interval integral and evaluated via Complex.Gamma_mul_Gamma_eq_betaIntegral combined with the reflection formula Complex.Gamma_mul_Gamma_one_sub, cast down to \(\R \) via Complex.ofReal_cpow (valid uniformly on \(x\in [0,1]\), both endpoints included) and intervalIntegral.integral_ofReal. Not attempted: the substitution \(x=t/(1{+}t)\) mapping \((0,1)\leftrightarrow (0,\infty )\) needed to reach the paper’s actual \((0,\infty )\) dispersion kernel — the natural tool is MeasureTheory.integral_image_eq_integral_abs_deriv_smul with a fresh \(\mathrm{Ioo}\, 0\, 1\to \mathrm{Ioi}\, 0\) diffeomorphism, genuine new infrastructure this repository has not built (the algebra was checked by hand, not yet coded), left open as the well-scoped next step.
Logistic Fourier pair (item 3 of 3).
Modular_Thermality_of_the_Celestial_Spectral_Weight.tex and Spectral_Weight_from_Principal_Series.tex also characterize \(P(\lambda )\) (already proved in closed hyperbolic form, \(P(\lambda )=\pi \lambda /\sinh (\pi \lambda )\), in Theorem 17.7) as the Fourier transform of the logistic density.
For every real \(\lambda \neq 0\),
\(\int _{-\infty }^{\infty } \frac{\dd x}{4\cosh ^2(x/2)} = 1\), matching \(P(0)=1\).
The route. Substituting the logistic distribution function \(u = 1/(1+e^{-x})\) turns the weight into \(\dd u\) and the character \(e^{i\lambda x}\) into \(u^{i\lambda }(1-u)^{-i\lambda }\), so the integral is the Beta integral \(B(1+i\lambda ,\, 1-i\lambda ) = \Gamma (1+i\lambda )\, \Gamma (1-i\lambda )\), and Euler’s reflection formula gives \(\pi \lambda /\sinh (\pi \lambda )\).
Why this sat as a stub. From 2026-08 until 2026-09-26 this was a True-stub recorded as out of reach: the pinned Mathlib (v4.19.0) had no sech, no closed-form Fourier transform beyond the Gaussian, no Poisson-kernel pair, and no residue calculus. That census was accurate — sech still has zero occurrences at v4.33.1 — but it listed the tools of the textbook residue proof without asking whether another proof needed them. The Beta route uses none of them.
What this does not give. The First Moment Theorem needs the inverse direction, \(\frac{1}{2\pi }\int P(\lambda )\cos (\lambda y)\, \dd \lambda = 1/(4\cosh ^2(y/2))\). That follows by Fourier inversion and is not proved here.
7.4 Dispersion Reconstruction: the Mechanism Behind sewing_identity
From a fresh session (2026-08-17) attacking Definition 7.5’s open hypothesis head-on. DispersionReconstruction.lean proves the general, physics-convention-independent complex-analysis mechanism — the algebraic core of the Sokhotski–Plemelj formula — by which a discontinuity across a real pole determines the meromorphic function having that pole. This is not a celestial calculation: it is the classical dispersion-relation fact \(F(z) = \tfrac {1}{2\pi i}\int _\R [\mathrm{Disc}\, F(x)]/(x-z)\, dx\) that Theorem 7.1’s own Step 6 invokes (via cut-constructibility) without deriving.
For real \(z_0,\varepsilon ,x\) with \(\varepsilon \neq 0\), \(\dfrac {1}{(x-z_0)+i\varepsilon } - \dfrac {1}{(x-z_0)-i\varepsilon } = \dfrac {-2i\varepsilon }{(x-z_0)^2+\varepsilon ^2}\), exactly, with no limiting procedure — the finite-\(\varepsilon \) content of “the jump of a regulated simple pole is a Lorentzian kernel.”
Away from \(x=z_0\), the Lorentzian kernel \(\varepsilon /((x-z_0)^2+\varepsilon ^2)\) tends to \(0\) as \(\varepsilon \to 0^+\) — the rigorous, non-distributional half of “the regulated jump concentrates at the pole.” The complementary mass statement \(\int _\R \varepsilon /((x-z_0)^2+\varepsilon ^2)\, dx = \pi \) for every \(\varepsilon {\gt}0\) (a standard Cauchy/Poisson-kernel fact, reducible to Mathlib’s integral_univ_inv_one_add_sq by the affine substitution \(x=z_0+\varepsilon u\)) is numerically certified in verify_dispersion.py but not additionally formalized this session — the substitution needs a translation-invariance-of-Lebesgue-measure lemma not chased down; named honestly as a gap rather than forced.
What this does and does not establish about sewing_identity. These two theorems make precise which three analytic facts about the actual six-point celestial tree would let sewing_identity be derived rather than assumed, via the classical dispersion relation (valid for \(F\) meromorphic off the real axis with a single real simple pole and suitable decay — Titchmarsh, Theory of Functions, Ch. 5): (H1) Meromorphy — after the \(\ell \)-space completeness/inverse-Mellin integral of \(\mathrm{dDisc}_{\rm sh}^{(56)}\widetilde T_6\), the result is meromorphic in \(\ell ^2\) with its only singularity a simple pole at \(\ell ^2=0\); (H2) Decay — that function vanishes at infinity fast enough for the dispersion contour to close; (H3) Residue match — the discontinuity computed via the shadow-pair OPE (the existing Steps 1–5 of Theorem 7.1) has, at \(\ell ^2=0\), exactly the residue \(-2\pi i\cdot T_6(\ell ,p_1,\dots ,p_4,-\ell )\) required. None of (H1)–(H3) is established here for the actual \((z,\bar z)\)-dependent celestial six-point amplitude — that is exactly the open boundary every paper in this program already names. What is new is that the mechanism (Sokhotski–Plemelj) is now a proved fact in this tree instead of an implicit citation, and the remaining gap is three named, checkable analytic properties of \(G_6^{\rm tree}\) instead of one opaque hypothesis. This section does not discharge sewing_identity or touch any GppShadowDisc stub.