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, honestly parked).
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 \(1/(4\cosh ^2(x/2))\): \(P(\lambda ) = \int _{-\infty }^{\infty } e^{i\lambda x}/(4\cosh ^2(x/2))\, \dd x\). Genuinely attempted and confirmed out of reach this session, not merely assumed hard: direct grep of the pinned Mathlib source (v4.19.0) shows zero occurrences of sech anywhere, no closed-form Fourier transform outside the Gaussian family, no Poisson-kernel \(1/(1{+}x^2)\) closed form, and no residue-calculus API (the textbook proof is a residue sum over \(\mathrm{sech}^2\)’s double poles at \(x=i\pi (2k{+}1)\)). Parked as GppLogisticFourierPair.logistic_fourier_pair : True := trivial in QuantumGravity/LogisticFourierPair.lean, per this repository’s own documented convention for honestly recording an open gap — not an axiom, not a sorry.
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.