Talks

Quantum information theory is the study of the how features of quantum mechanics can be used to do useful `information processing' tasks - things like run a computation, communicate, or hide information. While this theory was developed for these practical goals, it also finds many applications in theoretical physics. I'll introduce quantum information theory and discuss how it comes into the study of fundamental physics. 

Learn more about Alex and his work here. 

Higher-curvature gravity can offer UV completions of GR, but generically suffers from 4th-order propagating degrees of freedom often spoiling unitarity, e.g. Stelle gravity. Recently it was noticed that “Einsteinian gravities” allow for higher curvature interactions match Einstein’s spectrum at the linearised level, avoiding the dangerous 4th-order propagating degrees of freedom. We investigate the renormalisation group flow of Einstein cubic gravity couplings and identify the entire phase diagram of the theory, showing that Einstein cubic gravity remains ghost-free in the quantum regime. To tackle questions of unitarity and causality directly, we make a Lorentzian computation of the asymptotically safe graviton propagators of the transverse-traceless and scalar mode. We showed that beyond the requirement of using a causality-preserving regulator, such as Callan-Symanzik, setting up differential equations for coupled spectral functions must satisfy additional constraints related to diffeomorphism and BRST symmetry. We found three avenues to solve the coupled system of running Kallen-Lehmann spectral representations, leading to 1-loop exact spectral functions which are compatible with causality and unitarity. Furthermore, they provide the first direct asymptotically safe predictions to the full quantum propagators, the corresponding Weyl-tensor and Ricci-scalar form factors in the quantum effective action.

The Generalized Quantum Stein's Lemma is a theorem in quantum hypothesis testing that provides an operational meaning to the relative entropy within the context of quantum resource theories. Its original proof was found to have a gap, which led to a search for a corrected proof. We formalize the proof presented in [Hayashi and Yamasaki (2024)] in the Lean interactive theorem prover. This is the most technically demanding theorem in physics with a computer-verified proof to date, building with a variety of intermediate results from topology, analysis, and operator algebra. In the process, we rectified minor imprecisions in [HY24]'s proof that formalization forces us to confront, and refine a more precise definition of quantum resource theory. Formalizing this theorem has ensured that our Lean-QuantumInfo library, which otherwise has begun to encompass a variety of topics from quantum information, includes a robust foundation suitable for a larger collaborative program of formalizing quantum theory more broadly.

We derive a cutting rule for equal-time in-in correlators, including cosmological correlators based on Keldysh r/a basis, which decomposes diagrams into fully retarded functions and cut-propagators consisting of Wightman functions. Our derivation relies only on basic assumptions such as unitarity, locality, and the causal structure of the in-in formalism. We apply the cutting rule to simplify the extraction of non-local cosmological collider signals, and prove the absence of one-loop scale-invariant corrections from enhanced small-scale perturbations to superhorizon curvature and tensor perturbations.