All missions

Motivation

The Virasoro–Shapiro amplitude is the tree-level scattering amplitude of four tachyons in the closed bosonic string. Together with the Veneziano amplitude for open strings it is historically the first formula of string theory: both were written down around 1968–69 as closed-form guesses with striking properties, before anyone knew they described strings (Veneziano 1968, Virasoro 1969, Shapiro 1970). In David Tong's Cambridge Part III lecture notes on string theory, the amplitude is reduced in Section 6.2.2 to a single integral over the complex plane, and the whole physical content of the answer (the symmetry in the Mandelstam variables, the infinite tower of poles at the string masses, the soft high-energy behaviour) is read off from the closed form of that integral in terms of Euler's Gamma function, eq. (6.11). The evaluation itself is carried out in the Appendix, Section 6.5.

Setting

For complex numbers $a,b$ define the Virasoro–Shapiro integral

$$C(a,b)=\int_{\mathbb C} d^2z\,|z|^{2a-2}\,|1-z|^{2b-2},$$

where, following Tong's convention, $d^2z = 2\,dx\,dy$ for $z=x+iy$ (twice Lebesgue measure on $\mathbb R^2$). Powers of the positive reals $|z|$ and $|1-z|$ are $r^{w}=e^{w\log r}$. The integral converges absolutely exactly when

$$\operatorname{Re}a>0,\qquad \operatorname{Re}b>0,\qquad \operatorname{Re}c>0,\qquad\text{where } a+b+c=1,$$

the three conditions controlling integrability near $z=0$, near $z=1$ and at $z=\infty$ respectively. $\Gamma$ denotes Euler's Gamma function, defined by $\Gamma(z)=\int_0^\infty t^{z-1}e^{-t}\,dt$ for $\operatorname{Re}z>0$ (eq. (6.26)) and continued analytically.

In the physics application $a=1+\alpha' p_2\cdot p_3/2$ and $b=1+\alpha' p_3\cdot p_4/2$ are determined by the tachyon momenta, and the three Gamma-function ratios become $\Gamma(-1-\alpha's/4)/\Gamma(2+\alpha's/4)$ and its $t,u$ analogues (eq. (6.12)).

Formalization targets

Goal: eq. (6.11)

For $a+b+c=1$ with $\operatorname{Re}a,\operatorname{Re}b,\operatorname{Re}c>0$,

$$C(a,b)=\frac{2\pi\,\Gamma(a)\,\Gamma(b)\,\Gamma(c)}{\Gamma(1-a)\,\Gamma(1-b)\,\Gamma(1-c)}.$$

Milestones (Appendix 6.5, in the order of the notes)

1. Eq. (6.27), the Euler Beta integral $\int_0^1 t^{x-1}(1-t)^{y-1}dt=\Gamma(x)\Gamma(y)/\Gamma(x+y)$ (already published on the platform; used as a reference).
2. The Gamma-function representation $|z|^{2a-2}=\Gamma(1-a)^{-1}\int_0^\infty t^{-a}e^{-|z|^2t}\,dt$.
3. The Gaussian reduction of $C(a,b)$ to a double integral over $t,u>0$.
4. The change of variables $t=\alpha\beta$, $u=(1-\beta)\alpha$.
5. The $\alpha$-integral $\int_0^\infty \alpha^{-a-b}e^{-\beta(1-\beta)\alpha}d\alpha=[\beta(1-\beta)]^{a+b-1}\Gamma(1-a-b)$.
6. The Beta-integral form $C(a,b)=\frac{2\pi\Gamma(c)}{\Gamma(1-a)\Gamma(1-b)}\int_0^1(1-\beta)^{a-1}\beta^{b-1}d\beta$.

Significance

The result. Eq. (6.11) is what turns the four-point function (6.10) into the Virasoro–Shapiro amplitude (6.12). Every property Tong extracts in Section 6.2.3 — the manifest $s\leftrightarrow t\leftrightarrow u$ symmetry, the poles at $s=4(n-1)/\alpha'$ reproducing the closed-string mass formula, and the exponential fall-off at high energy — is a property of the Gamma-function expression, not of the raw integral. The same integral (with general exponents) is the basic building block of Coulomb-gas computations in two-dimensional conformal field theory (Dotsenko–Fateev 1984).

Formalizing it. The identity is classical and its proof is elementary but analytically delicate. No machine-checked proof of the complex-plane integral is known to the mission author. A formal proof requires a reusable toolkit: Fubini–Tonelli manipulations of absolutely convergent iterated integrals with complex powers, two-dimensional Gaussian integrals, and a polar/affine change of variables on $(0,\infty)\times(0,1)$. The Beta integral (milestone 1) is already in Mathlib.

Difficulty

Each step of the textbook computation interchanges the order of integration in an integral with integrable but unbounded singularities at $z=0$, $z=1$ and at infinity, so each interchange must be justified by absolute convergence under exactly the three conditions above. The naive approach of applying Fubini directly to the original integrand in Cartesian coordinates does not factor; the proof in the notes instead introduces two auxiliary Gamma-function integrals, making the integral four-dimensional before any variable is integrated out, and the justification of Tonelli for that four-dimensional integrand is the main technical point.

Formalization scope

The integral is TongString.virasoroShapiroIntegral a b, defined as 2 * ∫ z : ℂ, (‖z‖ : ℂ) ^ (2a-2) * (‖1-z‖ : ℂ) ^ (2b-2), the integral being the Bochner integral against Lebesgue measure on $\mathbb C\cong\mathbb R^2$; the factor $2$ implements $d^2z=2\,dx\,dy$. Complex powers are Mathlib's principal-branch cpow applied to non-negative real bases, which agrees with $e^{w\log r}$ for $r>0$ (the point $z=0$, $z=1$ is a null set). The parameters $a,b,c$ are complex; the notes use real Mandelstam-type exponents, which are a special case. Since the Bochner integral of a non-integrable function is $0$ in Lean, every statement carries the convergence hypotheses; with them the integral is a genuine absolutely convergent integral, so the goal cannot be satisfied vacuously. The Gamma function is Mathlib's Complex.Gamma.

Contributions welcome: proofs of any milestone, and general lemmas on iterated integrals over $(0,\infty)^2$ with complex-power weights, which are reusable for other Selberg- and Dotsenko–Fateev-type integrals.

Selected references

• D. Tong, String Theory, Cambridge Part III lecture notes, 2009, Sections 6.2.2 and 6.5. http://www.damtp.cam.ac.uk/user/tong/string.html (arXiv:0908.0333)
• M. A. Virasoro, Alternative constructions of crossing-symmetric amplitudes with Regge behavior, Phys. Rev. 177 (1969) 2309. https://doi.org/10.1103/PhysRev.177.2309
• J. A. Shapiro, Electrostatic analogue for the Virasoro model, Phys. Lett. B 33 (1970) 361. https://doi.org/10.1016/0370-2693(70)90157-8
• J. Polchinski, String Theory, Vol. 1, Cambridge University Press, 1998, Section 6.6.
• Vl. S. Dotsenko, V. A. Fateev, Conformal algebra and multipoint correlation functions in 2D statistical models, Nucl. Phys. B 240 (1984) 312. https://doi.org/10.1016/0550-3213(84)90269-4

Motivation

The MDL and Occam principles of Chapter 7 rank hypotheses by description length and pay for a hypothesis according to its rank. Chapter 31 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), generalizes this to the PAC-Bayesian approach of McAllester: prior knowledge is a prior distribution $P$ over the class, the learner outputs a posterior $Q$, read as the randomized predictor that draws $h \sim Q$, and the price of $Q$ is its Kullback–Leibler divergence from $P$. The PAC-Bayes theorem (Theorem 31.1) says that with probability $1 - \delta$, simultaneously for every posterior, the generalization loss exceeds the training loss by at most $\sqrt{(D(Q\|P) + \ln(m/\delta))/(2(m-1))}$. Its proof is a compact and elegant argument: Markov's inequality for an exponential moment, a change of measure from $Q$ to $P$ by Jensen's inequality, an exchange of expectations that is possible because the prior does not depend on the sample, and a moment bound for the deviation of a single hypothesis. The bound suggests the learning rule of Remark 31.1, minimize $L_S(Q)$ plus the divergence penalty, which is regularized risk minimization in disguise, and for a finite class with a uniform prior it recovers an Occam-type bound (Exercise 2).

Setting

$H$ is a measurable space of hypotheses, $\ell : H \times Z \to [0,1]$ a jointly measurable loss, $D$ a distribution over $Z$, and $P$ a prior probability measure on $H$. For a posterior $Q$, $\ell(Q, z) = \mathbb{E}_{h \sim Q}[\ell(h, z)]$, $L_D(Q) = \mathbb{E}_{h \sim Q}[L_D(h)]$ and $L_S(Q) = \mathbb{E}_{h \sim Q}[L_S(h)]$, and $D(Q\|P) = \mathbb{E}_{h \sim Q}[\ln(dQ/dP)]$ is the Kullback–Leibler divergence, a real number when $Q \ll P$ and the log-density is $Q$-integrable.

Formalization targets

Goal: Theorem 31.1

For $m \ge 2$ and $\delta \in (0,1)$, with probability at least $1 - \delta$ over $S \sim D^m$, every probability measure $Q \ll P$ with finite divergence satisfies

$$L_D(Q) \le L_S(Q) + \sqrt{\frac{D(Q\|P) + \ln(m/\delta)}{2(m-1)}}.$$

Milestones

The identity $\mathbb{E}_{z \sim D}[\ell(Q, z)] = L_D(Q)$ (§31.1); the moment bound $\mathbb{E}_S[e^{2(m-1)\Delta(h)^2}] \le m$ of the proof (p. 417); Exercise 2, the bound for a finite class with the uniform prior.

Significance

PAC-Bayes bounds are among the tightest generalization bounds known in practice, and the reason is visible in Theorem 31.1: the complexity term is not a property of the class but of the posterior actually chosen, measured against a prior, so a learner that stays close to its prior generalizes even in a huge class. The theorem is the ancestor of a large literature (Seeger, Langford, Catoni, Maurer) and of modern nonvacuous bounds for neural networks. Formally it is a pleasant target: the change-of-measure inequality $\mathbb{E}_{h \sim Q}[f(h)] - D(Q\|P) \le \ln\mathbb{E}_{h \sim P}[e^{f(h)}]$ is the Donsker–Varadhan inequality, of independent value, and the moment bound is a sharp sub-Gaussian fact. On the platform, the mission introduces Gibbs risks and the Kullback–Leibler divergence between measures on a class, ending the book's series with its last learning principle.

Difficulty

The Gibbs risk identity is Fubini for a bounded jointly measurable function. The moment bound is the delicate step: the book derives it from Hoeffding's tail bound through Exercise 1, whose one-sided hypothesis is not enough (a constant negative variable satisfies it with an unbounded moment), and even the two-sided tail integrates only to $2m - 1$; the claim $\le m$ is nevertheless true, for instance by writing $e^{a\Delta^2} = \mathbb{E}_g[e^{\sqrt{2a}\,g\Delta}]$ for a standard Gaussian $g$ and applying Hoeffding's lemma to the sample mean, which gives $\mathbb{E}_S[e^{2(m-1)\Delta^2}] \le (1 - (m-1)/m)^{-1/2} = \sqrt m$. Theorem 31.1 then follows the book: Markov's inequality on $e^{f(S)}$ with $f(S) = \sup_Q(2(m-1)\mathbb{E}_{h \sim Q}\Delta(h)^2 - D(Q\|P))$, the change of measure (31.2) by Jensen's inequality for $\ln$ applied to the density $dQ/dP$ (the Donsker–Varadhan inequality, which needs $Q \ll P$ and an integrable log-density), the exchange of expectations (31.4) by Fubini, the moment bound, and finally Jensen for $x^2$ in (31.6); formally the supremum over all posteriors is handled by proving the bound for each $Q$ on the event $\{S : \mathbb{E}_{h \sim P}[e^{2(m-1)\Delta(h)^2}] \le m/\delta\}$, whose complement has probability at most $\delta$ by Markov, which sidesteps any measurability question about $f$. Exercise 2 is the theorem with $Q = \delta_h$, for which $D(Q\|P) = \ln|H|$.

Formalization scope

The class is an arbitrary measurable space, priors and posteriors are probability measures on it, and $Q(h)/P(h)$ is Mathlib's Radon–Nikodym derivative; the divergence is a Bochner integral, so the theorem quantifies over posteriors $Q \ll P$ whose log-density is $Q$-integrable, exactly the posteriors with a finite divergence, for which the bound has content, and no junk value can make a case false. Posteriors may depend on the sample: the statement bounds the outer measure of the set of samples for which some admissible $Q$ violates the bound. The loss is jointly measurable so that $h \mapsto L_D(h)$ and $(S, h) \mapsto L_S(h)$ are measurable and the Gibbs risks are genuine integrals; $m \ge 2$ is forced by the denominator $2(m-1)$. The moment bound is stated as the claim the proof needs rather than as Exercise 1, whose printed hypothesis is insufficient; the item text records this. Exercise 2 is stated as a simultaneous bound over the finite class, the form in which the theorem delivers it.

Not stated: Remark 31.1 (a learning rule, not a theorem), Exercise 1 as printed, and the second part of Exercise 2.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 31. doi:10.1017/CBO9781107298019
• D. A. McAllester, Some PAC-Bayesian theorems, Machine Learning 37, 1999. doi:10.1023/A:1007618624809
• D. A. McAllester, PAC-Bayesian stochastic model selection, Machine Learning 51, 2003. doi:10.1023/A:1021840411064
• A. Maurer, A note on the PAC Bayesian theorem, arXiv:cs/0411099, 2004.
• M. Seeger, PAC-Bayesian generalisation error bounds for Gaussian process classification, Journal of Machine Learning Research 3, 2002.
• J. Langford, J. Shawe-Taylor, PAC-Bayes and margins, NIPS 2002.

Motivation

A feedforward neural network is a directed acyclic graph of neurons, each computing a fixed scalar activation of a weighted sum of its inputs; fixing the graph and the activation and letting the weights vary gives a hypothesis class. Chapter 20 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), studies these classes through the book's three lenses. Approximation: every Boolean function is implemented by a network of depth 2 (Claim 20.1), but only at exponential size (Theorem 20.2), while a sign neuron implements conjunctions and disjunctions (Lemma 20.4), the bridge to Boolean circuits and hence to everything computable in bounded time. Estimation: the VC dimension of the class of sign networks over a graph with $|E|$ edges is $O(|E|\log|E|)$ (Theorem 20.6), so the sample complexity is governed by the number of weights. Optimization: training is NP-hard even for tiny networks, and the practical answer is SGD with the gradient computed by backpropagation, whose correctness the chapter derives from the chain rule.

Setting

A layered graph has layers $V_0, \dots, V_T$, every edge joining $V_{t-1}$ to $V_t$; $V_0$ holds the $n$ inputs and a constant neuron outputting $1$. With weights $w : E \to \mathbb{R}$ and an activation $\sigma$, the outputs are computed layer by layer, $a_{t+1,i} = \sum_{j : (v_{t,j}, v_{t+1,i}) \in E} w_{t,i,j}\,o_{t,j}$ and $o_{t+1,i} = \sigma(a_{t+1,i})$. The class $H_{V,E,\sigma} = \{h_{V,E,\sigma,w} : w : E \to \mathbb{R}\}$ (20.1); for binary classification the output layer is a single neuron and $\sigma$ is the sign function, so $H_{V,E,\operatorname{sign}}$ is a set of $\{\pm1\}$-valued predictors on $\mathbb{R}^n$. The size of the network is $|V|$, its depth $T$. The growth function $\tau_H(m) = \max_{|C| \le m}|H_C|$ extends to classes with any finite codomain (p. 275), and the proof of Theorem 20.6 uses two of its properties, stated as Exercises 3 and 4: the growth function of a product class is at most the product of the growth functions, and likewise for a composition class. For backpropagation the activation is any differentiable $\sigma$ and the loss is $\frac12\|o_T - y\|^2$; the backward pass sets $\delta_T = o_T - y$ and $\delta_t = \delta_{t+1}\operatorname{diag}(\sigma'(a_{t+1}))W_t$.

Formalization targets

Goal: Theorem 20.6

The VC dimension of $H_{V,E,\operatorname{sign}}$ is $O(|E|\log|E|)$. Explicitly, for a layered graph of depth at least $1$ with a single output neuron,

$$\operatorname{VCdim}(H_{V,E,\operatorname{sign}}) \le 2|E|\log_2(16|E|),$$

stated as: every $m \le \operatorname{VCdim}$ satisfies this bound (so the VC dimension is finite).

Milestones

Claim 20.1 (the depth-2 graph with $|V_1| = 2^n + 1$ whose sign class contains every function $\{\pm1\}^n \to \{\pm1\}$); Theorem 20.2 (every sign network implementing all functions $\{0,1\}^n \to \{0,1\}$ has $2^{n/3} \le 2|V|$); Lemma 20.4 (conjunction and disjunction as sign neurons); Exercise 4 (growth function of a composition); the correctness of backpropagation (§20.6: the partial derivative for the edge $(v_{t,j}, v_{t+1,i})$ is $\delta_{t+1,i}\sigma'(a_{t+1,i})o_{t,j}$). Further items: Exercise 3 (growth function of a product) and the intermediate bound $\tau_H(m) \le (em)^{|E|}$ of the proof of Theorem 20.6.

Significance

Theorem 20.6 is the reason networks are learnable at all in the book's sense: by the fundamental theorem, a class with finite VC dimension is agnostic PAC learnable with sample complexity linear in that dimension, and here the dimension is essentially the number of tunable parameters. The proof technique, due to Kakade and Tewari's lecture notes, is a composition-and-product argument on growth functions that applies to any layered class of threshold units and is reusable well beyond this chapter. Theorem 20.2 is the matching negative fact on expressive power, and it is a corollary of the same bound: a class that shatters $2^n$ points needs $\Omega(2^n)$ edges. Backpropagation's correctness is the one theorem about training the chapter can offer, given the hardness results, and it is the algorithm every practitioner runs.

Difficulty

Claim 20.1 and Lemma 20.4 are explicit constructions: the neuron $g_i(x) = \operatorname{sign}(\langle x, u_i\rangle - n + 1)$ detects $x = u_i$ because $\langle x, u_i\rangle \le n - 2$ otherwise, and the output neuron takes the disjunction; formally one must build the weight function and evaluate the forward pass on the $2^n$ inputs. Exercises 3 and 4 are counting: a restricted product is determined by its two restricted factors, and a restricted composition $f_2 \circ f_1$ on $C$ is determined by $f_1|_C$ and $f_2|_{f_1(C)}$, with $|f_1(C)| \le |C|$. Theorem 20.6 then needs: the class of one neuron is the class of homogenous halfspaces on its $d_{t,i}$ incoming coordinates, of VC dimension at most $d_{t,i}$ (Mission VI), Sauer's lemma in the form $\tau(m) \le (em)^{d}$ for every $m \ge 1$ (Mission IV; for $m \le d$ use $2^m \le (em)^m$), the layer class as a product and the network as a composition of layer classes, and finally the arithmetic $2^m \le (em)^{|E|} \Rightarrow m \le 2|E|\log_2(16|E|)$, which replaces the book's appeal to Lemma A.2 (for $m \ge 8|E|$ one has $\ln m \le \frac{m\ln 2}{2|E|}$). Theorem 20.2 follows from the goal with $|E| \le |V|^2$. Backpropagation is a chain-rule computation in a single real variable: the loss as a function of one weight is a composition of finitely many differentiable maps, and the derivative unwinds to the backward recursion; the formal effort is in the induction along layers with the natural-number indexing of the model.

Formalization scope

Layers and neurons are indexed by natural numbers: a LayeredGraph records the depth, the layer widths and, for each $t < T$, the finite set of edges $(v_{t,j}, v_{t+1,i})$ as pairs $(i, j)$ within the layer widths. Weights are functions on all index triples, and only those on edges are used, so the class is the image of all weight functions, as in (20.1). The forward computation netOutput is a recursion on the layer index; netInput is $a_{t+1,i}$. The sign activation returns $\pm1$ with $\operatorname{sign}(0) = -1$, the book's convention elsewhere, and a neuron with no incoming edges outputs $\sigma(0)$ (p. 270). The binary class signNetClass n G is Bool-valued, true iff the output neuron's input is positive, and is stated for graphs of depth at least $1$ (for depth $0$ the edges out of the input layer would be used but not counted in $|E|$). Growth functions with finite codomain are growthY, an sSup over restriction sizes, well defined because the codomains are finite; the Bool case is Mission IV's growth, and VC dimension and shattering are Mission IV's. Theorem 20.6 and Theorem 20.2 are given with explicit constants derived from the proof, since $O(\cdot)$ statements have no formal content; the drafter verified $\max\{m : 2^m \le (em)^{|E|}\} \le 2|E|\log_2(16|E|)$ numerically for $|E|$ up to $3000$ and at $10^4, \dots, 10^7$, and $2^n \le 2|V|^2\log_2(16|V|^2) \le 8|V|^3$. Backpropagation is stated for an arbitrary layered graph (phantom edges have weight $0$, p. 279), any differentiable activation, and one edge at a time as a HasDerivAt of the loss in that weight; $\delta_t$ is defined by recursion on $T - t$. The book's layer indices in (20.3) are shifted by one in the statement.

Not stated: Theorem 20.3 (Turing machines), Theorem 20.5 and Exercise 1 (sigmoid approximation, which needs a convention for outputs in $[-1,1]$ that the chapter leaves open), Theorem 20.7 and Exercise 6 (NP-hardness), Exercise 5 (the $\Omega(|E|^2)$ sigmoid lower bound, which assumes an exact threshold), the sigmoid half of Theorem 20.2, and the SGD pseudocode of §20.6, which is a heuristic without a stated guarantee.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 20. doi:10.1017/CBO9781107298019
• M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. doi:10.1017/CBO9780511624216
• D. E. Rumelhart, G. E. Hinton, R. J. Williams, Learning representations by back-propagating errors, Nature 323, 1986. doi:10.1038/323533a0
• I. Parberry, Circuit Complexity and Neural Networks, MIT Press, 1994.
• E. B. Baum, D. Haussler, What size net gives valid generalization?, Neural Computation 1(1), 1989. doi:10.1162/neco.1989.1.1.151

Motivation

Whether the gravitational field must be quantized is a long-standing foundational question. A well-known family of arguments tries to settle it by consistency alone: if a classical field were coupled to a quantum system, some basic principle — momentum conservation, the uncertainty relations, or the impossibility of superluminal signalling — would allegedly be violated. The two best-known versions are the gedanken experiment of Eppley and Hannah (1977) and the measurement-theoretic argument of DeWitt (1962).

Albers, Kiefer and Reginatto (Phys. Rev. D 78, 064051 (2008)) re-examine both arguments. Their paper is largely conceptual, but several of its steps are precise, checkable mathematical claims. This mission collects those claims and makes them machine-checkable.

Timeline.

• 1962 — DeWitt's measurement analysis of the gravitational field, using Peierls brackets and a "universal principle" for apparatus uncertainties.
• 1977 — Eppley and Hannah's gedanken experiment: a classical gravitational wave scattered off a quantum particle would imply momentum non-conservation, a violation of the uncertainty principle, or superluminal signalling.
• 2008 — Albers, Kiefer and Reginatto argue that neither gedanken experiment forces quantization, and exhibit a consistent hybrid classical–quantum model.

Setting

Photon pair and detector (Sec. II). Each photon carries a polarization qubit with orthonormal basis $|\uparrow\rangle$ (horizontal) and $|\downarrow\rangle$ (vertical). A detector with state space $\mathcal H$ (an arbitrary complex inner-product space) is coupled to photon 1. Before the measurement the joint state of photon 1, photon 2 and the detector is

$$|\Psi_0\rangle = \tfrac{1}{\sqrt2}\bigl(|\uparrow\rangle_1|\downarrow\rangle_2 - |\downarrow\rangle_1|\uparrow\rangle_2\bigr)|\Phi_0\rangle, \qquad (1)$$

and after the detector has measured photon 1 it is

$$|\Psi\rangle = \tfrac{1}{\sqrt2}\bigl(|\uparrow\rangle_1|\downarrow\rangle_2|\Phi_\uparrow\rangle - |\downarrow\rangle_1|\uparrow\rangle_2|\Phi_\downarrow\rangle\bigr). \qquad (2)$$

The reduced density operator of photon 2 is obtained from $|\Psi\rangle\langle\Psi|$ by tracing out photon 1 and the detector; the paper asserts that for both states it equals

$$\hat\rho = \tfrac12\bigl(|\uparrow\rangle_2\langle\uparrow|_2 + |\downarrow\rangle_2\langle\downarrow|_2\bigr). \qquad (3)$$

Mass cube and gravitational wave (Sec. III B). The disturbance $\delta T^{\mathrm{GW}}_{00}$ of the averaged energy density of the scattered wave depends on the cube's edge length $a$ and speed $v$, with sensitivities $T_a = \partial\,\delta T^{\mathrm{GW}}_{00}/\partial a$ and $T_v = \partial\,\delta T^{\mathrm{GW}}_{00}/\partial v$. With $\Delta a \approx \Delta x$ and $\Delta v \gtrsim \hbar/(2m\Delta x)$ the uncertainty $\Delta T^{\mathrm{GW}}_{00} = \sqrt{(T_a\Delta a)^2 + (T_v\Delta v)^2}$ has a strictly positive lower bound.

DeWitt's argument (Sec. V). A system observable $s$ reconstructed from apparatus data has uncertainty $\Delta s^2 = \Delta A^2/g^2 + g^2(\Delta D_\Omega s)^2$, where $g$ is the coupling constant.

Formalization targets

Goal — no signalling through photon 2 (Eq. (3))

For all unit vectors $\Phi_0, \Phi_\uparrow, \Phi_\downarrow \in \mathcal H$,

$$\rho_2(\Psi_0) = \hat\rho \quad\text{and}\quad \rho_2(\Psi) = \hat\rho .$$

Milestones

1. Eq. (1) ⇒ (3): $\rho_2(\Psi_0) = \hat\rho$.
2. Eq. (2) ⇒ (3): $\rho_2(\Psi) = \hat\rho$.
3. Sec. III B lower bound: $\Delta T^{\mathrm{GW}}_{00} \ge \sqrt{\tfrac{\hbar}{m} T_v T_a}$ whenever $\Delta x > 0$ and $\Delta v \ge \hbar/(2m\Delta x)$.
4. Sec. III B optimum: the function $\Delta x \mapsto \sqrt{(T_a\Delta x)^2 + (T_v\hbar/(2m\Delta x))^2}$ attains its minimum over $\Delta x>0$ at $\Delta x_{\min} = \sqrt{\tfrac{\hbar}{2m}\tfrac{T_v}{T_a}}$, with value $\sqrt{\tfrac{\hbar}{m}T_vT_a}$.
5. Eq. (61): $\min_{g\ne0}\sqrt{\Delta A^2/g^2 + g^2\Delta D^2} = \sqrt{2\,\Delta A\,\Delta D}$.
6. Eq. (64): if $\Delta A\,\Delta C \ge \hbar/2$ then $\sqrt{\hbar\,|D_s s|} \le \sqrt{2\,\Delta A\,\Delta C\,|D_s s|}$.

Significance

The goal is the precise content of the paper's rebuttal of the superluminal-signalling branch of the Eppley–Hannah argument: the state of photon 2 accessible to a probe (such as a classical gravitational wave) is the same whether or not photon 1 has been measured, so a probe of photon 2 alone cannot tell whether photon 1 was measured. Milestones 3–6 are the quantitative estimates the paper uses in Sec. III B (a coupling to a test body obeying the uncertainty principle transfers a minimum uncertainty to the classical wave) and Sec. V (DeWitt's limitation on a single observable, Eq. (64)).

The results are elementary once stated; the value of the mission is to pin the paper's claims down exactly, including the hypotheses under which they hold. None of the statements has, to our knowledge, a machine-checked proof on the platform.

Difficulty

The goal and Milestones 1–2 need a workable representation of the partial trace over a factor that is an arbitrary (possibly infinite-dimensional) inner-product space; the cross terms between the two branches vanish because the two branches are orthogonal on photon 1, not because of any property of the detector states. Milestones 3–6 are single-variable optimization statements; the main care is in the side conditions (positivity, excluding $g=0$ and $\Delta x = 0$).

Formalization scope

• The joint space $\mathbb C^2\otimes\mathbb C^2\otimes\mathcal H$ is represented by functions $\{0,1\}\times\{0,1\}\to\mathcal H$ (component $\Psi_{ij}$ along $|i\rangle_1|j\rangle_2$; index $0 = \uparrow$, $1 = \downarrow$). The reduced density matrix of photon 2 has entries $\rho_2(j,j') = \sum_i \langle \Psi_{ij'}, \Psi_{ij}\rangle_{\mathcal H}$, and $\hat\rho$ is a $2\times2$ complex matrix.
• The detector states are only assumed to be unit vectors. Orthogonality of $|\Phi_\uparrow\rangle$ and $|\Phi_\downarrow\rangle$ (a physical property of a detector that records the outcome) is not assumed, because Eq. (3) does not depend on it.
• In Sec. III B the sensitivities $T_a, T_v$, the mass $m$ and $\hbar$ are positive reals; the paper's approximate relations $\Delta a\approx\Delta x$ and $\Delta p\gtrsim\hbar/\Delta x$ are encoded as $\Delta a = \Delta x$ and the hypothesis $\Delta v \ge \hbar/(2m\Delta x)$.
• In Eq. (61) the coupling constant ranges over all non-zero reals.
• Sections IV (hybrid classical–quantum ensembles for Nordström gravity) and the appendices are out of scope for this mission.

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

The book The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) develops a perturbative, physics-style theory of wide deep neural networks. Every later computation in the book, from the statistics of preactivations at initialization to the neural tangent kernel, reduces to Gaussian expectations of polynomials. The single tool that evaluates these expectations is Wick's theorem (eq. 1.45), which the authors ask the reader to "put a box around". This mission formalizes Chapter 1, §1.1 (Gaussian Integrals), culminating in that theorem. It is the first mission of a series formalizing the book, all in the Lean namespace DeepLearningTheory.

Setting

Fix $N \ge 0$ and a symmetric positive-definite real $N\times N$ matrix $K = (K_{\mu\nu})$, the covariance. Write $K^{\mu\nu} = (K^{-1})_{\mu\nu}$ for its inverse. The zero-mean multivariable Gaussian distribution with covariance $K$ (eq. 1.31) has density on $\mathbb{R}^N$

$$p(z) = \frac{1}{\sqrt{|2\pi K|}} \exp\Big(-\tfrac12 \sum_{\mu,\nu=1}^N z_\mu K^{\mu\nu} z_\nu\Big), \qquad |2\pi K| = \det(2\pi K) = (2\pi)^N \det K,$$

and the expectation of an observable $F$ is $\mathbb{E}[F(z)] = \int d^N z\, p(z) F(z)$ (eqs. 1.36, 1.46), an integral against Lebesgue measure. A pairing of the labels $1,\dots,2m$ is a partition into $m$ unordered pairs; equivalently, a fixed-point-free involution $\sigma$ of $\{1,\dots,2m\}$ pairing $a$ with $\sigma(a)$. There are $(2m-1)!!$ pairings.

Formalization targets

Goal: Wick's theorem (eq. 1.45)

For all indices $\mu_1,\dots,\mu_{2m} \in \{1,\dots,N\}$ (repetitions allowed),

$$\mathbb{E}[z_{\mu_1}\cdots z_{\mu_{2m}}] = \sum_{\text{pairings } \sigma}\ \prod_{a<\sigma(a)} K_{\mu_a \mu_{\sigma(a)}}.$$

Milestones

1. Eq. (1.30) — the normalization $\int d^N z\, e^{-\frac12 z^\top K^{-1} z} = \sqrt{|2\pi K|}$.
2. Eq. (1.41) — the generating function $\int d^N z\, e^{-\frac12 z^\top K^{-1} z + J\cdot z} = \sqrt{|2\pi K|}\, e^{\frac12 J^\top K J}$ for every source $J \in \mathbb{R}^N$.
3. Odd moments vanish (p. 22, discussion after eq. 1.42).
4. Eq. (1.43) — $\mathbb{E}[z_{\mu_1} z_{\mu_2}] = K_{\mu_1\mu_2}$.
5. Eq. (1.44) — $\mathbb{E}[z_{\mu_1}z_{\mu_2}z_{\mu_3}z_{\mu_4}] = K_{\mu_1\mu_2}K_{\mu_3\mu_4} + K_{\mu_1\mu_3}K_{\mu_2\mu_4} + K_{\mu_1\mu_4}K_{\mu_2\mu_3}$.

Significance

Wick's theorem (also known as Isserlis' theorem, 1918) is used throughout the book: the Gaussianity of the first layer (Chapter 4), the four-point correlators of deep linear networks (Chapter 3), and all perturbative expansions around the infinite-width limit are evaluated by Wick contractions. A machine-checked version stated in the book's own density-based conventions gives later missions of this series a dependable foundation. The result is classical; the work remaining is its formalization in exactly this form. A related statement for general (possibly degenerate) Gaussian measures already exists on the platform as FeynmanWick.wick_theorem_gaussian; the present mission keeps the book's formulation via the explicit density and a positive-definite covariance.

Difficulty

The book's derivation differentiates the generating function (1.41) $2m$ times at $J=0$, which requires justifying differentiation under the integral sign and organizing the combinatorics of the product rule into pairings. Both the analytic step (dominated convergence for Gaussian tails, in $N$ dimensions) and the combinatorial step (a bijection between surviving terms and pairings, with the $1/(2^m m!)$ normalization) are routine on paper but need care in Lean. Computing the normalization (1.30) itself requires diagonalizing $K$ and a linear change of variables.

Formalization scope

• Vectors are functions Fin N → ℝ with Lebesgue measure; $K$ is a Matrix (Fin N) (Fin N) ℝ with K.PosDef (which includes symmetry). The inverse is Mathlib's K⁻¹.
• gaussianDensity K z and gaussExpect K F are exactly the book's $p(z)$ and $\mathbb{E}[F]$; gaussQuadForm K z is $\sum z_\mu K^{\mu\nu} z_\nu$.
• pairings (2m) is the finite set of fixed-point-free involutions of Fin (2m); the product is over labels $a$ with $a<\sigma(a)$, so each pair contributes once.
• Positive definiteness is assumed exactly as in the book; no statement is vacuous since, e.g., $K = I$ satisfies every hypothesis.

Selected references

• D. A. Roberts, S. Yaida (with B. Hanin), The Principles of Deep Learning Theory, Cambridge University Press, 2022. arXiv:2106.10165
• L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12 (1918). doi:10.1093/biomet/12.1-2.134

Motivation

A magnetohydrodynamic (MHD) equilibrium is a magnetic field $B$ and a scalar pressure $p$ on a region of $\mathbb R^3$ satisfying

$$(\nabla\times B)\times B=\nabla p,\qquad \nabla\cdot B=0 .$$

Under the substitution $B\mapsto u$ these are exactly the equations of a steady incompressible Euler flow, with $p$ replaced by the Bernoulli function, so every statement in this mission is simultaneously a statement about stationary solutions of the 3D Euler equations. Magnetic confinement of a fusion plasma requires equilibria whose pressure surfaces are nested tori, because $B\cdot\nabla p=0$ forces $p$ to be constant on the surfaces swept out by field lines.

Whether such equilibria exist without a continuous symmetry has been open since Grad, who conjectured in 1967 that smooth toroidal equilibria with non-constant pressure do not exist unless the configuration is symmetric (for instance axisymmetric), and restated the claim in 1985 as the assertion that, apart from the symmetric exceptions, there are no families of solutions depending smoothly on a parameter. Modern formulations of the conjecture appear in the work of Constantin–Drivas–Ginsberg (2021), Enciso–Luque–Peralta-Salas (2025) and Cardona–Duignan–Perrella (2025, Conjecture 2.5). Partial results have always relaxed something: Lortz (1970) obtained non-symmetric toroidal equilibria only with mirror symmetry and vanishing rotational transform; Bruno–Laurence (1996) and Enciso–Luque–Peralta-Salas (2025) allow discontinuous pressure and current sheets; Weitzner–Sengupta (2020) work in a topological torus rather than true toroidal geometry; near-axis and high-aspect-ratio expansions (Mercier 1964, Garren–Boozer 1991) give only approximate solutions.

Landreman (2026) exhibits explicit, fully non-axisymmetric, smooth analytic solutions on a genuine solid torus, with exact nested flux surfaces, finite aspect ratio and non-zero rotational transform. This mission formalizes the first of the two families presented there — the family with uniform rotational transform $\iota=2$ — in Lean 4.

Setting

Fix a parameter $0<\epsilon<1$ and set $a=\sqrt{1+\epsilon}$, $b=\sqrt{1-\epsilon}$. For a Cartesian point $x=(x_0,x_1,x_2)$ (written $(x,y,z)$ in the paper) define

$$s=\frac{x_0^2}{a^2}+\frac{x_1^2}{b^2},\qquad F=\sqrt{1-(1-s)^2-4x_2^2},$$

and the vector field

$$B=\left(\frac{2x_2x_0-(a/b)Fx_1}{s},\ \frac{2x_2x_1+(b/a)Fx_0}{s},\ 1-s\right).$$

The natural domain is the open set $U_\epsilon=\{x: 1-(1-s)^2-4x_2^2>0\}$, on which $s>0$ and all the expressions above are smooth. With

$$Q=\frac{x_0^2+x_1^2+4x_2^2}{2},\qquad H=Q+\frac{|B|^2}{2},$$

the flux label and the pressure are

$$\psi=\frac{H-1+\epsilon^2/2}{2},\qquad p=p_a-2\psi ,$$

where $p_a$ is an arbitrary constant. The level sets of $\psi$ are the pressure surfaces. For $0<\delta<(1-\epsilon)^2/4$ the region $\Omega_\delta=\{x\in U_\epsilon:\psi\le\delta\}$ is a solid torus bounded by a $\psi$-surface, and this is the plasma domain.

Field lines are described by a second coordinate system. For labels $(u,v)$ with $u^2+v^2<1/4$, putting $q^2=u^2+v^2$ and $L=\big((1+\sqrt{1-4q^2})/2\big)^{1/2}$, the position map is

$$r(u,v,\zeta)=\Big(a\big[L\cos\zeta+\tfrac{u\cos\zeta+v\sin\zeta}{L}\big],\ b\big[L\sin\zeta+\tfrac{v\cos\zeta-u\sin\zeta}{L}\big],\ v\cos2\zeta-u\sin2\zeta\Big).$$

The curve $\zeta\mapsto r(u,v,\zeta)$ is an integral curve of $B$, the pair $(u,v)$ labels the field line, and $\zeta$ acts as a toroidal angle of period $2\pi$. The magnetic axis is the field line $u=-\epsilon/2$, $v=0$, on which $\psi=0$; it is the non-planar closed curve $\gamma(\zeta)=(\sqrt{1-\epsilon^2}\cos\zeta,\ \sqrt{1-\epsilon^2}\sin\zeta,\ \tfrac{\epsilon}{2}\sin 2\zeta)$.

Target

The goal theorem asserts that for every $0<\epsilon<1$, every $0<\delta<(1-\epsilon)^2/4$ and every constant $p_a$, the pair $(B,p)$ above is a smooth equilibrium on $U_\epsilon$ that is genuinely three-dimensional:

$$\nabla\cdot B=0,\qquad (\nabla\times B)\times B=\nabla p,\qquad B\cdot\nabla p=0 \quad\text{on } U_\epsilon,$$ $$\nabla p(x)=0 \iff \psi(x)=0 \quad\text{for } x\in\Omega_\delta ,$$

together with smoothness of $B$ and $p$ on $U_\epsilon$ and the failure of axisymmetry: there is a rotation about the $z$ axis and a point of $\Omega_\delta$ whose image lies in $\Omega_\delta$ and carries a different pressure.

The milestones are the individual equations of Section 2 of the paper: divergence-freedom, the tension identity $(B\cdot\nabla)B=-\nabla Q$, force balance, invariance of $\psi$ along $B$, the field-line position map and its Jacobian $-ab$, the expressions $H=1+2\epsilon u+2(u^2+v^2)$ and $\psi=(u+\epsilon/2)^2+v^2$ in field-line labels, the magnetic axis, the enclosed volume $V=2\pi^2ab\,\psi$, the uniform rotational transform $\iota=2$, and the averages $\frac{1}{2\pi}\int_0^{2\pi}|B|^2\,d\zeta=1-\epsilon^2/2+2\psi$ and $\langle|B|^2\rangle_V=1-\epsilon^2/2+\delta$.

Significance

The solutions contradict the strict formulation of Grad's conjecture used in the recent literature (for example Conjecture 2.5 of Cardona–Duignan–Perrella), since they are smooth, have non-constant pressure, exact nested toroidal flux surfaces, no continuous Euclidean symmetry, finite aspect ratio and non-zero rotational transform, and they form continuous families parameterized by $\epsilon$ and $\delta$. Because MHD equilibrium is isomorphic to steady Euler flow, the same objects are explicit non-symmetric stationary Euler flows with invariant tori. They also serve as exact benchmarks for numerical equilibrium codes, where analytic three-dimensional solutions with known flux surfaces are otherwise unavailable.

The paper's derivations are elementary but long: they are algebraic identities among square roots and rational functions, verified in the paper by hand and by supporting numerical scripts. A machine-checked development removes the remaining doubt about sign conventions and domains, which is precisely what a counterexample to a conjecture requires. Nothing in this development is currently formalized in Mathlib: there is no curl, no divergence, and no notion of MHD equilibrium, so the mission also produces a small reusable vector-calculus layer on $\mathbb R^3$.

Difficulty

Force balance is an identity between derivatives of expressions containing $\sqrt{1-(1-s)^2-4z^2}$ and division by $s$; differentiating it directly produces large expressions whose simplification needs the domain hypotheses ($s>0$ and positive radicand) at every step, so field_simp-style automation must be driven with those side conditions in hand. The statements about field-line coordinates require knowing that the position map is a diffeomorphism onto its image, which the paper establishes by a covering argument rather than by computation. The transform $\iota=2$ is the hardest milestone: it is a winding-number statement about the poloidal displacement of a field line relative to the magnetic axis, and the paper's proof is a continuity-in-$\epsilon$ argument, which in Lean needs an honest treatment of continuous angle lifts. The volume and average identities need the change of variables theorem with the constant Jacobian $-ab$ over a solid torus.

Formalization scope

Points of space are Fin 3 → ℝ; partial derivatives are fderiv applied to the standard basis vector, and gradient, divergence, curl, cross product, the directional derivative $B\cdot\nabla f$ and the tension $(B\cdot\nabla)B$ are defined from it in the first definition file. Squared length is $\sum_i u_i^2$, so the Pi-type norm is never used. All the paper's objects — $a$, $b$, $s$, $F$, $B$, $U_\epsilon$, $Q$, $H$, $\psi$, $p$, $\Omega_\delta$, $L$, $r(u,v,\zeta)$, $\gamma$, rotation about the $z$ axis, and the complex poloidal displacement used for the transform — are given in the second definition file, in the same notation as this description. Smoothness is ContDiffOn ℝ ⊤; volumes are the Lebesgue measure on Fin 3 → ℝ; integrals are Bochner integrals.

Everything is stated with the explicit field of Section 2 rather than an abstract existence claim, so no statement can be satisfied by a degenerate or symmetric configuration. The equilibrium conditions are asserted pointwise on $U_\epsilon$, which is open and non-empty for $0<\epsilon<1$, so no milestone is vacuous. Contributions of the auxiliary calculus lemmas (differentiability of $s$, $F$ and $B$ on $U_\epsilon$, and the product and quotient rules in this partialD formulation) are welcome and reusable by the companion family of Section 3, which is not part of this mission.

Selected references

• M. Landreman, Analytic toroidal 3D MHD equilibria and steady Euler flows with invariant surfaces, J. Plasma Phys. (submitted), arXiv:2609.26742 (2026). https://arxiv.org/abs/2609.26742
• H. Grad, Toroidal containment of a plasma, Phys. Fluids 10 (1967) 137–154. https://doi.org/10.1063/1.1761965
• R. Cardona, N. Duignan, D. Perrella, Asymmetry of MHD equilibria for generic adapted metrics, Arch. Ration. Mech. Anal. 249 (2025) 1. https://doi.org/10.1007/s00205-024-02072-x
• A. Enciso, A. Luque, D. Peralta-Salas, MHD equilibria with nonconstant pressure in nondegenerate toroidal domains, J. Eur. Math. Soc. 27 (2025) 2251–2291. https://doi.org/10.4171/JEMS/1328
• P. Constantin, T. D. Drivas, D. Ginsberg, Flexibility and rigidity in steady fluid motion, Comm. Math. Phys. 385 (2021) 521–563. https://doi.org/10.1007/s00220-021-04048-4
• O. P. Bruno, P. Laurence, Existence of three-dimensional toroidal MHD equilibria with nonconstant pressure, Comm. Pure Appl. Math. 49 (1996) 717–764. https://doi.org/10.1002/(SICI)1097-0312(199607)49:7<717::AID-CPA3>3.0.CO;2-C

Motivation

Chapter 3 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks how many random examples suffice to learn a concept from an infinite class. The cardinality bound of Occam's Razor is useless there, yet the rectangle game of Chapter 1 shows that some infinite classes are learnable from a finite sample. The answer is the Vapnik–Chervonenkis dimension: the size of the largest set on which the class realizes every labeling. Sauer's lemma says that a class of VC dimension $d$ realizes only $\Phi_d(m) = \sum_{i \le d}\binom{m}{i} \le (em/d)^d$ labelings on any $m$ points, polynomially many rather than $2^m$, and the ε-net theorem of Blumer, Ehrenfeucht, Haussler and Warmuth turns this into a sample bound: a consistent hypothesis from a class of VC dimension $d$ is probably approximately correct once $m$ is of order $(1/\epsilon)(\log(1/\delta) + d\log(1/\epsilon))$. A matching lower bound shows that $\Omega(d/\epsilon)$ examples are necessary. The chapter thus gives a single combinatorial parameter that characterizes, up to a logarithmic factor, the sample complexity of learning any class in the distribution-free model.

Setting

For a class $C$ of concepts $X \to \{0,1\}$ and a finite $S \subseteq X$, $\Pi_C(S)$ is the set of dichotomies of $S$ realized by $C$; $S$ is shattered if all $2^{|S|}$ are realized; $\mathrm{VCD}(C)$ is the supremum of the sizes of shattered sets, possibly $\infty$; $\Pi_C(m)$ is the largest $|\Pi_C(S)|$ over $|S| = m$; and $\Phi_d(m)$ is defined by $\Phi_d(m) = \Phi_d(m-1) + \Phi_{d-1}(m-1)$, $\Phi_d(0) = \Phi_0(m) = 1$. For a target $c$ the error regions are $c \,\Delta\, h$ for $h$ in the hypothesis class, and a set of points is an ε-net if it meets every error region of weight at least $\epsilon$ under the target distribution $D$. Samples, their product law, consistency and the error of a hypothesis are those of Mission I.

Formalization targets

Goal: Theorems 3.3 and 3.4

Let $H$ be a class of VC dimension at most $d$, well-behaved for the target $c$ (the double-sample event of the proof is null-measurable), and $m \ge 8/\epsilon$. The points of a random sample of $m$ examples of a target $c$ fail to be an ε-net for the error regions $\{c \,\Delta\, h : h \in H\}$ with probability at most

$$2\,\Phi_d(2m)\,2^{-\epsilon m/2},$$

so any algorithm that outputs a hypothesis in $H$ consistent with its sample has error greater than $\epsilon$ with at most that probability; with $m \ge (4/\epsilon)\log_2(2/\delta)$ and $m \ge (8d/\epsilon)\log_2(13/\epsilon)$ the probability is at most $\delta$; and, if $H$ is nonempty, every class contained in $H$ for whose targets $H$ is well-behaved is PAC learnable using $H$.

Milestones

Lemma 3.1 (Sauer's lemma, $\Pi_C(m) \le \Phi_d(m)$); Lemma 3.2 ($\Phi_d(m) = \sum_{i \le d}\binom{m}{i}$); the polynomial bound $\Phi_d(m) \le (em/d)^d$ of p. 57; Theorem 3.5 (the $\Omega(d/\epsilon)$ lower bound, in the two explicit forms of its proof).

Significance

Theorem 3.3 is the fundamental theorem of PAC learning: it replaces $\log|H|$ in Occam's Razor by the VC dimension and thereby covers rectangles, halfspaces, polygons, neural networks with a fixed architecture, and every class whose dichotomies grow polynomially. Its proof, the double sample and random partition argument, is the origin of symmetrization in empirical process theory. Sauer's lemma is a cornerstone of extremal combinatorics with independent proofs by Sauer, Shelah and Vapnik–Chervonenkis, and the lower bound of Theorem 3.5 shows that the upper bound is tight to within $\log(1/\epsilon)$, so the VC dimension genuinely characterizes sample complexity. None of these is machine-checked. Formalizing them puts on the platform the VC dimension, the growth function and the ε-net theorem with explicit constants, stated on the same sample law as the rest of this series, and the first information-theoretic lower bound for learning.

Difficulty

Sauer's lemma is a double induction on $d$ and $m$ through the auxiliary class $C'$ of dichotomies whose two extensions to a distinguished point are both realized, which needs care with the identification of dichotomies of $S$ and of $S \setminus \{x\}$. The ε-net theorem needs: the reduction $\Pr[A] \le 2\Pr[B]$ from a failed ε-net on the first half to a region hit at least $\epsilon m/2$ times by the second half, which is a Chebyshev bound on a binomial variable and is where $m \ge 8/\epsilon$ enters; the exchangeability of the $2m$ draws with a random partition into two halves; the counting bound $\binom{m}{\ell}/\binom{2m}{\ell} \le 2^{-\ell}$; and Sauer's lemma applied to the error regions, whose growth function equals that of $H$. The explicit constants require the numerical inequality $2(2em/d)^d 2^{-\epsilon m/2} \le \delta$ under the two stated conditions. The lower bound is a probabilistic argument with a random target: conditional on the sample, the labels of unseen points are fair coins, so the number of errors on them is binomial and exceeds half its range with probability at least $1/2$; the refined bound scales this construction to a region of weight $16\epsilon$ and uses Markov's inequality to bound the number of draws landing in it. Measurability of the failure sets is avoided by stating outer-measure bounds, except for the double-sample event, which the proof integrates: it is assumed null-measurable (the well-behavedness of Blumer et al., without which the theorem is false for a class of VC dimension $1$ on $\omega_1$). For the lower bound it is avoided by working over a finitely supported distribution on a space with measurable singletons.

Formalization scope

The VC dimension is a supremum in $\mathbb{N} \cup \{\infty\}$, the growth function a supremum in $\mathbb{N}$ (bounded by $2^m$), and $\Phi_d$ the book's recurrence, with its closed form and polynomial bound stated as separate theorems. The goal is stated for a hypothesis class $H$ (Theorem 3.4), Theorem 3.3 being the case $C = H$; it carries the exact bound of the proof, the explicit constants of Blumer et al. in place of the book's $c_0$, the requirement $m \ge 8/\epsilon$ of the proof's Chebyshev step, measurability of the hypotheses and the target, well-behavedness of $H$ for the target, and $0 < \epsilon, \delta < 1$. PAC learnability of the subclasses of $H$ needs $H$ nonempty, since no algorithm outputs hypotheses in the empty class. The lower bound is stated for every deterministic learning function, on an instance space with measurable singletons, for a class shattering some set of $d \ge 1$ points, with the explicit constants derived in the proof sketch ($m \le d/2$: error $\ge 1/8$ with probability $\ge 1/2$; $\epsilon \le 1/16$ and $m \le (d-1)/(64\epsilon)$: error $> \epsilon$ with probability $\ge 1/4$). Running time is not modelled. The composition bound for layered networks (Theorems 3.6 and 3.7) is not stated.

Trivializing readings are excluded: the ε-net event ranges over every hypothesis of $H$, the failure bounds are uniform over all consistent learners, and the lower bound holds for every learning function. Welcome contributions: Sauer's lemma, the closed form and the $(em/d)^d$ bound, the random-partition counting lemma, and the binomial median inequality used in the lower bound.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 3. doi:10.7551/mitpress/3897.001.0001
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4), 1989. doi:10.1145/76359.76371
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16(2), 1971. doi:10.1137/1116025
• N. Sauer, On the density of families of sets, Journal of Combinatorial Theory, Series A 13(1), 1972. doi:10.1016/0097-3165(72)90019-2
• A. Ehrenfeucht, D. Haussler, M. Kearns, L. Valiant, A general lower bound on the number of examples needed for learning, Information and Computation 82(3), 1989. doi:10.1016/0890-5401(89)90002-3

Motivation

A decision-maker has $n$ projects, each a Markov reward process, and at every decision time may advance exactly one of them; the others stay frozen. Which project to advance so as to maximize the expected total discounted reward? Posed as a dynamic program the problem has a state space that is the product of the $n$ state spaces, and the size of that product defeats every general method. The index theorem of Gittins and Jones (1974) says the dynamic program is solved exactly by an index policy: there is a real number $\nu(B, x)$, computable for each bandit process $B$ from its own data and its own current state $x$, such that always advancing a process of greatest index is optimal. Chapter 2 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), introduces the index, proves the theorem three times, and works out the properties of the index that the rest of the book, from jobs and superprocesses to restless bandits, is built on: which stopping time attains it, how it is computed, how it moves with the discount factor, and when it collapses to the myopic rule.

The index theorem itself is already on the platform, proved, as BanditAlgorithm.gittins_index_theorem in the Bandit Algorithms series (Lattimore and Szepesvári, Theorem 35.9). This mission cites it and formalizes what Chapter 2 establishes around it.

Setting

A bandit process $B$ (§2.3–2.4) is a Markov reward process on a countable state space $E$: transition probabilities $P(y \mid x)$, a bounded reward $r(x)$ received each time the continuation control is applied in state $x$, and a discount factor $a \in (0, 1)$; the freeze control leaves the state unchanged and yields nothing. The law of the process started at $x$ is $\mathbb{P}_x$ and $x(t)$ is its state at process time $t = 0, 1, 2, \dots$. A stopping time $\tau$ is a past-measurable rule for switching from continuation to freezing, taking values in $\{1, 2, \dots\} \cup \{\infty\}$. For such $\tau$, $R_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t r(x(t))]$ is the expected discounted reward and $W_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t]$ the expected discounted time; their ratio $\nu_\tau(B, x)$ (2.7) is the equivalent constant reward rate of that portion of $B$. The Gittins index is

$$\nu(B, x) = \sup_{\tau > 0} \frac{R_\tau(B, x)}{W_\tau(B, x)} \tag{2.6}$$

and, equivalently, the fair charge (2.5): the greatest rent $\lambda$ per period for which continuing $B$ for one or more periods, paying $\lambda$ each period, can be done without expected loss. A simple family of alternative bandit processes (SFABP) is $n$ such processes with a common discount factor, one of which is continued at each decision time; an index policy continues a process of greatest index. In the Lean development the single-arm model is the platform's (GittinsIndex): the chain law is built by the Ionescu–Tulcea construction, stopping times are adapted $\mathbb{N}\cup\{\infty\}$-valued maps on trajectories, and gittinsIndex P r a x is (2.6).

Formalization targets

Goal: Lemma 2.2, the optimal stopping set

The supremum in (2.6) is attained. For the initial state $\xi$, the attaining stopping rule may be taken to be "stop at the first time $t \ge 1$ at which the state lies in $\Sigma_0$" for any set $\Sigma_0$ with

$$\{x : \nu(B, x) < \nu(B, \xi)\} \subseteq \Sigma_0 \subseteq \{x : \nu(B, x) \le \nu(B, \xi)\},$$

and every such rule has $\nu_\tau(B, \xi) = \nu(B, \xi)$.

Milestones

Theorem 2.1 as a reference to the proved platform theorem; Eq. (2.5), the fair-charge characterization of the index; the restart-in-state formulation of §2.6.4 as the convergence of the Katehakis–Veinott value iteration; Theorem 2.3, monotonicity in the discount factor; Lemma 2.4, the interchange of two bandit portions; Propositions 2.5–2.8, the monotone-index cases in which the index is the immediate reward, or is attained only after the first step, or only at $\tau = \infty$.

Significance

Lemma 2.2 is the working form of the index: it turns the supremum over all stopping times into a specific rule, the first time the index falls below its starting value, and it is what the interchange proof of §2.7, the modified-forwards-induction policies of §2.6.6, the monotone-index propositions of §2.11 and the treatment of jobs in Chapter 3 all use. The fair-charge form (2.5) is the prevailing-charge proof of the theorem (Weber 1992) and the interpretation that carries over to superprocesses and restless bandits. The restart formulation is how indices are computed in practice (Katehakis and Veinott 1987), and Theorem 2.3 is the first of the comparative statics used throughout Chapters 7 and 8. Lemma 2.4 is the elementary inequality behind the original proof of Gittins and Jones.

Of these, only the index theorem has a machine-checked proof today. Formalizing the rest gives the platform the index as a usable object: a characterization of the optimal stopping rule, a convergent algorithm for it, and the monotonicity facts, all stated against the existing model so that every later mission of this series and every future use of the L&S model can build on them.

Difficulty

The obvious first move for Lemma 2.2, "take the stopping time that achieves the supremum", is what has to be proved: the supremum is over an uncountable family, and attainment comes from the optimal stopping problem with charge $\lambda = \nu(B, \xi)$, whose value function satisfies $\varphi(x) = \max\{0, r(x) - \lambda + a\mathbb{E}[\varphi(x(1)) \mid x(0) = x]\}$, together with the fact that its optimal stopping set is characterized by the strict and non-strict inequalities $\lambda > \nu(B, x)$ and $\lambda \ge \nu(B, x)$. That last step is the content: it identifies the local decision "stop or continue" with a comparison of indices, which is why any set between the two level sets works. On the platform's model this requires the dynamic-programming theory of discounted optimal stopping on a countable space (Theorem 2.10 of the book), the identification of fairChargeProfit with that value function, and the strong Markov property of markovChainMeasure at a trajectory stopping time. Theorem 2.3 needs randomized stopping times (a geometric kill) and the fact that they do not enlarge the supremum. The restart iteration is monotone and bounded but its operator is not a contraction in the restart value, so its limit has to be identified with the restart problem's value directly; that value is $\max(0, \nu/(1-a))$, not $\nu/(1-a)$, because restarting forever is free.

Formalization scope

The state space is a countable type with measurable singletons, so every subset is measurable; rewards are bounded; $a \in (0, 1)$. The chain law, stopping times, the discounted stopped sums and the index are the platform's, unchanged. Expectations are Bochner integrals; with bounded rewards they are finite and no total-function default value enters. IsPositiveStoppingTime fixes $\tau \ge 1$ everywhere, so $W_\tau \ge 1$ and the ratio (2.7) is a genuine quotient. The stopping rule of Lemma 2.2 is the hitting time from time $1$ of a set, with $\infty$ when the set is never hit. The fair-charge profit is a real supremum over the nonempty bounded family of positive stopping times, and (2.5) is stated with the outer supremum over $\{\lambda : \text{profit}(\lambda) \ge 0\}$, a nonempty set bounded above. The restart iteration is stated as a limit, with the value $\max(0, \nu(B, \xi)/(1-a))$: for a nonnegative index this is the book's $\nu/(1-a)$, and the maximum is forced by a one-state example with negative reward. The propositions' hypotheses are almost-sure events under $\mathbb{P}_x$, written as events of measure one.

Two trivializing readings are excluded: the index is never taken over all $\mathbb{N}\cup\{\infty\}$-valued maps but over adapted stopping times, and the stopping set of the goal is not restricted to the two extreme level sets. Contributions welcome: the optimal-stopping dynamic program on markovChainMeasure (value iteration, the strong Markov property at a stopping time), the equivalence of randomized and non-randomized stopping times for the supremum, and the monotone convergence of the restart iteration.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 2. doi:10.1002/9780470980033
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (Gani, ed.), North-Holland, 1974.
• R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4), 1992. doi:10.1214/aoap/1177005588
• M. N. Katehakis, A. F. Veinott, The multi-armed bandit problem: decomposition and computation, Mathematics of Operations Research 12(2), 1987. doi:10.1287/moor.12.2.262
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401