All missions

Motivation

The virial theorem relates the long-time average of the total kinetic energy of a bound system of particles to the average of the virial $-\frac12\sum_k \mathbf F_k\cdot\mathbf r_k$ of the forces acting on them. It gives the average kinetic energy of systems too complicated to solve exactly, such as stars, planetary systems, galaxies and galaxy clusters. Fritz Zwicky used it to infer the existence of unseen matter, and it enters the derivation of the Chandrasekhar limit for white dwarfs. It does not depend on the notion of temperature and holds for systems that are not in thermal equilibrium.

Timeline (as recounted in the source article):

• 1772: Lagrange's identity appears in Lagrange's Essay on the Problem of Three Bodies.
• Jacobi generalizes the identity to $n$ bodies.
• 1870: Clausius, lecture On a Mechanical Theorem Applicable to Heat: the mean vis viva of a system equals its virial.
• Later development by Maxwell, Rayleigh, Poincaré, Chandrasekhar, Fermi, Ledoux, Bader and Parker; quantum versions sketched in 1926 and proved by Finkelstein (1928) and Fock (1930).

Setting

$N$ point particles move in $\mathbb R^3$. Particle $k$ has a constant mass $m_k$, position $r_k(t)$, velocity $v_k(t)=\dot r_k(t)$ and momentum $p_k=m_kv_k$; the net force on it is $F_k=\dot p_k$. The kinetic energy is $T=\frac12\sum_km_k\|v_k\|^2$, the moment of inertia is $I=\sum_km_k\|r_k\|^2$, and

$$G=\sum_{k=1}^Np_k\cdot r_k .$$

The time average over a duration $\tau$ is $\langle f\rangle_\tau=\frac1\tau\int_0^\tau f(t)\,dt$.

When forces come from pair potentials $V_{jk}$ depending only on the distance $r_{jk}=\|r_k-r_j\|$, the force of $j$ on $k$ is $F_{jk}=-\nabla_{r_k}V_{jk}(r_{jk})$, $F_k=\sum_jF_{jk}$, and the total potential energy is $V_{\mathrm{TOT}}=\sum_k\sum_{j<k}V_{jk}(r_{jk})$. Power-law potentials are $V_{jk}=\alpha_{jk}r_{jk}^n$; gravity is $n=-1$.

Formalization targets

Goal: the virial theorem

For a motion with $\dot r_k=v_k$, $\dot p_k=F_k$ (continuous forces) that is bounded (positions and velocities bounded for $t\ge0$),

$$\lim_{\tau\to\infty}\Big(2\langle T\rangle_\tau+\sum_{k=1}^N\langle F_k\cdot r_k\rangle_\tau\Big)=0 .$$

Milestones

1. $\frac12\,\dot I=G$.
2. $\dot G=2T+\sum_kF_k\cdot r_k$.
3. With Newton's third law, $\sum_kF_k\cdot r_k=\sum_k\sum_{j<k}F_{jk}\cdot(r_k-r_j)$.
4. Potential pair forces are central: $F_{jk}=-\frac{V_{jk}'(r_{jk})}{r_{jk}}(r_k-r_j)$.
5. Potential pair forces satisfy $F_{jk}=-F_{kj}$.
6. $\sum_kF_k\cdot r_k=-\sum_k\sum_{j<k}V'_{jk}(r_{jk})\,r_{jk}$.
7. Power law: $\sum_kF_k\cdot r_k=-nV_{\mathrm{TOT}}$.
8. Power law: $\dot G=2T-nV_{\mathrm{TOT}}$.
9. Lagrange's identity ($n=-1$): $\frac12\ddot I=2T+V_{\mathrm{TOT}}$.
10. $\langle\dot G\rangle_\tau=\frac{G(\tau)-G(0)}{\tau}=2\langle T\rangle_\tau+\sum_k\langle F_k\cdot r_k\rangle_\tau$.
11. Bounded motion: $\langle\dot G\rangle_\tau\to0$.
12. Power-law virial theorem: $\langle T\rangle_\tau-\frac n2\langle V_{\mathrm{TOT}}\rangle_\tau\to0$ for bounded collision-free motion.

Significance

The theorem turns boundedness of a motion into a quantitative relation between averaged energies, without solving the equations of motion; with $n=-1$ it gives $\langle T\rangle=-\frac12\langle V_{\mathrm{TOT}}\rangle$ for self-gravitating systems, the relation used for mass estimates of galaxy clusters. The result is classical and proved in the literature. This mission formalizes the standard derivation: the calculus identities for $I$ and $G$, the pair-force algebra under Newton's third law, the gradient computation for distance potentials, and the averaging argument.

Difficulty

The mathematics is elementary; the work lies in the formal infrastructure: product rules for inner products of vector-valued trajectories, the gradient of $y\mapsto V(\|y-x\|)$ in $\mathbb R^3$, re-indexing a double sum over ordered pairs into a sum over $j<k$, and the fundamental theorem of calculus for $\int_0^\tau\dot G$ with the required integrability. A tempting oversimplification is to assume that $\langle T\rangle_\tau$ and $\langle F\cdot r\rangle_\tau$ converge individually; bounded motion does not guarantee this, so the targets are stated as limits of the combined expression.

Formalization scope

Space is EuclideanSpace ℝ (Fin 3) and particles are indexed by Fin N. Trajectories are functions $\mathbb R\to\mathbb R^3$; the equations of motion are hypotheses HasDerivAt (r k) (v k t) t and HasDerivAt (fun s => m k • v k s) (F k t) t. Masses are constant real numbers. Time averages are $\tau^{-1}\int_0^\tau$ (interval integral). Pair forces are defined with Mathlib's gradient, with $F_{kk}=0$. Power-law coefficients $\alpha_{jk}$ may depend on the pair (symmetric), which contains the article's single constant $\alpha$. Real powers are Real.rpow; collision-freeness is assumed wherever pair distances enter. Boundedness is imposed only for $t\ge0$. The hypotheses are satisfiable (for instance by a uniform circular two-body motion), so no target holds vacuously.

Selected references

• Wikipedia, Virial theorem. https://en.wikipedia.org/wiki/Virial_theorem
• R. Clausius, On a mechanical theorem applicable to heat, Philosophical Magazine, Series 4, 40 (1870), 122–127.

Motivation

The Standard Model of particle physics does not explain the values of its dimensionless constants, nor does it require them to be constant in time. The proton-to-electron mass ratio $\mu = m_p/m_e \approx 1836$ is one such constant: it compares the scale of the strong interaction (which sets most of the proton mass) with the electroweak scale (which sets the electron mass). A measured change of $\mu$ over cosmic time would signal physics beyond the Standard Model, while a tight null result constrains models with additional scalar fields.

The standard test compares the frequencies of molecular transitions observed in distant galaxies with laboratory values. Different transitions respond differently to a change of $\mu$, so a relative shift between them cannot be confused with the overall cosmological redshift.

Timeline. Optical studies of molecular hydrogen at redshifts $z>2$ reached $|\Delta\mu/\mu| < 10^{-5}$ (Malec et al. 2010; van Weerdenburg et al. 2011). Ammonia inversion lines, about 100 times more sensitive, moved the field to radio astronomy and gave constraints at the $10^{-7}$ level toward the lensing galaxy of PKS 1830−211 at $z=0.89$ (Henkel et al. 2009; Kanekar 2011). Jansen et al. (2011) and Levshakov, Kozlov & Reimers (2011) pointed out that methanol transitions have sensitivity coefficients ranging from about $-42$ to $+53$. Ellingsen et al. (2012) gave a first methanol limit from two lines. Bagdonaite et al. (Science, 2013) observed four methanol lines in PKS 1830−211 with the Effelsberg 100-m telescope and derived the limit $\Delta\mu/\mu = (0.0\pm1.0)\times10^{-7}$ at a look-back time of about 7 billion years.

Setting

A transition with frequency $\nu$ has sensitivity coefficient $K_\mu$ defined by

$$\frac{\Delta\nu}{\nu} = K_\mu\,\frac{\Delta\mu}{\mu},$$

or, in infinitesimal form, $K_\mu = \frac{\mu}{\nu}\frac{d\nu}{d\mu}$. Pure rotational transitions have frequency inversely proportional to the reduced mass, hence to $\mu$, so $K_\mu=-1$. Mixed torsion–rotation transitions of methanol have strongly enhanced coefficients (Table 1 of the paper: $-32.8$ and $-7.4$).

Each observed line is assigned a position $V$, a velocity (km/s) on a common scale centred on redshift $z=0.88582$. If $\mu$ in the absorbing galaxy differs from the laboratory value by $\Delta\mu = \mu_z-\mu_{\mathrm{lab}}$, the positions satisfy

$$\frac{V}{c} = -K_\mu\,\frac{\Delta\mu}{\mu}$$

up to a velocity offset common to all lines, where $c$ is the speed of light. Plotting $V$ against $K_\mu$ and fitting a straight line $V = a + bK_\mu$ therefore gives $\Delta\mu/\mu = -b/c$.

The fit is a weighted least-squares fit with weights $1/\sigma_i^2$, where $\sigma_i$ is the 1σ uncertainty of the $i$-th position. With $S=\sum 1/\sigma_i^2$, $S_K=\sum K_i/\sigma_i^2$, $S_V=\sum V_i/\sigma_i^2$, $S_{KK}=\sum K_i^2/\sigma_i^2$, $S_{KV}=\sum K_iV_i/\sigma_i^2$ and $\Delta=SS_{KK}-S_K^2$, the slope, intercept and slope standard error are $b=(SS_{KV}-S_KS_V)/\Delta$, $a=(S_{KK}S_V-S_KS_{KV})/\Delta$ and $\sigma_b=\sqrt{S/\Delta}$. The reduced chi-squared is $\chi^2_\nu=\frac{1}{n-2}\sum_i\big((V_i-a-bK_i)/\sigma_i\big)^2$.

The data (Table 1) are four lines: $3_{-1}$–$2_0\,E$ ($K_\mu=-32.8$, $V=9.06\pm0.67$), $0_0$–$1_0\,A^+$ ($-1$, $8.40\pm0.10$), $0_0$–$1_0\,E$ ($-1$, $9.12\pm0.30$) and $2_{-1}$–$1_0\,E$ ($-7.4$, $9.83\pm0.43$). Because A- and E-symmetry methanol behave as separate species that may be spatially segregated, the fiducial fit uses only the three E lines.

Formalization targets

Goal: the headline limit

With the E-line estimate $\widehat{\Delta\mu/\mu}=-b/c$, its statistical error $\sigma_{\mathrm{stat}}=\sigma_b/c$ and the adopted systematic error $\sigma_{\mathrm{sys}}=7.0\times10^{-8}$,

$$\big|\widehat{\Delta\mu/\mu}\big| < 0.05\times10^{-7},\qquad \Big|\sqrt{\sigma_{\mathrm{stat}}^2+\sigma_{\mathrm{sys}}^2}-1.0\times10^{-7}\Big| < 0.05\times10^{-7},$$

i.e. $\Delta\mu/\mu=(0.0\pm1.0)\times10^{-7}$ to the printed precision.

Milestones

1. Pure rotational transitions ($\nu\propto1/\mu$) have $K_\mu=-1$.
2. Under the exact relation $V_i=a-c\,\delta\,K_i$, the weighted fit returns $-b/c=\delta$ and intercept $a$.
3. E-line fit: $\Delta\mu/\mu=(-0.1\pm7.6)\times10^{-8}$, $\chi^2_\nu\approx2.0$.
4. The E-line result is consistent with $\Delta\mu=0$ at the $1.5\times10^{-7}$ (two-standard-error) level.
5. Four-line fit: $\Delta\mu/\mu=(11.0\pm6.8)\times10^{-8}$, $\chi^2_\nu\approx6.4$.
6. The $0_0$–$1_0$ $A^+$ and $E$ lines are separated by $0.72\pm0.32$ km/s.
7. The $A^+$ anchor line shifted by $0.48\pm0.26$ km/s between December 2011 and April 2012.

Significance

The result. The authors report the limit as statistically more constraining than previous radio-domain tests of a drifting $\mu$. Because it uses a single molecular species, it is much less exposed to the main systematic of multi-species comparisons, namely that different molecules sit in different gas at slightly different velocities. The milestones record the internal evidence behind the choice of the fiducial fit: the poor four-line $\chi^2_\nu$ and the A–E velocity separation.

Formalizing it. The physical inputs (sensitivity coefficients, measured positions, the systematic budget) are taken as data. What the mission checks by machine is the chain from those data to the printed numbers: the definition of the sensitivity coefficient and its value for rotational lines, the correctness of the line-fit estimator, and the arithmetic of every reported fit, separation and error combination.

Difficulty

The numerical milestones are exact statements about explicit rational data, but they involve nested sums, quotients and square roots, so a certified proof requires careful interval bounds rather than floating-point evaluation. The paper's numbers are rounded from unrounded measurements: recomputing from the rounded Table 1 entries gives, for example, $\sigma_b/c\approx7.69\times10^{-8}$ instead of $7.6\times10^{-8}$, and $\chi^2_\nu\approx6.27$ instead of $6.4$ for the four-line fit. Tolerances therefore had to be chosen so that every statement is both faithful to the printed value and true for the tabulated data. The general recovery milestone requires showing that the normal equations are nondegenerate whenever the $K_i$ are not all equal.

Formalization scope

• All quantities are real numbers in Lean; data are finite families indexed by Fin n. Velocities are in km/s and $c=299792.458$ km/s.
• The sensitivity coefficient is the logarithmic derivative $(\mu/\nu(\mu))\,\nu'(\mu)$ using Mathlib's deriv.
• The fit uses the closed-form weighted least-squares formulas above; the reduced chi-squared divides by $n-2$.
• The systematic uncertainty $7.0\times10^{-8}$ is an input; the variability model behind it is out of scope, as are the radiative-transfer column densities and the spectroscopic computation of $K_\mu$ for mixed transitions.
• "95% confidence level" is formalized as the two-standard-error interval.
• Trivializing readings are excluded: every numerical statement is a closed statement about the tabulated data, with no free hypotheses, and the general recovery statement requires non-constant $K$ and nonzero uncertainties.

Reusable pieces: the weighted least-squares definitions and the exact-recovery lemma apply to any straight-line fit with known uncertainties.

Selected references

• J. Bagdonaite, P. Jansen, C. Henkel, H. L. Bethlem, K. M. Menten, W. Ubachs, A Stringent Limit on a Drifting Proton-to-Electron Mass Ratio from Alcohol in the Early Universe, Science, 2013. https://doi.org/10.1126/science.1224898
• P. Jansen, L.-H. Xu, I. Kleiner, W. Ubachs, H. L. Bethlem, Methanol as a sensitive probe for spatial and temporal variations of the proton-to-electron mass ratio, Phys. Rev. Lett. 106, 100801, 2011. https://doi.org/10.1103/PhysRevLett.106.100801
• S. P. Ellingsen, M. A. Voronkov, S. L. Breen, J. E. J. Lovell, First cosmological constraints on the proton-to-electron mass ratio from observations of rotational transitions of methanol, Astrophys. J. Lett. 747, L7, 2012. https://doi.org/10.1088/2041-8205/747/1/L7
• Ph. R. Bevington, D. K. Robinson, Data Reduction and Error Analysis for the Physical Sciences, 3rd ed., McGraw-Hill, 2003.

Motivation

In the paper that introduced the AdS/CFT correspondence (hep-th/9711200), Maldacena takes a stack of branes in string or M-theory, sends the string or Planck length to zero while holding the energies of the worldvolume theory fixed, and follows the supergravity solution of the branes through the same limit. The field theory on the branes decouples from the bulk, and the supergravity metric converges, after an overall rescaling, to a product of an anti-de Sitter space and a round sphere. The conjectured duality is between the worldvolume conformal field theory and string/M-theory on that product.

Section 2 of the paper treats D3-branes, whose limit is $\mathrm{AdS}_5\times S^5$; that case, together with the Appendix on Poincaré coordinates for anti-de Sitter space, is the subject of the separate mission Maldacena 1999: the near-horizon geometry of D3-branes is AdS5 × S5. This mission covers the next three cases in the paper:

1. Section 3.1: $N$ coincident M5-branes, with limit $\mathrm{AdS}_7\times S^4$;
2. Section 3.2: $N$ coincident M2-branes, with limit $\mathrm{AdS}_4\times S^7$;
3. Section 4: the D1–D5 system ($Q_1$ D-strings and $Q_5$ D5-branes wrapped on a four-manifold $M^4$), with limit $\mathrm{AdS}_3\times S^3$ (times $M^4$).

In each case the paper states the ratio of the sphere radius to the anti-de Sitter "radius", and how both depend on the number of branes.

Setting

Anti-de Sitter space. For $p\ge 0$ and $R>0$, $\mathrm{AdS}_{p+2}$ of radius $R$ is the hyperboloid

$$-X_{-1}^2-X_0^2+X_1^2+\dots+X_p^2+X_{p+1}^2=-R^2$$

in flat $\mathbb R^{2,p+1}$ (Appendix, eq. (A.1)). The Poincaré coordinates $(U,x)$, with $U>0$ and $x\in\mathbb R^{1,p}$, are given by $U=X_{-1}+X_{p+1}$, $x^a=X^aR/U$ and $X_{-1}-X_{p+1}=x^2U/R^2+R^2/U$ (eq. (A.2)). In these coordinates the induced metric is

$$ds^2=\frac{U^2}{R^2}\,dx^2+R^2\,\frac{dU^2}{U^2}\qquad\text{(A.3)},$$

where $dx^2=-dx_0^2+dx_1^2+\dots+dx_p^2$. In Lean these objects are AdS, poincareEmbedding, ambientForm and minkowskiForm, taken from the published definition file Maldacena1999_Defs; the induced metric of a tangent vector is ambientForm applied to the Fréchet derivative of poincareEmbedding.

Brane metrics. Each brane solution has the form $ds^2=A(r)\,dx_\parallel^2+B(r)\,(dr^2+r^2d\Omega_n^2)$, with $dx_\parallel^2$ the Minkowski metric along the branes and $d\Omega_n^2$ the round metric of the unit $n$-sphere:

1. M5 (eq. (3.1)): $A=f^{-1/3}$, $B=f^{2/3}$, $f=1+\pi Nl_p^3/r^3$, $n=4$;
2. M2 (eq. (3.3)): $A=f^{-2/3}$, $B=f^{1/3}$, $f=1+2^5\pi^2Nl_p^6/r^6$, $n=7$;
3. D1–D5 (eq. (4.2)): $A=f_1^{-1/2}f_5^{-1/2}$, $B=f_1^{1/2}f_5^{1/2}$, $f_1=1+g\alpha'Q_1/(vr^2)$, $f_5=1+g\alpha'Q_5/r^2$, $n=3$.

The decoupling limits hold fixed $U^2=r/l_p^3$ (M5), $U^{1/2}=r/l_p^{3/2}$ (M2), and $U=r/\alpha'$, $v$ and $g_6=g/\sqrt v$ (D1–D5), while $l_p\to 0$ or $\alpha'\to 0$. The Lean definitions m5Metric, m2Metric and d1d5Metric evaluate these metrics on a tangent vector $(\delta x,\delta r,\delta\omega)$, where $\delta\omega$ is tangent at a point $\omega$ of the unit sphere and $d\Omega_n^2=\|\delta\omega\|^2$.

Formalization targets

Explicit limit metrics (milestones)

With $\delta r$ written in terms of $\delta U$ by the chain rule, the rescaled metrics converge to

$$\frac{ds^2}{l_p^2}\to\frac{U^2}{(\pi N)^{1/3}}dx_\parallel^2+4(\pi N)^{2/3}\frac{dU^2}{U^2}+(\pi N)^{2/3}d\Omega_4^2\qquad(3.2)$$

for M5-branes; to

$$\frac{ds^2}{l_p^2}\to\frac{U^2}{(2^5\pi^2N)^{2/3}}dx_\parallel^2+\frac{(2^5\pi^2N)^{1/3}}{4}\frac{dU^2}{U^2}+(2^5\pi^2N)^{1/3}d\Omega_7^2$$

for M2-branes; and to

$$\frac{ds^2}{\alpha'}\to\frac{U^2}{g_6\sqrt{Q_1Q_5}}dx_\parallel^2+g_6\sqrt{Q_1Q_5}\frac{dU^2}{U^2}+g_6\sqrt{Q_1Q_5}\,d\Omega_3^2\qquad(4.3)$$

for the D1–D5 system.

Goal: identification with AdS × sphere

The goal asserts that each limit equals the metric of $\mathrm{AdS}_{p+2}\times S^n$ (induced metric (A.3) plus a round sphere), with radii, in units of $l_p$ or $\sqrt{\alpha'}$:

1. M5: $R_{\rm AdS}=2(\pi N)^{1/3}$, $R_{\rm sph}=(\pi N)^{1/3}=R_{\rm AdS}/2$;
2. M2: $R_{\rm AdS}=(2^5\pi^2N)^{1/6}/2$, $R_{\rm sph}=(2^5\pi^2N)^{1/6}=2R_{\rm AdS}$;
3. D1–D5: $R_{\rm AdS}^2=R_{\rm sph}^2=g_6\sqrt{Q_1Q_5}$.

Significance

These three limits are the geometric input for the paper's conjectures that the six-dimensional $(0,2)$ theory is dual to M-theory on $\mathrm{AdS}_7\times S^4$, the M2-brane theory to M-theory on $\mathrm{AdS}_4\times S^7$, and the two-dimensional $(4,4)$ theory of the D1–D5 system to IIB string theory on $\mathrm{AdS}_3\times S^3\times M^4$. The radii set the regime in which supergravity can be trusted (large $N$, or large $g_6Q_i$). They also fix which anti-de Sitter isometry group appears ($SO(2,6)$, $SO(2,3)$, $SO(2,2)$); the paper matches it with the bosonic conformal group of the brane theory.

The paper derives these limits in a few lines each. To our knowledge they have not been formalized. The mission produces machine-checked statements and proofs of the three limits and of their identification with anti-de Sitter geometry, reusing the published Poincaré-coordinate results of the D3-brane mission.

Difficulty

The computation is elementary but full of exponents. Each case needs a change of radial variable, a fractional power of a harmonic function whose constant term is dropped in the limit, and a comparison of the coefficient of $dU^2$ with the Poincaré form, which in the M5 and M2 cases requires a constant rescaling of $U$. In Lean, the limits are one-sided limits $l_p\to0^+$ of expressions built from real powers Real.rpow, and the goal requires a Fréchet-derivative computation on $\mathbb R\times\mathbb R^{p+1}$ (available from the published theorem Maldacena1999.induced_metric_poincare).

Formalization scope

All metrics are evaluated pointwise on tangent vectors; no manifold structure is used. The round sphere $S^n$ is the unit sphere in Euclidean $\mathbb R^{n+1}$ and a tangent vector at $\omega$ is a $\delta\omega$ with $\langle\omega,\delta\omega\rangle=0$. The limits are taken along $l_p\to0^+$ (resp. $\alpha'\to0^+$) with $U$, $N$, $g$, $v$, $Q_i$ and the tangent vector fixed. For the D1–D5 system only the six-dimensional metric (4.2) is formalized: the compact factor $M^4$, whose volume is constant in the limit, is not modelled. In the goal the anti-de Sitter coordinate is the paper's $U$ up to a constant factor ($U'=2(\pi N)^{1/6}U$ for M5, $U'=U/(2(2^5\pi^2N)^{1/6})$ for M2, $U'=U$ for D1–D5), so that the limit metric has exactly the form (A.3). All physical parameters are strictly positive. Fluxes, supersymmetry and the duality conjectures themselves are out of scope.

Selected references

• J. Maldacena, The Large-N Limit of Superconformal Field Theories and Supergravity, Int. J. Theor. Phys. 38 (1999) 1113–1133. https://arxiv.org/abs/hep-th/9711200
• G. Horowitz and A. Strominger, Black strings and p-branes, Nucl. Phys. B 360 (1991) 197. https://doi.org/10.1016/0550-3213(91)90440-9

Motivation

In 1997 Maldacena observed that the low-energy limit of a stack of $N$ coincident D3-branes in type IIB string theory can be described in two ways: as four-dimensional $\mathcal N=4$ $U(N)$ super-Yang–Mills theory living on the branes, and as supergravity (ultimately string theory) on the near-horizon geometry of the branes. The paper computes that this near-horizon geometry is five-dimensional anti-de Sitter space times a five-sphere, $\mathrm{AdS}_5\times S^5$, with both factors of the same radius $R$, $R^4=4\pi gN$ in string units, and conjectures that the two descriptions are dual. This AdS/CFT correspondence became one of the most cited results in theoretical physics (Maldacena 1999; see also Gubser–Klebanov–Polyakov 1998, Witten 1998).

The duality itself is a physical conjecture with no complete mathematical formulation. What the paper does contain is a small body of exact geometric computations on which the conjecture rests: the decoupling limit of the D3-brane metric, the description of AdS as a hyperboloid with its $SO(2,p+1)$ symmetry, the Poincaré coordinates in which the limiting metric is written, and the ordinary differential equation expressing broken conformal invariance of a probe brane. This mission formalizes exactly those computations.

Setting

Fix $p\ge0$. The ambient space $\mathbb R^{2,p+1}$ has coordinates $X_{-1},X_0,X_1,\dots,X_p,X_{p+1}$ and flat metric $\eta=\mathrm{diag}(-1,-1,1,\dots,1)$. Anti-de Sitter space of radius $R$ is the hyperboloid (eq. (A.1))

$$\mathrm{AdS}_{p+2}(R)=\{X : -X_{-1}^2-X_0^2+X_1^2+\cdots+X_p^2+X_{p+1}^2=-R^2\}.$$

Linear maps preserving $\eta$ form the group $O(2,p+1)$, which contains the conformal group $SO(2,p+1)$ of $(p+1)$-dimensional Minkowski space.

The Poincaré coordinates (eq. (A.2)) are $U=X_{-1}+X_{p+1}$ and $x_\alpha=X_\alpha R/U$ for $\alpha=0,\dots,p$; on the hyperboloid, $V=X_{-1}-X_{p+1}=x^2U/R^2+R^2/U$, where $x^2=-x_0^2+x_1^2+\cdots+x_p^2$. Written in reverse, this is a map $\Phi_R:(U,x)\mapsto X$.

The D3-brane metric (eq. (2.2)) for string coupling $g$, $N$ branes and string scale $\alpha'$ is

$$ds^2=f^{-1/2}dx_\parallel^2+f^{1/2}\big(dr^2+r^2d\Omega_5^2\big),\qquad f=1+\frac{4\pi gN\alpha'^2}{r^4},$$

where $x_\parallel\in\mathbb R^{1,3}$ are the worldvolume coordinates and $d\Omega_5^2$ is the round metric of the unit five-sphere. The decoupling limit (eq. (2.1)) sends $\alpha'\to0$ keeping $U=r/\alpha'$ fixed.

Formalization targets

Goal: the near-horizon geometry is $\mathrm{AdS}_5\times S^5$

For $g>0$, $N\ge1$, $R>0$ with $R^4=4\pi gN$, $U>0$ and every tangent vector $(\delta x,\delta U,\delta\omega)$ with $\delta\omega$ tangent to $S^5$,

$$\lim_{\alpha'\to0^+}\frac{1}{\alpha'}\,ds^2_{\alpha'}\Big|_{r=\alpha'U,\ \delta r=\alpha'\delta U}=\big\langle d\Phi_R[\delta U,\delta x],d\Phi_R[\delta U,\delta x]\big\rangle_\eta+R^2\|\delta\omega\|^2 ,$$

which is eq. (2.3): the metric of $\mathrm{AdS}_5(R)$ in Poincaré coordinates plus the round metric of $S^5$ of the same radius.

Milestones

1. (A.1)–(A.2) $\Phi_R(U,x)\in\mathrm{AdS}_{p+2}(R)$ for $U>0$.
2. Appendix $\Phi_R$ is a bijection from $\{U>0\}$ onto $\{X\in\mathrm{AdS}_{p+2}(R): X_{-1}+X_{p+1}>0\}$.
3. (A.3) the induced metric is $\frac{U^2}{R^2}dx^2+R^2\frac{dU^2}{U^2}$.
4. Appendix every $A$ with $A^{\mathsf T}\eta A=\eta$ preserves $\mathrm{AdS}_{p+2}(R)$.
5. (2.2)→(2.3) the three metric coefficients divided by $\alpha'$ converge to $U^2/\sqrt{4\pi gN}$, $\sqrt{4\pi gN}/U^2$ and $\sqrt{4\pi gN}$.
6. (2.9) on $z>-1/\tilde R^4$, the differentiable solutions of $f(z)+c=2(z+\tilde R^{-4})f'(z)$ are exactly $f=b\sqrt{1+\tilde R^4z}-c$.

Significance

The goal is the precise sense in which "the near-horizon geometry of $N$ D3-branes is $\mathrm{AdS}_5\times S^5$ with $R^4=4\pi gN$": the radius formula is what later links the 't Hooft coupling $g^2_{YM}N$ of the gauge theory to the curvature of the string background, and the Poincaré-patch form (A.3) is the coordinate system in which essentially all subsequent AdS/CFT computations are carried out. Milestones 1–4 give a reusable, self-contained account of anti-de Sitter space as a quadric in $\mathbb R^{2,p+1}$ with its Poincaré chart, useful to any development of Lorentzian geometry. Milestone 6 is the step by which the paper argues that the probe D3-brane action (2.6) is fixed by conformal symmetry.

All of these statements are standard computations in the physics literature; none is open. The value of the mission is a machine-checked version of the geometric content of the paper, stated with the paper's own conventions, not a new result. The duality conjecture itself is outside the scope of the mission.

Difficulty

The computations are elementary but bookkeeping-heavy. The induced-metric identity (A.3) requires differentiating a map from $\mathbb R\times\mathbb R^{p+1}$ to $\mathbb R^{p+3}$ with $p$ arbitrary, so sums over the index sets must be split into the timelike, spacelike and light-cone components; a computation for one fixed $p$ does not suffice. The bijection statement needs an explicit inverse and the observation that the hyperboloid equation determines $V$ from $U$ and $x$. The limit statements require controlling square roots of expressions that blow up like $\alpha'^{-2}$. The ODE characterisation requires a uniqueness argument on an interval, not only verification that the stated function is a solution.

Formalization scope

Coordinates of $\mathbb R^{2,p+1}$ are indexed by $\{0,\dots,p+2\}$ with index $0$ for $X_{-1}$, index $1$ for $X_0$ and index $k+1$ for $X_k$; worldvolume coordinates are indexed by $\{0,\dots,p\}$ with index $0$ timelike. Metrics are represented by the quadratic forms they induce on tangent vectors; the induced metric is expressed through the Fréchet derivative of $\Phi_R$. The round metric of $S^5$ is the Euclidean norm squared of a tangent vector of the unit sphere in $\mathbb R^6$. Square roots and divisions are Lean's total functions; all statements restrict to $R>0$, $U>0$, $g>0$, $N\ge1$, $\alpha'>0$, where no junk values arise. The symmetry milestone is stated for the full group $O(2,p+1)$, which contains the $SO(2,p+1)$ named in the paper.

No new infrastructure beyond Mathlib's calculus, real analysis and matrix libraries is needed. Contributions of general lemmas about quadrics in pseudo-Euclidean spaces are welcome.

Selected references

• J. Maldacena, The Large-N Limit of Superconformal Field Theories and Supergravity, Int. J. Theor. Phys. 38 (1999) 1113–1133. https://arxiv.org/abs/hep-th/9711200
• S. S. Gubser, I. R. Klebanov, A. M. Polyakov, Gauge theory correlators from non-critical string theory, Phys. Lett. B 428 (1998) 105–114. https://arxiv.org/abs/hep-th/9802109
• E. Witten, Anti de Sitter space and holography, Adv. Theor. Math. Phys. 2 (1998) 253–291. https://arxiv.org/abs/hep-th/9802150

Motivation

Projective measurement is usually taught together with state update: an observable is measured, a value is obtained, and the conditional state is assigned. These are two different questions. The first is the prediction of the outgoing ensemble from the incoming ensemble and the measured observable alone, before the outcome is known; the second is the incorporation of the outcome once it is known. The technical brief by G. Carcassi for the Assumptions of Physics collaboration (AoP technical briefs) isolates the first question and treats the measurement as a black-box process that only relates incoming and outgoing ensembles, without committing to a mechanism.

Within this view the standard prediction, the nonselective (Lüders) post-measurement ensemble, admits several characterizations that come from different traditions: the algebraic pinching map, the long-time limit of a dephasing Lindblad equation (open quantum systems, see Lindblad 1976), and a closest-point principle, either in Hilbert–Schmidt distance or in quantum relative entropy (Umegaki 1962). The brief's Theorem 1 states that these characterizations select the same process.

Setting

Fix a finite index set $n$; the Hilbert space is $\mathbb C^n$ and operators are complex $n\times n$ matrices. A density matrix is a positive semidefinite matrix $\rho$ with $\operatorname{tr}\rho=1$. An observable is a Hermitian matrix $X$ with spectral decomposition

$$X=\sum_{x}x\,P_x ,$$

where $x$ ranges over the distinct eigenvalues of $X$ and $P_x$ is the orthogonal projection onto the $x$-eigenspace.

• The pinching of $\rho$ is $\mathcal P_X(\rho)=\sum_x P_x\rho P_x$.
• The dephasing Lindblad equation with vanishing Hamiltonian and jump operator $X$ is $\dfrac{d\rho}{dt}=X\rho X-\tfrac12\{X^2,\rho\}$, $t\ge0$.
• The Hilbert–Schmidt distance is $\|\rho-\sigma\|_{HS}=\big(\operatorname{tr}(\rho-\sigma)^*(\rho-\sigma)\big)^{1/2}$.
• The relative entropy is $D(\rho\|\sigma)=\operatorname{tr}(\rho\log\rho)-\operatorname{tr}(\rho\log\sigma)$ when $\operatorname{supp}\rho\subseteq\operatorname{supp}\sigma$ and $+\infty$ otherwise; the von Neumann entropy is $S(\rho)=-\operatorname{tr}(\rho\log\rho)$.

The spectral equilibration process $\Phi_X$ is an unknown map on density matrices. The brief's four conditions on it are:

• EQ-MEAS: $\Phi_X(\rho)=\sum_xP_x\rho P_x$.
• EQ-LIND: $\Phi_X(\rho)=\lim_{t\to\infty}\rho(t)$ for the Lindblad evolution with $\rho(0)=\rho$.
• EQ-HS: $\Phi_X(\rho)=\operatorname{argmin}\{\|\rho-\sigma\|_{HS}^2:\ \sigma \text{ a density matrix},\ [\sigma,X]=0\}$.
• EQ-KL: $\Phi_X(\rho)=\operatorname{argmin}\{D(\rho\|\sigma):\ \sigma \text{ a density matrix},\ [\sigma,X]=0\}$.

Formalization targets

Goal: Theorem 1 (finite-dimensional form)

For every Hermitian $X$ and every map $\Phi$,

$$\text{EQ-MEAS}\iff\text{EQ-LIND},\qquad \text{EQ-MEAS}\iff\text{EQ-HS},\qquad \text{EQ-MEAS}\iff\text{EQ-KL}.$$

Milestones

The milestones follow the steps of the brief's proof: the block decomposition $\rho=\sum_{x,y}P_x\rho P_y$ (eq. 2); the blockwise solution $P_x\rho(t)P_y=e^{-\frac t2(x-y)^2}P_x\rho(0)P_y$ (eqs. 4–5); convergence $\rho(t)\to\mathcal P_X(\rho)$ (eqs. 9–10) and EQ-LIND $\Leftrightarrow$ EQ-MEAS; the equivalence $[\sigma,X]=0\iff\mathcal P_X(\sigma)=\sigma$; $\mathcal P_X$ preserves density matrices; the Pythagorean identity (eq. 11) and EQ-HS $\Leftrightarrow$ EQ-MEAS; the relative-entropy chain rule (eq. 12); $D(\rho\|\mathcal P_X\rho)=S(\mathcal P_X\rho)-S(\rho)$ (eq. 13); non-negativity and definiteness of $D$; and EQ-KL $\Leftrightarrow$ EQ-MEAS.

Significance

The result says that "projective measurement" can be specified without reference to wave-function collapse: any of the three dynamical or variational descriptions pins down the same input–output map. Downstream, this justifies treating repeatable measurements as equilibration processes whose outputs are fixed points, and treating the outcome-update step as classical conditioning on a mixture.

The mathematics in finite dimension is classical; this mission asks for a machine-checked proof of the equivalence in Lean 4 with Mathlib. A complete development produces reusable pieces: spectral projections and the pinching map for Hermitian matrices, explicit solutions and asymptotics of a dephasing Lindblad semigroup, and an extended-real relative entropy with Klein's inequality.

Difficulty

The Hilbert–Schmidt part is linear algebra once block-diagonality is in place. The Lindblad part requires uniqueness of solutions of a linear matrix ODE on the closed half-line, to transfer the explicit blockwise formula to an arbitrary solution. The relative-entropy part is the most delicate: it needs the interaction between the functional-calculus logarithm and block structure ($\log\sigma$ is block diagonal when $\sigma$ commutes with $X$), the support conventions that make $D$ take the value $+\infty$, and Klein's inequality with its equality case for matrices, which the development must supply if the library does not already provide it.

Formalization scope

• Finite dimension only. The Hilbert space is $\mathbb C^n$ for a finite type $n$, so all observables are bounded with pure point spectrum and every density matrix has finite entropy. The brief also covers separable infinite-dimensional spaces and unbounded observables (where Condition [B]FINENT is a genuine restriction); that regime is not part of this mission.
• Spectral data. $P_x$ is built from Mathlib's eigen-decomposition of a Hermitian matrix and is defined for every real $x$ (zero when $x$ is not an eigenvalue); the pinching sums over the finite set of distinct eigenvalues.
• Lindblad solutions. A solution is any function $\mathbb R\to M_n(\mathbb C)$ with the given initial value whose derivative within $[0,\infty)$ satisfies the equation for $t\ge0$. EQ-LIND requires existence of a solution and convergence of every solution, so it cannot hold vacuously.
• Argmin. "$\Phi(\rho)=\operatorname{argmin}$" is encoded as "$\Phi(\rho)$ is a feasible minimizer"; uniqueness is a consequence proved by the theorem, not an assumption.
• Logarithm and relative entropy. $\log$ is the continuous functional calculus applied to Real.log (so $\log0=0$, i.e. the logarithm on the support); $D$ takes values in the extended reals and equals $+\infty$ unless $\ker\sigma\subseteq\ker\rho$.
• Convergence is in the entrywise topology, which coincides with the trace-norm and Hilbert–Schmidt topologies in finite dimension.

Contributions of general-purpose lemmas (Klein's inequality, uniqueness for linear ODEs on half-lines, properties of pinching) are welcome as separate theorems.

Selected references

• G. Carcassi (Assumptions of Physics collaboration), Projective measurements are equilibration processes, AoP Technical Brief 017. https://assumptionsofphysics.org/resources/briefs
• G. Lindblad, On the generators of quantum dynamical semigroups, Comm. Math. Phys. 48 (1976) 119–130. https://doi.org/10.1007/BF01608499
• H. Umegaki, Conditional expectation in an operator algebra. IV. Entropy and information, Kodai Math. Sem. Rep. 14 (1962) 59–85. https://doi.org/10.2996/kmj/1138844604

Motivation

In 1948 R. P. Feynman published a third formulation of non-relativistic quantum mechanics, alongside Schrödinger's differential equation and Heisenberg's matrix algebra (Feynman 1948). The probability amplitude for a particle to follow a path $x(t)$ is postulated to be $\exp\big(\tfrac{i}{\hbar}S[x]\big)$, with $S$ the classical action, and the amplitude to arrive at $(x,t)$ is the sum of these contributions over all paths from the past. This is the path integral, now a standard tool across quantum field theory, statistical mechanics and probability.

The formulation is claimed to be mathematically equivalent to ordinary quantum mechanics. The key step of that claim is Section 6 of the paper, "The wave equation": the wave function defined by the path integral satisfies Schrödinger's equation. This mission formalizes that step for a particle in one dimension, as the paper does.

Timeline:

• 1933/1945 — Dirac remarks on the role of the classical action in quantum mechanics, the starting point cited by Feynman.
• 1948 — Feynman, Rev. Mod. Phys. 20, 367: path-integral postulates, definition of the wave function (Section 5), derivation of Schrödinger's equation (Section 6).
• 1949 — Kac gives the rigorous imaginary-time (Wiener-measure) analogue, the Feynman–Kac formula.
• 1964 — Nelson derives the real-time Feynman formula rigorously from the Trotter product formula; oscillatory-integral approaches follow later.

Setting

Fix $\hbar>0$, a mass $m>0$ and a potential $V:\mathbb R\to\mathbb R$. For a time step $\varepsilon>0$ the short-time action between positions $y$ (time $t$) and $x$ (time $t+\varepsilon$) is (Eq. 22)

$$S(x,y)=\frac{m\varepsilon}{2}\Big(\frac{x-y}{\varepsilon}\Big)^2-\varepsilon V(x),$$

and the normalizing factor is $A(\varepsilon)=(2\pi\hbar\varepsilon i/m)^{1/2}$ (Eq. 28, principal branch). The one-step path-integral evolution (Eqs. 18, 23) takes a wave function $\psi:\mathbb R\to\mathbb C$ to

$$(U_\varepsilon\psi)(x)=\frac{1}{A(\varepsilon)}\int_{\mathbb R}\exp\!\Big(\frac{i}{\hbar}S(x,y)\Big)\psi(y)\,dy .$$

Iterating $U_\varepsilon$ and letting $\varepsilon\to0$ is the path integral (15) of Section 5. The Hamiltonian is $H\psi=-\frac{\hbar^2}{2m}\psi''+V\psi$. The paper also uses the Gaussian moments of Eq. (26), which are oscillatory; footnote 13 defines them by replacing $\hbar$ with $\hbar(1-i\delta)$ and letting $\delta\to0^+$:

$$M_n(\delta)=\int_{\mathbb R}\xi^n\exp\!\Big(\frac{im\xi^2}{2\hbar(1-i\delta)\varepsilon}\Big)d\xi .$$

Formalization targets

Goal — Eq. (30)

For every Schwartz function $\psi$ and every $x\in\mathbb R$,

$$\lim_{\varepsilon\to0^+}\frac{(U_\varepsilon\psi)(x)-\psi(x)}{\varepsilon}=-\frac{i}{\hbar}\Big(-\frac{\hbar^2}{2m}\psi''(x)+V(x)\psi(x)\Big),$$

that is, $-\frac{\hbar}{i}\partial_t\psi=\frac{1}{2m}\big(\frac{\hbar}{i}\partial_x\big)^2\psi+V\psi$ for the path-integral evolution, which is Schrödinger's equation (30). This is the content of Feynman's statement that (18), valid to first order in $\varepsilon$, yields (30).

Milestones

1. Eq. (26), the three regularized Fresnel integrals: $M_0(\delta)\to A$, $M_1(\delta)=0$, $M_2(\delta)\to\frac{\hbar\varepsilon i}{m}A$.
2. Eqs. (27)–(28), zero-order agreement: $(U_\varepsilon\psi)(x)\to\psi(x)$; this is the condition that fixes $A$.
3. Eq. (27) for the free particle: $\big((U_\varepsilon\psi)(x)-\psi(x)\big)/\varepsilon\to\frac{\hbar i}{2m}\psi''(x)$ when $V=0$.
4. Footnote 15: for the free particle (18) is exact, $U_\varepsilon U_\delta\psi=U_{\varepsilon+\delta}\psi$.

Significance

The goal is the step that connects the path-integral postulates to the ordinary formulation: without it the formulation of Sections 3–5 is not known to reproduce any quantum mechanics. The Fresnel integrals of (26) and the short-time kernel appear throughout semiclassical analysis and in every derivation of path integrals from the Schrödinger equation.

The physics result is classical and its rigorous versions are known (via the Trotter product formula or oscillatory-integral estimates). The work here is the formalization: Mathlib has the complex Gaussian integral and Schwartz functions, but not Fresnel integrals, the free Schrödinger kernel, or the short-time asymptotics of oscillatory integrals. None of the targets is currently formalized on the platform.

Difficulty

Feynman's derivation expands $\psi(x-\xi)$ in a Taylor series under the integral and integrates term by term against $\exp(im\xi^2/2\hbar\varepsilon)$. Those integrals are not absolutely convergent, and the higher moments do not even exist as improper Riemann integrals, so the term-by-term step is not justified as written. A proof has to control the Taylor remainder against an oscillatory kernel whose width is of order $\sqrt{\hbar\varepsilon/m}$, uniformly as $\varepsilon\to0^+$, with a prefactor $1/A$ that blows up like $\varepsilon^{-1/2}$. The naive dominated-convergence argument does not apply, because the kernel has modulus $|A|^{-1}$ everywhere and does not concentrate in absolute value.

Formalization scope

• One space dimension, real potential $V$ with no regularity assumptions (it enters only through $V(x)$ at the fixed point, as in Eq. (23)).
• Wave functions are Schwartz functions 𝓢(ℝ, ℂ), which formalizes the paper's "relatively smooth" $\psi$ that "falls off sufficiently for large $x$". For such $\psi$ the integral defining $U_\varepsilon\psi$ is absolutely convergent, so the Lebesgue (Bochner) integral is used.
• $\hbar>0$, $m>0$ are hypotheses; limits in $\varepsilon$ and $\delta$ are one-sided, $\to0^+$.
• $A$ uses Mathlib's principal complex power $z^{1/2}$.
• The Gaussian moments are regularized as in footnote 13 ($\hbar\to\hbar(1-i\delta)$), because the bare integrals are not Lebesgue integrable and the Bochner integral would silently return $0$.
• The goal is pointwise in $x$ and concerns the generator of one step; it does not assert convergence of the full time-sliced path integral (a Trotter-type statement), which would be a natural follow-up mission.

Useful infrastructure: Fresnel integrals, Fourier representation of the free Schrödinger kernel on Schwartz space, and differentiation of oscillatory integrals with a parameter. All are reusable beyond this mission.

Selected references

• R. P. Feynman, Space-Time Approach to Non-Relativistic Quantum Mechanics, Rev. Mod. Phys. 20, 367 (1948). https://doi.org/10.1103/RevModPhys.20.367
• P. A. M. Dirac, On the Analogy Between Classical and Quantum Mechanics, Rev. Mod. Phys. 17, 195 (1945). https://doi.org/10.1103/RevModPhys.17.195
• M. Kac, On distributions of certain Wiener functionals, Trans. Amer. Math. Soc. 65, 1 (1949).
• E. Nelson, Feynman integrals and the Schrödinger equation, J. Math. Phys. 5, 332 (1964).

Motivation

A coincident pair of a D-brane and an anti-D-brane in type II string theory carries an open-string tachyon, a mode of negative mass squared. In Sen, hep-th/9805019 it was conjectured that at the minimum of the tachyon potential the negative potential energy exactly cancels the sum of the tensions of the brane and the anti-brane, so that the system decays to a configuration of zero energy density, i.e. the supersymmetric vacuum. The paper formalized here, A. Sen, Tachyon condensation on the brane antibrane system, JHEP 08 (1998) 012, gives a short argument for this, and the author says explicitly that it is not a rigorous mathematical proof. The argument follows Gava–Narain–Sarmadi, hep-th/9704006 and belongs to the programme of tachyon condensation. Later work, starting with open string field theory computations, tested the same conjecture numerically.

Setting

Work in string units ($\alpha'=1$). Wrap a D2-brane and an anti-D2-brane on a torus $T^2=S^1\times S^1$ with radii $R_1,R_2$ and area $V=4\pi^2R_1R_2$. Each brane carries one unit of magnetic flux, $F_{12}=2\pi/V$, with signs chosen so that each carries $+1$ unit of D0-brane charge. T-duality on both circles gives a dual torus with radii $\tilde R_i=1/R_i$ and coupling $\tilde g=g/(R_1R_2)$. On the dual torus the system is described by a $U(2)$ gauge theory: a gauge field is a pair $A=(A_1,A_2)$ of $2\times2$ complex-matrix-valued functions of $x=(x^1,x^2)$, with field strength $F_{12}=\partial_1A_2-\partial_2A_1-i[A_1,A_2]$. The gauge transform by a matrix-valued $\Omega$ is $(\Omega\circ A)_\mu=\Omega A_\mu\Omega^{-1}-i(\partial_\mu\Omega)\Omega^{-1}$. The background configuration is

$$A_1=0,\qquad A_2=\frac{2\pi x^1\sigma_3}{\tilde V},\qquad \tilde V=4\pi^2\tilde R_1\tilde R_2,$$

subject to twisted boundary conditions with transition functions $\Omega_1=\exp(ix^2\sigma_3/\tilde R_2)$ and $\Omega_2=1$. A D-brane with coupling $g$ has tension $1/(4\pi^2g)$.

Formalization targets

Goal

With $M(R_1,R_2,g)$ the mass at the classical minimum (two D2-branes with zero field strength on the dual torus, re-expressed through $R_1,R_2,g$), for each fixed $g>0$:

$$\lim_{R_1,R_2\to\infty}\frac{M(R_1,R_2,g)}{4\pi^2R_1R_2}=0 .$$

Milestones (in the paper's order)

1. Eq. (1): $2\pi/(4\pi^2R_1R_2)\to0$ as $R_1,R_2\to\infty$.
2. The background (4) is traceless Hermitian (no $U(1)$ part).
3. Eqs. (5)–(6): the background satisfies the twisted boundary conditions.
4. Eq. (7): $\Omega_2(2\pi\tilde R_1)\Omega_1(0)=\Omega_1(2\pi\tilde R_2)\Omega_2(0)$.
5. The background has field strength $F_{12}=(2\pi/\tilde V)\sigma_3\neq0$.
6. Eq. (8): there is a smooth $SU(2)$-valued $g$ with the boundary behaviour (8).
7. Gauge transformations preserve $F_{12}\equiv0$.
8. Eq. (9): $M=2\tilde R_1\tilde R_2/\tilde g$.
9. Eq. (10): $M=2/g$.
10. Eq. (11): $M/(4\pi^2R_1R_2)=1/(2\pi^2R_1R_2g)$.

Significance

The vanishing of the energy at the tachyon minimum is the basis for identifying stable non-BPS D-branes as tachyonic solitons on brane–antibrane pairs, as discussed at the end of the paper, and it was a starting point for later work on tachyon condensation. The paper's argument is heuristic. This mission makes explicit which steps are mathematics (the gauge-theoretic facts (4)–(8), the gauge covariance used on p. 3, and the algebra (9)–(11) and its limit) and machine-checks them. The physical inputs (the BPS argument that the mass (9) persists as parameters vary, and the identification of the minimum-energy configuration) are recorded as modelling assumptions in the definitions, not proved.

Difficulty

The algebraic milestones (9)–(11) and the limits are elementary. The substantive formal work is in the gauge-theory milestones: computing derivatives of the matrix exponential in (5), the smooth homotopy with flat ends required by (8) (existence rests on the simple connectivity of $SU(2)$, but the statement asks for an explicit smooth $SU(2)$-valued map with prescribed boundary values and vanishing normal derivative), and the covariance computation of the field strength under a non-unitary, merely invertible $\Omega$.

Formalization scope

Coordinates are $x=(x^1,x^2)\in\mathbb R\times\mathbb R$; the paper's index $\mu\in\{1,2\}$ is Fin 2 ($1\mapsto0$, $2\mapsto1$). Matrices are Matrix (Fin 2) (Fin 2) ℂ; partial derivatives are taken entrywise; the inverse is the Mathlib matrix inverse; the exponential is NormedSpace.exp. Radii and couplings are real, with positivity assumed wherever the paper's quantities are physical. The goal cannot be trivialized by division by zero, because it is a statement about the limit of large positive radii. All definitions live in a single definition file under the namespace SenTachyon.

Selected references

• A. Sen, Tachyon condensation on the brane antibrane system, JHEP 08 (1998) 012. https://doi.org/10.1088/1126-6708/1998/08/012 (arXiv: https://arxiv.org/abs/hep-th/9805170)
• A. Sen, Stable non-BPS bound states of BPS D-branes, JHEP 08 (1998) 010. https://arxiv.org/abs/hep-th/9805019
• E. Gava, K. S. Narain, M. H. Sarmadi, On the bound states of p- and (p+2)-branes, Nucl. Phys. B 504 (1997) 214. https://arxiv.org/abs/hep-th/9704006
• G. 't Hooft, Some twisted self-dual solutions for the Yang–Mills equations on a hypertorus, Comm. Math. Phys. 81 (1981) 267. https://doi.org/10.1007/BF01208900