All missions

Motivation

Twin-width was introduced by Bonnet, Kim, Thomassé and Watrigant (J. ACM 69(1), Article 3, 2021) as a graph parameter under which first-order model checking is fixed-parameter tractable when a contraction sequence is given. Its interest lies in the classes it covers at once: planar and, more generally, $K_t$-minor-free graphs, bounded-degree grids, unit ball graphs of bounded clique number, and the classes of bounded rank-width or clique-width. These are the classical dense-graph width measures, for which FO (indeed MSO$_1$) model checking was already known to be tractable through Courcelle–Makowsky–Rotics.

This mission formalizes the link to the dense width measures, stated in the paper through boolean-width (Bui-Xuan, Telle and Vatshelle, Theor. Comput. Sci. 412(39), 2011). It is known that $\operatorname{boolw}(G)\le\operatorname{modw}(G)\le\operatorname{cw}(G)\le 2^{\operatorname{rw}(G)+1}-1$ (Vatshelle's PhD thesis, Chapter 4), so a bound on twin-width in terms of boolean-width shows that bounded twin-width captures bounded rank-width, clique-width, module-width and boolean-width simultaneously.

Setting

Let $G$ be a finite simple graph on a vertex set $V$.

Two vertex sets $X,Y\subseteq V$ are homogeneous if either all pairs $(x,y)\in X\times Y$ are edges or none is. For a partition $\mathcal P$ of $V$, a part $X$ has red degree equal to the number of other parts $Y\ne X$ that are not homogeneous to $X$; $\mathcal P$ is a $d$-partition if every part has red degree at most $d$. The graph $G$ has twin-width at most $d$, written $\operatorname{tww}(G)\le d$, if there are partitions $\mathcal P_0,\dots,\mathcal P_N$ of $V$ with $\mathcal P_0$ the partition into singletons, $\mathcal P_N$ having at most one part, each $\mathcal P_{i+1}$ obtained from $\mathcal P_i$ by merging two parts, and every $\mathcal P_i$ a $d$-partition. This is the paper's partition form (p. 3:32) of its definition through trigraphs and red edges (pp. 3:11–3:12).

A decomposition tree of $G$ is a rooted binary tree $T$, every internal node having exactly two children, whose leaves are in one-to-one correspondence with $V$. Each edge $e$ of $T$ lies above exactly one rooted subtree and induces a cut $P_e=(A_e,B_e)$ of $V$: $A_e$ is the set of leaf labels of that subtree and $B_e=V\setminus A_e$. For disjoint $A,B$ write

$$\nu_G(A,B)=\bigl|\{N(S)\cap B: S\subseteq A\}\bigr|,$$

the number of different neighbourhoods in $B$ of subsets of $A$, the empty subset included. The boolean-width of the cut is $\log_2\nu_G(A,B)$, the boolean-width of $T$ is its maximum over the edges of $T$, and $\operatorname{boolw}(G)$ is the minimum over all decomposition trees. In Lean, nbhdCount G A B is $\nu_G(A,B)$, and BoolWidthLE G N states that some decomposition tree has $\nu_G(A_e,B_e)\le N$ on every edge, so $\operatorname{boolw}(G)\le k$ is BoolWidthLE G (2^k).

Formalization targets

Goal: Theorem 4.2 (p. 3:14)

Every graph with boolean-width $k$ has twin-width at most $2^{k+1}-1$. With $N=2^{k}$, the integer neighbourhood count,

$$\operatorname{BoolWidthLE}(G,N)\ \Longrightarrow\ \operatorname{tww}(G)\le 2N-1 .$$

Milestones (proof of Theorem 4.2, p. 3:14)

1. A graph with at most $N$ vertices has $\operatorname{tww}(G)\le N$.
2. A rooted binary tree with more than $2N$ leaves ($N\ge1$) has a rooted subtree below some edge with between $N+1$ and $2N$ leaves.
3. If $\nu_G(A,B)\le N$ and $|A|\ge N+1$, two distinct vertices of $A$ have the same neighbourhood in $B$.
4. If $(A,B)$ partitions $V$, $|A|\le 2N$, and $u\ne v\in A$ have the same neighbourhood in $B$, then contracting $u$ and $v$ yields a $(2N-1)$-partition.

Significance

The theorem places the classes of bounded boolean-width, and therefore of bounded clique-width and rank-width, inside the classes of bounded twin-width, with a single-exponential bound. Combined with the paper's model-checking algorithm, it recovers tractability of FO model checking on these classes once a contraction sequence is computed, and it situates twin-width as a common generalization of the dense width measures and of sparse classes such as $K_t$-minor-free graphs.

No machine-checked version of twin-width or boolean-width is known to exist; neither notion is in Mathlib. The mission produces Lean definitions of twin-width in partition form, of decomposition trees and of the neighbourhood count behind boolean-width, together with the four combinatorial steps the paper's proof states explicitly. The definitions are shared, in identical form, with the other missions of this series on the same paper.

Difficulty

The first three milestones are elementary: a counting bound on contraction sequences, a walk down a binary tree, and a pigeonhole argument. The fourth is a direct count of non-homogeneous parts.

The difficulty is the iteration. After the first contraction the leaves of the updated tree are contracted vertices, so "the same neighbourhood in $B_e$" must be read as homogeneity to all of $B_e$ for a set of vertices, and the boolean-width bound of the cuts must be re-established for sets rather than single vertices. The paper asserts the invariant that the contractions never create a red component of more than $2^{k+1}$ vertices without proving it. A complete proof of the goal therefore has to supply an invariant, carried through all $|V|-1$ contractions, that keeps every part's red degree below $2N-1$. The naive repetition of the first step does not by itself control red edges between previously contracted parts.

Formalization scope

Twin-width is the predicate TwinWidthLE G d, never a numerical infimum, so a junk value of an empty or unbounded infimum cannot make the goal trivial. A contraction sequence must merge exactly two parts at each step and start from singletons; it cannot jump to one part. Homogeneity counts all pairs between two parts, in both of its alternatives. Boolean-width is bounded on every edge of the decomposition tree, not only at the root, and the count runs over neighbourhoods of all subsets of $A_e$, not only of single vertices. The bound $2N-1$ depends only on $N$, not on the graph.

Boolean-width is kept as the integer count $N=2^{\operatorname{boolw}(G)}$; since $\operatorname{boolw}(G)=k$ means that the least admissible count is $2^k$, the Lean goal for this $N$ is exactly the printed theorem. Subtractions $2N-1$ are in $\mathbb N$ and exact where used. Graphs live on a Fintype vertex type with decidable equality and decidable adjacency. A graph on the empty vertex set has no decomposition tree; the goal is silent about it, and it has twin-width $0$. No hypothesis is added to any statement relative to the page except $N\ge 1$ in milestone 2, which the page has implicitly ($2^k\ge1$) and without which the conclusion is impossible.

The definitions needed are the setting module TwinWidthI.BoolWidth.Setting: merge steps, homogeneity, $d$-partitions, twin-width, decomposition trees (DTree), the count $\nu_G$ and BoolWidthLE. Proofs of the milestones, a proof of the goal, and lemmas towards the iteration invariant are welcome.

Selected references

• É. Bonnet, E. J. Kim, S. Thomassé and R. Watrigant, Twin-width I: Tractable FO Model Checking, J. ACM 69(1), Article 3, 2021. https://doi.org/10.1145/3486655
• B.-M. Bui-Xuan, J. A. Telle and M. Vatshelle, Boolean-width of graphs, Theoretical Computer Science 412(39), 5187–5204, 2011. https://doi.org/10.1016/j.tcs.2011.05.022
• M. Vatshelle, New Width Parameters of Graphs, PhD thesis, University of Bergen, 2012 (reference [39] of Bonnet et al.; source of the chain boolw ≤ modw ≤ cw ≤ 2^{rw+1} − 1).

Motivation

A risk-controlling prediction set is a set-valued predictor $\mathcal T$ that, with probability at least $1-\delta$ over a calibration sample, has expected loss at most a target level $\alpha$. Bates, Angelopoulos, Lei, Malik and Jordan (arXiv:2101.02703, J. ACM 2021) build such sets for any black-box predictor and any bounded loss by a procedure called upper confidence bound (UCB) calibration: for each value of a tuning parameter $\lambda$, compute from the calibration data an upper confidence bound $\widehat R^+(\lambda)$ for the risk $R(\lambda)$, and pick the smallest $\lambda$ beyond which all these bounds sit below $\alpha$. The guarantee of the procedure (their Theorem 1) holds for any choice of the pointwise bound, so the size of the resulting sets is governed by how tight that bound is.

The paper compares several such bounds: Hoeffding, Bentkus, the empirical Bernstein bound of Maurer and Pontil, and a bound adapted from the hedged capital confidence interval of Waudby-Smith and Ramdas (arXiv:2010.09686). The last one, the Waudby-Smith–Ramdas (WSR) bound, adapts to the unknown variance of the loss and is the one the authors recommend for non-binary losses; their experiments use it throughout. Proposition 5 of the paper states that the WSR bound is a valid $(1-\delta)$ upper confidence bound for the mean of a $[0,1]$-valued loss. This mission formalizes that proposition.

Timeline: Ville (1939) proved the maximal inequality for nonnegative supermartingales that underlies all betting-based confidence bounds. Waudby-Smith and Ramdas (2020) introduced the hedged capital process and its confidence sequences for bounded means. Bates et al. (2021) extracted the one-sided, fixed-sample variant stated as Proposition 5, with the explicit betting fractions $\nu_i$ below.

Setting

Fix the tuning parameter $\lambda$; it is dropped from the notation. The calibration losses $L_1, \dots, L_n$ are independent and identically distributed with law $Q$ on $[0,1]$ (the loss is nonnegative and, by the standing assumption of §3.1 of the paper, bounded by one), and their mean is the risk

$$R = \int x \, dQ(x).$$

Fix a level $\delta \in (0,1)$. For $i \ge 0$ define the running mean and variance

$$\hat\mu_i = \frac{1/2 + \sum_{j=1}^{i} L_j}{1+i}, \qquad \hat\sigma^2_i = \frac{1/4 + \sum_{j=1}^{i} (L_j - \hat\mu_j)^2}{1+i},$$

so $\hat\sigma^2_0 = 1/4$, and for $i \ge 1$ the betting fraction

$$\nu_i = \min\left\{1, \sqrt{\frac{2\log(1/\delta)}{n\,\hat\sigma^2_{i-1}}}\right\},$$

which depends only on $L_1, \dots, L_{i-1}$. For a candidate mean $R' \in \mathbb R$, the capital process is

$$\mathcal K_i(R') = \prod_{j=1}^{i} \bigl\{1 - \nu_j (L_j - R')\bigr\}, \qquad \mathcal K_0(R') = 1,$$

the wealth of a gambler who, starting with one unit, bets the fraction $\nu_j$ of their wealth against the hypothesis that the mean is $R'$. The WSR bound is

$$\widehat R^+_{\mathrm{WSR}} = \inf\Bigl\{R' \ge 0 : \max_{i=1,\dots,n} \mathcal K_i(R') > \frac1\delta\Bigr\},$$

the smallest candidate mean the gambler has discredited by multiplying their wealth by more than $1/\delta$. In Lean these are obs, muHat, sigmaSqHat, nu, K and wsrUCB in the namespace RiskControl.WSR, and $\mathcal F_i = \sigma(L_1,\dots,L_i)$ is filt n.

Formalization targets

Goal: Proposition 5 (p. 7)

For $n \ge 1$ and $\delta \in (0,1)$,

$$\mathbb P\bigl(\widehat R^+_{\mathrm{WSR}} < R\bigr) \le \delta, \qquad\text{that is}\qquad \mathbb P\bigl(R \le \widehat R^+_{\mathrm{WSR}}\bigr) \ge 1-\delta,$$

the probability being the product law $Q^{\otimes n}$ of the sample.

Milestones (proof of Proposition 5, p. 26)

1. Nonnegative factors. $\nu_i \in [0,1]$, and for losses in $[0,1]$ and $R \in [0,1]$, $1 - \nu_j(L_j - R) \ge 0$.
2. Martingale. At the true mean, $i \mapsto \mathcal K_{\min(i,n)}(R)$ is a martingale for $(\mathcal F_i)$:

$$\mathbb E\bigl[\mathcal K_i(R) \mid \mathcal F_{i-1}\bigr] = \mathcal K_{i-1}(R).$$

3. Ville's inequality (referenced, already proved on the platform): a nonnegative supermartingale started at most $1$ exceeds $1/\delta$ with probability at most $\delta$.
4. Monotonicity. For losses in $[0,1]$, $R' \mapsto \mathcal K_i(R')$ is nondecreasing on $[0,\infty)$.
5. Inclusion. For losses in $[0,1]$ and $R \ge 0$, $\widehat R^+_{\mathrm{WSR}} < R$ implies $\max_{i \le n} \mathcal K_i(R) \ge 1/\delta$.

Significance

The result is the validity half of the WSR bound: with it, UCB calibration (Theorem 1 of the paper) applied to $\widehat R^+_{\mathrm{WSR}}$ gives the paper's Theorem 4, a risk-controlling prediction set built from the variance-adaptive bound that the experiments of the paper use for classification, segmentation and protein-structure tasks. It is also a self-contained instance of the betting approach to confidence bounds for bounded means, which now underlies a family of nonasymptotic, variance-adaptive procedures in statistics and machine learning.

The proposition is proved in the paper (p. 26), following the proof of Theorem 4 of Waudby-Smith and Ramdas. To our knowledge neither it nor the hedged capital construction has a machine-checked proof. The mission produces one: a Lean statement of the WSR bound with its exact constants, and a proof that reuses the platform's Ville inequality. The capital process and its martingale property are the reusable part; the same construction with other predictable betting fractions gives other confidence bounds.

Difficulty

The bound is not obtained by inverting a tail inequality for the empirical mean, so Hoeffding- or Bernstein-type arguments do not apply. The probabilistic core is the martingale step: one must show that $\nu_i$ is a measurable function of $L_1,\dots,L_{i-1}$ only (it involves $\hat\sigma^2_{i-1}$, which involves every $\hat\mu_j$ for $j < i$), and compute a conditional expectation on the product space $\mathbb R^n$ using independence of the coordinates. Ville's inequality then holds only at the true mean $R$, a single unknown point, while $\widehat R^+_{\mathrm{WSR}}$ is an infimum over all candidate means; the passage between them needs the monotonicity of $\mathcal K_i$ in its argument, which fails without the bound $L_j \le 1$ (a factor can turn negative). A union bound over candidate means, the first idea, gives nothing here.

Formalization scope

The sample is $\omega : \mathrm{Fin}\,n \to \mathbb R$ under Measure.pi (fun _ => Q), with $L_j = \omega(j-1)$ for $1 \le j \le n$ (1-based indices as on the page). $Q$ is the law of the loss $L(Y, \mathcal T_\lambda(X))$ for the fixed $\lambda$, assumed concentrated on $[0,1]$: this is the §3.1 standing assumption together with $L \ge 0$. The goal adds two hypotheses implicit on the page: $n \ge 1$ and $0 < \delta < 1$ (so that $\log(1/\delta) > 0$). The empty sum gives $\hat\sigma^2_0 = 1/4$; "$\max_{i=1,\dots,n} \mathcal K_i > 1/\delta$" is written as an existential over $i \in \{1,\dots,n\}$; the infimum is an extended-real infimum, equal to $+\infty$ when no candidate qualifies. The failure probability is bounded through the outer measure of $\{\widehat R^+_{\mathrm{WSR}} < R\}$, which equals the page's statement for a measurable event. The martingale is extended constantly past time $n$ so that it is indexed by $\mathbb N$.

Two printed slips are corrected: the proof's "then $P(\max_i \mathcal K_i \ge 1/\delta)$" (a stray $P$) is stated as the event, and "increasing in $R$" is stated as nondecreasing on $R \ge 0$.

The infimum must not be a real infimum: a real sInf of an empty set is $0$, which would make $\widehat R^+_{\mathrm{WSR}} < R$ true for every positive mean and the goal false; with the extended-real infimum the empty case gives $+\infty$, and the goal is the paper's proposition, not a vacuous one.

Contributions welcome: the measurability of $\nu_i$ with respect to $\mathcal F_{i-1}$, conditional expectations of products of independent coordinates under Measure.pi, and a finite-horizon form of Ville's inequality (Mathlib's Doob maximal inequality MeasureTheory.maximal_ineq is an alternative route).

Selected references

• S. Bates, A. Angelopoulos, L. Lei, J. Malik, M. I. Jordan, Distribution-Free, Risk-Controlling Prediction Sets, J. ACM 68(6), 2021. arXiv:2101.02703v3
• I. Waudby-Smith, A. Ramdas, Estimating means of bounded random variables by betting, J. R. Stat. Soc. B, 2024. arXiv:2010.09686
• J. Ville, Étude critique de la notion de collectif, Gauthier-Villars, 1939.
• A. Maurer, M. Pontil, Empirical Bernstein Bounds and Sample Variance Penalization, COLT 2009. arXiv:0907.3740

Motivation

Loop quantum gravity (LQG) is a proposal for a quantum theory of the gravitational field in which space itself is built from discrete quanta. Its kinematics rests on two mathematical facts that C. Rovelli's review Loop quantum gravity: the first 25 years (Class. Quantum Grav. 28 (2011) 153002, arXiv:1012.4707) singles out. First, the spin–geometry theorem of Penrose, in the extended form based on a theorem of Minkowski (1897): the angular-momentum vectors attached to the links around a node of a spin network, once they satisfy the closure (gauge-invariance) relation, are exactly the data of a flat polyhedron, so every quantum of space carries a geometry (§2.1). Second, the discreteness of geometric spectra: areas take values $8\pi\gamma\hbar G\sum_n\sqrt{j_n(j_n+1)}$ with half-integer spins $j_n$, with a strictly positive area gap (§2.1, §2.3, §4.3), which the review calls "the most solid result in loop gravity".

Timeline. Minkowski proved the existence and uniqueness of a convex polyhedron with prescribed face normals and areas in 1897. Penrose introduced spin networks and the spin–geometry theorem around 1971. The discreteness of area and volume in LQG was found by Rovelli and Smolin (1995), with the full area spectrum computed by Ashtekar–Lewandowski and others in 1995–1997.

Setting

Work in Euclidean three-space $\mathbb E^3=\mathbb R^3$ with its standard inner product $\langle\cdot,\cdot\rangle$. Given finitely many vectors $u_1,\dots,u_v\in\mathbb E^3$ and real numbers $h_1,\dots,h_v$, the half-space polyhedron is

$$P(u,h)=\{x\in\mathbb E^3:\ \langle u_l,x\rangle\le h_l\ \text{for all } l\},$$

and its $l$-th face is $F_l=P(u,h)\cap\{x:\langle u_l,x\rangle=h_l\}$. The area of a set lying in a plane orthogonal to a nonzero vector $u$ is its two-dimensional Lebesgue measure, computed as the measure of its orthogonal projection onto the plane $u^\perp$. For a nonzero vector $n$, $\hat n=n/\|n\|$ is its direction.

On the quantum side, a node of a spin network with $v$ links carries vectors $\vec L_1,\dots,\vec L_v$ (the left-invariant derivative operators), subject to the closure relation $\sum_l \vec L_l=0$ (eq. (6)). The review's classical content is: the $\vec L_l$ behave as the area-weighted normals of a polyhedron, whose face areas are $|\vec L_l|$ and whose volume (for $v=4$) is given by the triple product (eq. (10)). Spins $j\in\{0,\tfrac12,1,\tfrac32,\dots\}$ label links; the quantity $\sqrt{j(j+1)}$ is the square root of the $SU(2)$ Casimir. The area spectrum (eq. (26)) is the set of numbers $8\pi\gamma\hbar G\sum_n\sqrt{j_n(j_n+1)}$ over finite families of spins, with $\gamma$ the Barbero–Immirzi parameter, $\hbar$ the reduced Planck constant and $G$ Newton's constant.

Formalization targets

Goal: Minkowski's theorem in the form of the spin–geometry theorem

For nonzero $n_1,\dots,n_v\in\mathbb E^3$ with pairwise distinct directions $\hat n_l$, spanning $\mathbb E^3$, and with $\sum_l n_l=0$:

$$\exists\,h:\ P(\hat n,h)\ \text{bounded, with nonempty interior, and}\ \operatorname{area}(F_l)=\|n_l\|\ \ \forall l,$$

and any two such polyhedra are translates of each other.

Milestones (in the order of the review)

1. Eq. (6), closure: for a bounded polyhedron with nonempty interior and distinct unit normals $u_l$, $\sum_l \operatorname{area}(F_l)\,u_l=0$.
2. Eq. (10), tetrahedron volume: with face area vectors $L_1,L_2,L_3$ of three faces through a vertex, $V^2=\tfrac29\,|L_1\cdot(L_2\times L_3)|$.
3. Eq. (13), area gap: $\min\{\sqrt{j(j+1)}: j\in\{\tfrac12,1,\tfrac32,\dots\}\}=\tfrac{\sqrt3}{2}$.
4. Eq. (18), area gap in physical units: the least positive element of the area spectrum is $8\pi\hbar G\gamma\,\tfrac{\sqrt3}{2}$.
5. Eq. (26), discreteness: for $\gamma,\hbar,G>0$ the area spectrum has only finitely many elements below any bound.

Significance

The goal theorem is the precise mathematical content behind the statement that "the algebraic structure of the momentum operators determines the existence of a metric at each node and therefore equips each quantum of space with a geometry" (§2.1). Its necessity half (milestone 1) is the classical counterpart of the gauge-invariance constraint (6); its sufficiency and uniqueness halves are what allow LQG states to be read as quantum polyhedra and underlie the "twisted geometry" and polyhedral-volume constructions. The spectral milestones encode the review's discrete-geometry claims in the elementary, operator-free form in which they are stated in eqs. (13), (18) and (26).

All statements here are known theorems; none is open. A search of Mathlib (at the revision used to check these statements) found no theory of convex polytopes, facet areas, the Brunn–Minkowski inequality, or Minkowski's theorem for polyhedra.

Difficulty

The necessity direction (closure) is a divergence-theorem or projection argument, but requires relating the facets of an H-described polytope to its boundary. The existence direction of Minkowski's theorem is a variational argument (maximize volume subject to a linear constraint on support numbers) whose difficulty lies in showing that the optimum has all prescribed faces with positive area; uniqueness is classically deduced from the equality case of the Brunn–Minkowski (or Minkowski mixed-volume) inequality. The spectral milestones are elementary.

Formalization scope

Lean represents $\mathbb E^3$ as EuclideanSpace ℝ (Fin 3). A polyhedron is given by a finite family of normals and support numbers (halfspacePolyhedron), faces by polyhedronFace, and face area by planarArea, the Haar (Lebesgue) measure of the orthogonal projection onto the plane orthogonal to the normal, valued in $[0,\infty]$; areas are compared as extended reals so that an infinite area cannot be confused with $0$. Unit normals are obtained as $n/\|n\|$ (unitDir). The cross product is Mathlib's crossProduct transported to EuclideanSpace. Spins are encoded as $k/2$ with $k\in\mathbb N$, and the area spectrum sums over finite multisets of spins.

The goal excludes trivializing readings: the spanning and distinct-direction hypotheses are the classical non-degeneracy conditions of Minkowski's theorem (without them the existence claim is false), and the conclusion demands a bounded polyhedron with nonempty interior, so empty or flat polyhedra do not count. The review's eq. (10) omits numerical constants; the milestone uses the exact Euclidean constant $2/9$. The operator-theoretic statements of the review (spectra of area and volume operators on $L^2(SU(2)^L/SU(2)^N)$) are out of scope; only their stated numerical content is formalized.

Reusable infrastructure: H-polytopes in $\mathbb R^3$, facet areas, the closure identity, and the Brunn–Minkowski equality case. Contributions of general convex-geometry lemmas are welcome.

Selected references

• C. Rovelli, Loop quantum gravity: the first 25 years, Class. Quantum Grav. 28 (2011) 153002. https://doi.org/10.1088/0264-9381/28/15/153002 (arXiv:1012.4707)
• H. Minkowski, Allgemeine Lehrsätze über die konvexen Polyeder, Nachr. Ges. Wiss. Göttingen (1897) 198–219.
• E. Bianchi, P. Doná, S. Speziale, Polyhedra in loop quantum gravity, Phys. Rev. D 83 (2011) 044035. https://arxiv.org/abs/1009.3402
• A. D. Alexandrov, Convex Polyhedra, Springer (2005).

Motivation

The Yukawa potential (or screened Coulomb potential)

$$V_{\mathrm{Yukawa}}(r) = -g^2\,\frac{e^{-\alpha m r}}{r}$$

was introduced by Hideki Yukawa in 1935 to model the short-range nuclear force as the exchange of a massive particle, later identified with the pion. The same profile reappears as the Debye–Hückel screened interaction in plasmas and electrolytes, as the static Green's function of the massive Klein–Gordon (screened Poisson) operator, and as the Newtonian correction in massive-graviton models. The mathematical facts behind these uses are classical, short, and stated in every textbook treatment — which makes them a natural, self-contained target for formalization: each one is an explicit identity of real analysis in three dimensions.

Timeline. Heisenberg (1932–33) proposed a short-range exchange interaction between nucleons; Fermi (1934) introduced exchange of light particles in beta decay; Yukawa (1935, Proc. Phys.-Math. Soc. Japan 17, 48) combined the two ideas, derived the potential above, and predicted a mediating particle of mass about 200 electron masses; the pion was observed in 1947.

Setting

Throughout, $g\in\mathbb R$ is the coupling (amplitude) constant, $\alpha>0$ a scaling constant, $m\ge 0$ the mass of the exchanged particle and $r>0$ the radial distance; $1/(\alpha m)$ is the range. The potential is the function

$$V(r) = -g^2\,\frac{e^{-\alpha m r}}{r}.$$

Points of space are $x\in\mathbb R^3$ with Euclidean norm $|x|$, and the potential of a point source at the origin is $x\mapsto V(|x|)$. The Laplacian $\Delta$ is the usual sum of unmixed second partial derivatives on $\mathbb R^3$. For a uniform, infinitesimally thin spherical shell of radius $R$ with total scaling constant $G$, the potential felt by a point of scaling constant $g$ located at $x$ is

$$V_{\mathrm{shell}}(x) = G\,g\;\frac{1}{4\pi}\int_{S^2}\frac{e^{-\alpha m |x-Ru|}}{|x-Ru|}\,d\sigma(u),$$

the average over the unit sphere $S^2$ (uniform surface measure $\sigma$) of the pair interaction.

Formalization targets

Goal — Fourier transform of the Yukawa potential

For $\alpha m>0$ and every $k\in\mathbb R^3$,

$$\int_{\mathbb R^3} e^{-i k\cdot x}\,V(|x|)\,d^3x \;=\; -g^2\,\frac{4\pi}{|k|^2+(\alpha m)^2}.$$

This is the identity the article's sections Fourier transform and Feynman amplitude rest on: the momentum-space Yukawa potential is the massive propagator $4\pi/(k^2+(\alpha m)^2)$ times $-g^2$.

Milestones (in the order of the article)

1. Negativity and monotonicity — for $g\neq0$, $V<0$ on $(0,\infty)$ and $V$ is strictly increasing there.
2. Massless limit — for $m=0$, $V(r) = -g^2\cdot\frac1r$ (the Coulomb potential).
3. Screened Poisson equation — $\Delta\,V(|x|) = (\alpha m)^2\,V(|x|)$ for $x\neq0$.
4. Inverse Fourier representation — for $x\ne0$, $V(|x|) = \lim_{\Lambda\to\infty} \frac{-g^2}{(2\pi)^3}\int_{|k|<\Lambda} e^{ik\cdot x}\frac{4\pi}{|k|^2+(\alpha m)^2}\,d^3k$.
5. Born amplitude — $\frac{-2\mu}{\hbar^2 q}\int_0^\infty r\,V(r)\sin(qr)\,dr = \frac{2\mu g^2}{\hbar^2[(\alpha m)^2+q^2]}$ for $q>0$.
6. Momentum transfer — $|\vec p-\vec p'| = 2p\sin(\theta/2)$ when $|\vec p|=|\vec p'|=p$ and $\theta$ is the angle between them.
7. Total cross section — $\frac{4\mu^2g^4}{\hbar^4}\int_0^\pi\frac{2\pi\sin\theta\,d\theta}{[(\alpha m)^2+4p^2\sin^2(\theta/2)]^2} = \frac{4\mu^2g^4}{\hbar^4}\,\frac{4\pi}{(\alpha m)^2[(\alpha m)^2+4p^2]}$.
8. Shell, exterior — for $|x|>R$, $V_{\mathrm{shell}}(x) = G g\,\frac{e^{-\alpha m|x|}}{|x|}\,\frac{\sinh(\alpha m R)}{\alpha m R}$.
9. Shell, interior — for $0<|x|<R$, $V_{\mathrm{shell}}(x) = G g\,\frac{e^{-\alpha m R}}{R}\,\frac{\sinh(\alpha m |x|)}{\alpha m |x|}$.

Significance

The results. The Fourier identity is what makes the Yukawa potential the non-relativistic limit of single-meson exchange; milestone 3 identifies it as the Green's function of the screened Poisson operator $-\Delta + (\alpha m)^2$; milestones 5–7 give the Born-approximation scattering amplitude and the closed-form total cross section quoted in quantum mechanics textbooks (e.g. Griffiths); milestones 8–9 are the Yukawa analogue of Newton's shell theorem, whose failure to reduce to a point source of the same strength is the reason massive-graviton models violate the weak equivalence principle.

Formalizing them. All statements are classical and proved on paper. The mission produces machine-checked versions together with reusable infrastructure: three-dimensional Fourier integrals of radial functions, Laplacians of radial functions, spherical averages with respect to the surface measure, and conditionally convergent oscillatory integrals.

Difficulty

The individual computations are short on paper but each crosses a gap in the library. The goal requires reducing a three-dimensional Lebesgue integral of a radial function to a one-dimensional integral (polar coordinates in $\mathbb R^3$), then evaluating $\int_0^\infty e^{-ar}\sin(kr)\,dr$. The inverse transform is not absolutely convergent — $1/(|k|^2+a^2)$ is not integrable on $\mathbb R^3$ — so the naive Lebesgue statement is false (it would assign the value $0$); only the ball-truncated limit is meaningful, and its evaluation needs the improper integral $\int_0^\infty \frac{k\sin(kr)}{k^2+a^2}dk = \frac{\pi}{2}e^{-ar}$. The shell theorem needs the surface measure on $S^2$ and the Archimedes-type change of variables $u\mapsto |x-Ru|$.

Formalization scope

All quantities are real numbers; space is EuclideanSpace ℝ (Fin 3) with Lebesgue measure. The potential is a single definition YukawaPotential.yukawaPotential g α m r; at $r=0$ Lean's division convention gives the junk value $0$, so every statement either restricts to $r>0$ / $x\neq0$ or integrates (where a single point is null). The physical conventions $\alpha>0$, $m\ge0$ (and $m>0$ where the article divides by $\alpha m$) are explicit hypotheses. The Fourier transform uses the convention $\hat V(k)=\int e^{-ik\cdot x}V$, $V=(2\pi)^{-3}\int e^{ik\cdot x}\hat V$; the inverse is stated as a limit over balls. The shell potential averages over the unit sphere with Mathlib's Measure.toSphere (uniform surface measure); since it is an average, its normalisation is irrelevant. The Laplacian is Mathlib's Laplacian.laplacian on inner-product spaces. Physical constants $\mu,\hbar$ in milestones 5 and 7 are arbitrary reals: the identities hold without sign assumptions on them.

Out of scope: the historical mass estimate of the pion, the heuristic wave-equation derivation of the photon/pion dispersion relations, the perturbative asymptotic expansions of Schrödinger eigenvalues and Regge trajectories (stated in the source only up to unspecified $\mathcal O(K^{-7})$ and "$\cdots$" terms), and the $m\to0$ limits of the shell formulas.

Contributions welcome: polar-coordinate integration for radial functions on $\mathbb R^3$, spherical-average lemmas, and the improper integrals above as standalone lemmas.

Selected references

• H. Yukawa, On the interaction of elementary particles, Proc. Phys.-Math. Soc. Japan 17, 48 (1935). https://doi.org/10.11429/ppmsj1919.17.0_48
• D. J. Griffiths, Introduction to Quantum Mechanics, Cambridge University Press (2017), p. 415.
• R. P. Feynman, R. B. Leighton, M. Sands, The Feynman Lectures on Physics, Vol. II, Ch. 28 (1964). https://www.feynmanlectures.caltech.edu/II_28.html
• K. McDonald, A Naïve Estimate of the Coupling Constant in Yukawa Theory (1984/2021). http://kirkmcd.princeton.edu/examples/yukawa.pdf
• Wikipedia, Yukawa potential, revision 1371658231. https://en.wikipedia.org/w/index.php?title=Yukawa_potential&oldid=1371658231

Motivation

In the usual textbook presentation, quantum theory starts from postulates that have no obvious operational meaning: states are density operators on a complex Hilbert space, measurements are positive operators, and probabilities are given by the trace formula $p=\mathrm{tr}(\hat A\hat\rho)$. In Quantum Theory From Five Reasonable Axioms (Hardy 2001), Lucien Hardy asks whether this structure can instead be derived from simple statements about preparations, transformations and measurements, in the same way that classical probability theory can be set up by pure thought. He proposes five axioms (probabilities, simplicity, subspaces, composite systems, continuity) and argues that they single out finite- and countably-infinite-dimensional quantum theory. Dropping a single word, "continuous" in Axiom 5, leaves classical probability theory instead.

The paper is one of the starting points of the operational or generalized probabilistic theory (GPT) approach to the foundations of quantum mechanics. It was followed by reconstructions that replace the simplicity axiom, e.g. Dakić–Brukner 2009, Masanes–Müller 2011 and Chiribella–D'Ariano–Perinotti 2011.

Setting

A system is described by two integers. The dimension $N$ is the maximum number of states that can be distinguished in a single-shot measurement. The number of degrees of freedom $K$ is the minimum number of probability measurements needed to determine the state. The state is the vector $p=(p^1,\dots,p^K)\in\mathbb R^K$ of the probabilities of $K$ fiducial measurements. States are not assumed normalized: the null state $p=0$ (no system present) is allowed. The set $S$ of allowed states is convex, and its pure states are its extremal points other than $0$.

The five axioms are:

1. Probabilities. Relative frequencies converge to the same limit for every ensemble prepared by a given preparation.
2. Simplicity. $K=K(N)$ is a function of $N=1,2,\dots$, and for each $N$ it takes the minimum value consistent with the axioms.
3. Subspaces. A system whose state is constrained to an $M$-dimensional subspace behaves like a system of dimension $M$.
4. Composite systems. A composite of systems $A$ and $B$ has $N=N_AN_B$ and $K=K_AK_B$.
5. Continuity. Between any two pure states there is a continuous reversible transformation.

A probability theory can be summarized by its signature $x=(x_1,x_2,\dots)$, defined through

$$K=Nx_1+\tfrac1{2!}N(N-1)x_2+\tfrac1{3!}N(N-1)(N-2)x_3+\cdots=\sum_{k\ge1}\binom Nk x_k .$$

Classical probability theory has $x=(1,0,0,\dots)$ and $K=N$. Complex quantum theory has $x=(1,2,0,\dots)$ and $K=N^2$. Real and quaternionic quantum theory have $x=(1,1,0,\dots)$ and $x=(1,4,0,\dots)$.

Formalization targets

Goal: $K(N)=N^r$

Section 8.1 shows that Axiom 3 forces $K(N+1)\ge K(N)+1$, and Axiom 4 forces $K(N_AN_B)=K(N_A)K(N_B)$. The goal theorem is the purely arithmetic consequence (Eq. (57)):

$$K(N+1)\ge K(N)+1\ \text{ and }\ K(N_AN_B)=K(N_A)K(N_B)\ \ (N,N_A,N_B\ge1)\quad\Longrightarrow\quad \exists r\in\{1,2,3,\dots\}:\ K(N)=N^r\ \ \forall N\ge1 .$$

Milestones

The milestones follow the paper's own steps, in the paper's numbering:

• Appendix 2: a strictly increasing, completely multiplicative $K$ on the positive integers satisfies $K(n)=n^\alpha$. Section 8.1: if every $n^\alpha$ is an integer, then $\alpha$ is a positive integer.
• Section 6.6 / Appendix 1: measured probabilities are linear in the state, $p_{\rm meas}=r\cdot p$. Section 6.7: transformations act as matrices, $p\mapsto Zp$. Section 7: reversible transformations send pure states to pure states.
• Section 4 / 8.5: in classical probability theory the pure states are exactly the $N$ basis states, and no continuous path of pure states joins two distinct ones. The equations $\sum_k(p^k)^2=1$, $0\le p^k\le1$, $\sum_kp^k=1$ force a basis vector.
• Sections 5 and 8.1: the signatures of the classical, quantum, real, quaternionic and $K=N^3$ theories, and the failure of $K=K_AK_B$ for real (too many) and quaternionic (too few) composites.
• Section 5: the $N^2$ projectors $|n\rangle\langle n|$, $|mn\rangle_x\langle mn|$, $|mn\rangle_y\langle mn|$ are linearly independent over $\mathbb R$ and span the Hermitian operators.
• Sections 5 and 8.6 ($N=2$): the overlap formula (35) for $c$; $\det D>0 \iff c_-<c<c_+$; the decomposition $r^TDr'=\vec v^{\,T}A\vec v'+\mu\mu'/2$; $A$ positive definite $\iff c_-<c<c_+$; the Bloch matrix (87).
• Section 8.7 ($N=3$): the $9\times9$ matrix $D_{ij}=\mathrm{tr}(\hat P_i\hat P_j)$ with $h=1/2$, $q=1/4$.

Significance

The goal is the step at which the two structural axioms (subspaces and composites) cut the space of possible theories down to a single integer parameter $r$. Combined with Section 8.5, which rules out $r=1$ by continuity, and with the simplicity axiom, it gives $K=N^2$. Everything after that in the paper (the Bloch sphere, general $N$, the trace formula, complete positivity) is carried out inside the $K=N^2$ case. The milestones on signatures make precise in which sense real and quaternionic quantum theory are excluded: their degree-of-freedom counts are not multiplicative under composition.

The paper's argument is informal physics. This mission isolates the mathematically precise statements that the argument relies on, so that they can be proved independently of the physical interpretation. It does not formalize the axioms themselves as a single Lean structure.

Difficulty

The arithmetic goal is an instance of a classical question about monotone completely multiplicative functions. Complete multiplicativity alone fixes $K$ only through its values at the primes, which are a priori unrelated to one another, and monotonicity is the only link between different primes. The step from a real exponent $\alpha$ to an integer exponent is a separate integrality argument that the paper does not spell out. The linearity milestones need care because the hypotheses hold only on a convex set containing $0$, not on all of $\mathbb R^K$. The $N=2$ milestones are explicit but delicate algebra with square roots and boundary cases $a,b\in\{0,1\}$.

Formalization scope

• All theorems live in the namespace HardyFiveAxioms. State vectors are functions Fin K → ℝ. Indices are $0$-based, so the paper's fiducial vector $k$ is index $k-1$.
• $K(N)$ is a function ℕ → ℕ (goal) or ℕ → ℝ (Appendix 2), constrained only at arguments $\ge1$. The value at $0$ is irrelevant.
• The signature is a finite list [x₁, …, x_L], and $\frac1{k!}N(N-1)\cdots(N-k+1)$ is written as the binomial coefficient $\binom Nk$.
• Pure states are Set.extremePoints ℝ S \ {0}. The classical state space is $\{p\ge0,\ \sum_np_n\le1\}$.
• The quantum projectors are explicit matrices vecMulVec v (star v) over ℂ, and the qubit matrices $D$, $C$, $A$ and the roots $c_\pm$ are explicit definitions.
• Axiom 5's "continuous reversible transformation" enters only through the classical milestone, as a continuous path unitInterval → ℝᴺ that stays inside the pure states.
• The goal does not assume the conclusion in disguise. Its hypotheses are the two consequences of Axioms 3 and 4 derived in Section 8.1. It is not vacuous: $K(N)=N^r$ satisfies both hypotheses for every $r\ge1$.

Contributions are welcome on any milestone. The linearity, extreme-point and positive-definiteness lemmas are reusable beyond this mission.

Selected references

• L. Hardy, Quantum Theory From Five Reasonable Axioms, arXiv:quant-ph/0101012v4, 2001. https://arxiv.org/abs/quant-ph/0101012
• B. Dakić, Č. Brukner, Quantum Theory and Beyond: Is Entanglement Special?, 2009. https://arxiv.org/abs/0911.0695
• Ll. Masanes, M. P. Müller, A derivation of quantum theory from physical requirements, New J. Phys. 13, 063001, 2011. https://arxiv.org/abs/1004.1483
• G. Chiribella, G. M. D'Ariano, P. Perinotti, Informational derivation of quantum theory, Phys. Rev. A 84, 012311, 2011. https://arxiv.org/abs/1011.6451

Motivation

Whether the gravitational field must be quantized is a long-standing foundational question. One family of arguments, due to DeWitt (1962) and Eppley and Hannah (1977), claims that consistency alone forces quantization: a classical field coupled to a quantum system would supposedly violate momentum conservation, the uncertainty relations, or the impossibility of superluminal signalling. Albers, Kiefer and Reginatto (Phys. Rev. D 78, 064051 (2008)) dispute this claim. In their Sec. IV they give an explicit counterexample: a hybrid model in which a classical gravitational wave interacts with a quantized massive scalar field. The model is the two-dimensional scalar theory of gravity of Nordström, written in the formalism of ensembles in configuration space.

This mission is the second one on this paper. The first, Albers–Kiefer–Reginatto 2008: Measurement Analysis and Quantum Gravity, formalizes Sec. II (the reduced state of photon 2), Sec. III B and Sec. V, and lists Sec. IV and the appendices as out of scope. This mission covers the explicit non-interacting solution of Sec. IV A and the harmonic-oscillator analogy of Appendix A, which the authors use to interpret it.

Timeline.

• 1912–13: Nordström's scalar theory of gravity.
• 1962: DeWitt's measurement analysis argues that quantizing one system forces quantization of every system it couples to.
• 1977: Eppley and Hannah's gedanken experiment with a classical gravitational wave and a quantum particle.
• 2008: Albers, Kiefer and Reginatto construct a consistent hybrid classical–quantum model and solve it explicitly for $g=0$, and to first order in $g$ for a class of states.

Setting

Ensembles in configuration space. The state of the gravitational field $\phi$ together with the scalar field $\psi$ is a probability functional $P[\phi,\psi,t]$ and a conjugate functional $S[\phi,\psi,t]$. They obey a modified Hamilton–Jacobi equation (37) and a continuity equation (38). The coupling constant is $g$. For $g=0$ the authors use the ansatz $S=S^c[\phi,t]-E^qt$ and $P=P^c[\phi,t]P^q[\psi]$, with Gaussian functionals

$$S^c=\tfrac12\iint\phi_yF_{yz}(t)\phi_z,\qquad P^c=N^c(t)\,e^{-\frac12\iint(\phi_a-\beta_a)K_{ab}(\phi_b-\beta_b)},$$

and a one-particle Gaussian $P^q$ with kernel $G$. Substituting the ansatz yields the kernel equations (43)–(48).

Mode representation. Every kernel is expanded in real orthonormal eigenfunctions $f^{(k)}$ of $-\partial_x^2$ with eigenvalue $k^2$. A kernel $A_{xy}=\sum_kA_kf^{(k)}_xf^{(k)}_y$ is then represented by its mode coefficient $A_k$. Under this expansion $\int dx\,A_{yx}B_{xz}\mapsto A_kB_k$, $\partial_z^2\delta(y-z)\mapsto-k^2$, and $\int dx\,A_{xx}\mapsto\sum_kA_k$. The paper's solution is

$$F_k=-k\tan(kt),\quad G_k=\sqrt{k^2+m^2},\quad K_k=\frac{\tau_k}{\cos^2(kt)},\quad \beta_k=w_k\cos(kt),\quad N^c\sim\frac{1}{\prod_k\cos(kt)},$$

Eqs. (49)–(51), (54), (55), where $\tau_k$ and $w_k$ are arbitrary constants.

Oscillator ensemble (Appendix A). For a unit-mass oscillator of frequency $\omega$, a state is a pair $(P_{\mathrm{osc}},S_{\mathrm{osc}})$. It satisfies $\dot S+\frac12(\partial_xS)^2+\frac12\omega^2x^2=0$ and $\dot P+\partial_x(P\,\partial_xS)=0$. The paper takes $S_{\mathrm{osc}}=-\frac{\omega x^2}{2}\tan(\omega t)$, and the Gaussian

$$P_{\mathrm{osc}}(x,t)=\sqrt{\frac{\tau}{2\pi\cos^2(\omega t)}}\exp\Bigl\{-\frac12\frac{\tau}{\cos^2(\omega t)}\bigl(x-w\cos(\omega t)\bigr)^2\Bigr\}.$$

Formalization targets

Goal: the non-interacting solution of Sec. IV A

For every finite family of modes and every time $t$ with $\cos(k_it)\neq0$, the coefficients (49)–(51), (54), (55) satisfy the mode forms of Eqs. (44), (45), (46), (47) and (48).

Milestones

1. Eqs. (44)/(49): $\dot F_k+F_k^2+k^2=0$.
2. Eqs. (45)/(50): $G_k^2=k^2+m^2$.
3. Eqs. (46)/(55): $\dot N^c/N^c-\frac12\frac{d}{dt}\sum_k\beta_kK_k\beta_k+\sum_kF_k=0$.
4. Eqs. (47)/(54): $\frac{d}{dt}(\beta_kK_k)+\beta_kK_kF_k=0$.
5. Eqs. (48)/(51): $-\frac12\dot K_k-K_kF_k=0$.
6. Appendix A: $S_{\mathrm{osc}}$ solves the Hamilton–Jacobi equation.
7. Appendix A: on $|\omega t|<\pi/2$, the $C^1$ solutions of the continuity equation are exactly $P=\frac{1}{\cos(\omega t)}f(\frac{x}{\cos(\omega t)})$.
8. Appendix A: $P_{\mathrm{osc}}$ solves the continuity equation.
9. Appendix A: at $t=0$, $\int P=1$, $\langle x\rangle=w$, $\Delta x=\tau^{-1/2}$, $\langle p\rangle=0$ and $\Delta p=0$.
10. Appendix A: $P_{\mathrm{osc}}\to\delta_0$ weakly as $\omega t\to\pm\frac\pi2,\pm\frac{3\pi}2,\dots$
11. Appendix A: $E=\langle-\partial_tS_{\mathrm{osc}}\rangle=\frac12\omega^2(\tau^{-1}+w^2)$.

Significance

The goal is the precise content of the paper's explicit $g=0$ solution. It is the base point of the first-order hybrid solution in Sec. IV B, and it underlies the paper's counterexample to DeWitt's claim that "the quantization of a given system implies also the quantization of any other system to which it can be coupled". Appendix A provides the interpretation of that solution: the classical sector behaves like an oscillator ensemble prepared with zero momentum and no momentum uncertainty but localized in space.

Formalization adds exact hypotheses: where the cosines must be non-zero, the regularity under which the paper's "most general solution" claim holds, and a correction to the printed energy formula. The paper prints $E=\frac12\omega^2\tau^{-1}$, which is correct only for $w=0$; Milestone 11 targets the corrected value. None of these statements has a machine-checked proof on the platform.

Difficulty

The Sec. IV A identities are trigonometric computations once they are reduced to modes, so their difficulty lies mainly in the side conditions. Milestone 7 is a uniqueness statement for a first-order linear PDE on a strip. It requires an argument along characteristics: exhibiting a solution is not enough. Milestones 9–11 are Gaussian integrals, and Milestone 10 is a weak limit of Gaussians whose variance tends to $0$ while the centre tends to $0$.

Formalization scope

• All fields are real. The mode family is a finite index type, a truncation of the paper's sums and of the formal infinite product in $N^c$. The kernel equations are stated mode by mode.
• $N^c$ is fixed to the representative $1/\prod_k\cos(kt)$ of the paper's "$\sim$".
• Time derivatives and partial derivatives are one-variable derivatives. Lean returns $0$ for tan, division, and deriv at degenerate points, so every statement assumes $\cos\neq0$ where it is needed.
• Milestone 7 assumes $P$ is $C^1$ on $\mathbb R^2$ and is stated on $|t|<\pi/(2\omega)$ with $\omega>0$.
• Eqs. (43) and (53), which involve the divergent zero-point energy, and the first-order solution of Sec. IV B are out of scope.

Selected references

• M. Albers, C. Kiefer, M. Reginatto, Measurement analysis and quantum gravity, Phys. Rev. D 78, 064051, 2008. https://doi.org/10.1103/PhysRevD.78.064051
• K. Eppley, E. Hannah, The necessity of quantizing the gravitational field, Found. Phys. 7, 51–68, 1977. https://doi.org/10.1007/BF00715241
• B. S. DeWitt, Definition of commutators via the uncertainty principle, J. Math. Phys. 3, 619, 1962. https://doi.org/10.1063/1.1724265

Motivation

In the holographic correspondence (AdS/CFT), a strongly coupled quantum field theory in $d+1$ spacetime dimensions is described by classical gravity on an $(d+2)$-dimensional anti-de Sitter spacetime. The first entry of the dictionary relates a scalar field of mass $m$ in the bulk to a scalar operator $\mathcal O$ of scaling dimension $\Delta$ in the boundary theory. This relation is used throughout applications to condensed matter ("AdS/CMT"): it fixes which operators are relevant, how sources and expectation values are read off from bulk solutions, and when a bulk field signals an instability towards an ordered phase (Hartnoll–Lucas–Sachdev, §1.6.2 and §6.2; see also Natsuume, AdS/CFT Duality User Guide).

This mission formalizes the elementary ODE facts behind that entry of the dictionary, as stated in the review of Hartnoll, Lucas and Sachdev.

Setting

The boundary theory has $d$ spatial dimensions. The bulk is Poincaré $\mathrm{AdS}_{d+2}$ of radius $L>0$,

$$ds^2=L^2\,\frac{-dt^2+d\vec x_d^2+dr^2}{r^2},$$

with the conformal boundary at $r\to0$. A scalar of mass squared $m^2\in\mathbb R$ (possibly negative) obeys $\nabla^2\phi=m^2\phi$. Writing $\phi=\phi(r)e^{-i\omega t+ik\cdot x}$ gives the radial equation (27)

$$\phi''-\frac{d}{r}\phi'+\Big(\omega^2-k^2-\frac{m^2L^2}{r^2}\Big)\phi=0,\qquad r>0 .$$

Near the boundary, solutions behave as powers $r^{\Delta}$ with the mass–dimension relation (29)

$$\Delta(\Delta-d-1)=m^2L^2,$$

whose roots are

$$\Delta_\pm=\frac{d+1}{2}\pm\sqrt{\frac{(d+1)^2}{4}+m^2L^2}.$$

Formalization targets

Goal: the two integration constants (eq. (28) at $\omega=k=0$)

For $m^2L^2>-(d+1)^2/4$, a $C^2$ function $\phi$ on $r>0$ solves the radial equation with $\omega=k=0$ if and only if

$$\phi(r)=A\,r^{\Delta_-}+B\,r^{\Delta_+}\quad(r>0)$$

for some constants $A,B$. These are the two constants of integration $\phi_{(0)}$ (source) and $\phi_{(1)}$ (response) of (28); at $\omega=k=0$ the expansion (28) is exact.

Milestones

1. Eq. (29). $r^{\Delta}$ solves the $\omega=k=0$ radial equation iff $\Delta(\Delta-d-1)=m^2L^2$.
2. Roots. For $m^2L^2\ge-(d+1)^2/4$ the real roots of (29) are exactly $\Delta_\pm$.
3. Reflection. $d+1-\Delta_\pm=\Delta_\mp$.
4. Breitenlohner–Freedman bound (627). (29) has a real root iff $m^2L^2\ge-(d+1)^2/4$ (here $D_{\rm eff}=d+1$).

Significance

The result itself. The goal says the space of zero-momentum solutions is two-dimensional and spanned by the two power laws, which is why a bulk scalar carries exactly one source and one response and why the source term scales as $r^{d+1-\Delta}$. The Breitenlohner–Freedman bound identifies the masses for which $\Delta$ becomes complex, the criterion used in §6.2 to detect infrared instabilities.

Formalizing it. These facts are standard and proved in the physics literature at the level of rigor of a textbook computation. No machine-checked version is known to the drafter. The mission produces a small reusable layer (radial operator, solution predicate, exponents $\Delta_\pm$) on which later statements of the review can build.

Difficulty

The milestones about $\Delta_\pm$ are algebra. The goal needs uniqueness for a second-order linear ODE with a regular singular point at $r=0$, on the open half-line: the naive "guess the power laws" argument only shows that $A r^{\Delta_-}+Br^{\Delta_+}$ are solutions, not that every $C^2$ solution is of this form. Mathlib's ODE uniqueness results are stated for Lipschitz vector fields, so an Euler-type equation has to be reduced to that setting (or handled by a change of variables) on $(0,\infty)$.

Formalization scope

Fields are real-valued functions $\mathbb R\to\mathbb R$; only values on $r>0$ matter. Derivatives are Mathlib's deriv, and solutions are required to be $C^2$ on $(0,\infty)$. The mass squared is a real parameter msq of any sign; $d$ is a natural number and $d=0$ is allowed. $\Delta_\pm$ use the real square root, which is $0$ on negative input, so every statement that relies on $\Delta_\pm$ being roots carries the Breitenlohner–Freedman hypothesis. The goal uses the strict bound, which excludes the saturating case $\Delta_+=\Delta_-$ where a logarithmic solution appears. Only $\omega=k=0$ is formalized; the general-$\omega,k$ asymptotic expansion (28), with Bessel-function solutions (37) and resonant logarithms, is out of scope.

Selected references

• S. A. Hartnoll, A. Lucas, S. Sachdev, Holographic quantum matter, MIT Press, 2018. https://arxiv.org/abs/1612.07324
• M. Natsuume, AdS/CFT Duality User Guide, Lecture Notes in Physics 903, Springer, 2015. https://arxiv.org/abs/1409.3575
• P. Breitenlohner, D. Z. Freedman, Positive energy in anti-de Sitter backgrounds and gauged extended supergravity, Phys. Lett. B 115 (1982) 197–201 (reference [111] of Hartnoll–Lucas–Sachdev).

Motivation

The discrete optimal transport problem between two histograms is a linear program, and much of the algorithmic theory of optimal transport is the theory of solving that linear program well. Chapter 3 of Peyré and Cuturi's Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019) surveys the classical combinatorial solvers: the network simplex, dual ascent methods, and the auction algorithm. Dual ascent methods work entirely with the dual variables, the Kantorovich potentials $(f, g)$: they keep a feasible pair of potentials and improve it step by step until it is optimal. The specialisation of this idea to assignment problems is the Hungarian algorithm of Kuhn (1955), and its general form is the primal-dual method for network flow problems presented in Bertsimas and Tsitsiklis, Introduction to Linear Optimization (1997, §7.7), on which §3.6 of the book is modelled.

The mathematical engine of every dual ascent method is one alternative: a feasible pair of potentials is either already optimal, or it can be improved along a direction of a very special, combinatorial form. This mission formalizes that alternative (Proposition 3.6 of the book) together with the results it rests on.

Setting

Fix integers $n, m \ge 1$, a cost matrix $C \in \mathbb{R}^{n\times m}$, and two histograms $a \in \Sigma_n$, $b \in \Sigma_m$, where $\Sigma_n = \{a \in \mathbb{R}^n_+ : \sum_i a_i = 1\}$ is the probability simplex. Write $[\![n]\!] = \{1, \dots, n\}$ for the row indices and, following the book, $[\![m]\!]' = \{1', \dots, m'\}$ for the column indices.

The couplings between $a$ and $b$ form the transportation polytope

$$U(a,b) = \{P \in \mathbb{R}^{n\times m}_+ : P\mathbb{1}_m = a,\ P^{\mathsf T}\mathbb{1}_n = b\},$$

and the primal problem is $\mathrm{L}_C(a,b) = \min_{P\in U(a,b)} \langle C, P\rangle$ with $\langle C, P\rangle = \sum_{i,j} C_{i,j}P_{i,j}$. A pair of vectors $(f, g) \in \mathbb{R}^n \times \mathbb{R}^m$ is dual feasible, written $(f,g) \in R(C)$, when $f_i + g_j \le C_{i,j}$ for all $(i, j)$. The dual problem (3.4) is

$$\mathrm{L}_C(a,b) = \max_{(f,g)\in R(C)} \langle f, a\rangle + \langle g, b\rangle .$$

For a feasible pair $(f, g)$, a pair of indices $(i, j')$ is balanced if $f_i + g_j = C_{i,j}$ and inactive if $f_i + g_j < C_{i,j}$. A matrix $P$ and a pair $(f, g)$ are complementary if $P_{i,j} > 0$ implies $C_{i,j} = f_i + g_j$, that is, $P$ is supported on balanced pairs. For $S \subset [\![n]\!]$ the vector $\mathbb{1}_S \in \mathbb{R}^n$ has ones at the indices in $S$ and zeros elsewhere; likewise $\mathbb{1}_{S'} \in \mathbb{R}^m$ for $S' \subset [\![m]\!]'$.

Formalization targets

Goal: Proposition 3.6 (p. 416)

For $a \in \Sigma_n$, $b \in \Sigma_m$ and $(f,g) \in R(C)$: either $(f, g)$ is optimal for (3.4), or there exist $S \subset [\![n]\!]$, $S' \subset [\![m]\!]'$ and $\varepsilon_0 > 0$ such that for every $0 < \varepsilon \le \varepsilon_0$,

$$(\tilde f, \tilde g) = (f, g) + \varepsilon(\mathbb{1}_S, -\mathbb{1}_{S'}) \in R(C) \quad\text{and}\quad \langle \tilde f, a\rangle + \langle \tilde g, b\rangle > \langle f, a\rangle + \langle g, b\rangle .$$

Milestones

1. Proposition 3.3 (p. 405). If $P \in U(a,b)$ and $(f,g) \in R(C)$ are complementary, then $P$ is primal optimal and $(f,g)$ is dual optimal.
2. Proposition 3.5 (p. 415). If every balanced pair $(i, j')$ with $i \in S$ has $j' \in S'$, then $(f,g) + \varepsilon(\mathbb{1}_S, -\mathbb{1}_{S'}) \in R(C)$ for all sufficiently small $\varepsilon > 0$.
3. Objective change (proof of Proposition 3.6, pp. 416–417). The step changes the dual objective by exactly $\varepsilon(\mathbb{1}_S^{\mathsf T}a - \mathbb{1}_{S'}^{\mathsf T}b)$.
4. Labeled sets (proof of Proposition 3.6, pp. 416–417). If no coupling in $U(a,b)$ is complementary to $(f,g)$, then there are $S, S'$ with every balanced pair leaving $S$ landing in $S'$, and

$$\mathbb{1}_S^{\mathsf T}a - \mathbb{1}_{S'}^{\mathsf T}b > 0 .$$

Significance

The result. Proposition 3.6 says that non-optimality of a feasible dual pair is always witnessed by a direction with entries in $\{0, \pm 1\}$, determined by two index sets, which keeps the pair feasible for a positive step and strictly improves the objective. This is what makes dual ascent a finite combinatorial method rather than a generic linear-programming iteration: the search for an ascent direction reduces to a maximum-flow computation on the bipartite graph of balanced pairs. Combined with the step length of Proposition 3.5, it is the primal-dual method, which reduces to the Hungarian algorithm on assignment problems. Milestone 1 is the optimality certificate of complementary slackness, used throughout the book's chapter 3.

Formalizing it. These results are classical and proved in the book and in Bertsimas and Tsitsiklis; no machine-checked proof of them is known to exist. The mission produces a formal statement and proof of the optimality-or-ascent alternative for the discrete Kantorovich dual, together with the complementary-slackness certificate in the transport setting. Milestone 4 is a Hall-type statement (a supply–demand theorem on a bipartite graph) whose formal proof is reusable for other matching and transportation results.

Difficulty

Milestones 1–3 are short computations. The content of the goal is in milestone 4. The obvious argument is linear-programming duality: if $(f,g)$ is not optimal, some feasible direction improves the objective. But LP duality only produces an arbitrary real direction; the claim that a direction of the form $(\mathbb{1}_S, -\mathbb{1}_{S'})$ suffices is a combinatorial statement. The book obtains $S, S'$ as the labeled nodes of a maximal flow (Ford–Fulkerson) and argues through max-flow/min-cut; the flow bookkeeping printed on p. 417 is garbled, so the step from "no complementary coupling exists" to "$\mathbb{1}_S^{\mathsf T}a > \mathbb{1}_{S'}^{\mathsf T}b$ for a set closed under balanced edges" has to be supplied carefully. Separately, connecting "not optimal" to "no complementary coupling exists" needs the converse direction of complementary slackness or strong duality for the transport problem.

Formalization scope

Row and column indices are Fin n and Fin m (0-based); the primed column set $[\![m]\!]'$ is just Fin m. Cost matrices and couplings are Matrix (Fin n) (Fin m) ℝ; histograms and potentials are real functions on Fin n, Fin m; $\Sigma_n$ is Mathlib's stdSimplex ℝ (Fin n). Index sets $S, S'$ are Finsets and $\mathbb{1}_S$ is indicatorVec S. "Optimal for Problem (3.4)" is the predicate IsDualOptimal: feasible, and no feasible pair has a larger objective (no real infimum or supremum is used, so no junk value can enter). The book's "for a small enough $\varepsilon > 0$" is stated as "for every $\varepsilon \in (0, \varepsilon_0]$", which is equivalent because $R(C)$ is convex and the objective is linear.

Standing assumptions, all from the book: $(f, g)$ is dual feasible (p. 415, "In what follows, $(f,g)$ is a feasible dual pair in $R(C)$"); $a, b$ are histograms in the simplex (used for the goal and milestone 4; without equal masses the dual is unbounded and optimality fails for every pair). Milestone 4 replaces the book's flow hypothesis "the throughput is strictly smaller than 1" by the equivalent flow-free statement "no coupling in $U(a,b)$ is complementary to $(f,g)$"; flows, capacities and the labeling algorithm appear in no statement.

The goal admits a trivializing formalization: allowing an arbitrary direction $(u, v)$ instead of $(\mathbb{1}_S, -\mathbb{1}_{S'})$ turns Proposition 3.6 into plain non-optimality of a linear program. The statement here fixes the direction to $(\mathbb{1}_S, -\mathbb{1}_{S'})$ exactly as the book does.

A complete development needs finite LP duality or complementary slackness for the transportation problem, and a max-flow/min-cut or Hall-type theorem on bipartite graphs with vertex capacities. Both are reusable well beyond this mission. Contributions welcome: proofs of the milestones, a self-contained proof of milestone 4 by induction or by a max-flow argument, and alternative proofs of the goal through LP duality plus a vertex argument.

Selected references

• G. Peyré, M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073 (§3.1–3.3, §3.6, pp. 400–417)
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §7.7 (the primal-dual method) and pp. 305–308 (Ford–Fulkerson and the labeling algorithm).
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2(1–2):83–97, 1955. https://doi.org/10.1002/nav.3800020109
• L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5