Mathematical Physics

Motivation

The second law of thermodynamics is a physical law based on universal empirical observation concerning heat and energy interconversions. Two of its classical statements are impossibility statements about machines. Rudolf Clausius (1854): "Heat can never pass from a colder to a warmer body without some other change, connected therewith, occurring at the same time." Lord Kelvin: "It is impossible for any system to operate in a thermodynamic cycle and deliver a net amount of energy by work to its surroundings while receiving energy by heat transfer from a single thermal reservoir." The Wikipedia article Second law of thermodynamics records that these two have been shown to be equivalent.

The law is not only prohibitive. Sadi Carnot's analysis of heat engines (1824) yields an upper bound on the efficiency of any engine running between two heat reservoirs, attained by reversible engines and strictly missed by irreversible ones, and — crucially — the same for all reversible engines whatever the working substance. That substance-independence is what makes a thermodynamic temperature possible: as the article puts it, "The second law allows a distinguished temperature scale, which defines an absolute, thermodynamic temperature, independent of the properties of any particular reference thermometric body."

This mission formalizes that chain: from the two impossibility statements, through Carnot's theorem, to the existence and uniqueness of the absolute temperature scale normalized by the Kelvin convention at the triple point of water.

Setting

A cyclically operating device is recorded by the heat it exchanges with thermal reservoirs over one complete cycle. Reservoirs are labelled by empirical temperature, an element of a linearly ordered type $\Theta$ ($s<t$: the reservoir at $s$ is colder). A cycle is a finitely supported function $c:\Theta\to\mathbb R$, where $c(t)$ is the net heat absorbed by the device from the reservoir at $t$ (negative if rejected). Because the device returns to its initial state, the first law makes the net work delivered equal to the total heat absorbed:

$$W(c)=\sum_{t}c(t).$$

The cycles that can actually be realized form a set $\mathcal C$, assumed to be a convex cone: the null cycle is realizable; two realizable devices can be run side by side, their heat exchanges adding; and a realizable device can be scaled by any factor $r\ge0$. A cycle is reversible when $c\in\mathcal C$ and $-c\in\mathcal C$, and operates between $h$ and $k$ when it exchanges heat with no other reservoir. A Carnot engine between a hot $h$ and a cold $k$ is a reversible cycle operating between them with $c(h)>0$, $c(k)<0$ and $W(c)>0$. The efficiency relative to the hot reservoir is $\eta=W(c)/c(h)$.

In this language:

• Clausius statement. For $k<h$: every realizable cycle operating between $h$ and $k$ with $W(c)=0$ satisfies $c(k)\le0$.
• Kelvin statement. Every realizable cycle exchanging heat with a single reservoir satisfies $W(c)\le0$.
• $\mathcal C$ admits Carnot engines when a Carnot engine exists between every pair of reservoirs at different temperatures.

Formalization targets

Goal: the thermodynamic temperature scale

Assume $\mathcal C$ is a convex cone satisfying the Clausius statement and admitting Carnot engines, and fix a reference reservoir $T_0$. Then there is exactly one $T:\Theta\to\mathbb R$ with

$$T>0,\qquad T(T_0)=273.16,\qquad \frac{|e(k)|}{|e(h)|}=\frac{T(k)}{T(h)}\quad\text{for every Carnot engine } e \text{ between } k<h.$$

The content is that the left-hand ratio, a property of an engine, depends on the engine only through its two reservoirs, and does so as a ratio of numbers attached to the reservoirs. The normalization $273.16$ at $T_0$ is the Kelvin convention; as the article notes, "any reference temperature and any positive numerical value could be used".

The two impossibility statements

$$\text{Clausius}(\mathcal C)\iff\text{Kelvin}(\mathcal C)$$

for a convex cone admitting Carnot engines over at least two reservoir temperatures.

Carnot's theorem

For $k<h$ and a Carnot engine $e$ between them, every realizable engine $c$ between the same two reservoirs satisfies $\eta(c)\le\eta(e)$, with strict inequality when $c$ is irreversible ($-c\notin\mathcal C$); and any two Carnot engines between $h$ and $k$ have equal efficiency.

Significance

The goal makes explicit which features of the realizable processes are used when a textbook defines absolute temperature. The three hypotheses — convex cone, Clausius statement, existence of Carnot engines — are exactly what the derivation needs; the working substance, the equation of state, and the mechanism of a device never appear. Uniqueness is the part that is usually left implicit: the Kelvin normalization at one reservoir pins the scale completely.

The milestones follow the article's own order: equation (1) for the efficiency of an arbitrary engine; the equivalence of the Clausius and Kelvin statements; the three clauses of Carnot's theorem; the composition law $f(T_1,T_3)=f(T_1,T_2)f(T_2,T_3)$ for the reversible heat ratio across an intermediate reservoir; the conversion of that law into a scale; and the resulting Carnot efficiency $\eta=1-T_{\mathrm C}/T_{\mathrm H}$.

Difficulty

The mathematics is elementary — convex cones in a space of finitely supported real functions, and one functional equation — but the bookkeeping is where faithfulness is won or lost. Carnot's theorem is proved by scaling a candidate engine against a reversed Carnot engine so that the composite does no net work, which makes the Clausius statement applicable; the equality case has to identify the candidate as a positive multiple of the Carnot engine before concluding that it is reversible. The composition law requires the intermediate reservoir to be exactly balanced, so that the composite is again a two-reservoir engine — the article's remark that "the heat $q_2$ flown from the engine 2 to the intermediate reservoir must be equal to the heat $q_2^*$ flown out from the reservoir to the engine 3". The functional equation must be solved without assuming the reference reservoir is the hottest or the coldest, so the scale is defined by $f(T_0,\cdot)$ below $T_0$ and by $1/f(\cdot,T_0)$ above it, and the composition law is applied in four different orderings.

Formalization scope

• Reservoir temperatures form an arbitrary linearly ordered type; the order is the empirical hotter/colder relation and nothing else is assumed of it.
• Heat is positive into the device. Work is the sum of the heats, which is the first law for a cycle; the first law is therefore built into the model rather than stated.
• A device is recorded only by its heat exchanges. Working substance, the states traversed, quasi-staticity and the internal construction do not appear; "reversible" means exactly that the reversed heat exchange pattern is also realizable.
• The Clausius statement is formalized for a cycle with zero net work exchanging heat with exactly two reservoirs: that is the article's "without some other change, connected therewith, occurring at the same time".
• Out of scope for this mission: the Clausius inequality $\oint \delta Q/T_{\mathrm{surr}}\le0$, the definition of entropy as a state function, Carathéodory's and Planck's formulations, the statistical-mechanical derivations, and the Clausius–Duhem inequality for continua.

Selected references

• Wikipedia, Second law of thermodynamics, revision oldid=1378607758. https://en.wikipedia.org/w/index.php?title=Second_law_of_thermodynamics&oldid=1378607758
• S. Carnot, Réflexions sur la puissance motrice du feu, 1824.
• R. Clausius, Über eine veränderte Form des zweiten Hauptsatzes der mechanischen Wärmetheorie, Annalen der Physik 93 (1854), 481–506.

Motivation

The Einstein field equations (EFE) are the field equations of general relativity. They relate the curvature of spacetime, encoded in the metric $g_{\mu\nu}$, to its matter–energy content, encoded in the stress–energy tensor $T_{\mu\nu}$:

$$G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu},\qquad \kappa=\frac{8\pi G}{c^4}.$$

They were published by Einstein in 1915. A structural requirement on any such equation is that it be compatible with the local conservation of energy and momentum, $\nabla_\beta T^{\alpha\beta}=0$. For the EFE this compatibility is automatic: the left-hand side is identically divergence-free by the contracted Bianchi identity, so the field equations force conservation of the right-hand side. This mission formalizes that implication together with the standard algebraic reformulations of the equations, following the Wikipedia article Einstein field equations (revision 1374672993).

Setting

Everything is written in one coordinate chart. A point is $x\in\mathbb{R}^D$, where $D$ is the spacetime dimension (not fixed to $4$). A 2-tensor field is a matrix-valued function $x\mapsto T_{ab}(x)$. A metric on an open set $U$ is a 2-tensor field $g$ whose components are $C^\infty$ on $U$ and which is symmetric and nondegenerate at each point of $U$; $g^{ab}$ denotes the inverse matrix. Partial derivatives $\partial_a$ are coordinate (Fréchet) derivatives. Using the Misner–Thorne–Wheeler $(+\,+\,+)$ convention adopted by the source:

• Christoffel symbols $\Gamma^c_{ab}=\tfrac12g^{cs}(\partial_ag_{sb}+\partial_bg_{sa}-\partial_sg_{ab})$;
• Riemann tensor $R^\mu{}_{\alpha\beta\gamma}=\partial_\beta\Gamma^\mu_{\alpha\gamma}-\partial_\gamma\Gamma^\mu_{\alpha\beta}+\Gamma^\mu_{\sigma\beta}\Gamma^\sigma_{\gamma\alpha}-\Gamma^\mu_{\sigma\gamma}\Gamma^\sigma_{\beta\alpha}$;
• Ricci tensor $R_{\mu\nu}=R^\alpha{}_{\mu\alpha\nu}$, scalar curvature $R=g^{\mu\nu}R_{\mu\nu}$, Einstein tensor $G_{\mu\nu}=R_{\mu\nu}-\tfrac12Rg_{\mu\nu}$;
• covariant derivative $\nabla_\lambda T_{\mu\nu}=\partial_\lambda T_{\mu\nu}-\Gamma^\sigma_{\lambda\mu}T_{\sigma\nu}-\Gamma^\sigma_{\lambda\nu}T_{\mu\sigma}$ and divergence $(\operatorname{div}T)_\mu=g^{\nu\lambda}\nabla_\lambda T_{\mu\nu}$, the index-lowered form of $\nabla_\nu T^{\mu\nu}$;
• the field equations on $U$: $G_{\mu\nu}(x)+\Lambda g_{\mu\nu}(x)=\kappa T_{\mu\nu}(x)$ for all $x\in U$.

Formalization targets

Goal: local energy–momentum conservation

For a smooth nondegenerate symmetric metric $g$ on an open $U\subseteq\mathbb{R}^D$, constants $G,c>0$, $\kappa=8\pi G/c^4$, any $\Lambda$, and any $T$ such that the field equations hold on $U$:

$$g^{\beta\lambda}\nabla_\lambda T_{\alpha\beta}=0\quad\text{on }U.$$

Milestones

• Symmetry of the Einstein tensor, $G_{\mu\nu}=G_{\nu\mu}$.
• Metric compatibility, $\nabla_\lambda g_{\mu\nu}=0$.
• The differential Bianchi identity $R^\mu{}_{\alpha[\beta\gamma;\varepsilon]}=0$.
• The contracted Bianchi identity, $G^{\alpha\beta}{}_{;\beta}=0$.
• The trace of the EFE, $R-\tfrac D2R+D\Lambda=\kappa T$.
• Equivalence with the trace-reversed form $R_{\mu\nu}-\tfrac2{D-2}\Lambda g_{\mu\nu}=\kappa(T_{\mu\nu}-\tfrac1{D-2}Tg_{\mu\nu})$ for $D\neq2$.
• The vacuum equations $R_{\mu\nu}=\Lambda g_{\mu\nu}/(\tfrac D2-1)$ when $T=0$, $D\neq2$.
• The cosmological term as vacuum stress–energy $T^{(\mathrm{vac})}_{\mu\nu}=-\tfrac\Lambda\kappa g_{\mu\nu}$, with $\rho_{\mathrm{vac}}=-p_{\mathrm{vac}}=\Lambda/\kappa$.
• Minkowski space $\operatorname{diag}(-1,1,1,1)$ is a vacuum solution.

Significance

Conservation of $T_{\mu\nu}$ is a consistency condition that any relativistic field equation for gravity has to satisfy; it is also the starting point for deriving the motion of matter (for dust, the geodesic equation) from the field equations alone. The trace-reversed and vacuum forms are the ones used in practice to study vacuum solutions such as Schwarzschild and Kerr, and Einstein manifolds in geometry.

All of these results are classical and fully proved in the literature. What is not yet available is a machine-checked development of the Levi-Civita curvature calculus in coordinates suitable for these statements: Mathlib currently has no Riemann or Ricci tensor of a pseudo-Riemannian metric. The mission produces that layer and the proofs on top of it.

Difficulty

The algebraic milestones (trace, trace reversal, vacuum form, vacuum energy) only need matrix algebra and the symmetry of $g$; without symmetry the identity $g^{\mu\nu}g_{\mu\nu}=D$ fails, so symmetry is essential. The analytic core is the contracted Bianchi identity: it needs the symmetry of mixed second and third partial derivatives (Schwarz's theorem on an open set), derivatives of the matrix inverse $g^{-1}$, and lengthy index bookkeeping with sums over $\operatorname{Fin} D$. Since all objects are total functions, every derivative step must be justified by differentiability on the open set $U$, not taken for granted.

Formalization scope

• Coordinates: $\mathbb{R}^D$ is represented as Fin D → ℝ; tensors are Matrix (Fin D) (Fin D) ℝ-valued functions; no manifold structure. $D$ is arbitrary, and no Lorentzian signature is imposed (the results hold for any nondegenerate symmetric metric, which includes the Lorentzian case).
• Regularity: the metric components are $C^\infty$ on the open set $U$; $T$ carries no assumptions, as the field equations determine it on $U$.
• Total-function conventions: the inverse of a singular matrix is $0$ and the derivative of a non-differentiable function is $0$; nondegeneracy on $U$ and openness of $U$ make these junk values irrelevant at points of $U$.
• Divergence is taken on the second index; for symmetric tensors such as $G$ this is the same as the first.
• Not formalized: the Newtonian limit (it rests on approximations), the Einstein–Maxwell system, and the polynomial form.
• Reusable output: coordinate Christoffel/Riemann/Ricci calculus, metric compatibility, Bianchi identities.

Selected references

• Wikipedia, Einstein field equations, revision 1374672993. https://en.wikipedia.org/w/index.php?title=Einstein_field_equations&oldid=1374672993
• C. W. Misner, K. S. Thorne, J. A. Wheeler, Gravitation, W. H. Freeman, 1973.
• S. Carroll, Spacetime and Geometry: An Introduction to General Relativity, Addison Wesley, 2004.

Motivation

The electroweak interaction is the unified description of electromagnetism and the weak nuclear force in the Standard Model of particle physics. Glashow, Salam and Weinberg shared the 1979 Nobel Prize in Physics for this unification, and its central predictions — neutral weak currents (Gargamelle, 1973) and the massive $W^\pm$ and $Z^0$ bosons (UA1/UA2, 1983) — have been confirmed experimentally. The algebraic core of the theory is short: an $\mathrm{SU}(2)\times\mathrm{U}(1)$ gauge theory whose symmetry is broken by the vacuum value of a Higgs doublet, after which the neutral gauge fields are rotated by the weak mixing angle $\theta_W$ into the photon and the $Z^0$, and the masses satisfy $m_Z = m_W/\cos\theta_W$.

This mission formalizes those tree-level algebraic facts as they are stated in the Wikipedia article Electroweak interaction (revision 1360331872), sections Formulation and Lagrangian.

Timeline (as recounted in the article). After the Wu experiment (1956) exposed parity violation, Glashow combined a chiral and an achiral symmetry and predicted a $Z$ boson; Salam and Ward (1964) proposed a massless photon and three massive gauge bosons with manually broken symmetry; Weinberg (1967) used spontaneous symmetry breaking (Englert–Brout, Higgs, Guralnik–Hagen–Kibble, 1964) and predicted rough $W$ and $Z$ masses; 't Hooft (1971) proved that spontaneously broken gauge theories are renormalizable. Neutral currents were observed in 1973 and the $W$, $Z$ in 1983.

Setting

Fix the weak isospin coupling $g>0$ and the weak hypercharge coupling $g'>0$. The gauge fields at a spacetime point, for one Lorentz component, are real numbers $W_1, W_2, W_3$ (weak isospin) and $B$ (weak hypercharge).

1. Weak mixing angle. $\theta_W = \arctan(g'/g)$, the angle of the right triangle with legs $g$, $g'$ and hypotenuse $\sqrt{g^2+g'^2}$ (the figure Weinberg's weak mixing angle in the article). The electromagnetic coupling is the altitude of that triangle, $e = gg'/\sqrt{g^2+g'^2}$.
2. Physical neutral fields. $\gamma = \cos\theta\,B + \sin\theta\,W_3$ and $Z^0 = -\sin\theta\,B + \cos\theta\,W_3$.
3. Charged fields. $W^\pm = (W_1 \mp i W_2)/\sqrt 2$.
4. Higgs sector. The Higgs field is a complex doublet $h\in\mathbb C^2$ with $|h|^2 = |h_1|^2+|h_2|^2$ and potential $V(h) = \lambda\,(|h|^2 - v^2/2)^2$. Its vacuum is $h_0 = (0, v/\sqrt2)$.
5. Covariant derivative. $D_\mu = \partial_\mu - i\tfrac{g'}{2} Y B_\mu - i \tfrac{g}{2}\sigma_j W^j_\mu$ with $\sigma_j$ the Pauli matrices. On the constant vacuum the derivative term vanishes, so $|D_\mu h_0|^2 = |M h_0|^2$ with $M = \tfrac{g'}{2}YB\,\mathbb 1 + \tfrac g2(W_1\sigma_1+W_2\sigma_2+W_3\sigma_3)$ and $Y=1$ for the Higgs.
6. Charge. $Q = T_3 + \tfrac12 Y$.
7. Masses. $m_W = gv/2$ and $m_Z = \sqrt{g^2+g'^2}\,v/2$.

Formalization targets

Goal: the gauge boson mass terms

For all real $v, W_1, W_2, W_3, B$,

$$|M h_0|^2 = m_W^2\, W^+ W^- + \tfrac12 m_Z^2 \,(Z^0)^2 ,$$

which is the mass part $m_W^2 W^+_\mu W^{-\mu} + \tfrac12 m_Z^2 Z_\mu Z^\mu$ of $\mathcal L_K$ in the article. The photon field $\gamma$ does not appear: it stays massless.

Milestones

1. The Weinberg triangle: $\cos\theta_W = g/\sqrt{g^2+g'^2}$, $\sin\theta_W = g'/\sqrt{g^2+g'^2}$.
2. $e = g\sin\theta_W = g'\cos\theta_W$.
3. $(\gamma, Z^0)$ is a rotation of $(B, W_3)$: it can be inverted and $\gamma^2+(Z^0)^2 = B^2+W_3^2$.
4. $W^- = \overline{W^+}$, $W_1 = (W^++W^-)/\sqrt2$, $W_2 = i(W^+-W^-)/\sqrt2$, $W^+W^- = (W_1^2+W_2^2)/2$.
5. $m_Z = m_W/\cos\theta_W$.
6. $h_0$ minimizes the Higgs potential, and the zero set of $V$ is the sphere $|h|^2 = v^2/2$.
7. $Q = T_3 + \tfrac12 Y$ annihilates $h_0$, and (for $v\neq0$) it is the only combination $aT_3 + b\,Y/2$, up to scale, that does.
8. The neutral-current coupling: $gT_3W_3 + g'\tfrac Y2 B = eQ\,\gamma + \frac{g}{\cos\theta_W}(T_3 - \sin^2\theta_W\,Q)\,Z^0$.

Significance

These identities are the content behind the article's statements that "the axes ... have been rotated by the angle $\theta_W$", that $m_Z = m_W/\cos\theta_W$, that $e = g\sin\theta_W = g'\cos\theta_W$, and that $\mathrm U(1)_{em}$ is unbroken because it does not couple to the Higgs. The formal library produced here (Pauli matrices, the Higgs doublet, the mixing rotation, the mass formulas) can be reused by later missions on the full electroweak Lagrangian, on the Yukawa sector, or on the custodial relation $\rho = m_W^2/(m_Z^2\cos^2\theta_W) = 1$.

All statements are classical tree-level results. None is open; the work is to formalize them.

Difficulty

The mathematics is finite-dimensional linear algebra and trigonometry. The main pitfalls are conventions: the factor $\tfrac12$ in front of the Pauli matrices, the hypercharge normalization $Q = T_3 + Y/2$ (so the Higgs has $Y=1$), and the sign conventions in the rotation matrix. The goal also requires handling complex doublets, $\sqrt 2$ factors and the inverse trigonometric definition of $\theta_W$ at the same time.

Formalization scope

All fields are real numbers at one spacetime point and for one Lorentz component; the Lorentz contraction and the kinetic (derivative) terms are not modeled. The Higgs doublet is a function Fin 2 → ℂ, and its squared norm is written out as $|h_1|^2 + |h_2|^2$ (not the sup norm of the product type). The Pauli matrices are defined explicitly. The angle is $\theta_W = \arctan(g'/g)$; with $g>0$ this agrees with the triangle. The standing convention $g, g' > 0$ is a hypothesis wherever $\theta_W$ appears. The goal is stated as an equation in $\mathbb C$ so that the product $W^+W^-$ appears exactly as in $\mathcal L_K$.

All declarations live in the namespace ElectroweakWiki.

Selected references

• Wikipedia contributors, Electroweak interaction, revision 1360331872. https://en.wikipedia.org/w/index.php?title=Electroweak_interaction&oldid=1360331872
• S. Weinberg, A Model of Leptons, Phys. Rev. Lett. 19 (1967) 1264. https://doi.org/10.1103/PhysRevLett.19.1264
• D. J. Griffiths, Introduction to Elementary Particles, Wiley, 1987.

Motivation

The Wheeler–DeWitt equation is the quantum version of the Hamiltonian constraint of general relativity. In the canonical formulation, a spacetime is described by the evolution of the metric $h_{ab}$ of a spatial slice, and Einstein's equations include a constraint: the Hamiltonian density vanishes at every point of space. Quantizing this constraint, as DeWitt did (Phys. Rev. 160, 1967), gives a second-order functional differential equation for a wavefunctional $\Psi[h]$ with no external time parameter.

Three structural facts make the equation distinctive:

• its kinetic term is built from an indefinite metric on the space of metrics, the DeWitt supermetric, so the equation is hyperbolic;
• the timelike direction of that supermetric is the local volume, which serves as an intrinsic time;
• in the limit $\hbar\to0$, a WKB ansatz turns the equation into the Einstein–Hamilton–Jacobi equation, recovering classical general relativity.

A fourth issue is not settled: consistency. In the continuum, the Poisson bracket of two Hamiltonian constraints is a combination of the momentum constraints, so imposing all constraints is consistent (Dirac's first-class condition). Any regularization of the quantum equation, a lattice for instance, must reproduce this. Generic lattice discretizations do not: the constraints become second class (Bander 1987; Dittrich 2008; Bahr–Dittrich 2009). Whether, and with which anomaly, the Hamiltonian-constraint commutators close as the lattice is refined was singled out as an open question by Loll (Living Rev. Rel. 1998, §2.12).

The first three facts are the standard entry points of quantum geometrodynamics, as reviewed by Kiefer (arXiv 0812.0295): Section 2 for the constraints and their quantization, eqs. (3)–(8), and Section 3 for the Hamilton–Jacobi equation, eq. (10), and the semiclassical approximation, eq. (11).

Setting

A spatial metric at a point is a symmetric positive-definite $3\times3$ matrix $h=(h_{ab})$. Write $\sqrt h=\sqrt{\det h}$. The DeWitt supermetric is

$$G_{abcd}(h)=\frac{h_{ac}h_{bd}+h_{ad}h_{bc}-h_{ab}h_{cd}}{2\sqrt h}.$$

It is a quadratic form $G(p,p)=G_{abcd}\,p^{ab}p^{cd}$ on symmetric momenta. Its inverse $G^{abcd}=\tfrac12\sqrt h\,(h^{ac}h^{bd}+h^{ad}h^{bc}-2h^{ab}h^{cd})$ acts on velocities.

Space is represented by a finite set $X$ of sites; this is a lattice regularization. A configuration assigns to each site $x$ a matrix $h(x)$. All nine entries are coordinates, so configuration space is $\mathbb{R}^{9|X|}$, and physical configurations are those that are symmetric and positive definite at every site. A wavefunction is a function $\Psi$ from configurations to $\mathbb{C}$. The functional derivative $\delta/\delta h_{ab}(x)$ is the partial derivative $\partial_{ab}(x)$ with respect to the coordinate $h_{ab}(x)$, with the cell volume normalized to one.

The Wheeler–DeWitt operator at site $x$, with gravitational coupling $\kappa$, cosmological constant $\Lambda$, and a supplied potential $R(h,x)$ playing the role of the spatial scalar curvature, is

$$\widehat{\mathcal H}_x\Psi=-2\kappa\hbar^2\,G_{abcd}(h(x))\,\partial_{ab}(x)\,\partial_{cd}(x)\Psi-\frac{\sqrt{h(x)}}{2\kappa}\,(R-2\Lambda)\,\Psi .$$

Write $V_z(h)=-\tfrac{\sqrt{h(z)}}{2\kappa}(R(h,z)-2\Lambda)$ for the potential at site $z$. On the classical phase space of pairs $(h,p)$, with $p^{ab}(z)$ conjugate to $h_{ab}(z)$, the lattice constraints are

$$H_z(h,p)=2\kappa\,G_{abcd}(h(z))\,p^{ab}(z)\,p^{cd}(z)+V_z(h),$$

with the canonical Poisson bracket. They are first class if each bracket $\{H_x,H_y\}$ vanishes wherever all constraints vanish.

The supermetric stands to the left of both derivatives (Kiefer, eq. (7), vacuum case; the coupling is $\kappa=8\pi G$, so $2\kappa=16\pi G$ as in Kiefer's eq. (10)). The kinetic term involves only derivatives at the same site, as in the continuum; it is ultralocal. The potential may couple neighbouring sites.

Formalization targets

Milestones: geometry of the supermetric

• Signature. $G(p,p)>0$ for every nonzero symmetric $p$ with $\operatorname{tr}(hp)=0$, and $G(h^{-1},h^{-1})<0$.
• Inverse. $G^{abcd}G_{cdef}\,p^{ef}=p^{ab}$ for symmetric $p$.
• Intrinsic time. With $h=s\hat h$, $\det\hat h=1$ and $\tau=\sqrt{32/3}\,s^{3/4}$, the velocity form of the supermetric is $-d\tau^2+\tfrac{3}{32}\tau^2\operatorname{tr}\big((\hat h^{-1}d\hat h)^2\big)$.

Milestone: the conformal sector

For $\Psi=f(\sqrt{\det h(x_0)})$ with $f\in C^2$ and $v=\sqrt{\det h(x_0)}$:

$$G_{abcd}\,\partial_{ab}\partial_{cd}\Psi=-\tfrac38\,\big(vf''(v)+7f'(v)\big).$$

Milestone: the semiclassical limit

For every real $C^2$ function $S$ and $\hbar\neq0$:

$$e^{-iS/\hbar}\,\widehat{\mathcal H}_x\,e^{iS/\hbar}=2\kappa\,G_{abcd}\,\partial_{ab}S\,\partial_{cd}S-\frac{\sqrt h}{2\kappa}(R-2\Lambda)\;-\;i\hbar\,2\kappa\,G_{abcd}\,\partial_{ab}\partial_{cd}S .$$

The $\hbar$-independent part is the Einstein–Hamilton–Jacobi functional of Kiefer's eq. (10), Hamiltonian part, with $S$ the eikonal of the WKB form (11) (amplitude $C=1$). This is the weakest statement exhibiting the classical limit, and it holds for every potential.

Milestone: the lattice commutator

For $\Psi\in C^4$ and sites $x\neq y$:

$$[\widehat{\mathcal H}_x,\widehat{\mathcal H}_y]\Psi=-2\kappa\hbar^2\Big(G_{abcd}(h(x))\big(2\,\partial^{x}_{ab}V_y\,\partial^{x}_{cd}\Psi+\partial^{x}_{ab}\partial^{x}_{cd}V_y\,\Psi\big)-(x\leftrightarrow y)\Big).$$

Milestone: the strong-coupling case

If every $V_z$ depends only on $h(z)$, then $\{H_x,H_y\}=0$ identically.

Goal: lattice constraints are second class

If the symmetric part of $\partial V_y/\partial h_{ab}(x)$ is nonzero at a physical $h$, for some $x\neq y$, then there is a point of the constraint surface over $h$ at which $\{H_x,H_y\}\neq0$.

Every finite-difference curvature couples neighbouring sites, so the goal applies to every such discretization. It is the weakest statement that the discretized constraint algebra is inconsistent, and it holds uniformly in the discretization.

Stronger targets

• The limit form $\hbar\to0$, as a Tendsto statement.
• The same results with the Laplace–Beltrami ordering of the kinetic term on the six-dimensional fibre of symmetric matrices, and an explicit formula for the difference between the two orderings.
• A potential realized as the scalar curvature of a smooth metric field on a coordinate patch, computed from Christoffel symbols, with its scaling law $R[sh]=R[h]/s$ for constant $s>0$.
• The momentum constraints (Kiefer, eq. (8)).
• Open as far as the drafter could determine. Fix a cubic lattice of spacing $\varepsilon$ and a standard finite-difference scalar curvature. Determine the limit $\varepsilon\to0$ of the suitably rescaled commutator $[\widehat{\mathcal H}_x,\widehat{\mathcal H}_y]$, and decide whether it reproduces the continuum Dirac algebra $\{H(x),H(y)\}=(h^{ab}H_b(x)+h^{ab}H_b(y))\,\partial_a\delta(x,y)$ or leaves an anomaly. Give the anomaly explicitly if there is one. This is the metric-variable analogue of the question Loll raised.

Significance

The signature theorem is the mathematical content behind two physical facts: the hyperbolic character of the Wheeler–DeWitt equation, and the instability of the conformal mode (the "conformal factor problem" of Euclidean quantum gravity). DeWitt's cone form identifies the local volume as an intrinsic clock. On this rests the reading of the equation as a wave equation in superspace, with $\tau$ as time. The conformal-sector reduction shows explicitly how the timelike direction appears in the operator, with the sign opposite to the traceless modes. The WKB identity is the precise sense in which the quantum constraint contains classical general relativity: its leading order is the Hamilton–Jacobi form of the Einstein constraint (Peres 1962; Kiefer, eq. (10)), and its next order is the one used in derivations of the Schrödinger equation from quantum gravity.

All of these are classical computations. The drafter knows of no machine-checked version. A formalization fixes conventions that the literature handles loosely:

• the normalization of $G_{abcd}$;
• the treatment of symmetric versus independent metric components;
• the ordering of operators.

It does so with genuine derivatives in place of formal symbols.

The constraint-algebra part turns a phenomenon described qualitatively in the literature into a theorem with exact hypotheses. Lattice constraints are second class as soon as curvature couples sites, and the quantum commutator is given in closed form. It also isolates precisely what a consistent discretization would have to cancel. The continuum-limit target addresses an open question in canonical quantum gravity.

Difficulty

The supermetric statements are finite-dimensional, but none is a single computation. The signature requires a positivity argument for $\operatorname{tr}\big((h^{1/2}ph^{1/2})^2\big)$ on an $h$-traceless subspace. The cone form requires separating the trace part of a velocity in a non-orthonormal frame.

The analytic targets require second derivatives of compositions through the determinant and the matrix inverse. The derivative of $\det$ at $h$ in the direction of a single entry is $\det h\,(h^{-1})_{ba}$, and the derivative of $h^{-1}$ produces terms like $h^{-1}E_{ab}h^{-1}$; a sign or index slip changes the constant $7$. Treating the nine entries as independent coordinates, rather than the six symmetric ones, changes the numerical coefficients; the conventions below fix this.

For the constraint algebra, the quantum commutator involves up to fourth derivatives of $\Psi$, which cancel only by the symmetry of mixed partials. The classical goal needs a point on the constraint surface where the bracket is nonzero. Each constraint fixes the value of an indefinite quadratic form in the momenta, and the bracket is linear in them, so the proof must use the Lorentzian signature to show that the bracket is not constant on that quadric.

A naive formalization that replaces $\partial_{ab}$ by an abstract linear map reduces every target to ring arithmetic, and is ruled out by the definitions.

Formalization scope

• Definitions (module Def_WheelerDeWittSuperspace):
  • metric components as Fin 3 → Fin 3 → ℝ, so that configuration space X → Fin 3 → Fin 3 → ℝ with X a Fintype is a normed space;
  • matrices via Matrix.of;
  • $\partial_{ab}(x)$ as fderiv ℝ Ψ h applied to the coordinate direction of $h_{ab}(x)$;
  • $\sqrt h$ as Real.sqrt of the determinant;
  • the operator with the supermetric on the left.
• Conventions:
  • all nine metric entries are independent coordinates, and statements that need symmetry assume it at the evaluation point (Matrix.PosDef includes symmetry);
  • lattice cell volume equal to $1$;
  • vacuum (no matter term).
• Not formalized; the potential is an interface: the potential $R$ is supplied data on configurations and sites, and every target holds for all such $R$. The continuum limit of the lattice, a Hilbert-space domain for $\widehat{\mathcal H}$, regularization of coincident derivatives in the continuum, and existence of solutions are outside the mission and must not be inferred from it.
• Trivial cases to rule out:
  • the WKB milestone must hold for every $C^2$ phase $S$, not only for $\Psi=0$ or constant $S$;
  • the goal must exhibit a point on the full constraint surface, with every $H_z$ vanishing, not merely a point where the bracket is nonzero;
  • the dependence hypothesis is on the symmetric part, because antisymmetric metric directions are invisible to $G$.
• Phase-space convention: the bracket is the canonical one on all nine components per site. The symmetric reduction changes off-diagonal normalizations but not the first-class property.
• Welcome contributions: the stronger targets, a matter field with its energy density, and minisuperspace reductions (e.g. homogeneous isotropic metrics $h=a^2\delta$) derived from the operator here rather than postulated.

Selected references

• B. S. DeWitt, Quantum Theory of Gravity. I. The Canonical Theory, Phys. Rev. 160 (1967), 1113–1148. https://doi.org/10.1103/PhysRev.160.1113
• C. Kiefer, Quantum Geometrodynamics: whence, whither?, Gen. Relativ. Gravit. 41 (2009), 877–901. https://arxiv.org/abs/0812.0295
• A. Peres, On Cauchy's problem in general relativity – II, Nuovo Cimento 26 (1962), 53–62. https://doi.org/10.1007/BF02754342
• C. Kiefer, Quantum Gravity, 3rd ed., Oxford University Press (2012), Chapter 5. https://doi.org/10.1093/acprof:oso/9780199585205.001.0001
• R. Loll, Discrete approaches to quantum gravity in four dimensions, Living Rev. Relativ. 1 (1998), 13, Section 2.12. https://arxiv.org/abs/gr-qc/9805049
• R. Loll, On the diffeomorphism-commutators of lattice quantum gravity, Class. Quantum Grav. 15 (1998), 799–809. https://arxiv.org/abs/gr-qc/9708025
• P. Renteln, Some results of SU(2) spinorial lattice gravity, Class. Quantum Grav. 7 (1990), 493–502.
• M. Bander, Hamiltonian lattice gravity. Deformations of discrete manifolds, Phys. Rev. D 36 (1987), 2297. https://doi.org/10.1103/PhysRevD.36.2297
• R. Gambini, J. Pullin, Canonical quantization of general relativity in discrete space-times, 2002. https://arxiv.org/abs/gr-qc/0206055
• B. Dittrich, Diffeomorphism symmetry in quantum gravity models, 2008. https://arxiv.org/abs/0810.3594
• B. Bahr, B. Dittrich, (Broken) Gauge symmetries and constraints in Regge calculus, 2009. https://arxiv.org/abs/0905.1670
• C. J. Isham, Some quantum field theory aspects of the superspace quantization of general relativity, Proc. R. Soc. Lond. A 351 (1976), 209.
• K. Pilati, Strong-coupling quantum gravity. I. Solution in a particular gauge, Phys. Rev. D 26 (1982), 2645. https://doi.org/10.1103/PhysRevD.26.2645
• H. W. Hamber, R. M. Williams, Discrete Wheeler–DeWitt equation, 2011. https://arxiv.org/abs/1109.2530

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 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