All missions

Motivation

Many decision problems contain a constraint whose coefficients are an expectation under a probability vector that is not known exactly: an expected cost under uncertain scenario probabilities, an expected payoff of an asset under an estimated distribution, the expected demand in a newsvendor model. The probabilities are usually estimated from data, and a solution that is feasible for the estimate can be infeasible for the true distribution. Robust optimization protects against this by requiring the constraint to hold for every probability vector in an uncertainty region around the estimate.

A natural region is a ball in a φ-divergence, a family of statistical distances between probability vectors that contains the Kullback–Leibler divergence, the Burg entropy, the χ² distances, the Hellinger distance and the variation distance. Such balls arise as asymptotic confidence sets for the true distribution given observed frequencies (Pardo 2006), so the radius has a statistical meaning. Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) showed that the robust version of a linear constraint over such a ball is equivalent to a finite convex system involving the convex conjugate of φ. This reformulation is a standard tool in the later literature on distributionally robust optimization.

Setting

A φ-divergence function is a function $\phi:\mathbb R\to\mathbb R\cup\{+\infty\}$ that is convex on $[0,\infty)$, finite on $(0,\infty)$, and satisfies $\phi(1)=0$; the value $\phi(0)$ may be $+\infty$. Examples are $\phi(t)=t\log t-t+1$ (Kullback–Leibler), $\phi(t)=-\log t+t-1$ (Burg), $\phi(t)=(t-1)^2$ (modified χ²) and $\phi(t)=|t-1|$ (variation). For $p,q\in\mathbb R^m$ with $q>0$ the φ-divergence is

$$I_\phi(p,q)=\sum_{i=1}^m q_i\,\phi\!\left(\frac{p_i}{q_i}\right),$$

and the conjugate of $\phi$ is $\phi^*(s)=\sup_{t\ge0}\{st-\phi(t)\}$, a function with values in $\mathbb R\cup\{+\infty\}$.

Fix $a\in\mathbb R^n$, $B\in\mathbb R^{n\times m}$ with columns $b_i$, $\beta\in\mathbb R$, $C\in\mathbb R^{k\times m}$ with columns $c_i$, $d\in\mathbb R^k$, a nominal vector $q\in\mathbb R^m$ and a radius $\rho>0$. The uncertainty region is

$$U=\{p\in\mathbb R^m\mid p\ge0,\ Cp\le d,\ I_\phi(p,q)\le\rho\},$$

where the linear constraints $Cp\le d$ can encode $e^\top p=1$ and any further information on $p$. A decision $x\in\mathbb R^n$ satisfies the robust linear constraint if

$$(a+Bp)^\top x\le\beta\qquad\text{for all }p\in U. \tag{11}$$

Inequalities between vectors are componentwise throughout.

Formalization targets

Goal: Theorem 1

Assume $q>0$ and $q\in U$. Then $x$ satisfies (11) if and only if there are $\eta\in\mathbb R^k$ and $\lambda\in\mathbb R$ with

$$a^\top x+d^\top\eta+\rho\lambda+\lambda\sum_{i}q_i\,\phi^*\!\left(\frac{b_i^\top x-c_i^\top\eta}{\lambda}\right)\le\beta,\qquad\eta\ge0,\ \lambda\ge0, \tag{13}$$

where $0\phi^*(s/0):=0$ for $s\le0$ and $0\phi^*(s/0):=+\infty$ for $s>0$. The statement fixes no constants and no particular φ; it holds for the whole class.

Milestones

The proof in the paper has three displayed steps, which are the milestones. With the Lagrange function $L(p,\lambda,\eta)=(a+Bp)^\top x+\rho\lambda-\lambda I_\phi(p,q)+\eta^\top(d-Cp)$ and the dual objective $g(\lambda,\eta)=\sup_{p\ge0}L(p,\lambda,\eta)$:

1. Closing identity. For $\lambda\ge0$, $(\lambda\phi)^*(s)=\sup_{t\ge0}\{st-\lambda\phi(t)\}$ equals $\lambda\phi^*(s/\lambda)$, with the convention above at $\lambda=0$.
2. Eq. (15). For $q>0$ and $\lambda\ge0$,

$$g(\lambda,\eta)=a^\top x+d^\top\eta+\rho\lambda+\sum_{i=1}^m q_i(\lambda\phi)^*(b_i^\top x-c_i^\top\eta).$$

3. Duality. Under the hypotheses of Theorem 1, $x$ satisfies (11) if and only if $g(\lambda,\eta)\le\beta$ for some $\lambda\ge0$, $\eta\ge0$. This is split into the weak-duality direction and the strong-duality direction with attainment.

An additional item states Corollary 1, the specialization to $U=\{p\ge0,\ e^\top p=1,\ I_\phi(p,q)\le\rho\}$, where the multiplier $\eta\in\mathbb R$ of the normalization is free in sign.

Significance

Theorem 1 turns a semi-infinite constraint, one inequality for each $p$ in a convex set, into a single convex inequality in $(x,\lambda,\eta)$. The left side of (13) is jointly convex because $\lambda\phi^*(s/\lambda)$ is the perspective of a convex function. For the divergences of Table 4 of the paper the conjugate has a closed form, and the robust constraint becomes a linear, conic quadratic or self-concordant-barrier-representable constraint. The paper's applications (robust asset pricing, a robust newsvendor, and the tractability results of its §5) all start from this theorem, as do its Corollaries 2–5.

The theorem is proved in the paper; no machine-checked proof of it is known. Formalizing it adds a checked robust-counterpart theorem for φ-divergence regions, a reusable encoding of φ-divergences with extended values, and a strong-duality statement with attainment for convex programs whose constraint function takes the value $+\infty$ on the boundary of the orthant. It also records a correction: the paper states the theorem for $q\ge0$, and that version is false (see Formalization scope).

Difficulty

The separation step (15) and the conjugate identity are elementary manipulations of suprema, but in extended arithmetic: $\phi$ may be $+\infty$ at $0$, the conjugate may be $+\infty$, and the case $\lambda=0$ follows its own convention. The central difficulty is the duality step. The worst-case problem is a convex program whose constraint $I_\phi(p,q)\le\rho$ is not a finite convex function on a closed set: for the Burg or χ² divergence it is $+\infty$ on the boundary of the orthant, and $U$ itself need not be closed. Textbook statements of Slater-type strong duality usually assume finite-valued convex functions on a closed domain, so they do not apply as stated. The statement also requires attainment of the dual minimum, not only the absence of a duality gap, and this is the part a naive limiting argument does not give.

Formalization scope

Conventions:

• Vectors are Fin n → ℝ with the componentwise order; $B$ and $C$ are Matrix (Fin n) (Fin m) ℝ and Matrix (Fin k) (Fin m) ℝ; $b_i$ and $c_i$ are the columns fun j => B j i and fun j => C j i.
• $\phi$ is ℝ → EReal, never $-\infty$, finite on $(0,\infty)$, with $\phi(1)=0$ and convexity on $[0,\infty)$ written out in EReal. $\phi(0)=+\infty$ is allowed, so the Burg, χ² and J divergences are covered.
• $I_\phi(p,q)$, $\phi^*$, $(\lambda\phi)^*$, $L$, $g$ and the left side of (13) are EReal-valued. $\lambda\phi(t)$ is the EReal product, in which $0\cdot(+\infty)=0$. The term $\lambda\phi^*(s/\lambda)$ is defined by an explicit case split at $\lambda=0$, and $\lambda\sum_i q_i\phi^*(\cdot/\lambda)$ in (13) is read as $\sum_i q_i\,(\lambda\phi^*(\cdot/\lambda))$ with the convention applied term by term.
• The paper's $\max_{p\ge0}$ in $g$ is a supremum; $\min_{\lambda,\eta\ge0}g\le\beta$ is stated in its attained form, $\exists\,\lambda\ge0,\eta\ge0$ with $g(\lambda,\eta)\le\beta$.
• $m$ and $k$ may be $0$.

Corrected slip. The paper's standing assumption is $q\ge0$. The third equality of (15) substitutes $p_i=q_it$, which needs $q_i>0$, and Theorem 1 is false for $q\ge0$: with $m=k=2$, $n=1$, $\phi(t)=|t-1|$, $q=(1,0)$, both columns of $C$ equal to $(1,-1)^\top$, $d=(1,-1)$, $a=0$, $B=(0\ \ 1)$, $x=1$, $\rho=1$, $\beta=0$, the vector $p=(1/2,1/2)$ lies in $U$ and violates (11), while $\eta=0$, $\lambda=0$ satisfy (13). Every statement of the mission therefore assumes $q_i>0$ for all $i$. The hypothesis $q\in U$ (the paper's "such that $q\in U$") and $\rho>0$ are kept.

Ruled-out trivializations: a conjugate taken as a supremum over all $t\in\mathbb R$ of a real-valued φ with junk values at $t<0$ is a different function; computing the $\lambda=0$ term as $0\cdot\phi^*(s/0)$ with Lean's $s/0=0$ makes it identically $0$; a real-valued, everywhere finite φ silently excludes the Burg, χ² and J divergences; dropping $q\in U$ or $\rho>0$ removes the Slater point and changes the theorem. The mission's definitions avoid all four.

Needed infrastructure: suprema of EReal-valued families over half-lines and orthants, the interchange of a supremum over a product with a finite sum, and a Lagrangian strong-duality theorem with attainment for a convex program with finitely many affine inequality constraints and one convex, possibly infinite-valued, inequality constraint with a Slater point in the interior of its domain. That duality theorem, and the φ-divergence definitions, are reusable beyond this mission, in particular for the paper's Corollaries 2–5 and for other distributionally robust formulations. Contributions of any of these pieces as separate theorems are welcome.

Selected references

• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
• L. Pardo, Statistical Inference Based on Divergence Measures, Chapman & Hall/CRC, 2006. https://doi.org/10.1201/9781420034813
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Networks of queues model computer systems, communication networks and manufacturing lines: customers (jobs, packets, parts) move between service centers, wait, receive service and move on. Their equilibrium behaviour determines throughputs, utilizations and response times, and for most networks it can only be computed by solving the full balance equations of a continuous-time Markov chain whose state space grows combinatorially with the number of centers and customers. A product-form network is one whose equilibrium distribution factorizes over the centers; for such networks performance measures can be computed exactly by efficient algorithms (convolution, mean value analysis), and this is the basis of much of classical computer-performance modelling.

Timeline of the main product-form results:

• 1957–1963, Jackson (Oper. Res. 5, 1957; Manag. Sci. 10, 1963): open networks of exponential FCFS queues, one customer class, Poisson arrivals.
• 1967, Gordon and Newell (Oper. Res. 15): the closed single-class exponential case.
• 1975, Baskett, Chandy, Muntz and Palacios (J. ACM 22): several customer classes with class switching, four service disciplines (FCFS, processor sharing, infinite server, preemptive-resume LCFS), service times with rational Laplace transforms at the last three, and open, closed or mixed networks with state-dependent Poisson arrivals. This is the BCMP theorem, the subject of this mission.
• 1975–1979, Kelly (J. Appl. Prob. 12, 1975; Reversibility and Stochastic Networks, Wiley 1979): symmetric queues and quasi-reversibility, a general framework containing the BCMP disciplines.

Setting

A network has $N$ service centers and $R$ customer classes. A class-$r$ customer finishing service at center $i$ next requires center $j$ in class $s$ with probability $p_{i,r;j,s}$ and leaves the network with probability $1-\sum_{j,s}p_{i,r;j,s}$. The pairs $(i,r)$ are partitioned into subchains $E_1,\dots,E_m$ that routing never leaves. Each center has one of four types:

1. FCFS, with an exponential service time of rate $\mu_i$ common to all classes;
2. a single processor-sharing server (each of $n$ customers is served at rate $1/n$);
3. an infinite-server center;
4. a single preemptive-resume LCFS server.

At types 2–4 the class-$r$ service time is Coxian: $u_{ir}\ge1$ exponential stages of rates $\mu_{irl}$, and after stage $l$ the customer continues with probability $a_{irl}$ or finishes with probability $b_{irl}=1-a_{irl}$. The state $S=(x_1,\dots,x_N)$ records the FCFS order of classes at type 1, the number $m_{irl}$ of class-$r$ customers in stage $l$ at types 2 and 3, and the LCFS order of (class, stage) pairs at type 4. External arrivals are Poisson, either with rate $\lambda(M(S))$ depending on the total population $M(S)$ (process A) or with one stream per subchain of rate $\lambda_k(M(S/E_k))$ (process B); an arrival joins center $j$ in class $s$ with probability $q_{js}$. A subchain with $q\equiv0$ is closed and keeps a fixed population $K_k$.

With relative arrival rates $e_{ir}\ge0$ solving the traffic equations $\sum_{(i,r)}e_{ir}p_{i,r;j,s}+q_{js}=e_{js}$ and $A_{irl}=\prod_{j<l}a_{irj}$ (the probability of reaching stage $l$, stages numbered from 0), the paper defines $f_i(x_i)$ per center type and a factor $d(S)$ from the arrival rates.

Formalization targets

Goal: the BCMP theorem (§3.2, pp. 253–254)

$$\pi(S)=d(S)\,f_1(x_1)\,f_2(x_2)\cdots f_N(x_N)$$

satisfies the global balance equations of the network, and, under the paper's assumption that the equilibrium distribution is unique, every equilibrium distribution equals $\pi/Z$ whenever $Z=\sum_S\pi(S)$ is finite and positive. The goal covers all four center types, open, closed and mixed networks, and both arrival processes.

Milestones

• §3.1 (p. 252): independent balance implies global balance.
• §3.2 (p. 254): the product form satisfies the independent balance equations.
• §4.1 (p. 254): the aggregate-state probabilities are $C\,d(S)\,g_1(y_1)\cdots g_N(y_N)$.

A further supporting item, also from §4.1 (p. 254), states that summing $f_i$ over local states with fixed class counts gives $g_i$. So $g_i$ depends on the service times only through their means $1/\mu_{ir}=\sum_lA_{irl}/\mu_{irl}$.

Significance

The theorem places the four disciplines, class switching and mixed open/closed populations under one formula. Its corollary in §4.1, that aggregate probabilities depend on service time distributions only through their means (insensitivity), is what makes the model usable with measured mean service times, and it underlies the convolution and mean value analysis algorithms for normalizing constants.

The result is classical and proved on paper. As far as the platform's catalogue shows, it is not formalized: the platform has Kelly's single-class migration process with exponential service, a special case. A machine-checked BCMP theorem would provide a verified multiclass queueing-network model (states, event-driven transition rates, balance equations) on which later results can build: mean value analysis, the state-dependent rates of §5, and the open-network marginals of §4.2.

The printed statement contains an error. The paper defines $A_{irl}=\prod_{j=1}^{l}a_{irj}$ (p. 253). With the branching of its Figs. 1 and 3, this product includes the branch out of stage $l$. For exponential service ($u_{ir}=1$) it gives $A_{ir1}=a_{ir1}=0$, so every $f_i$ of a type 2–4 center with a customer present vanishes, and a closed network of such centers would have no normalizable solution. The mission states the corrected theorem with $A_{irl}=\prod_{j<l}a_{irj}$, which the mean-service-time identity of §4.1 also requires. The type-2 factor $1/m_{ikl}!$ is read as $1/m_{irl}!$.

Difficulty

The algebra of the paper's proof is local: each independent balance equation reduces to the traffic equations. The difficulty is in making that statement precise for a real state space. The independent balance equations need a consistent labelling of each moving customer by the "stage" it leaves and enters. That labelling has to cover FCFS centers, where per-class labels are inconsistent (p. 253), the outside world of each open subchain, and LCFS preemption. Every in-flow into a state is a sum over predecessor states, and those states differ by list operations (appending at an FCFS tail, pushing on an LCFS head) or by stage-count updates. The factorials in the processor-sharing and infinite-server factors, and the telescoping identity $\sum_lA_{irl}b_{irl}=1$ for departures, must line up exactly with the rates. The obvious shortcut is to check global balance directly for a single class with exponential service. That covers neither class switching, nor Coxian stages, nor mixed networks.

Formalization scope

Centers are Fin N, classes Fin R and subchains Fin m. The class-$r$ stages at center $i$ are Fin (u i r) with u i r : ℕ+, numbered from 0. A local state is an inductive type with three shapes (FCFS list, stage-count array, LCFS list of (class, stage) pairs). The state space is the subtype of configurations whose shapes match the center types and whose closed subchains hold their fixed populations. Transition rates are the sums of the rates of explicit events (arrivals, FCFS completions, stage moves and completions, LCFS moves and completions). Global balance uses tsum; every state has finitely many successors and predecessors with nonzero rate, so these sums are finite. The standing assumptions (substochastic routing closed on subchains, closed subchains with no arrivals and no departures, positive rates, continuation probabilities in $[0,1]$ vanishing at the last stage) are collected in Network.IsValid. Irreducibility of subchains is not assumed, and any nonnegative solution of the traffic equations is allowed. Under process B the product in $d(S)$ runs over open subchains only. Uniqueness of the equilibrium is a hypothesis, as in the paper. The type-1 rate is constant, and the state-dependent rates of Condition 1 and §5 are not covered.

The following formalizations would trivialize the mission and are ruled out: stating only global balance of $\pi$ (satisfied by $\pi\equiv0$), quantifying over arbitrary rate functions instead of the rates built from the network data, and restricting the goal to exponential service or to a single class.

Needed infrastructure: finite-support tsum manipulations, multinomial identities for the §4.1 sums over orderings and stage assignments, and bookkeeping for list and array updates. The model and the balance-equation layer can be reused for later queueing missions. Contributions are welcome on each milestone, on the per-center-type pieces of the independent balance check, and on helper lemmas about the event system.

Selected references

• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, Closed, and Mixed Networks of Queues with Different Classes of Customers, J. ACM 22(2):248–260, 1975. https://doi.org/10.1145/321879.321887
• J. R. Jackson, Networks of Waiting Lines, Operations Research 5(4):518–521, 1957. https://doi.org/10.1287/opre.5.4.518
• J. R. Jackson, Jobshop-like Queueing Systems, Management Science 10(1):131–142, 1963. https://doi.org/10.1287/mnsc.10.1.131
• W. J. Gordon, G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2):254–265, 1967. https://doi.org/10.1287/opre.15.2.254
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979. http://www.statslab.cam.ac.uk/~frank/rsn.html
• D. R. Cox, A Use of Complex Probabilities in the Theory of Stochastic Processes, Proc. Cambridge Phil. Soc. 51:313–319, 1955. https://doi.org/10.1017/S0305004100030231

This mission formalizes §6 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: the definition of Thompson's group $V$ and Thompson's proof that $V$ is simple.

Motivation

Thompson's groups $T$ and $V$, introduced in unpublished notes of Richard Thompson in 1965, were the first known examples of infinite, finitely presented, simple groups. The notes of Cannon, Floyd and Parry were written in part "to make available Thompson's unpublished proofs … of the simplicity of $T$ and $V$" (p. 216); §6 is the proof for $V$.

$V$ contains $T$, which contains $F$. Earlier missions on this platform formalize $F$ and its commutator subgroup (§1 and §4), its tree-diagram normal form (§2), its presentations (§3), and the simplicity of $T$ (§5). Unlike $T$, the elements of $V$ need not be continuous: they cut the circle into pieces and rearrange them in any order, so $V$ contains every finite symmetric group.

Setting

The circle $S^1$ is $[0,1]$ with its endpoints identified, in Lean UnitAddCircle ($\mathbb{R}/\mathbb{Z}$); $[x]$ denotes the image of $x \in \mathbb{R}$. Maps compose right to left, $(fg)(t) = f(g(t))$, and $[x, y] = xyx^{-1}y^{-1}$.

The group $V$ (p. 240) consists of the right-continuous bijections of $S^1$ that map images of dyadic rationals to images of dyadic rationals, are differentiable except at finitely many images of dyadic rationals, and are linear with slope a power of $2$ on each maximal interval of differentiability. In Lean a permutation $f$ of the circle satisfies IsThompsonV f when it maps dyadic points to dyadic points and, for a finite set of dyadic breakpoints, is $[z] \mapsto [2^n z + c]$ on each half-open piece between consecutive breakpoints modulo $1$. V is the subgroup generated by these maps; that they already form a group is the first milestone.

The elements. $A$, $B$, $C$ are $T$'s generators, and $\pi_0$ (mapPi0) exchanges $[0, \tfrac12)$ and $[\tfrac12, \tfrac34)$ by $x \mapsto x/2 + \tfrac12$ and $x \mapsto 2x - 1$. The words $X_0 = A$, $X_n = A^{-(n-1)}BA^{n-1}$, $C_n = A^{-(n-1)}CB^{n-1}$, $\pi_1 = C_2^{-1}\pi_0C_2$ and $\pi_n = A^{-(n-1)}\pi_1A^{n-1}$ (p. 241) are defined once, as words in four symbols, and read both as maps of the circle and in $V_1$.

The presented group $V_1$ (p. 242) is the free group on $A$, $B$, $C$, $\pi_0$ modulo fourteen relators: the six relators of $T_1$ (§5), and eight more involving the $\pi_n$, such as $\pi_1^2$, $(\pi_2\pi_1)^3$ and $(\pi_1C_2)^3$. In $V_1$, $\Pi(n)$ is the subgroup generated by $\pi_0, \dots, \pi_{n-1}$, $\Pi = \bigcup_n \Pi(n)$, and an element is positive when it is a product of nonnegative powers of the $X_i$.

Target

The goal is the sentence in which the notes state what §6 does, "In §6 we define $V$ and give Thompson's proof that $V$ is simple" (p. 216):

$$V \text{ is simple.}$$

The route is the section's own. Lemma 6.1 shows that $A$, $B$, $C$, $\pi_0$ generate $V$ and satisfy the fourteen relations, so $V_1$ maps onto $V$. Lemmas 6.2–6.8 establish how the $\pi_i$ move past the $X_j$ and $C_n$, leading to Theorem 6.9, $V_1$ is simple, and hence $V_1 \cong V$. The goal follows.

Significance

The result. $V$ is the third of Thompson's groups and the one whose elements rearrange pieces of the circle: it is infinite, finitely presented and simple, and it contains every finite group (through the finite symmetric groups). Together with $T$ it gave the first examples of infinite finitely presented simple groups.

Formalizing it. No machine-checked proof that $V$ is simple exists on this platform, and Mathlib has nothing on Thompson's groups. This mission reuses the formalization of $F$ and $T$: $V_1$'s first six relators are $T_1$'s, and the proof of Theorem 6.9 applies Theorem 5.7 and Theorem 5.8 inside $V_1$.

Difficulty

The central difficulty is the generation half of Lemma 6.1. The notes' proof uses tree diagrams with labelled leaves: every element of $V$ permutes the intervals of one standard dyadic partition onto those of another, $F$ moves any partition to a standard comb, and the subgroup generated by $\pi_0$ and $C_{n-2}$ acts as the full symmetric group on the comb's intervals. Each step is stated in one sentence; the milestones make each a separate statement.

The algebra of $V_1$ (Lemmas 6.2–6.6) is a chain of inductions. The proofs lean on two facts the notes use without isolating them: that $T_1$ maps to $V_1$ (so §5's lemmas hold in $V_1$), and the normal form $g = p\pi C_n^m q^{-1}$ in $V_1$, stated inside the proof of Theorem 6.9. Both are milestones here. The notes also cite two facts about the finitary symmetric group $\Sigma$ without proof, its presentation and the behaviour of its proper quotients, and deduce $\Pi \cong \Sigma$; the proof of Theorem 6.9 uses all three, and each is a milestone.

What is left out

• Figures 16–19, tree-diagram computations for relations 11) and 12); the relations are stated directly in Lemma 6.1.

Formalization scope

• $V$ is a Subgroup (Equiv.Perm UnitAddCircle) generated by IsThompsonV. Half-open pieces make every element right-continuous; "linear" is read modulo $1$, so a piece may wrap past $[0]$, as a rotation does. Unlike $T$, no lift to the line is available, since elements of $V$ need not be monotone.
• $V_1$ is Mathlib's PresentedGroup on the four-element type FormalV. Relators are written out as $xyx^{-1}y^{-1}$.
• $\Sigma$ is SigmaPerm, the subgroup of Equiv.Perm ℕ of permutations moving finitely many points, and $s_i$ is the transposition of $i$ and $i + 1$; its presentation is a PresentedGroup on ℕ. $\Pi$ is taken as the subgroup of $V_1$ generated by all the $\pi_i$, which is the union of the $\Pi(n)$.
• Lemma 6.1's surjection and the isomorphism $V_1 \cong V$ pin the images of the four symbols, so no isomorphism ignoring the generators satisfies them.
• Reused platform theorems, which solutions may import: Theorem 3.4, Corollary 2.6, Lemma 4.2, Theorem 4.11, and from §5 Lemma 5.2, Lemmas 5.5 and 5.6, Theorem 5.7 and Theorem 5.8. The standard dyadic partitions of the tree-diagram milestone are the §2 bundle's IsStandardDyadicPartition.

Selected references

• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, §6 pp. 240–248. doi:10.5169/seals-87877

Motivation

Gibbons and Hawking conjectured that the cosmological horizon of a de Sitter static patch carries an entropy, computed semiclassically by the Euclidean gravitational path integral on the sphere. For three-dimensional de Sitter gravity the relevant quantity is $\log|Z^{S^3}_{\mathrm{grav}}|$, whose leading term is the Gibbons–Hawking entropy $S_{\mathrm{GH}} = \pi\ell_{\mathrm{dS}}/(2G_N)$. A microscopic account of this entropy — a count of states in some ordinary quantum or statistical system — is one of the long-standing goals of de Sitter holography.

Collier, Eberhardt and Mühlmann (arXiv:2501.01486) propose that pure dS$_3$ quantum gravity is dual to the double-scaled two-matrix integral of the complex Liouville string (arXiv:2409.17246). In §4.4 they test this by counting the "effective number of eigenvalues" of the matrix model and comparing $2\log N_{\mathrm{eff}}$ with $\log|Z^{S^3}_{\mathrm{grav}}|$. The comparison reduces to explicit identities between elementary functions of the Liouville parameter $b$; this mission formalizes exactly those identities.

Setting

Fix a complex number $b$ with $-ib^2 \in \mathbb{R}_{>0}$, i.e. $b^2 = i\beta$ with $\beta>0$ (the paper's footnote 2; then the central charge $c = 1+6(b+b^{-1})^2$ lies in $13+i\mathbb{R}$). Write $b^{-2} = (b^2)^{-1}$ and let $S_0\in\mathbb{R}$ be the genus-counting parameter of the matrix model.

• Eigenvalue density (eq. (C.4)): for real $E$,

$$\rho_0(E) = \frac{2}{\pi}\,\sinh(-i\pi b^2)\,\sin\!\Big(-ib^2\,\operatorname{arccosh}\frac{E}{2}\Big).$$

• First zero (§4.4): $E_0 = 2\cos(\pi b^{-2})$.
• Effective number of eigenvalues (eq. (4.32)): $N_{\mathrm{eff}} = \int_2^{E_0} e^{S_0}\rho_0(E)\,dE$.
• Microscopic entropy (eq. (4.33)): $S^{\mathrm{micro}}_{\mathrm{dS}} = 2\log N_{\mathrm{eff}}$.
• ZZ-instanton tension (eq. (4.34)): $\widehat T^{(b)}_{1,1} = \dfrac{8b^2\sin(\pi b^2)\sin(\pi b^{-2})}{1-b^4}$ and $T^{(b)}_{1,1} = e^{S_0}\,\widehat T^{(b)}_{1,1}$.
• Sphere normalization (eq. (4.4)): $C^{(b)}_{S^2} = 32\pi^4\Big(\dfrac{\sin(\pi b^2)\sin(\pi b^{-2})}{b^2-b^{-2}}\Big)^2$.
• Sphere partition function (eq. (4.5)): $Z^{S^3}_{\mathrm{grav}} \sim e^{2S_0}\,\dfrac{\sin(\pi b^2)^2\sin(\pi b^{-2})^2}{(b^{-2}-b^2)^2}$, where $\sim$ is equality up to a $b$-independent constant.

Formalization targets

Goal (eq. (4.35))

For any function $Z(b,S_0)$ whose modulus equals $K\cdot\big|e^{2S_0}\sin(\pi b^2)^2\sin(\pi b^{-2})^2/(b^{-2}-b^2)^2\big|$ for a fixed constant $K>0$ (the content of (4.5)), there is a real constant $c$, independent of $b$ and $S_0$, such that

$$S^{\mathrm{micro}}_{\mathrm{dS}}(b,S_0) = \log|Z(b,S_0)| + c \qquad\text{for all admissible } b \text{ and all } S_0.$$

This is the paper's statement that the matrix-model count reproduces the de Sitter entropy "regardless of the specific value of $Z^{S^3}_{\mathrm{grav}}$", up to the order-one constants that (4.37) later fixes.

Milestones

1. $E_0$ is real, $E_0>2$, $\rho_0(E_0)=0$, and $\rho_0$ is real and positive on $(2,E_0)$ (§4.4, App. C).
2. Closed form of $N_{\mathrm{eff}}$ (eqs. (4.32)–(4.33)).
3. The two expressions for $S^{\mathrm{micro}}_{\mathrm{dS}}$ in eq. (4.33).
4. $(\widehat T^{(b)}_{1,1})^2 \sim C^{(b)}_{S^2}$ (eq. (4.36)).

Significance

The identity (4.36) is the step the authors single out as "a genuinely nontrivial check": it holds for the complex Liouville string but, as they note, not for the Virasoro minimal string. The goal packages the argument of §4.4 into one exact statement, valid for every admissible $b$ (i.e. exactly in $G_N$), under the single physical input (4.5). The physical assumptions — the choice of cutoff at the first zero, the interpretation of $\log N^2$ as an entropy, and (4.5) itself — are not formalized; they enter as definitions and as the hypothesis on $Z$. The mathematical content is a definite-integral evaluation plus trigonometric/hyperbolic identities for complex arguments.

Difficulty

The integral in (4.32) has a complex-looking integrand, a branch of $\operatorname{arccosh}$, and an upper limit given by a complex cosine; one must first show that everything is real in the admissible regime and then evaluate the integral exactly, including the endpoint behaviour at $E=2$ where $\operatorname{arccosh}$ is not differentiable. The entropy statements additionally involve the complex principal logarithm, so one must control the argument (positivity) of $N_{\mathrm{eff}}$ and of the tension ratio; identities such as $\log(e^{S_0}x) = S_0+\log x$ fail for general complex $x$.

Formalization scope

• $b\in\mathbb{C}$ with the hypothesis $\exists\beta>0,\ b^2 = i\beta$; all objects depend on $b$ only through $b^2$.
• $\rho_0 : \mathbb{R}\to\mathbb{C}$ uses Mathlib's Real.arcosh (defined as $\log(x+\sqrt{x^2-1})$); its values for $E<2$ never enter.
• $N_{\mathrm{eff}}$ is the oriented interval integral from $2$ to $\operatorname{Re}E_0$; milestone 1 shows $E_0$ is real, so taking the real part loses nothing.
• $\log$ is the complex principal logarithm (Complex.log), and $S^{\mathrm{micro}}_{\mathrm{dS}}$ is complex-valued; the goal forces it to equal a real number.
• The "$\sim$" of (4.5) is encoded as a constant factor $K>0$ in the modulus; the "$\sim$" of (4.36) as a nonzero $b$-independent complex constant.
• A trivialization is ruled out: the goal quantifies $c$ before $b$ and $S_0$, and $K>0$ is required.

Selected references

• S. Collier, L. Eberhardt, B. Mühlmann, A microscopic realization of dS$_3$, arXiv:2501.01486 (2025). https://arxiv.org/abs/2501.01486
• S. Collier, L. Eberhardt, B. Mühlmann, V. A. Rodriguez, The complex Liouville string, arXiv:2409.17246 (2024). https://arxiv.org/abs/2409.17246
• G. W. Gibbons, S. W. Hawking, Cosmological event horizons, thermodynamics, and particle creation, Phys. Rev. D 15 (1977) 2738. https://doi.org/10.1103/PhysRevD.15.2738

Motivation

Heisenberg's uncertainty principle is the first quantitative statement a student meets about the incompatibility of position and momentum measurements in quantum mechanics. In A. O. Lopes' textbook Uma Breve Introdução à Matemática da Mecânica Quântica (31º Colóquio Brasileiro de Matemática, IMPA, 2017), written for mathematics students with no physics background, it is the capstone of Chapter 8 (Princípio da Incerteza e o Pacote de Onda Gaussiano), Teorema 8.2, p. 131. It collects the operator formalism built in Chapters 1, 3 and 4 — position and momentum operators, commutators, expected values — into one inequality. This mission is the first of a series formalizing the capstone results of the book.

Setting

A wave function is a map $\psi:\mathbb R^n\to\mathbb C$. The book uses the $L^2$ inner product $\langle \varphi,\psi\rangle=\int_{\mathbb R^n}\varphi(x)\,\overline{\psi(x)}\,dx$ (linear in the first slot) and the norm $|\psi|=\langle\psi,\psi\rangle^{1/2}$. A state is a wave function with $|\psi|=1$. Fix $n\ge 1$, an index $j\in\{1,\dots,n\}$ and the (reduced) Planck constant $\hbar>0$.

• The position operator is $(X_j\psi)(x)=x_j\,\psi(x)$, with domain $D(X_j)=\{\psi\in L^2 : x_j\psi\in L^2\}$.
• The momentum operator is $(P_j\psi)(x)=-i\hbar\,\dfrac{\partial\psi}{\partial x_j}(x)$ (Definição 1.20), with domain $D(P_j)$ the $C^1$ functions of compact support.
• The commutator of two operators is $[A,B]=AB-BA$ (Definição 3.1).
• The expected value of $A$ in $\psi$ is $E_\psi(A)=\dfrac{\langle A\psi,\psi\rangle}{\langle\psi,\psi\rangle}$ (Definição 8.1, p. 125, and p. 128).
• The dispersion of $A$ in $\psi$ is $\Delta_\psi(A)=\big|\,(A-E_\psi(A)\,I)\psi\,\big|$ (Definição 8.2).
• The Gaussian wave packet with parameters $a>0$, $x_0,p_0\in\mathbb R^n$ is $\psi(x)=(2\pi a^2)^{-n/4}\,e^{-|x-x_0|^2/(4a^2)}\,e^{\,i\langle p_0,x\rangle/\hbar}$ (Definição 8.3).

Formalization targets

Goal — Teorema 8.2 (Heisenberg)

For every state $\psi\in D(X_j)\cap D(P_j)$,

$$\Delta_\psi(X_j)\,\Delta_\psi(P_j)\;\ge\;\frac{\hbar}{2}.$$

Milestones

1. Lema 3.2 (canonical commutation relations): $[X_k,X_j]=[P_k,P_j]=0$, $\tfrac{i}{\hbar}[P_j,X_j]=\mathrm{Id}$, and $\tfrac{i}{\hbar}[P_j,X_k]=0$ for $j\ne k$.
2. p. 23 — $X_j$ is symmetric: $\langle X_j\psi,\varphi\rangle=\langle\psi,X_j\varphi\rangle$ on $D(X_j)$.
3. pp. 26–27 — $P_j$ is symmetric: $\langle P_j\psi,\varphi\rangle=\langle\psi,P_j\varphi\rangle$ on $D(P_j)$.
4. Proposição 8.1 — $\Delta_\psi(A)=0$ if and only if $\psi$ is an eigenfunction of $A$.
5. Definição 8.3 / p. 133 — the Gaussian packet is a state with $E(X_j)=(x_0)_j$, $E(P_j)=(p_0)_j$, $\Delta(X_j)=a$, and it attains equality $\Delta(X_j)\,\Delta(P_j)=\hbar/2$.

Significance

The inequality is the prototype of all Robertson-type uncertainty relations and is the point where the commutator formalism of the book produces a numerical, physically testable consequence. Milestone 5 shows the constant $\hbar/2$ cannot be improved. The mathematics is classical and fully proved in the source; what this mission adds is a machine-checked version of the textbook's operator calculus on $L^2(\mathbb R^n)$ — integration by parts for compactly supported $C^1$ functions, symmetry of $X_j$ and $P_j$, commutation relations, and explicit Gaussian integrals — reusable by later missions of the series (Ehrenfest's theorem, density operators, quantum statistical mechanics).

Difficulty

The algebraic core is a short Cauchy–Schwarz argument, but it silently uses facts about unbounded operators: that $\langle\psi,[P_j,X_j]\psi\rangle$ may be rewritten as $\langle P_j\psi,X_j\psi\rangle-\langle X_j\psi,P_j\psi\rangle$ requires integration by parts with vanishing boundary terms, and the reduction to mean-zero observables requires the expected values to be real. Each of these needs integrability bookkeeping that the book leaves implicit. The Gaussian milestone requires evaluating first and second moments of Gaussian integrals in $n$ dimensions.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure; wave functions are plain functions ℝⁿ → ℂ (not $L^2$ classes), operators are maps on such functions, and domains are imposed as explicit hypotheses (InPositionDomain, InMomentumDomain).
• The partial derivative $\partial/\partial x_j$ is the Fréchet derivative applied to the $j$-th basis vector.
• Integrals are Bochner integrals, which return $0$ for non-integrable integrands; every statement carries domain hypotheses guaranteeing integrability, so this junk value never enters a meaningful claim.
• Expected values are complex numbers by definition; for symmetric operators they are real, which is part of what solvers must prove.
• The goal is not vacuous: $D(P_j)$ contains nonzero compactly supported $C^1$ functions, which can be normalized.

Contributions welcome: integration-by-parts lemmas on $\mathbb R^n$ for compactly supported $C^1$ functions, Gaussian moment computations, and an abstract Robertson inequality.

Selected references

• A. O. Lopes, Uma Breve Introdução à Matemática da Mecânica Quântica, 31º Colóquio Brasileiro de Matemática, IMPA, 2017. Extended version: http://mat.ufrgs.br/~alopes/hom/livroquantum.pdf
• S. Gustafson, I. M. Sigal, Mathematical Concepts of Quantum Mechanics, Springer. https://doi.org/10.1007/978-3-030-59562-3

This mission formalizes §5 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: the definition of Thompson's group $T$ and Thompson's proof that $T$ is simple.

Motivation

Thompson's groups $T$ and $V$, introduced in unpublished notes of Richard Thompson in 1965, were the first known examples of infinite, finitely presented, simple groups. Every finitely presented simple group known before them was finite. The notes of Cannon, Floyd and Parry were written in part "to make available Thompson's unpublished proofs … of the simplicity of $T$ and $V$" (p. 216), and §5 is that proof for $T$.

$T$ is the circle's counterpart of Thompson's group $F$. Earlier missions on this platform formalize $F$ and its commutator subgroup (§1 and §4 of the same notes), its tree-diagram normal form (§2), and its two presentations (§3). $F$ is not simple: its abelianization is $\mathbb{Z}^2$. $T$ is simple, it has elements of finite order (the generator $C$ below has order $3$), and it contains $F$ as the stabilizer of a point.

Setting

The circle $S^1$ is $[0,1]$ with its endpoints identified, in Lean UnitAddCircle ($\mathbb{R}/\mathbb{Z}$); $[x]$ denotes the image of $x \in \mathbb{R}$. Maps compose right to left, $(fg)(t) = f(g(t))$, and $[x, y] = x y x^{-1} y^{-1}$, the convention of the notes.

The group $T$ (pp. 233–234) consists of the piecewise linear homeomorphisms of $S^1$ that map images of dyadic rationals to images of dyadic rationals, are differentiable except at finitely many images of dyadic rationals, and have slopes that are powers of $2$. In Lean a permutation $f$ of the circle satisfies IsThompsonCircle f when it has a lift to the line: an order isomorphism $L$ of $\mathbb{R}$ with $L(x+1) = L(x) + 1$ and $f[x] = [L(x)]$, mapping dyadic rationals to dyadic rationals, and affine with slope a power of $2$ between consecutive integer translates of finitely many dyadic breakpoints. T is the subgroup generated by these maps. That they already form a group is the first milestone.

The elements $A$, $B$, $C$ (Example 5.1). $A$ and $B$ are the generators of $F$ from the §1 mission (mapA, mapB), carried to the circle by toCircle, which sends an order isomorphism $g$ of $[0,1]$ to $[x] \mapsto [g(x)]$. $C$ (mapC) is given on $[0,1]$ by $x/2 + 3/4$, $2x - 1$ and $x - 1/4$ on $[0, \tfrac12]$, $[\tfrac12, \tfrac34]$ and $[\tfrac34, 1]$. symT sends the formal symbols $A$, $B$, $C$ to these three maps.

The presented group $T_1$ (p. 236) is the free group on formal symbols $A$, $B$, $C$ modulo six relators:

$$[AB^{-1}, A^{-1}BA],\quad [AB^{-1}, A^{-2}BA^2],\quad C^{-1}B(A^{-1}CB),$$ $$((A^{-1}CB)(A^{-1}BA))^{-1}B(A^{-2}CB^2),\quad (CA)^{-1}(A^{-1}CB)^2,\quad C^3.$$

In $T_1$, $X_0 = A$ and $X_n = A^{-(n-1)}BA^{n-1}$ (XT1); $C_0 = 1$ and $C_n = A^{-(n-1)}CB^{n-1}$ (CT1) for $n \ge 1$. An element is positive (IsPositiveT1) when it is a product of nonnegative powers of the $X_i$.

Target

The goal is the sentence in which the notes state what §5 does, "In §5 we define $T$ and give Thompson's proof that $T$ is simple" (p. 216):

$$T \text{ is simple.}$$

The route is the section's own. Lemma 5.2 shows that $A$, $B$, $C$ generate $T$ and satisfy the six relations, so $T_1$ maps onto $T$ (Lemma 5.3). Lemmas 5.4–5.6 and a normal form (Theorem 5.7, every $g \in T_1$ is $p\,C_n^m q^{-1}$ with $p$, $q$ positive and $m < n + 2$) lead to Theorem 5.8, $T_1$ is simple, and hence to Corollary 5.9, $T_1 \cong T$. The goal follows.

Significance

The result. The simplicity of $T$ is one of the two facts that made Thompson's groups famous: $T$ is an infinite, finitely presented, simple group. Corollary 5.9 gives more, an explicit presentation of $T$ on three generators and six relators.

Formalizing it. No machine-checked proof that $T$ is simple exists on this platform, and Mathlib has nothing on Thompson's groups. The proof in the notes is short and complete. This mission connects the analytic definition of $T$ with the combinatorial group $T_1$, reusing the platform's formalization of $F$: the presentation of $F$ (Theorem 3.4), its normal form (Corollary 2.7), and the fact that its proper quotients are Abelian (Theorem 4.3).

Difficulty

The algebra of $T_1$ (Lemmas 5.5 and 5.6) is a chain of explicit inductions. The substance lies at two points.

The first is Theorem 5.7. The notes' proof that the set of elements $p\,C_n^m q^{-1}$ is closed under multiplication moves $q_1^{-1}p_2$ past $C_j^i$ and $C_l^k$ using the normal form of $F$, transported into $T_1$ through Lemma 5.4, and then re-indexes, all inside the abstract group $T_1$ with no geometry to lean on.

The second is the analytic side of Lemma 5.2. Generation reduces an arbitrary $f \in T$ to an element of $F$ by composing with $C$ and with an element of $F$ that moves $f([0])$ to $[\tfrac34]$. That needs the fact that an element of $T$ fixing $[0]$ comes from $F$, which the notes state in one line. The relations are identities between explicit piecewise linear maps of the circle.

What is left out

• The remark that $T$ is conjugate to a group of $C^\infty$ diffeomorphisms (Ghys–Sergiescu, p. 234). It is not used.
• Tree diagrams for $T$ and Figures 11–15. The notes use them only to verify relations 3)–6), and those relations are stated directly in Lemma 5.2.
• The observation on p. 237 that $C_n$ permutes $n + 2$ intervals cyclically, given "to gain some insight" and not used afterwards.

Formalization scope

• $T$ is a Subgroup (Equiv.Perm UnitAddCircle) generated by IsThompsonCircle. The lift makes every element an orientation-preserving homeomorphism, so continuity is not stated separately. Unlike for $F$, the condition that dyadics map to dyadics cannot be dropped: an irrational rotation satisfies every other clause.
• $T_1$ is Mathlib's PresentedGroup on the three-element type FormalABC. Relators are written out as $xyx^{-1}y^{-1}$, not with commutator notation.
• Lemma 5.3 and Corollary 5.9 pin the images of the three symbols, so no isomorphism that ignores the generators can satisfy them. Lemma 5.4 pins the images of $A$ and $B$.
• Reused platform theorems, which solutions may import: Theorem 3.4 ($F_1 \cong F$), Corollary 2.6 ($A$, $B$ generate $F$), Lemma 4.2, Corollary 2.7, Lemma 2.8, Theorem 4.3, line (3.2), and Theorem 4.11 ($F$ is totally ordered, hence torsion-free).
• Welcome beyond the milestones: §6's group $V$, whose presentation extends $T_1$.

Selected references

• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, §5 pp. 233–240. doi:10.5169/seals-87877
• É. Ghys, V. Sergiescu, Sur un groupe remarquable de difféomorphismes du cercle, Comment. Math. Helv. 62 (1987) 185–239. doi:10.1007/BF02564445

Motivation

General relativity is summed up, in S. M. Carroll's A No-Nonsense Introduction to General Relativity (2001), by two statements: spacetime is a curved pseudo-Riemannian manifold with a metric of signature $(-+++)$, and the metric obeys Einstein's equation $R_{\mu\nu}-\frac12Rg_{\mu\nu}=8\pi GT_{\mu\nu}$. The first exact solution of that equation, and still the most important one, is the Schwarzschild metric: it describes the gravitational field of the Sun outside its surface, the classical tests of GR (perihelion precession, light bending), and non-rotating black holes. Carroll's notes state its key property in one sentence: for a spherically symmetric metric, the vacuum equation has a unique solution, (72) — Birkhoff's theorem. This mission is the first of a series formalizing the capstone results of those notes.

Setting

We work in a single coordinate chart of four-dimensional spacetime. A point is $x=(x^0,x^1,x^2,x^3)\in\mathbb R^4$; a metric is a field $x\mapsto g_{\mu\nu}(x)$ of real symmetric $4\times4$ matrices of signature $(-+++)$, i.e. congruent to $\eta=\mathrm{diag}(-1,1,1,1)$. From $g$ and its inverse $g^{\mu\nu}$ one builds, exactly as in Carroll's equations:

• the Christoffel symbols $\Gamma^\sigma_{\mu\nu}=\frac12g^{\sigma\rho}(\partial_\mu g_{\nu\rho}+\partial_\nu g_{\rho\mu}-\partial_\rho g_{\mu\nu})$ (36) and the covariant derivative (35);
• the Riemann tensor $R^\sigma{}_{\mu\alpha\beta}=\partial_\alpha\Gamma^\sigma_{\mu\beta}-\partial_\beta\Gamma^\sigma_{\mu\alpha}+\Gamma^\sigma_{\alpha\lambda}\Gamma^\lambda_{\mu\beta}-\Gamma^\sigma_{\beta\lambda}\Gamma^\lambda_{\mu\alpha}$ (44);
• the Ricci tensor $R_{\alpha\beta}=R^\lambda{}_{\alpha\lambda\beta}$ (45), Ricci scalar $R=g^{\mu\nu}R_{\mu\nu}$ (46) and Einstein tensor $G_{\mu\nu}=R_{\mu\nu}-\frac12Rg_{\mu\nu}$ (50).

In spherical coordinates $(t,r,\theta,\phi)=(x^0,x^1,x^2,x^3)$ the general spherically symmetric metric is (71)

$$ds^2=-A(r,t)\,dt^2+B(r,t)\,dr^2+r^2(d\theta^2+\sin^2\theta\,d\phi^2),$$

and the Schwarzschild metric (72) is the case $A=1-2Gm/r$, $B=(1-2Gm/r)^{-1}$.

Target

The goal is the uniqueness statement of §6 of the notes, in the form: for $A,B$ smooth and positive on a rectangle $(r_1,r_2)\times(t_1,t_2)$ with $r_1\ge0$,

$$R_{\mu\nu}\big[-A\,dt^2+B\,dr^2+r^2d\Omega^2\big]=0\iff\exists\,m,\ f>0:\ A=f(t)\Big(1-\frac{2Gm}{r}\Big),\ B=\Big(1-\frac{2Gm}{r}\Big)^{-1}.$$

The milestones follow the notes in order:

1. eqs. (18)–(20): Minkowski space in spherical coordinates;
2. eq. (25): $g^{\mu\nu}g_{\mu\nu}=4$;
3. after eq. (36): $\Gamma^\sigma_{\mu\nu}=\Gamma^\sigma_{\nu\mu}$;
4. eq. (37): metric compatibility $\nabla_\sigma g_{\mu\nu}=0=\nabla_\sigma g^{\mu\nu}$;
5. eq. (47): the algebraic symmetries of $R_{\mu\nu\rho\sigma}$;
6. eq. (48): $R_{\mu\nu}=R_{\nu\mu}$;
7. eq. (49): the Bianchi identity $\nabla_{[\lambda}R_{\mu\nu]\rho\sigma}=0$;
8. eq. (51): the contracted Bianchi identity $\nabla_\mu G^{\mu\nu}=0$;
9. eq. (67): $-R=8\pi GT$;
10. eq. (68): the trace-reversed Einstein equation;
11. eq. (69): in vacuum, Einstein's equation is $R_{\mu\nu}=0$;
12. eq. (72): the Schwarzschild metric is Ricci-flat for $r>0$, $r\ne2Gm$;
13. Birkhoff's theorem (the "only if" direction of the goal);
14. eqs. (73)–(75): Kruskal coordinates, showing $r=2Gm$ is a coordinate singularity.

Significance

The result. Birkhoff's theorem says the exterior field of any spherically symmetric body — static, pulsating or collapsing — is the Schwarzschild field, determined by a single constant $m$. It is why the Schwarzschild solution governs the solar system and spherical collapse, and why spherically symmetric gravitational radiation does not exist. The identities (37), (47)–(51) and (67)–(69) are the working toolkit of every GR computation; (51) is what makes Einstein's equation consistent with local energy–momentum conservation.

Formalizing it. All results here are classical and proved in the textbooks. The value of the mission is a machine-checked, coordinate-level development of the curvature identities in Carroll's exact conventions, and a checked proof of Birkhoff's theorem, which requires solving the vacuum equations as a system of PDEs rather than verifying a given solution. The platform already contains a separate Einstein-field-equations development (built from a Wikipedia-based definition file with a slightly different index placement) in which Ricci-flatness of the Schwarzschild metric is proved; this mission uses its own Carroll-faithful definitions, and that earlier work may help with milestone 12.

Difficulty

Verifying that a given metric is Ricci-flat (milestone 12) is a long but mechanical computation of derivatives of explicit functions. The goal is different in kind: in the "only if" direction one must extract from $R_{\mu\nu}=0$ that $\partial_tB=0$ (from $R_{tr}=0$), integrate an ODE in $r$ to get $B=(1-C/r)^{-1}$ with $C$ independent of $t$, and then show $A/(1-C/r)$ depends on $t$ only — all with the coordinate derivatives of the formal definitions, inside a region where $A,B$ are only known to be smooth and positive. The general identities (47)–(51) need symmetry of second and third derivatives and the derivative of the matrix inverse.

Formalization scope

• Everything lives in one chart: Coord = Fin 4 → ℝ, a metric is a function Coord → Matrix (Fin 4) (Fin 4) ℝ, partial derivatives are Fréchet derivatives in coordinate directions. All functions are total: non-differentiable points give derivative $0$, singular matrices have inverse $0$, and $a/0=0$. For that reason every statement names the open region (smoothness, signature $(-+++)$, $r>0$, $r\ne2Gm$, $0<\theta<\pi$) on which it is claimed.
• "Spacetime metric on $U$" means: $U$ open, components $C^\infty$ on $U$, and $g(y)$ congruent to $\eta$ for every $y\in U$ (Carroll's standing assumption that the metric has signature $(-+++)$).
• The goal is stated on a coordinate rectangle $(r_1,r_2)\times(t_1,t_2)$ with the angular coordinates ranging over $0<\theta<\pi$, $\phi\in\mathbb R$. The uniqueness is up to rescaling $t$ (the factor $f(t)$); omitting $f$ would make the statement false.
• Kruskal "takes the form" is encoded as the change-of-variables identity $J^{\mathsf T}KJ=g_{\text{Schw}}$, with the implicit relation (75) as a separate conclusion.
• Reusable beyond this mission: the definition file CarrollGR_Defs (Christoffel symbols, covariant derivatives, curvature, Einstein tensor in coordinates) is shared by the whole series. Contributions welcome: general lemmas about partialD of products, quotients and matrix inverses, and a tensoriality lemma for the Ricci tensor under changes of coordinates.

Selected references

• S. M. Carroll, A No-Nonsense Introduction to General Relativity, lecture notes, 2001 (the source; equation numbers above refer to it).
• S. M. Carroll, Lecture Notes on General Relativity, 1997, arXiv:gr-qc/9712019 (the full notes of which the source is an abridgment).
• R. M. Wald, General Relativity, University of Chicago Press, 1984.