All missions

Motivation

At high energies ($s\gg -t$, the Regge limit) scattering amplitudes of gauge theories simplify and organise into towers of logarithms $\log|s/t|$. For the four-gluon amplitude of $\mathcal N=4$ super-Yang–Mills theory with gauge group $SU(N)$, the colour structure is what makes the nonplanar (subleading in $1/N$) amplitude hard to control. Naculich (2020) builds a basis of colour factors $C_{ik}$ adapted to the Regge limit at every loop order, writes the $\ell$-loop amplitude in that basis, and uses one of its coefficients, $B^{(\ell)}_{\ell\ell}$, to motivate a conjectured all-loop relation with the Regge limit of the $\mathcal N=8$ supergravity four-graviton amplitude. The physics conjecture itself is not a mathematical statement; what is exact and checkable is the colour algebra underlying it — finite-dimensional linear algebra over polynomials in $N$.

Setting

Trace basis. Four-gluon colour factors are expanded in six single and double traces $c[1],\dots,c[6]$ of fundamental generators (eq. (2.1)). A colour vector is a column $v=(v_1,\dots,v_6)$ of polynomials in $N$, with complex coefficients.

Colour operators. The $t$-channel Casimir $\mathbf T_t^2$ and the crossing-odd combination $\mathbf T_{s-u}^2=\tfrac12(\mathbf T_s^2-\mathbf T_u^2)$ act on colour vectors as the explicit $6\times6$ matrices of eq. (4.15) (entries in $\mathbb Z[\tfrac12][N]$). The tree-level $t$-channel colour factor is $C_{00}=c[1]-c[3]$. Crossing (exchange of legs 2 and 3) is the permutation $P$: $c[1]\leftrightarrow c[3]$, $c[4]\leftrightarrow c[6]$.

Regge colour factors. With $[A,B]=AB-BA$,

$$C_{ii}=(\mathbf T_{s-u}^2)^iC_{00},\qquad C_{i1}=[\mathbf T_t^2,[\mathbf T_t^2,\dots,[\mathbf T_t^2,\mathbf T_{s-u}^2]\cdots]]C_{00},\qquad C_{i,i-1}=[\mathbf T_{s-u}^2,\dots,[\mathbf T_{s-u}^2,[\mathbf T_t^2,\mathbf T_{s-u}^2]]\cdots]C_{00},$$

each with exactly $i$ operators. The admissible pairs are $(0,0)$, $(1,1)$, $(2,1),(2,2)$ and $(i,1),(i,i-1),(i,i)$ for $i\ge3$.

Extended trace basis. At $\ell$ loops, $t^{(\ell)}_{\lambda+6k}=N^{\ell-2k}c[\lambda]$ for $\lambda=1,2,3$ and $N^{\ell-2k-1}c[\lambda]$ for $\lambda=4,5,6$, giving $3\ell+3$ elements (eq. (2.3)). The colour-ordered amplitudes $A^{(\ell)}_\lambda$ of an amplitude are its coordinates in this basis (eq. (2.4)).

Regge-basis amplitude. Eq. (4.24):

$$\mathcal A^{(\ell)}=A_1^{(0)}\tilde a^\ell\sum_{i=0}^{\ell}\sum_{k}B^{(\ell)}_{ik}\,N^{\ell-i}C_{ik}.$$

Null vectors. Four vectors per loop order $\ell\ge2$ (eqs. (2.10), (2.12), extended by prepending zeros) encode the $SU(N)$ group-theory relations among the $A^{(\ell)}_\lambda$.

Formalization targets

Goal: the all-loop coefficient $B^{(\ell)}_{\ell\ell}$ (eqs. (4.26)–(4.27))

For every even $\ell$,

$$A_1^{(0)}\tilde a^\ell\,B^{(\ell)}_{\ell\ell}=\frac{1}{2\cdot3^{\ell/2}}\Big(A^{(\ell)}_{3\ell+1}-A^{(\ell)}_{3\ell+3}\Big),$$

and for $\ell=1$, $A_1^{(0)}\tilde a\,B^{(1)}_{11}=-(A^{(1)}_1+A^{(1)}_3)$. The paper obtains the even-$\ell$ formula by guessing from explicit results through $\ell=9$; a proof for all $\ell$ is not given there.

Milestones

1. $\mathbf T_t^2C_{00}=NC_{00}$ (eqs. (4.2), (4.7)).
2. Crossing parity: $P\mathbf T_t^2P=\mathbf T_t^2$, $P\mathbf T_{s-u}^2P=-\mathbf T_{s-u}^2$, $PC_{00}=-C_{00}$ (eqs. (3.7), (4.7)).
3. Signature: $PC_{ik}=(-1)^{k+1}C_{ik}$ for every admissible $(i,k)$ (Sec. 4.4).
4. $N^{\ell-i}C_{ik}$ expands in $t^{(\ell)}_1,\dots,t^{(\ell)}_{3\ell+3}$ (eqs. (2.3), (4.24)).
5. Explicit components through three loops (eqs. (4.16), (4.20)).
6. Explicit coefficients $B^{(2)}_{ik}$, $B^{(3)}_{ik}$ (eqs. (4.18), (4.22)).
7. The Regge colour factors satisfy the four null-vector constraints and have no $t^{(\ell)}_2$ component, for all $\ell\ge2$.
8. The Regge colour factors are linearly independent, and for $\ell\ge2$ span all constrained Regge-limit amplitudes (the "basis" claim of Sec. 4).

Significance

The result. Eq. (4.26) is the input to the paper's analysis of the infrared behaviour of $B^{(\ell)}_{\ell\ell}$ (at most $1/\epsilon^\ell$, manifest for even $\ell$ because only most-subleading-colour amplitudes appear), and hence to the conjectured all-orders relation between $B^{(\ell)}_{\ell\ell}$ and the Regge limit of $\mathcal N=8$ supergravity (Sec. 6). An all-$\ell$ proof replaces an extrapolation from nine loop orders by a theorem.

Formalizing it. The low-loop tables (4.16), (4.20), (4.18), (4.22) are finite computations; the goal and milestones 3, 4, 7, 8 are statements for every loop order and need genuine arguments (induction on $\ell$, structure of the operators on the extended basis).

Difficulty

The coefficient $B^{(\ell)}_{\ell\ell}$ is defined through the whole $(3\ell-2)$-element basis: a formula for it must vanish on every other $N^{\ell-i}C_{ik}$, including the nested commutators $C_{i1}$ and $C_{i,i-1}$ whose components grow in complexity with $i$. Checking the formula loop order by loop order does not give a proof; one needs to control how $\mathbf T_t^2$ and $\mathbf T_{s-u}^2$ act on the two most-subleading slots of the extended basis uniformly in $\ell$.

Formalization scope

• Colour vectors are Fin 6 → ℂ[X], with $N$ the polynomial variable X; operators are Matrix (Fin 6) (Fin 6) ℂ[X] acting by Matrix.mulVec. Coefficients $B_{ik}$ and the prefactor $\kappa=A_1^{(0)}\tilde a^\ell$ are arbitrary complex numbers; $B$ is a function ℕ × ℕ → ℂ of which only the admissible pairs matter.
• Extended-basis indices $\lambda$ are 1-based natural numbers, $1\le\lambda\le3\ell+3$; the coordinate function returns $0$ outside this range. The colour-ordered amplitudes are defined as the coordinates of $\kappa\sum B_{ik}N^{\ell-i}C_{ik}$, so the goal says: whatever the coefficients, the stated combination of coordinates returns $\kappa B_{\ell\ell}$. This is equivalent to the paper's reading for amplitudes lying in the span of the Regge basis (milestone 8).
• The odd-$\ell$ formula (4.28) for $\ell>1$ is not included. It agrees with the model at $\ell=3$ (it is the $B_{33}$ line of eq. (4.22)), but an exploratory exact-rational computation (not machine-checked) found that at $\ell=5$ no linear combination of the six amplitudes $A_{3\ell-8},A_{3\ell-6},A_{3\ell-5},A_{3\ell-3},A_{3\ell-2},A_{3\ell}$ reproduces $B^{(5)}_{55}$ in this model. Including it would risk a false milestone.
• Local checks of the statements used Lean v4.28.0 with Mathlib; only standard Mathlib API (polynomials, matrices, LinearIndependent, finite sums) is used.
• Welcome contributions: lemmas describing $\mathbf T_t^2$ and $\mathbf T_{s-u}^2$ as operators on extended-basis coordinates (shift of $N$-degree), and general tools for iterated commutators.

Selected references

• S. G. Naculich, All-loop-orders relation between Regge limits of $\mathcal N=4$ SYM and $\mathcal N=8$ supergravity four-point amplitudes, arXiv:2012.00030 (2020), https://arxiv.org/abs/2012.00030.

Motivation

In 1997 Maldacena conjectured that $\mathcal N=4$ super-Yang–Mills theory with gauge group $U(N)$ is equivalent to type IIB string theory on $\mathrm{AdS}_5\times S^5$ (hep-th/9711200). The paper of Gubser, Klebanov and Polyakov (hep-th/9802109), together with Witten's paper of the same year (hep-th/9802150), turned the conjecture into a computational rule: the generating functional of connected gauge theory correlators equals the minimum of the supergravity action subject to boundary conditions at the edge of anti-de Sitter space. The concrete outputs of the paper are two-point functions and operator dimensions, read off from the small-momentum, non-analytic behaviour of solutions of a radial ordinary differential equation.

The mathematical core is classical analysis of modified Bessel functions: which solution is regular in the throat, how $K_\nu$ splits into $I_{\pm\nu}$, and what the leading non-analytic term of a logarithmic derivative is as the momentum tends to zero. The physical headline, Eq. (46), is that operators dual to massive string states at level $n$ acquire dimensions growing like $2(n\,g_{YM}\sqrt{2N})^{1/2}$ at large 't Hooft coupling.

Setting

Let $R>0$ be the AdS radius and $z>0$ the radial coordinate, with the boundary at $z=R$ and the horizon at $z=\infty$. For a bulk field $\phi(x,z)=e^{ik\cdot x}\tilde f_k(z)$ with Euclidean momentum $k>0$, the radial equation is

$$(\mathcal D_{k,\mu}f)(z)\;=\;z^3\,\partial_z\!\left(z^{-3}\partial_z f\right)-k^2 f-\frac{\mu}{z^2}\,f\;=\;0,$$

with $\mu=0$ for the massless s-wave (Eq. (20)), $\mu=l(l+4)$ for the $l$-th partial wave (Eq. (34)), and $\mu=(mR)^2$ for a scalar string state of mass $m$ (Eq. (40)).

The modified Bessel functions are defined for $x>0$ and real $\nu$ by

$$K_\nu(x)=\int_0^\infty e^{-x\cosh t}\cosh(\nu t)\,dt,\qquad I_\nu(x)=\sum_{j\ge0}\frac{(x/2)^{2j+\nu}}{j!\,\Gamma(j+\nu+1)}.$$

The normalised radial profile is $\tilde f_k(z)=z^2K_\nu(kz)/(R^2K_\nu(kR))$, the flux factor is $\mathcal F(k)=\big[z^{-3}\partial_z\log\tilde f_k(z)\big]_{z=R}$, and the two-point function is $\langle O(k)O(q)\rangle=(2\pi)^4\delta^4(k+q)\,\tfrac{N^2}{16\pi^2}\mathcal F(k)$ (Eq. (26)). For a level-$n$ string state $m^2=4n/\alpha'$, $R^4=2Ng_{YM}^2\alpha'^2$, the Bessel order is $\nu=\sqrt{4+(mR)^2}$ (Eq. (41)) and the dimension of the dual operator is $\Delta=2+\nu$ (Eq. (45)).

Formalization targets

Goal (Eqs. (41)–(46))

For $n\ge1$, $N,g_{YM},\alpha',m,R>0$ with $m^2=4n/\alpha'$, $R^4=2Ng_{YM}^2\alpha'^2$ and $\nu=\sqrt{4+(mR)^2}\notin\mathbb Z$: there is a function $A$ real-analytic at $0$ with

$$\frac{N^2}{16\pi^2}\mathcal F(k)=A(k^2)-\frac{N^2}{8\pi^2}\frac{\Gamma(1-\nu)}{\Gamma(\nu)}\Big(\frac{kR}{2}\Big)^{2\nu}R^{-4}+o(k^{2\nu})\quad(k\to0^+),$$

$\Delta=2+\nu=2+\sqrt{4+4n\,g_{YM}\sqrt{2N}}$, and $\Delta\big/\big(2(n\,g\sqrt{2N})^{1/2}\big)\to1$ as $g\to\infty$.

Milestones

Solutions of the radial equation (Eqs. (22), (35), (39)–(41)), regularity selecting $K_\nu$ (text after (23)), the connection formula $K_\nu=\frac{\pi}{2\sin\pi\nu}(I_{-\nu}-I_\nu)$ (Eq. (42)), the flux factor for integer order (Eqs. (36)–(37)) and non-integer order (Eqs. (43)–(44)), the relation $(mR)^2=4ng_{YM}\sqrt{2N}$ (Eq. (41)) and the asymptotics (45)–(46).

Significance

The computation is the prototype of the AdS/CFT dictionary between bulk masses and boundary dimensions, $\Delta(\Delta-4)=(mR)^2$ in five bulk dimensions. The massless case reproduces the non-renormalisation of dimensions of operators dual to supergravity fields; the massive case is the first prediction that unprotected operators acquire dimensions growing without bound at strong coupling.

The mathematical statements are classical, but their formalisation needs modified Bessel functions of real order, their connection formula, and asymptotic expansions near $0$ with logarithmic terms — material not currently present in Mathlib as far as the drafter checked. None of the statements below has a machine-checked proof yet.

Corrections to the source. Numerical exploration by the drafter (not machine-checked) indicates that the sign of the logarithmic coefficient printed in Eqs. (36)–(37) is reversed (the standard expansion has $(-1)^{n+1}\log(x/2)\,I_n(x)$ in $K_n(x)$), and that Eq. (27) is inconsistent with Eq. (37) at $l=0$: the correct leading term for $l=0$ is $-\tfrac14k^4\log(kR)=-\tfrac18k^4\log(k^2R^2)$. The partial-wave milestone is stated with the corrected coefficient. Eq. (44) (non-integer order), which carries the paper's main prediction, agrees with the standard expansions.

Difficulty

The flux factor is a logarithmic derivative of $K_\nu$ evaluated at the boundary. The leading term of $K_\nu$ near $0$ is a pure power, which contributes only an analytic part; the physical information sits in a subleading term of relative size $k^{2\nu}$ (or $k^{2l+4}\log k$ for integer order). Extracting it requires the full series structure of $K_\nu$ near $0$, not only its leading asymptotics, together with control of the remainder uniformly enough to pass through a logarithm and a derivative.

Formalization scope

All functions are real-valued; $K_\nu$ is defined by its integral representation and $I_\nu$ by its power series, both used only for $x>0$. The convention $1/\Gamma(\text{pole})=0$ is realised by Lean's $1/0=0$. "An analytic function of $k^2$ plus a term plus $o(\cdot)$" is encoded as: there exists $A$ with AnalyticAt ℝ A 0 such that the difference is little-$o$ of the given power as $k\to0^+$. Because $2\nu$ is not an even integer when $\nu\notin\mathbb Z$ (and because of the logarithm in the integer case), the coefficient of the leading non-analytic term is uniquely determined, so the statements are not vacuous. The physics steps (the identification of generating functionals, Eq. (12), and the Fourier transform to position space) are not formalised: the two-point function is defined through the flux factor, Eq. (26). Welcome contributions: general facts about $K_\nu$ and $I_\nu$ (differential equation, positivity, asymptotics, series near $0$), reusable beyond this mission.

Selected references

• S.S. Gubser, I.R. Klebanov, A.M. Polyakov, Gauge theory correlators from non-critical string theory, Phys. Lett. B 428 (1998) 105–114. https://arxiv.org/abs/hep-th/9802109
• J. Maldacena, The large N limit of superconformal field theories and supergravity, Adv. Theor. Math. Phys. 2 (1998) 231. https://arxiv.org/abs/hep-th/9711200
• E. Witten, Anti de Sitter space and holography, Adv. Theor. Math. Phys. 2 (1998) 253. https://arxiv.org/abs/hep-th/9802150
• NIST Digital Library of Mathematical Functions, Chapter 10 (Bessel functions). https://dlmf.nist.gov/10

Motivation

In February 1998 Witten's paper Anti de Sitter Space and Holography made precise Maldacena's proposal that large-$N$ conformal field theories in $d$ dimensions are described by gravity on $(d+1)$-dimensional anti de Sitter space $\mathrm{AdS}_{d+1}$. The dictionary it proposes identifies boundary values of bulk fields with sources of boundary operators, and reads correlation functions off the dependence of the bulk action on those boundary values. Its most quoted quantitative consequence is the mass–dimension relation: a scalar of mass $m$ on $\mathrm{AdS}_{d+1}$ corresponds to a boundary operator of conformal dimension

$$\Delta=\tfrac12\big(d+\sqrt{d^2+4m^2}\big),\qquad \Delta(\Delta-d)=m^2 .$$

Behind this physics statement sits a piece of classical analysis on hyperbolic space: the Dirichlet-type problem for the operator $\Delta_g-m^2$ with prescribed boundary asymptotics, solved by an explicit Poisson-type integral (Section 2 of the paper, eqs. (2.15)–(2.44)). This mission formalizes that analytic core.

Timeline. Maldacena 1997 (hep-th/9711200) conjectured the correspondence; Gubser–Klebanov–Polyakov (hep-th/9802109) and Witten (hep-th/9802150, both February 1998) proposed the precise dictionary; the Euclidean black-hole thermodynamics used in Section 3 goes back to Hawking–Page 1983.

Setting

Euclidean $\mathrm{AdS}_{d+1}$ is modelled as the upper half space $\{(x_0,x): x_0>0,\ x\in\mathbb R^d\}$ with the hyperbolic metric

$$ds^2=\frac{1}{x_0^2}\Big(dx_0^2+\sum_{i=1}^d dx_i^2\Big)\qquad\text{(eq. (2.15))}.$$

Its Laplace–Beltrami operator is

$$\Delta_g u=x_0^{d+1}\partial_0\big(x_0^{1-d}\partial_0 u\big)+x_0^2\sum_{j=1}^d\partial_j^2u = x_0^2\Big(\partial_0^2u+\sum_j\partial_j^2u\Big)-(d-1)x_0\,\partial_0u .$$

A massive scalar of squared mass $m^2\in\mathbb R$ solves $\Delta_g u=m^2u$ (eqs. (2.34), (2.37)). The conformal dimension is $\Delta=\tfrac12(d+\sqrt{d^2+4m^2})$ (eq. (2.44)), the bulk-to-boundary kernel is

$$K_\Delta(x_0,x)=\frac{x_0^{\Delta}}{(x_0^2+|x|^2)^{\Delta}}\qquad\text{(eqs. (2.19), (2.38))},$$

and the Poisson-type integral of a boundary datum $\varphi_0$ is $\int_{\mathbb R^d}K_\Delta(x_0,x-x')\,\varphi_0(x')\,dx'$ (eqs. (2.20), (2.41)).

Formalization targets

Goal (eq. (2.41) with (2.43)–(2.44))

For $m^2>-d^2/4$ there is a constant $c>0$ such that for every bounded continuous $\varphi_0$ on $\mathbb R^d$,

$$\varphi(x_0,x)=c\int_{\mathbb R^d}\frac{x_0^{\Delta}}{(x_0^2+|x-x'|^2)^{\Delta}}\,\varphi_0(x')\,dx'$$

is a $C^2$ solution of $\Delta_g\varphi=m^2\varphi$ on the upper half space and $x_0^{\Delta-d}\,\varphi(x_0,x)\to\varphi_0(x)$ as $x_0\to0^+$, i.e. $\varphi\sim x_0^{d-\Delta}\varphi_0$ at the boundary (eq. (2.36) with $f=x_0$).

Milestones

1. $x_0^{\Delta}$ solves the massive equation when $\Delta(\Delta-d)=m^2$ (eqs. (2.16)–(2.17), (2.37)).
2. The inverted kernel $K_\Delta$ solves it too (eqs. (2.18)–(2.19), (2.38)).
3. Scaling: $\int x_0^{2\Delta-d}(x_0^2+|x|^2)^{-\Delta}dx$ is independent of $x_0$ (eq. (2.40)).
4. Approximate identity: these kernels tend to a multiple of $\delta(x)$ (eq. (2.39)).
5. The massless case $\Delta=d$ with $\varphi\to\varphi_0$ (eq. (2.20)).
6. $\Delta=\tfrac12(d+\sqrt{d^2+4m^2})$ is the larger root of $\Delta(\Delta-d)=m^2$ (eqs. (2.43)–(2.44)).
7. The gauge-field profile $x_0^{d-2}$ solves the reduced Maxwell equation (eqs. (2.24)–(2.25)).
8. Hawking–Page, $d=3$: $\beta(r_+)=12\pi r_+/(1+3r_+^2)$ has a maximum and $I(r_+)=\pi r_+^2(1-r_+^2)/(1+3r_+^2)$ is negative for large $r_+$ (eqs. (3.15)–(3.16)).

Significance

The goal is the analytic statement underlying the mass–dimension relation $\Delta(\Delta-d)=m^2$ of the AdS/CFT dictionary: it shows that the boundary datum $\varphi_0$ of a massive field is naturally a density of weight $d-\Delta$, which is how the paper identifies the dimension of the dual operator. The same kernel is the starting point for the two-point function (2.42). The result is classical mathematics (scattering theory on hyperbolic space), proved informally in the paper; this mission produces a machine-checked version together with reusable infrastructure for the hyperbolic Laplacian in half-space coordinates.

Difficulty

The pointwise identities (milestones 1, 2, 6, 7, 8) are calculus. The substance is analytic: differentiating the Poisson-type integral twice under the integral sign with only boundedness of $\varphi_0$, and proving the approximate-identity limit with the right normalisation; the scaling integral requires $\Delta>d/2$, and the endpoint $m^2=-d^2/4$ (where $\Delta=d/2$ and the kernel is not integrable) must be excluded.

Formalization scope

Points are pairs $(x_0,x)\in\mathbb R\times\mathrm{EuclideanSpace}\ \mathbb R\ (\mathrm{Fin}\ d)$; partial derivatives are one-variable derivs, so the solution predicate also demands $C^2$ regularity on $\{x_0>0\}$, which rules out junk values of deriv. Real powers are Real.rpow; integrals are Bochner integrals for Lebesgue measure. Boundary data are bounded continuous functions. All declarations live in the namespace WittenAdSHolography, with the shared definitions in one definition file.

Selected references

• E. Witten, Anti de Sitter Space and Holography, Adv. Theor. Math. Phys. 2 (1998) 253–291. https://arxiv.org/abs/hep-th/9802150
• J. Maldacena, The Large N Limit of Superconformal Field Theories and Supergravity, Adv. Theor. Math. Phys. 2 (1998) 231–252. https://arxiv.org/abs/hep-th/9711200
• S. S. Gubser, I. R. Klebanov, A. M. Polyakov, Gauge Theory Correlators from Non-Critical String Theory, Phys. Lett. B 428 (1998) 105–114. https://arxiv.org/abs/hep-th/9802109
• S. W. Hawking, D. N. Page, Thermodynamics of Black Holes in Anti-de Sitter Space, Commun. Math. Phys. 87 (1983) 577–588. https://doi.org/10.1007/BF01208266

Motivation

A coupling constant is the number that fixes the strength of an interaction: in the modern formulation it is the parameter weighting the interaction part of a Lagrangian against its kinetic part. In a quantum field theory such a parameter is not constant. Probing a process at a higher energy resolves more of the virtual activity that dresses the interaction, and the value one measures depends on the energy scale $\mu$ at which the measurement is made. This scale dependence is called the running of the coupling, and it is the organising phenomenon behind two of the best-known qualitative facts about the Standard Model: the electromagnetic coupling grows with energy ($\alpha \approx 1/137$ at low energy, $\alpha \approx 1/127$ at the $Z$ mass, about 90 GeV) and apparently diverges at a finite energy — the Landau pole — while the strong coupling decreases logarithmically at high energy, the asymptotic freedom found by Gross, Politzer and Wilczek and recognised by the 2004 Nobel Prize.

The source treats the running through the beta function, defined there by

$$\beta(g) \;=\; \mu\,\frac{\partial g}{\partial \mu} \;=\; \frac{\partial g}{\partial \ln \mu},$$

and through the one-loop strong coupling

$$\alpha_s(k^2) \;\approx\; \frac{1}{\beta_0 \ln(k^2/\Lambda^2)} .$$

Everything in this mission is the mathematics of those two formulas: an autonomous scalar ordinary differential equation in the logarithm of the energy, and the behaviour of its solutions according to the sign of the one-loop coefficient.

Setting

Write $\mu > 0$ for the energy scale of a process and $g$, or $\alpha$, for a real-valued coupling as a function of that scale. The beta function in the energy scale is the logarithmic derivative used by the source,

$$\beta(g)(\mu) \;=\; \mu \cdot \frac{d g}{d \mu}(\mu),$$

a function of $\mu$ built from $g$; a theory whose beta function vanishes identically is scale-invariant, since its coupling then takes the same value at every scale.

A coupling is said to be one-loop running with coefficient $b$ on a set $S$ of scales when it satisfies, at every $\mu \in S$,

$$\mu \, \frac{d\alpha}{d\mu}(\mu) \;=\; b \, \alpha(\mu)^2 ,$$

equivalently $d\alpha/d\mu = b\,\alpha^2/\mu$. Here $b < 0$ is the asymptotically free sign (QCD) and $b > 0$ the sign the source attributes to QED. The equation is the one-loop truncation written in $\mu$ rather than in $t = \ln \mu$: both forms appear in the source, and the first milestone is precisely their agreement.

The one-loop strong coupling with one-loop coefficient $\beta_0 > 0$ and QCD scale $\Lambda > 0$ is the explicit function

$$\alpha(Q) \;=\; \frac{1}{\beta_0 \ln(Q^2/\Lambda^2)}, \qquad Q > \Lambda ,$$

the formula the source quotes for $\alpha_s(k^2)$. It is defined by an existing platform definition, which this mission reuses rather than restates.

Formalization targets

Goal — the running dichotomy in the energy scale

For every reference scale $\mu_0 > 0$ and every positive reference value $\alpha_0$ of the coupling at that scale:

$$b<0:\quad \alpha(\mu) \;=\; \frac{\alpha_0}{1 - b\,\alpha_0 \ln(\mu/\mu_0)} \ \ (\mu \ge \mu_0), \qquad \alpha(\mu) \xrightarrow[\mu \to \infty]{} 0 ;$$ $$b>0:\quad \text{no coupling obeys } \mu\,\frac{d\alpha}{d\mu} = b\,\alpha^2 \text{ on all of } \Big[\mu_0,\ \mu_0 e^{1/(b\alpha_0)}\Big] \text{ with } \alpha(\mu_0)=\alpha_0 .$$

The negative-coefficient half is asymptotic freedom together with the uniqueness of the solution; the positive-coefficient half is the Landau pole, stated as the non-existence of any solution up to the pole scale rather than as a divergence of one chosen formula. The pole scale $\mu_0 e^{1/(b\alpha_0)}$ is the one the one-loop equation itself predicts.

Supporting levels

The milestones below range from the definitional identity $\mu\,\partial_\mu g = \partial_{\ln \mu} g$, through the three qualitative readings of the sign of $\beta$ that the source states in words (vanishing beta function means scale invariance; positive beta function means the coupling grows with energy; negative means it falls), to the identification of the quoted QCD formula as an exact solution of the one-loop equation and the determination of $\Lambda$ from a single measured value.

Significance

The dichotomy is the mathematical content of two physical statements that the source presents side by side. Asymptotic freedom is what makes perturbative QCD predictive at high energy; the Landau pole is the reason the source warns that the perturbative beta function cannot be trusted at strong coupling, since the one-loop equation has no solution reaching the pole scale at all. Formalizing the uniqueness half also pins down what "the" running coupling means: the explicit formula is not merely one solution of the renormalization-group equation but the only one through a given data point.

An earlier public mission on the same source ("Coupling Constant: One-Loop Running, Asymptotic Freedom and the Landau Pole") formalized the one-loop flow in the logarithmic variable $t = \ln\mu$ with a cubic beta function $\beta(g) = b\,g^3$, and its statements are proved. This mission is stated in the other variable the source uses — the energy scale $\mu$ itself, with the quadratic one-loop equation for $\alpha$ — and adds the parts of the source that the earlier mission does not cover: the defining identity between the two forms of the beta function, the sign-to-monotonicity statements for an arbitrary (not necessarily one-loop) coupling, the explicit pole scale, and the determination of the QCD scale $\Lambda$ from a measurement. Where the earlier mission already settles a statement in the quoted formula's variables, this proposal references the published theorem instead of restating it.

Difficulty

The equation is elementary, and the difficulty is entirely in what the statements quantify over. The negative-coefficient half asserts that every function satisfying the equation on $[\mu_0,\infty)$ is the explicit one, so it needs a uniqueness argument for a nonlinear scalar ordinary differential equation rather than a verification that a formula works; the substitution $u = 1/\alpha$ that makes the equation linear is legitimate only while $\alpha$ is known not to vanish, which is part of what has to be proved. The positive-coefficient half is a non-existence statement on a closed interval reaching the pole, so no local solution can be extended to it; the naive attempt — differentiate the explicit formula and observe that it blows up — proves nothing about the other candidate solutions.

Formalization scope

Couplings are total functions $\mathbb{R} \to \mathbb{R}$, and every statement restricts to the scales it is about: the positive half-line for the beta-function statements, $(\Lambda,\infty)$ for the explicit QCD formula, $[\mu_0,\infty)$ or a closed interval for the one-loop flow. Outside those ranges nothing is claimed — in particular at $Q \le \Lambda$, where the logarithm in the quoted formula vanishes or is negative and the reciprocal returns a junk value. Differentiability is a hypothesis where it is needed, written as a two-sided derivative at each scale of the set, so that a statement cannot be satisfied by a one-sided artefact at an endpoint. The one-loop property is phrased as an exact differential equation, never as an asymptotic approximation, and the Landau-pole milestone is a non-existence claim rather than a divergence claim, so it cannot be discharged by exhibiting a formula with a singularity.

A complete development needs the mean value theorem, Gronwall- or uniqueness-type arguments for scalar ordinary differential equations, and the standard logarithm and exponential API; the uniqueness lemma for $\dot u = b u^2$ and the reciprocal substitution are reusable beyond this mission. Contributions of a general scalar-ODE uniqueness lemma, usable by both this mission and the earlier one, are especially welcome.

Selected references

• Wikipedia, Coupling constant, revision 1354339557. https://en.wikipedia.org/w/index.php?title=Coupling_constant&oldid=1354339557
• A. Deur, S. J. Brodsky, G. F. de Téramond, The QCD running coupling, Progress in Particle and Nuclear Physics 90 (2016) 1-74. https://arxiv.org/abs/1604.08082
• ATLAS Collaboration, A precise determination of the strong-coupling constant from the recoil of Z bosons with the ATLAS experiment at $\sqrt{s} = 8$ TeV, 2023. https://arxiv.org/abs/2309.12986
• P. A. Zyla et al. (Particle Data Group), Review of Particle Physics - Chapter 9, Quantum Chromodynamics, PTEP 2020 (8). https://doi.org/10.1093/ptep/ptaa104

Motivation

The Polyakov action is the standard action for the worldsheet of a bosonic string. It was introduced by Deser and Zumino and independently by Brink, Di Vecchia and Howe in 1976, and is associated with Polyakov after he used it to quantize the string in 1981. Its value over the Nambu–Goto (area) action is that it is quadratic in the embedding fields, which makes quantization tractable, while being classically equivalent to the area action. This mission formalizes the classical facts collected in the Wikipedia article Polyakov action.

Setting

A string sweeps out a two-dimensional worldsheet with coordinates $\sigma=(\tau,\sigma)$. Its embedding in a $D$-dimensional target is $X^\mu(\sigma)$; the target carries a metric $g_{\mu\nu}(X)$, and the worldsheet carries an independent (auxiliary) metric $h_{ab}(\sigma)$ with inverse $h^{ab}$ and determinant $h$. With the induced metric $G_{ab}=g_{\mu\nu}(X)\partial_aX^\mu\partial_bX^\nu$ and string tension $T$, the Polyakov and Nambu–Goto actions are

$$S_P=\frac T2\int d^2\sigma\,\sqrt{-h}\,h^{ab}G_{ab},\qquad S_{NG}=T\int d^2\sigma\,\sqrt{-\det G_{ab}} .$$

The stress–energy tensor is $T_{ab}=T\big(G_{ab}-\tfrac12h_{ab}h^{cd}G_{cd}\big)$. Signature convention: timelike $+$, spacelike $-$.

Formalization targets

Goal: on-shell equivalence with Nambu–Goto

If the auxiliary metric satisfies its equation of motion $T_{ab}=0$ (with $h^{cd}G_{cd}\ge0$), then

$$S_P=S_{NG}.$$

Milestones

1. Poincaré invariance of the target: translations $X\to X+b$ (exact) and infinitesimal Lorentz transformations $X\to X+\varepsilon\,\omega X$ (to $O(\varepsilon^2)$), for a constant target metric.
2. Worldsheet diffeomorphism invariance and Weyl invariance $h\to\Lambda h$.
3. Tracelessness of the stress–energy tensor, $T^a{}_a=0$.
4. The variations $\delta\sqrt{-h}=-\frac12\sqrt{-h}h_{ab}\delta h^{ab}$ and $\delta S/\delta h^{ab}=\frac T2\sqrt{-h}\,(G_{ab}-\frac12h_{ab}h^{cd}G_{cd})$.
5. On shell, $\det G=\frac14h\,(h^{cd}G_{cd})^2$.
6. Conformal gauge: $S=\frac T2\int(\dot X^2-X'^2)$, the constraints $\dot X\cdot X'=0$, $\dot X^2+X'^2=0$, the wave equation $\Box X^\mu=0$, and its light-cone solution $X=X_+(\tau+\sigma)+X_-(\tau-\sigma)$.

Significance

These are the classical foundations of bosonic string theory: the symmetries (Poincaré, diffeomorphism, Weyl) are what make the conformal gauge reachable, and the equivalence with Nambu–Goto justifies using the quadratic action. All statements are textbook results; the work here is to formalize them with explicit hypotheses (differentiability, integrability, positivity of $h^{cd}G_{cd}$) that the physics presentation leaves implicit.

Difficulty

The algebraic statements are $2\times2$ matrix identities. The diffeomorphism invariance needs the change-of-variables formula; the infinitesimal Lorentz statement needs care with integrability; the wave-equation milestone needs the fundamental lemma of the calculus of variations; and the light-cone solution is d'Alembert's theorem.

Formalization scope

Worldsheet $=\mathbb R^2$ (coordinates Fin 2 → ℝ, index $0=\tau$), target $=\mathbb R^D$. Actions are Bochner integrals over a region $U\subseteq\mathbb R^2$. The inverse metric is Mathlib's matrix inverse. Quantization, Virasoro operators, the Liouville action and string boundary conditions are out of scope.

Selected references

• Wikipedia, Polyakov action, revision 1292212311.
• S. Deser, B. Zumino, A complete action for the spinning string, Phys. Lett. B 65 (1976) 369–373.
• L. Brink, P. Di Vecchia, P. Howe, A locally supersymmetric and reparametrization invariant action for the spinning string, Phys. Lett. B 65 (1976) 471–474.
• A. M. Polyakov, Quantum geometry of bosonic strings, Phys. Lett. B 103 (1981) 207–210.

Motivation

Whether the many-worlds (Everett) interpretation of quantum mechanics is local in the sense of Bell is a recurring question in the foundations of physics. A number of authors have argued that Everett's theory escapes Bell-type nonlocality theorems because it drops the assumption that each measurement has a single outcome. A. Drezet's paper arXiv:2306.07794 (2023) argues against this claim by revisiting the Greenberger–Horne–Zeilinger (GHZ) nonlocality theorem, which, unlike Bell's inequality, uses only probability-one (perfect) correlations. Its central mathematical step, stated in Section II, is that no locally causal beable model can reproduce the quantum predictions for the GHZ state. The paper's argument is that this step makes no assumption about completeness or hidden variables, and so applies to Everett's theory as well.

Timeline:

• 1964–1976: J. S. Bell introduces Bell inequalities and, in "The theory of local beables" (1976), the notion of local causality phrased with beables $\lambda$ (collected in Speakable and Unspeakable in Quantum Mechanics, 2004).
• 1989: Greenberger, Horne and Zeilinger give a nonlocality proof for three spin-½ particles that uses no inequality ("Going beyond Bell's theorem").
• 2015: L. Vaidman discusses the GHZ argument in the many-worlds setting ("Bell inequality and Many-Worlds interpretation").
• 2023: Drezet's paper, the source of this mission.

Setting

Three spin-½ particles are sent to three distant observers, Alice, Bob and Charlie. Each one measures the spin of their particle along a direction $\hat n_j \in \{\hat x, \hat y\}$ and records an outcome $\alpha, \beta, \gamma \in \{+1, -1\}$. The particles are prepared in the GHZ state

$$|\psi\rangle = \tfrac{1}{\sqrt 2}\big(|{+z}\rangle_1|{+z}\rangle_2|{+z}\rangle_3 - |{-z}\rangle_1|{-z}\rangle_2|{-z}\rangle_3\big),$$

and quantum mechanics predicts the joint outcome probabilities through the Born rule, $P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2,\hat n_3,\psi) = |\langle \alpha_{\hat n_1},\beta_{\hat n_2},\gamma_{\hat n_3}|\psi\rangle|^2$. Here $|a_{\hat n}\rangle$ denotes the eigenvector of $\sigma_{\hat n}$ with eigenvalue $a$. In Lean this is bornProb n₁ n₂ n₃ α β γ.

A locally causal (Bell-local) model consists of

• a space $\Lambda$ of beables with a probability distribution $\rho(\lambda)$ that does not depend on the settings (Eq. (18), statistical independence), and
• local response probabilities $P_j(\alpha\mid\lambda,\hat n_j)$, where party $j$'s outcome depends only on $\lambda$ and its own setting (Eq. (17)).

Such a model predicts

$$P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2,\hat n_3) = \int_\Lambda P_1(\alpha\mid\lambda,\hat n_1)\,P_2(\beta\mid\lambda,\hat n_2)\,P_3(\gamma\mid\lambda,\hat n_3)\,d\rho(\lambda).$$

In Lean the model is a LocalCausalModel Λ and its prediction is M.predict. The beables are arbitrary: $\lambda$ may be a hidden variable, or the quantum state itself as in the Beltrametti–Bugajski representation, Eq. (15).

Formalization targets

Goal (Section II, Eqs. (10)–(27))

No locally causal model reproduces the quantum predictions on the four GHZ settings $(\hat x,\hat x,\hat x)$, $(\hat x,\hat y,\hat y)$, $(\hat y,\hat x,\hat y)$, $(\hat y,\hat y,\hat x)$:

$$\neg\Big(\forall\,\text{GHZ settings } \hat n,\ \forall \alpha,\beta,\gamma:\ P^{\mathrm{model}}(\alpha,\beta,\gamma\mid\hat n) = P^{\mathrm{Born}}(\alpha,\beta,\gamma\mid\hat n,\psi)\Big).$$

Milestones

1. Eqs. (2)–(5). $\sigma_x^{(1)}\sigma_x^{(2)}\sigma_x^{(3)}|\psi\rangle = -|\psi\rangle$, and the three $\sigma_x\sigma_y\sigma_y$-type operators fix $|\psi\rangle$.
2. Born probabilities (Section III, Eqs. (30)–(32)). For $(\hat x,\hat x,\hat x)$ each outcome triple has probability $1/4$ if $\alpha\beta\gamma=-1$ and $0$ otherwise. For the other three GHZ settings the same holds with $\alpha\beta\gamma=+1$.
3. Eqs. (10)–(13). No assignment $A_j, B_j \in\{\pm1\}$ satisfies all four GHZ constraints.
4. Eqs. (19)–(27). If a product of three probability distributions on $\{\pm1\}$ vanishes off the set $\{\alpha\beta\gamma = s\}$, then each factor is a point mass, and the three atoms multiply to $s$.
5. Section II, summary (ii). A locally causal model that reproduces the GHZ predictions is, for $\rho$-almost every $\lambda$, deterministic, with values satisfying (10)–(13).
6. Section III (B). Local causality implies non-signalling.
7. Eq. (29). Quantum non-signalling for the GHZ state, with Alice's marginal $P_1(\pm1\mid\hat x,\psi)=\tfrac12$.
8. Appendix 3, Eqs. (39)–(45). Keeping Eq. (17) but letting the beable density depend on the settings (a "superdeterministic" model) does reproduce the GHZ predictions.

Significance

The goal theorem is the mathematical core of the paper's conclusion that any beable account of the GHZ correlations, including one where $\lambda$ is just the quantum state, violates Bell's local causality. Milestones 6–8 formalize the paper's separation of notions of locality: non-signalling holds both in quantum mechanics and in every locally causal model, so it cannot tell them apart; and dropping statistical independence (Eq. (18)) is enough to reproduce the correlations. The GHZ theorem itself has been known since 1989. As far as the drafter is aware it has no machine-checked formalization on this platform, and this mission provides one, stated for general measurable beable spaces.

Difficulty

The combinatorial core (milestone 3) is a parity argument. The substance lies in the steps that connect it to probability: showing that perfect correlations force determinism almost surely when $\rho$ is an arbitrary probability measure (null sets, measurability, integrals of nonnegative functions), and computing the Born probabilities exactly in Lean from explicit matrices and eigenvectors.

Formalization scope

• Outcomes are elements of ℤˣ (exactly $\{+1,-1\}$). Settings form a two-element type Setting with values x and y. Qubit index 0 is $|{+z}\rangle$ and index 1 is $|{-z}\rangle$. Three-qubit operators are Kronecker products.
• A LocalCausalModel Λ has a probability measure ρ on a measurable space Λ and measurable response functions P j λ n α with values in $[0,1]$ that sum to one over $\alpha$. The fixed state $\psi$ is left implicit. Predictions are Bochner integrals, and all integrands are bounded and measurable.
• The goal quantifies over all such models on all measurable spaces. Its hypothesis is the equality of all $4\times 8$ predicted and Born probabilities. Because it uses the actual Born probabilities rather than an arbitrary list of constraints, it cannot hold vacuously.
• Needed infrastructure: finite-dimensional matrix computations over $\mathbb C$ with $\sqrt2$, and basic measure theory (a.e. vanishing of nonnegative integrands).

Selected references

• A. Drezet, An Elementary Proof That Everett's Quantum Multiverse Is Nonlocal: Bell-Locality and Branch-Symmetry in the Many-Worlds Interpretation, arXiv:2306.07794, 2023. https://arxiv.org/abs/2306.07794
• D. M. Greenberger, M. A. Horne, A. Zeilinger, Going beyond Bell's theorem, in Bell's Theorem, Quantum Theory and Conceptions of the Universe, Kluwer, 1989, pp. 69–72. https://arxiv.org/abs/0712.0921
• J. S. Bell, Speakable and Unspeakable in Quantum Mechanics, 2nd ed., Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511815676

Motivation

In emergent gravity proposals, spacetime and gravity are macroscopic descriptions of an underlying quantum system. In Verlinde (2016) it is argued that in de Sitter space (a universe with positive dark energy) the entanglement entropy has, besides the usual area-law part, a thermal volume-law part, and that matter displaces this volume-law entropy. The elastic response of the medium to this displacement produces an extra gravitational pull, which the paper proposes as the origin of the effects usually ascribed to dark matter in galaxies and clusters.

The physical derivation is heuristic, but it ends in explicit mathematical relations between the baryonic (visible) mass profile $M_B(r)$ and the apparent dark matter mass profile $M_D(r)$ of a spherically symmetric, isolated system. The central one is the integral relation (7.40),

$$\int_0^r \frac{G\,M_D(r')^2}{r'^2}\,dr' = \frac{M_B(r)\,a_0\,r}{6},$$

where $G$ is Newton's constant and $a_0 = cH_0$ is the Hubble acceleration scale. For a point mass it reproduces Milgrom's empirical acceleration relation and the baryonic Tully-Fisher relation $v_f^4 = a_M G M_B$ with $a_M = a_0/6$.

Setting

All quantities are real numbers or real functions of the radius $r>0$. $G>0$ and $a_0>0$ are constants. $M_B(r)$ and $M_D(r)$ are the baryonic and apparent dark masses inside radius $r$. The Newtonian accelerations are $g_B(r) = GM_B(r)/r^2$ and $g_D(r) = GM_D(r)/r^2$ (7.42). The averaged density inside radius $r$ is $\bar\rho(r) = 3M(r)/(4\pi r^3)$ (7.45), and the slope parameter is $\beta(r) = -\,d\log\bar\rho/d\log r = -r\bar\rho'(r)/\bar\rho(r)$ (7.46). A local density $\rho$ gives $M(r) = \int_0^r \rho(r')\,4\pi r'^2\,dr'$ (7.39).

The paper also uses two purely mathematical facts about elastic strain in $d-1$ spatial dimensions: a bound (7.30) on the largest principal strain of a traceless symmetric strain tensor, and the integration-by-parts identity (7.31) between the squared Hessian and the squared Laplacian.

Formalization targets

Goal: Milgrom relation for a central point mass (7.43)

If $M_B>0$ is constant and (7.40) holds for every $r>0$, then for every $r>0$

$$g_D(r) = \sqrt{a_M\, g_B(r)}, \qquad a_M = \frac{a_0}{6}.$$

Milestones

• (4.44) the strain-squared integral outside a spherical inclusion: $\int_{c}^{\infty} (c/V)^2\,dV = c$.
• (7.30) $\varepsilon^2 \le \frac{d-2}{d-1}\sum_{ij}\varepsilon'^2_{ij}$ for a traceless symmetric $\varepsilon'$ with eigenvalue $\varepsilon$.
• (7.31) $\int (\nabla_i\nabla_j\chi)^2\,dV = \int (\nabla^2\chi)^2\,dV$.
• (7.47) $\bar\rho_D(r)^2 = (4-\beta_B(r))\,\frac{a_0\,\bar\rho_B(r)}{8\pi G r}$ for a general baryonic profile.
• (7.48) $\rho_D(r) = (1-\tfrac13\beta_D(r))\,\bar\rho_D(r)$.
• (7.51) $\Omega_D^2 = \tfrac43\,\Omega_B$ when (7.47) is applied at the Hubble radius with $\beta_B = 0$.

Significance

The point-mass relation (7.43) is what connects the paper to the observed flat rotation curves and the baryonic Tully-Fisher law; (7.47) is its extension to extended mass profiles, which the paper uses to discuss galaxy clusters. The formal content checked here is the mathematics that turns the stated relation (7.40) into these observable consequences, plus the two elasticity lemmas used on the way to (7.40). The physical steps that lead to (7.40) (the entropy-displacement picture, the elastic interpretation, the identification (7.35)) are not mathematical statements and are outside the scope of this mission. None of these relations is known to have been machine-checked before.

Difficulty

The algebra is short once one may differentiate; the work is in the analysis. (7.40) is an integral identity with a singular weight $1/r'^2$ at the origin, so recovering pointwise information requires the fundamental theorem of calculus on $(0,\infty)$ with only continuity there, and care with integrability at $0$. (7.31) is a double integration by parts in $\mathbb R^n$ that must be justified for the chosen decay class. (7.30) needs the spectral theorem for symmetric matrices, or an equivalent argument.

Formalization scope

All statements live in the namespace Verlinde2016. Radial profiles are functions $\mathbb R\to\mathbb R$, with hypotheses only on $(0,\infty)$. The integral in (7.40) is Lean's interval integral over $[0,r]$; since it would be $0$ for a non-integrable integrand, the positivity of the right-hand side forces integrability. Continuity of $M_D$ (and of densities) on $(0,\infty)$ is taken as a standing physical convention. In (7.31) the paper's condition that "$\chi$ falls off rapidly enough" is formalized as $\chi$ smooth with compact support. Spatial dimension is $d-1$ in (7.30); (7.40)–(7.51) use $d=4$ as in Section 7.2. Definitions: avgDensity, slopeParam, partialDeriv.

Selected references

• E. Verlinde, Emergent Gravity and the Dark Universe, SciPost Phys. 2, 016 (2017). https://arxiv.org/abs/1611.02269
• M. Milgrom, A modification of the Newtonian dynamics as a possible alternative to the hidden mass hypothesis, Astrophys. J. 270 (1983) 365. https://doi.org/10.1086/161130

Motivation

Liouville field theory is a two-dimensional conformal field theory whose classical equation of motion generalizes Liouville's equation. It is one of the few interacting conformal field theories with a continuous spectrum that has been solved: its three-point function on the sphere is given by the DOZZ formula (Dorn–Otto 1994; Zamolodchikov–Zamolodchikov 1996), proved rigorously from a probabilistic construction of the path integral by Kupiainen–Rhodes–Vargas (2017), with the conformal bootstrap established by Guillarmou–Kupiainen–Rhodes–Vargas (2020). It appears in two-dimensional quantum gravity, non-critical string theory, and log-correlated random energy models.

This mission is the first in a series following the Wikipedia article on Liouville field theory. It formalizes the kinematic layer of the theory: the algebraic relations between the coupling constant, the background charge, the central charge, the conformal dimensions and the reflection coefficient, on which every later statement (the spectrum, the DOZZ formula, the bootstrap) is phrased.

Setting

Fix a complex number $b$, the coupling constant. Define

• the background charge $Q = b + \dfrac1b$;
• the central charge $c = 1 + 6Q^2$;
• the conformal dimension of the primary field with momentum $\alpha \in \mathbb C$, $\ \Delta(\alpha) = \alpha(Q - \alpha)$;
• the reflection coefficient with normalization parameter $\lambda$,

$$R_P = \pm\,\lambda^{-2iP}\,\frac{\Gamma(2ibP)\,\Gamma(2ib^{-1}P)}{\Gamma(-2ibP)\,\Gamma(-2ib^{-1}P)},$$

with sign $+1$ if $c \in (-\infty,1)$ and $-1$ otherwise.

Two symmetries act on these data: the reflection $\alpha \to Q - \alpha$ and the duality $b \to 1/b$. The spectrum of the theory is the set of dimensions $\Delta \in \frac{c-1}{24} + \mathbb R_+$, parametrized by momenta $\alpha = \frac Q2 + iP$, $P \in \mathbb R_+$.

Formalization targets

Goal: the spectrum parametrization

For every $b \in \mathbb C$, the map $P \mapsto \Delta\left(\frac Q2 + iP\right)$ is a bijection

$$[0,\infty) \;\xrightarrow{\ \sim\ }\; \frac{c-1}{24} + [0,\infty) \subset \mathbb C.$$

Milestones

1. Reflection invariance: $\Delta(Q-\alpha) = \Delta(\alpha)$.
2. Duality: $c$ and $\Delta$ are invariant under $b \to 1/b$.
3. Marginality: for $b \ne 0$, $b(Q - b) = 1 \iff Q = b + 1/b$.
4. Dimension in terms of momentum: $\Delta\left(\frac Q2 + iP\right) = \frac{c-1}{24} + P^2$.
5. Imaginary coupling: real nonzero $\beta = ib$ produce exactly the real central charges $c \le 1$.
6. Reflection relation consistency: $R_P R_{-P} = 1$ for $\lambda \ne 0$ and $2ibP, 2ib^{-1}P \notin \mathbb Z$.

Significance

These identities are the dictionary between the parameters used in the physics literature ($b$, $Q$, $c$, $\alpha$, $P$, $\Delta$) and fix the conventions for later missions in the series: the DOZZ formula, the pole structure of correlation functions, and the reflection and duality covariance of structure constants are all stated in these variables. None of these statements is open; the value of the mission is a vetted, reusable definition layer with machine-checked consistency of the conventions.

Difficulty

The individual statements are elementary algebra over $\mathbb C$, together with the non-vanishing of the Gamma function away from its poles. The care needed is in conventions: total functions in Lean ($0^{-1} = 0$, principal-branch complex powers, Gamma at its poles) must be handled by explicit hypotheses exactly where the source implicitly excludes degenerate values.

Formalization scope

All quantities are complex-valued functions of $b \in \mathbb C$, defined in the namespace LiouvilleFieldTheory. $1/b$ is Lean's inverse (so $b = 0$ gives junk values $Q = 0$, $c = 1$; statements that need $b \ne 0$ assume it). $\mathbb R_+$ is taken to be $[0,\infty)$. The condition $c \in (-\infty,1)$ is encoded as $\operatorname{Im} c = 0 \wedge \operatorname{Re} c < 1$. $\lambda^{-2iP}$ is the principal-branch complex power. The analytic content of the article (Virasoro representations, conformal blocks, the special function $\Upsilon_b$, the path integral, the DOZZ formula) is out of scope for this mission.

Selected references

• Wikipedia, Liouville field theory, revision 1376996606. https://en.wikipedia.org/w/index.php?title=Liouville_field_theory&oldid=1376996606
• S. Ribault, Conformal field theory on the plane, 2014. https://arxiv.org/abs/1406.4290
• H. Dorn, H.-J. Otto, Two and three point functions in Liouville theory, Nucl. Phys. B 429 (1994). https://arxiv.org/abs/hep-th/9403141
• A. Zamolodchikov, Al. Zamolodchikov, Conformal bootstrap in Liouville field theory, Nucl. Phys. B 477 (1996). https://arxiv.org/abs/hep-th/9506136
• A. Kupiainen, R. Rhodes, V. Vargas, Integrability of Liouville theory: proof of the DOZZ formula, 2017. https://arxiv.org/abs/1707.08785
• C. Guillarmou, A. Kupiainen, R. Rhodes, V. Vargas, Conformal bootstrap in Liouville theory, 2020. https://arxiv.org/abs/2005.11530

Why barycenters of histograms matter

A barycenter summarizes several objects by minimizing a weighted sum of distances to them. For probability histograms, ordinary coordinatewise averages depend strongly on how the bins are labeled. Optimal transport instead lets mass move between bins and charges for those moves through a cost matrix. The resulting Wasserstein barycenter can reflect the geometry of the bins: nearby bins can exchange mass at a lower cost than distant ones. Peyré and Cuturi use this construction in their treatment of variational transport problems, including shape interpolation and the representation of a measure as a barycenter of other measures. The finite histogram problem in this mission is the entropically regularized version developed in §9.2 of their textbook.

The computational question is how to connect three ways of describing the same solution: a histogram that is the barycenter, transport matrices coupling it to the inputs, and vectors of dual potentials. Proposition 9.1 on p. 530 identifies the dual potentials behind the scaling factors of the optimal transport matrices. This is the second proposition numbered 9.1 in the chapter; the one on p. 519 concerns derivatives with respect to histograms.

Finite histogram setting

There are $S$ input histograms. Source $s$ has $n_s$ bins and a probability vector $b_s$, while the barycenter has $n$ bins. The real matrix $C_s\in\mathbb R^{n\times n_s}$ gives the cost of transporting a unit of mass from barycenter bin $i$ to input bin $j$. A weight vector $\lambda\in\Sigma_S$ has nonnegative entries summing to one; $\Sigma_k$ denotes the probability simplex on $k$ bins. The unregularized barycenter problem (9.10) minimizes $\sum_s\lambda_s L_{C_s}(a,b_s)$ over $a\in\Sigma_n$, where $L_{C_s}$ is the minimum transport cost with marginals $a$ and $b_s$.

For a regularization parameter $\varepsilon>0$, the entropic transport cost $L^\varepsilon_{C_s}(a,b_s)$ minimizes $\langle C_s,P_s\rangle-\varepsilon H(P_s)$ over nonnegative coupling matrices $P_s$ with row marginal $a$ and column marginal $b_s$. Here $\langle C_s,P_s\rangle=\sum_{i,j}C_{s,ij}P_{s,ij}$ and $H(P_s)=\sum_{i,j}(-P_{s,ij}\log P_{s,ij}+P_{s,ij})$, with $0\log0=0$. The Gibbs kernel is $K_{s,ij}=e^{-C_{s,ij}/\varepsilon}$.

The book also writes the regularized barycenter as a weighted KL projection. Its variables are the matrices $(P_s)_s$; each matrix has column marginal $b_s$, and every matrix has the same row marginal. That shared row marginal is $a$, so the optimization can be expressed without carrying $a$ as a separate variable. The generalized matrix divergence is $\mathrm{KL}(P_s\mid K_s)=\sum_{i,j}[P_{s,ij}\log(P_{s,ij}/K_{s,ij})-P_{s,ij}+K_{s,ij}]$, using the continuous value at $P_{s,ij}=0$. See (9.15)–(9.17) in Peyré and Cuturi.

Formalization targets

The goal is Proposition 9.1 on p. 530. The dual variables are row potentials $f_s\in\mathbb R^n$ and column potentials $g_s\in\mathbb R^{n_s}$. They maximize

$$\sum_s\lambda_s\left[\langle g_s,b_s\rangle-\varepsilon\sum_{i,j}e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon}\right] \quad\text{subject to}\quad \sum_s\lambda_s f_s=0.$$

The theorem asserts that the primal and dual optima are attained, that every optimal primal family and every optimal dual family satisfy

$$P_{s,ij}=e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon},$$

and that the dual maximum is the minimum value of the entropic barycenter objective (9.15). The milestone targets are the scalar and matrix versions of the KL conjugate (9.22), followed by the closed form maximizer of one $g_s$ block, corresponding to the update (9.18). These statements retain the source's finite matrix setting and are listed in the order in which their concepts enter the dual formulation.

What the result supplies

The scaling formula turns the optimal couplings into a product of a row factor, a fixed positive kernel, and a column factor. It identifies those factors with exponentials of dual potentials and gives a constrained maximization problem whose value is the entropic barycenter cost. Thus a solver can reason about the couplings, the barycenter marginal, or the potentials while referring to one theorem that connects them. The book uses the same variables to describe the iterative scaling updates on pp. 529–531 and later illustrates barycenters of shapes and surface measures; those applications depend on interpreting the matrix factors correctly. Peyré and Cuturi give the mathematical proposition and its argument. A complete Lean proof of the proposition and its supporting KL identities is the work this mission calls for; the statements here are draft targets rather than machine-checked solutions.

Where the difficulty lies

The potential program is a constrained optimization problem, while the transport problem constrains nonnegative matrices by two kinds of marginals. Equality of their optimum values must preserve the normalization constants in generalized KL. The exponential form alone does not establish that a proposed matrix has the required marginals, nor does a feasible matrix alone identify dual potentials. In addition, the assertion concerns every optimizer: a choice of zero source weight would leave that source's coupling unconstrained by the objective, and a zero target entry would put a logarithmic column update on the boundary. These are substantive edge cases of the formulas, not merely notation.

Formalization scope

Lean uses Fin S, Fin n, and Fin (n_s) for the finite index sets; these are zero based versions of the book's one based indices. Histograms and potentials are real vectors, costs and couplings are real matrices, and the Gibbs kernel is defined entrywise. The theorem requires $S,n,n_s>0$, $\varepsilon>0$, strictly positive weights $\lambda_s$ that sum to one, and strictly positive input histograms $b_s$ that each sum to one. The strict positivity of weights and input entries is an explicit restriction beyond (9.15)–(9.21), needed for a statement about every optimizer and finite logarithmic potentials. Entropy uses $0\log0=0$ on nonnegative couplings. The shared row marginal is constructed by the constraints on the $P_s$; it is not a free histogram unrelated to them.

The definition layer includes finite matrix pairing, entropy, generalized KL, the Gibbs kernel, feasibility, and primal and dual objective functions. The KL conjugate identities and the block optimizer are separate theorem targets so they can be reused in other entropic transport developments. The main theorem asserts primal and dual attainment as well as their relationship; it does not assume strong duality or an optimal scaling as an input. The page has slips in the dimensions of the marginal equations and a missing subscript on $K$ in (9.17); the Lean statements use the dimensions specified by $P_s\in\mathbb R^{n\times n_s}$. The optional cost-gradient Proposition 9.2 on pp. 519–520 and the $f_s$ block update (9.19)–(9.20) lie outside this proposal.

Selected references

• Gabriel Peyré and Marco Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. DOI: 10.1561/2200000073.