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.

Proved clean:

• \(\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).