Mathematical Physics

Markov Chain Probability·Captain: mikedeng1

The Endpoint Distribution of Directed Polymers 1: In the Low-Temperature Phase the Endpoint Distribution Is Asymptotically Purely Atomic, and at High Temperature It Is NotResearch Paper

Motivation

A directed polymer in a random environment is a random walk whose paths are weighted by the disorder they encounter. The walk favors paths with large accumulated weight, and its endpoint distribution can concentrate on a small number of sites even though the number of possible paths grows exponentially. Understanding how much probability remains spread across many small endpoint masses is a basic question about localization. The distinction matters especially beyond exactly solvable polymer models, where explicit formulas for the endpoint law are rarely available. Bates and Chatterjee study this question for independent disorder in every spatial dimension $d\geq1$ under a finite exponential-moment condition Bates and Chatterjee, 2021.

The paper separates two temperature regimes using the limiting free energy. Earlier localization statements detected persistent large atoms. The target here asks whether those atoms account for all endpoint probability in a time-averaged sense. It also specifies the complementary high-temperature behavior, where a suitable vanishing mass threshold captures asymptotically none of the probability. The result is Theorem 1.1 of the preprint, restated as Theorem 6.3 Bates and Chatterjee, 2021, pp. 16, 43.

Setting

Fix $d\geq1$ . A path starts at the origin in $\mathbb Z^d$ and makes one of its $2d$ nearest-neighbor moves at each integer time. The environment $(X_{i,x})$ consists of independent, identically distributed real random variables with common law $\mathfrak L$ . The disorder law is nondegenerate: it is not concentrated at one number. An inverse temperature $\beta\geq0$ determines the weight of a path $\gamma$ of length $n$ :

w_\beta(\gamma)=\exp\!\left(\beta\sum_{i=1}^{n}X_{i,\gamma(i)}\right),\qquad Z_n=(2d)^{-n}\sum_{\gamma}w_\beta(\gamma).

The endpoint mass function $f_n(x)$ is the sum of weights of paths ending at $x$ , divided by the sum of all path weights. Thus $f_n$ is a probability mass function on $\mathbb Z^d$ . For $\varepsilon>0$ , the $\varepsilon$ -atoms are the sites $\mathcal A_n^\varepsilon=\{x:f_n(x)>\varepsilon\}$ , and $\rho_n(\omega_n\in\mathcal A_n^\varepsilon)$ is their total mass. The strict inequality matters at a threshold equal to an atom mass.

Write $F_n=\log Z_n/n$ for $n\geq1$ , with $F_0=0$ , and $\lambda(\alpha)=\log\mathbb E_{\mathfrak L}e^{\alpha X}$ . The standing condition is that this exponential moment is finite for every $\alpha\in[-2\beta,2\beta]$ . The paper's Theorem A characterizes the high-temperature phase by $\lim_n\mathbb E F_n=\lambda(\beta)$ and the low-temperature phase by $\lim_n\mathbb E F_n<\lambda(\beta)$ Bates and Chatterjee, 2021, pp. 4–5.

Formalization targets

Asymptotic pure atomicity

The goal is both clauses of Theorem 1.1. For every positive deterministic sequence $\varepsilon_i\to0$ , low temperature gives

\frac1n\sum_{i=0}^{n-1}\rho_i(\omega_i\in\mathcal A_i^{\varepsilon_i})\longrightarrow1 \quad\text{almost surely}.

At high temperature there exists a positive deterministic sequence $\varepsilon_i\to0$ for which the same average converges almost surely to $0$ . The sequence in this second clause is selected independently of the realized environment. Together the clauses characterize the paper's stronger, almost-sure form of asymptotic pure atomicity Bates and Chatterjee, 2021, Theorems 1.1 and 6.3.

The milestones are fifteen statements of the paper, in the order the proof of the goal uses them:

the triangle inequality for the distance $d$ on partitioned subprobability measures (Lemma 2.3) and sequential compactness of $(\mathcal S,d)$ (Theorem 2.8);
continuity of the update law $f\mapsto\mathcal Tf$ into $(\mathcal P(\mathcal S),\mathcal W)$ and of the log moments $f\mapsto\mathbb E\log^q\widetilde F$ (Proposition 3.2);
convergence of the empirical endpoint measures $\mu_n=\frac1n\sum_{i<n}\delta_{f_i}$ to the fixed-point set $\mathcal K$ (Corollary 4.3); invariant laws charge only states of mass $0$ or $1$ (Proposition 4.4);
the variational formula for the free energy: $|F_n-\mathcal R(\mu_n)|\to0$ (Proposition 4.5), the lower bound (Proposition 4.6), the key inequality $\sum_{i<n}\mathcal R(\mathcal T^i\delta_{f_0})\ge\mathbb E\log Z_n$ (Lemma 4.8), and $\lim F_n=\inf_{\nu\in\mathcal K}\mathcal R(\nu)$ (Theorem 4.7);
convergence of $\mu_n$ to the minimizing set $\mathcal M$ (Theorem 4.9), the extrema of $R$ (Lemma 5.1) and the fixed-point characterization of the two phases (Theorem 5.2);
semicontinuity of the atom functionals (Lemma 6.1), a fixed-threshold criterion for pure atomicity (Lemma 6.2), and a Dini theorem for semicontinuous functions (Lemma 6.4).

Significance

The low-temperature conclusion rules out a residual diffuse component in the time-averaged endpoint law. A vanishing threshold may still be used to collect almost all of the polymer's probability. The high-temperature clause shows that this property distinguishes the phases under the stated moment assumption. The result strengthens a statement that only asks for a positive amount of mass on large atoms, and gives an almost-sure conclusion for the Cesàro averages Bates and Chatterjee, 2021, §§1.2.3, 6.

A formal development would supply a reusable compactification of endpoint probability measures and a checked route from its invariant laws to localization observables. The milestones expose the pieces that need separate verification, and the compactification and variational formula are reusable for the companion mission on geometric localization. The paper proves the mathematical theorem; this mission asks for its Lean proof and the supporting definitions. A compiled statement with sorry is a proof obligation, not a completed machine-checked result.

Difficulty

The endpoint distribution may move through space as time grows, so ordinary pointwise convergence of mass functions does not capture concentration. The compact state space used by the paper permits separated clusters to live on different copies of $\mathbb Z^d$ . Its distance identifies translated representatives and loses information about remote mass. A direct application of weak convergence to the event $f(x)>\varepsilon$ also fails at a threshold, because the mass-above-threshold functional is not continuous. The proof must handle its one-sided semicontinuity and the limiting behavior of the update law Bates and Chatterjee, 2021, §§2–3, 6.

Formalization scope

Lean represents sites as Fin d → ℤ and paths as finite step sequences, so the starting point, the $2d$ choices per step, and the normalization of $Z_n$ are explicit. An environment is a measurable independent family on a probability space with common law $\mathfrak L$ . The unused time-zero row comes from indexing cells by $\mathbb N$ ; only rows with index at least one enter the polymer. The moment condition includes the full interval $[-2\beta,2\beta]$ , and the disorder law must be nondegenerate. Both phase predicates refer to the canonical product environment, making the classification depend on $\mathfrak L$ , $d$ , and $\beta$ rather than on an arbitrary realization.

Partitioned subprobability measures are structures of nonnegative summable functions with mass at most one. Their topology is generated by the paper's distance balls. The Borel representation identifies states at distance zero, corresponding to the paper's separation quotient $\mathcal S$ . Finite partial isometries carry the degree penalty $2^{-\deg\varphi}$ through an infimum over admissible degrees. The update uses an extended nonnegative sum before conversion to a real denominator. The intended probability law requires the almost-sure finiteness of that denominator and measurability of the update. The real-valued energy integrals require the stated moment condition; a default value for a nonintegrable integral cannot serve as the paper's expectation, and a non-measurable update would make the pushforward $\mathcal Tf$ the zero measure, which is not the paper's object either. The infimum $\inf_{\nu\in\mathcal K}\mathcal R(\nu)$ is taken over the set $\mathcal K$ itself, never as a real infimum whose empty inner range defaults to $0$ . The intermediate results in §§3–4 and Lemma 5.1 use the standing $\beta>0$ range. Theorems 1.1 and 5.2 explicitly include $\beta=0$ . Wasserstein cost imports the published RWPI.SqrtLasso.transportCost definition.

Solvers can contribute proofs of the compactness, continuity, variational-formula, invariant-law, and atom-functional milestones, or of reusable supporting results such as Lemma 2.11 (measurability of the update) and Corollary 2.5 (when $d(f,g)=0$ ). The strict positivity of thresholds, nondegenerate disorder, genuine probability laws, and full phase hypotheses are essential: removing any of them could make a formally easy statement unrelated to Theorem 1.1.

Selected references

Erik Bates and Sourav Chatterjee, The endpoint distribution of directed polymers, Annals of Probability 48 (2020); preprint arXiv:1612.03443v5 (2021). Preprint.

21 thms2 active usersReviewed

Completed

Algebra·Captain: Lucas

Celestial w_{1+∞} wedge algebra and gluon S-algebra (Zhu review, §7.1)Research Paper

Motivation

In celestial holography, scattering amplitudes of massless particles in four-dimensional flat spacetime are rewritten, by a Mellin transform in the particle energies, as correlation functions of operators on the two-dimensional celestial sphere. Soft theorems then become Ward identities of two-dimensional currents. Guevara, Himwich, Pate and Strominger (arXiv:2103.03961) found that the conformally soft graviton modes obtained this way close under the collinear OPE into an infinite-dimensional algebra, and Strominger (arXiv:2105.14346) identified it, after a rescaling, with the wedge subalgebra of $w_{1+\infty}$ , the Lie algebra of polynomial area-preserving (Hamiltonian) vector fields on a two-plane. The review of B. Zhu (arXiv:2606.24285, Section 7.1) summarises this derivation, together with its gauge-theory counterpart, the gluon $S$ -algebra, and the action of $w_{1+\infty}$ on it. The review describes the celestial $w$ -algebra as a consistency test for any proposed flat-space hologram.

Setting

The wedge range is the set of labels $(p,m)$ with

p\in\{1,\tfrac32,2,\tfrac52,\dots\},\qquad 1-p\le m\le p-1,\qquad p-1-m\in\mathbb Z,

equivalently: $p+m-1$ and $p-m-1$ are both natural numbers. Let $W$ be the complex vector space with basis $\{w^p_m\}$ indexed by the wedge range, and define a bilinear bracket on $W$ by Eq. (7.8),

[w^p_m,w^q_n]=\bigl(m(q-1)-n(p-1)\bigr)\,w^{p+q-2}_{m+n},

where the right-hand side is $0$ whenever $(p+q-2,m+n)$ falls outside the wedge.

Eq. (7.9) realises $w^p_m$ as the monomial $u^{p+m-1}v^{p-m-1}$ in the polynomial ring $\mathbb C[u,v]$ , equipped with the Poisson bracket $\{f,g\}=\partial_uf\,\partial_vg-\partial_vf\,\partial_ug$ .

The conformally soft graviton modes $H^k_m$ ( $k=2,1,0,-1,\dots$ , $\tfrac{k-2}{2}\le m\le\tfrac{2-k}{2}$ ) obey the commutator (7.5) with factorial coefficients and the gravitational coupling $\kappa$ . The rescaling (7.6), $w^p_m=\tfrac1\kappa(p-m-1)!(p+m-1)!\,H^{-2p+4}_m$ , turns (7.5) into (7.8).

On the gauge-theory side, with colour index $a$ and Lie-algebra structure constants $f^{ab}{}_c$ , the conformally soft gluon modes $R^{k,a}_n$ obey (7.14). The rescaling (7.15), $S^{q,a}_m=(q-m-1)!(q+m-1)!\,R^{3-2q,a}_m$ , gives the $S$ -algebra (7.16), $[S^{p,a}_m,S^{q,b}_n]=-if^{ab}{}_cS^{p+q-1,c}_{m+n}$ . The wedge algebra acts on it by (7.17), $[w^p_m,S^{q,a}_n]=\bigl(m(q-1)-n(p-1)\bigr)S^{p+q-2,a}_{m+n}$ .

Formalization targets

Goal: (7.8) is a Lie bracket

[X,X]=0,\qquad [X,[Y,Z]]=[[X,Y],Z]+[Y,[X,Z]]\qquad\text{for all }X,Y,Z\in W.

Milestones

Closure of the wedge (7.7)–(7.8): if $(p,m)$ and $(q,n)$ are in the wedge and $m(q-1)-n(p-1)\ne0$ , then $(p+q-2,m+n)$ is in the wedge.
Rescaling (7.5) $\Rightarrow$ (7.8): any family $H^k_m$ satisfying (7.5) in a complex vector space with a bilinear bracket, rescaled by (7.6), satisfies (7.8) (for $\kappa\neq 0$ ).
Poisson realisation on generators (7.9): $\{u^{p+m-1}v^{p-m-1},u^{q+n-1}v^{q-n-1}\}=2\bigl(m(q-1)-n(p-1)\bigr)u^{p+q+m+n-3}v^{p+q-m-n-3}$ . The review's "convention-dependent overall factor" is pinned to $2$ .
Poisson realisation, linear form (7.9): the linear map $w^p_m\mapsto u^{p+m-1}v^{p-m-1}$ intertwines (7.8) with $\tfrac12\{\cdot,\cdot\}$ .
Gluon rescaling (7.14) $\Rightarrow$ (7.16).
The $S$ -algebra is a Lie algebra (7.16), given that $f^{ab}{}_c$ are Lie structure constants.
$S$ is a $w_{1+\infty}$ -module (7.17): $[[X,Y],s]=[X,[Y,s]]-[Y,[X,s]]$ .

Significance

The statements fix, in a machine-checked form, the precise normalisations used in the celestial literature: the wedge range, the rescalings (7.6) and (7.15), and the overall factor in the Poisson realisation, which the review leaves convention-dependent. They form the algebraic base layer for later formalisations of deformations of $w_{1+\infty}$ , its loop algebra $Lw_{1+\infty}$ , and the gluon–graviton soft algebras. The results themselves are established in the physics literature. The formal work that remains is the combinatorics of the factorial coefficients, the closure of the finite wedge range, and the Jacobi identities.

Difficulty

None of the statements is deep, but each carries bookkeeping that is easy to get wrong. The factorial coefficients of (7.5) and (7.14) must cancel exactly against the rescalings. At the corners of the wedge ( $m=p-1$ , $n=q-1$ , or $p+q-2<1$ ) the target label leaves the wedge, and the structure constant must be shown to vanish there. The Jacobi identity for (7.8) does not follow term by term from the formula; the natural route is through the Poisson realisation, which must first be shown to be faithful.

Formalization scope

All objects are over $\mathbb C$ . Labels $p,m,q,n,k,l$ are rationals, and every label set is carved out by the predicate " $p+m-1$ and $p-m-1$ are natural numbers". Vector spaces with a given basis are finitely supported functions on the index set, and brackets are the bilinear extensions of the basis formulas. When the target label of a bracket falls outside the wedge, the bracket is defined to be $0$ (milestone 1 shows this only happens when the structure constant already vanishes). Factorials of rational arguments are taken of the truncation $\lfloor\cdot\rfloor_+$ to a natural number; on the relevant ranges the arguments are natural numbers, and at the single corner where (7.5) has argument $-1$ its prefactor vanishes. The operator-level identities (milestones 2 and 5) are stated for an arbitrary complex vector space with an arbitrary bilinear bracket, taking (7.5) resp. (7.14) as hypotheses on the given modes. The colour algebra is given by structure constants $f:\iota^3\to\mathbb C$ on a finite index set $\iota$ , with antisymmetry and the Jacobi identity as the definition of Lie structure constants. The factor $\kappa^{-1}$ uses the convention $0^{-1}=0$ , and milestone 2 assumes $\kappa\ne0$ .

Selected references

B. Zhu, Topics in Celestial holography: A bottom-up perspective, invited review for Physics Reports, arXiv:2606.24285v3, 2026. https://arxiv.org/abs/2606.24285 (Section 7.1, Eqs. (7.1)–(7.17)).
A. Guevara, E. Himwich, M. Pate, A. Strominger, Holographic symmetry algebras for gauge theory and gravity, JHEP 2021. https://arxiv.org/abs/2103.03961
A. Strominger, $w_{1+\infty}$ and the celestial sphere, Phys. Rev. Lett. 2021. https://arxiv.org/abs/2105.14346

10 thms2 active usersReviewed

Captain: Lucas

Gubser-Klebanov-Polyakov 1998: dimensions of operators dual to massive string statesResearch Paper

Motivation

In 1997 Maldacena conjectured that $\mathcal N=4$ super-Yang–Mills theory with gauge group $U(N)$ is equivalent to type IIB string theory on $\mathrm{AdS}_5\times S^5$ (hep-th/9711200). The paper of Gubser, Klebanov and Polyakov (hep-th/9802109), together with Witten's paper of the same year (hep-th/9802150), turned the conjecture into a computational rule: the generating functional of connected gauge theory correlators equals the minimum of the supergravity action subject to boundary conditions at the edge of anti-de Sitter space. The concrete outputs of the paper are two-point functions and operator dimensions, read off from the small-momentum, non-analytic behaviour of solutions of a radial ordinary differential equation.

The mathematical core is classical analysis of modified Bessel functions: which solution is regular in the throat, how $K_\nu$ splits into $I_{\pm\nu}$ , and what the leading non-analytic term of a logarithmic derivative is as the momentum tends to zero. The physical headline, Eq. (46), is that operators dual to massive string states at level $n$ acquire dimensions growing like $2(n\,g_{YM}\sqrt{2N})^{1/2}$ at large 't Hooft coupling.

Setting

Let $R>0$ be the AdS radius and $z>0$ the radial coordinate, with the boundary at $z=R$ and the horizon at $z=\infty$ . For a bulk field $\phi(x,z)=e^{ik\cdot x}\tilde f_k(z)$ with Euclidean momentum $k>0$ , the radial equation is

(\mathcal D_{k,\mu}f)(z)\;=\;z^3\,\partial_z\!\left(z^{-3}\partial_z f\right)-k^2 f-\frac{\mu}{z^2}\,f\;=\;0,

with $\mu=0$ for the massless s-wave (Eq. (20)), $\mu=l(l+4)$ for the $l$ -th partial wave (Eq. (34)), and $\mu=(mR)^2$ for a scalar string state of mass $m$ (Eq. (40)).

The modified Bessel functions are defined for $x>0$ and real $\nu$ by

K_\nu(x)=\int_0^\infty e^{-x\cosh t}\cosh(\nu t)\,dt,\qquad I_\nu(x)=\sum_{j\ge0}\frac{(x/2)^{2j+\nu}}{j!\,\Gamma(j+\nu+1)}.

The normalised radial profile is $\tilde f_k(z)=z^2K_\nu(kz)/(R^2K_\nu(kR))$ , the flux factor is $\mathcal F(k)=\big[z^{-3}\partial_z\log\tilde f_k(z)\big]_{z=R}$ , and the two-point function is $\langle O(k)O(q)\rangle=(2\pi)^4\delta^4(k+q)\,\tfrac{N^2}{16\pi^2}\mathcal F(k)$ (Eq. (26)). For a level- $n$ string state $m^2=4n/\alpha'$ , $R^4=2Ng_{YM}^2\alpha'^2$ , the Bessel order is $\nu=\sqrt{4+(mR)^2}$ (Eq. (41)) and the dimension of the dual operator is $\Delta=2+\nu$ (Eq. (45)).

Formalization targets

Goal (Eqs. (41)–(46))

For $n\ge1$ , $N,g_{YM},\alpha',m,R>0$ with $m^2=4n/\alpha'$ , $R^4=2Ng_{YM}^2\alpha'^2$ and $\nu=\sqrt{4+(mR)^2}\notin\mathbb Z$ : there is a function $A$ real-analytic at $0$ with

\frac{N^2}{16\pi^2}\mathcal F(k)=A(k^2)-\frac{N^2}{8\pi^2}\frac{\Gamma(1-\nu)}{\Gamma(\nu)}\Big(\frac{kR}{2}\Big)^{2\nu}R^{-4}+o(k^{2\nu})\quad(k\to0^+),

$\Delta=2+\nu=2+\sqrt{4+4n\,g_{YM}\sqrt{2N}}$ , and $\Delta\big/\big(2(n\,g\sqrt{2N})^{1/2}\big)\to1$ as $g\to\infty$ .

Milestones

Solutions of the radial equation (Eqs. (22), (35), (39)–(41)), regularity selecting $K_\nu$ (text after (23)), the connection formula $K_\nu=\frac{\pi}{2\sin\pi\nu}(I_{-\nu}-I_\nu)$ (Eq. (42)), the flux factor for integer order (Eqs. (36)–(37)) and non-integer order (Eqs. (43)–(44)), the relation $(mR)^2=4ng_{YM}\sqrt{2N}$ (Eq. (41)) and the asymptotics (45)–(46).

Significance

The computation is the prototype of the AdS/CFT dictionary between bulk masses and boundary dimensions, $\Delta(\Delta-4)=(mR)^2$ in five bulk dimensions. The massless case reproduces the non-renormalisation of dimensions of operators dual to supergravity fields; the massive case is the first prediction that unprotected operators acquire dimensions growing without bound at strong coupling.

The mathematical statements are classical, but their formalisation needs modified Bessel functions of real order, their connection formula, and asymptotic expansions near $0$ with logarithmic terms — material not currently present in Mathlib as far as the drafter checked. None of the statements below has a machine-checked proof yet.

Corrections to the source. Numerical exploration by the drafter (not machine-checked) indicates that the sign of the logarithmic coefficient printed in Eqs. (36)–(37) is reversed (the standard expansion has $(-1)^{n+1}\log(x/2)\,I_n(x)$ in $K_n(x)$ ), and that Eq. (27) is inconsistent with Eq. (37) at $l=0$ : the correct leading term for $l=0$ is $-\tfrac14k^4\log(kR)=-\tfrac18k^4\log(k^2R^2)$ . The partial-wave milestone is stated with the corrected coefficient. Eq. (44) (non-integer order), which carries the paper's main prediction, agrees with the standard expansions.

Difficulty

The flux factor is a logarithmic derivative of $K_\nu$ evaluated at the boundary. The leading term of $K_\nu$ near $0$ is a pure power, which contributes only an analytic part; the physical information sits in a subleading term of relative size $k^{2\nu}$ (or $k^{2l+4}\log k$ for integer order). Extracting it requires the full series structure of $K_\nu$ near $0$ , not only its leading asymptotics, together with control of the remainder uniformly enough to pass through a logarithm and a derivative.

Formalization scope

All functions are real-valued; $K_\nu$ is defined by its integral representation and $I_\nu$ by its power series, both used only for $x>0$ . The convention $1/\Gamma(\text{pole})=0$ is realised by Lean's $1/0=0$ . "An analytic function of $k^2$ plus a term plus $o(\cdot)$ " is encoded as: there exists $A$ with AnalyticAt ℝ A 0 such that the difference is little- $o$ of the given power as $k\to0^+$ . Because $2\nu$ is not an even integer when $\nu\notin\mathbb Z$ (and because of the logarithm in the integer case), the coefficient of the leading non-analytic term is uniquely determined, so the statements are not vacuous. The physics steps (the identification of generating functionals, Eq. (12), and the Fourier transform to position space) are not formalised: the two-point function is defined through the flux factor, Eq. (26). Welcome contributions: general facts about $K_\nu$ and $I_\nu$ (differential equation, positivity, asymptotics, series near $0$ ), reusable beyond this mission.

Selected references

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
J. Maldacena, The large N limit of superconformal field theories and supergravity, Adv. Theor. Math. Phys. 2 (1998) 231. https://arxiv.org/abs/hep-th/9711200
E. Witten, Anti de Sitter space and holography, Adv. Theor. Math. Phys. 2 (1998) 253. https://arxiv.org/abs/hep-th/9802150
NIST Digital Library of Mathematical Functions, Chapter 10 (Bessel functions). https://dlmf.nist.gov/10

11 thms2 active usersReviewed

Captain: Lucas

Wall 2013: The generalized second law implies a quantum singularity theoremResearch Paper

Motivation

The classical singularity theorems of general relativity, starting with Penrose's theorem (Penrose 1965), show that spacetime cannot be continued indefinitely along all light rays once gravity has trapped a surface. Every such theorem assumes a positivity condition on the stress–energy tensor, typically the null energy condition $T_{ab}k^ak^b\ge 0$ . Quantum fields violate every such pointwise condition, so the classical theorems say nothing about the regime where quantum effects near a would-be singularity are strongest.

Wall (2013) replaces the energy condition by the fine-grained generalized second law (GSL) of horizon thermodynamics: the generalized entropy (horizon area over $4\hbar G$ plus the entropy of the fields outside) of the exterior of any causal horizon never decreases. Generalizing the notion of trapped surface to a quantum trapped surface, on which the generalized entropy rather than the area decreases, the paper proves that a globally hyperbolic spacetime with a noncompact Cauchy surface containing a quantum trapped surface is null geodesically incomplete (Theorem 4).

Timeline: Penrose (1965) proved the classical theorem under the null energy condition; Hawking and Ellis (1973) give the standard textbook account; Wall (2010) derived the achronal averaged null energy condition from the GSL; Wall (2013) proved the quantum singularity theorem discussed here.

Setting

A spacetime is a smooth manifold $M$ with a smooth Lorentzian metric $g$ of signature $(-,+,\dots,+)$ and a continuous timelike vector field fixing the time orientation. Future-directed timelike and causal curves define the chronological relation $p\ll q$ and the causal relation $p\le q$ , and the sets $I^\pm(S)$ , $J^\pm(S)$ . Following §3.2 of the paper, $M$ is globally hyperbolic if there are no closed timelike curves and $J^+(p)\cap J^-(q)$ is compact for all $p,q$ . A Cauchy surface is a set met exactly once by every inextendible timelike curve. $M$ is null geodesically complete if every null geodesic can be extended to all values of its affine parameter.

The generalized entropy $S_{\rm gen}$ assigns a real number to the part of a time slice lying in a region. An observer is a future-infinite timelike worldline $W$ (or a null ray with infinite affine parameter); its causal horizon is $\partial I^-(W)$ , with exterior $I^-(W)$ . The fine-grained GSL (eq. (10)) says that for Cauchy surfaces $\Sigma'$ nowhere to the past of $\Sigma$ ,

S_{\rm gen}(\Sigma'\cap I^-(W))\ \ge\ S_{\rm gen}(\Sigma\cap I^-(W)).

A compact surface $T$ on a connected Cauchy surface $\Sigma$ , whose exterior on $\Sigma$ is noncompact, is quantum trapped if the generalized entropy outside the null surface $N$ shot outwards and to the future from $T$ is decreasing at every point of $T$ .

Formalization targets

Goal — Theorem 4 (quantum singularity theorem)

M \text{ globally hyperbolic},\ T \text{ quantum trapped},\ \text{semiclassical near } T,\ \text{fine-grained GSL}\ \Longrightarrow\ M \text{ is not null geodesically complete.}

Milestones

Theorem 3 — a null generator of a null surface along which the generalized entropy decreases at some point must leave the surface (or reach a singularity) in finite affine parameter.
Theorem 5 (appendix) — a trace-preserving, identity-preserving positive map can only equalize the eigenvalues of a density matrix: $\sum_{j\le i}\lambda_j^\downarrow(T\rho)\le\sum_{j\le i}\lambda_j^\downarrow(\rho)$ for every $i$ .
Corollary 4 (appendix) — consequently $\operatorname{tr} f(\rho)$ cannot decrease under such maps for every concave $f$ (in particular the von Neumann entropy).

Significance

The result. Theorem 4 makes the inevitability of black-hole and (time-reversed) Big Bang singularities independent of energy conditions, conditional only on the GSL, which is expected to hold in quantum gravity. Section 4 of the paper derives from it and its ingredients the absence of traversable wormholes, of warp drives between asymptotic regions, of time machines and of viable baby universes.

Formalizing it. No machine-checked account of Lorentzian causality theory, global hyperbolicity or the Penrose argument is currently available in Mathlib. This mission builds a self-contained Lean model of time-oriented Lorentzian manifolds, geodesics in coordinates, chronological and causal futures, Cauchy surfaces and global hyperbolicity, and pins down the exact logical content of the GSL-based singularity argument. The appendix milestones are pure matrix analysis (majorization under positive unital trace-preserving maps) and are reusable independently.

Difficulty

The goal splits into a thermodynamic step and a topological step. The thermodynamic step (every generator of $N$ terminates) is short once the hypotheses are in place. The topological step is the classical Penrose argument: turning "every generator terminates" into compactness of the achronal boundary and contradicting the noncompactness of the Cauchy surface. That requires the structure theory of achronal boundaries (generators, edges, the $C^0$ hypersurface property), limit-curve arguments for a uniform bound on the termination parameter, and the homeomorphism of achronal boundaries onto subsets of a Cauchy surface along a timelike flow. None of this exists in Mathlib.

Formalization scope

Spacetimes are manifolds M modelled on a finite-dimensional real inner product space E, smooth ( $C^\infty$ ), Hausdorff and second countable. The metric is a field of bilinear forms g x on the model space, smooth in every chart, with a continuous timelike field timeField giving signature $(-,+,\dots,+)$ and the time orientation.
Geodesics are affinely parametrized and defined by the coordinate geodesic equation (index lowered). Causal and chronological relations use finite concatenations of $C^1$ curves.
The generalized entropy is an arbitrary function Sgen : Set M → ℝ. The paper gives no rigorous definition of it or of "semiclassical", so the physical input enters as explicit hypotheses: the fine-grained GSL (eq. (10), extended to infinite null rays as in §2.2) and, at points of $T$ , the comparison principle of Theorem 1 restricted to comparisons against causal horizons (the formal stand-in for "the semiclassical approximation is valid near $T$ ").
"Decreasing" is strict ( $<$ ), since with eq. (33)'s $\le$ a constant Sgen would satisfy every hypothesis. $T$ is required nonempty. "Exterior noncompact" means the closure of the exterior is noncompact.
Corollary 4 is stated for concave $f$ on $[0,\infty)$ : the paper's own example (A.8)–(A.9) is concave, and the statement with convex $f$ fails (e.g. $f(p)=p^2$ under the completely depolarizing map).
Not included: Theorems 1 and 2 and Lemmas 1–3, whose statements depend on the semiclassical $\hbar$ -expansion and on the internal structure $S_{\rm gen}=A/4\hbar G+Q+S_{\rm out}$ , which this model treats abstractly.

Selected references

A. C. Wall, The generalized second law implies a quantum singularity theorem, Class. Quantum Grav. 30 (2013) 165003. https://doi.org/10.1088/0264-9381/30/16/165003
R. Penrose, Gravitational collapse and space-time singularities, Phys. Rev. Lett. 14 (1965) 57. https://doi.org/10.1103/PhysRevLett.14.57
S. W. Hawking and G. F. R. Ellis, The Large Scale Structure of Space-Time, Cambridge University Press, 1973. https://doi.org/10.1017/CBO9780511524646

6 thms2 active usersReviewed

Completed

Captain: Lucas

The new Minimal Standard ModelResearch Paper

Motivation

The Minimal Standard Model (MSM) — the $SU(3)_C\times SU(2)_L\times U(1)_Y$ gauge theory with three generations of quarks and leptons, one Higgs doublet and classical gravity — accounts for almost all laboratory phenomena, but it does not accommodate several empirical facts established since the late 1990s: non-baryonic dark matter, dark energy, neutrino masses and mixings, the baryon asymmetry of the universe, and nearly scale-invariant, adiabatic, Gaussian density fluctuations. Davoudiasl, Kitano, Li and Murayama (Phys. Lett. B 609 (2005) 117) propose the new Minimal Standard Model (NMSM): the most general renormalizable Lagrangian obtained by adding the minimal particle content needed for these facts — two right-handed Majorana neutrinos $N_1, N_2$ , one $\mathbb Z_2$ -odd real singlet scalar $S$ (dark matter), one real scalar $\varphi$ (the inflaton), and a cosmological constant — six new degrees of freedom in total.

Most of the paper's claims are phenomenological (relic abundance, the Higgs-mass window from one-loop running, direct-detection rates). A smaller set are exact mathematical consequences of the model's structure, and this mission collects those.

Setting

Neutrino sector (Eq. (4)). In the basis where the right-handed-neutrino mass matrix is real and diagonal, the model has masses $M_1, M_2>0$ and a complex $2\times 3$ Yukawa matrix $h_\nu=(h_\nu^{\alpha i})$ . With Higgs vacuum expectation value $\langle H\rangle = v/\sqrt2$ , the Dirac mass matrix is $m_D = h_\nu v/\sqrt 2$ . The neutral leptons $(\nu_1,\nu_2,\nu_3,N_1,N_2)$ then have the $5\times5$ complex symmetric Majorana mass matrix

\mathcal M = \begin{pmatrix} 0 & m_D^{\mathsf T} \\ m_D & \operatorname{diag}(M_1,M_2)\end{pmatrix},

and the seesaw light-neutrino mass matrix is $m_\nu = -m_D^{\mathsf T}\operatorname{diag}(M_1,M_2)^{-1} m_D$ . The physical masses described by a complex mass matrix $A$ are its singular values, the square roots of the eigenvalues of $A^\dagger A$ .

Inflaton sector (Eq. (5)). Inflation is driven by the quadratic potential $V(\varphi)=\tfrac12 m^2\varphi^2$ (chaotic inflation). With reduced Planck mass $M_{\rm Pl}$ , the slow-roll parameters are $\epsilon = \tfrac{M_{\rm Pl}^2}{2}(V'/V)^2$ and $\eta = M_{\rm Pl}^2 V''/V$ , inflation ends where $\epsilon = 1$ , the number of e-folds between $\varphi_{\rm end}$ and $\varphi$ is $N = M_{\rm Pl}^{-2}\int_{\varphi_{\rm end}}^{\varphi} V/V'$ , and the observables are $n_s = 1-6\epsilon+2\eta$ and $r=16\epsilon$ .

Scalar sector running (Eq. (10)). The singlet quartic coupling $h$ obeys the one-loop equation $(4\pi)^2\, dh/dt = 3h^2 + 12k^2$ , $t=\log\mu$ , where $k$ is the Higgs–singlet coupling.

Formalization targets

Goal — an exactly massless neutrino

For every $v\in\mathbb R$ , every complex $h_\nu$ and all $M_1,M_2>0$ , some physical mass of the full matrix $\mathcal M$ vanishes:

\exists\, i,\quad \sigma_i(\mathcal M)=0 .

This is the paper's statement that with only two right-handed neutrinos "one of the neutrino masses exactly vanishes" (pp. 119, 122).

Milestones

Seesaw rank (p. 119). $\operatorname{rank} m_\nu \le 2$ , and $m_\nu$ has a zero physical mass.
Enough parameters (p. 119). For $v>0$ and $M_1,M_2>0$ , every complex symmetric $3\times3$ matrix of rank at most $2$ equals $m_\nu$ for some $h_\nu$ .
Inflation predictions (pp. 119, 122). For $V=\tfrac12m^2\varphi^2$ : $\epsilon(\sqrt2 M_{\rm Pl})=1$ , and at $N$ e-folds before the end, $n_s = 1-\tfrac{4}{2N+1}$ , $r=\tfrac{16}{2N+1}$ ; at $N=50$ these are within $0.005$ of $0.96$ and $0.16$ .
Initial asymmetry is diluted (p. 120). If $N\ge \ln(10\,\mathrm{Gpc}/10\,\mathrm{kpc})$ and $\mu_F^4/\rho_\varphi = e^{-4N}$ , then $\mu_F^3/\rho_\varphi^{3/4}\le 10^{-18} < 8.8\times10^{-11}$ .
Eq. (10), monotonicity. On any interval where it solves Eq. (10), $h$ is non-decreasing.
Eq. (10), Landau pole. A solution on $[t_0,T)$ with $h(t_0)>0$ forces $T\le t_0 + \tfrac{16\pi^2}{3h(t_0)}$ .

Significance

The vanishing neutrino mass is a sharp, falsifiable prediction of the NMSM: as the paper notes, a positive neutrino-mass signal at KATRIN would require masses for all three neutrinos, and a neutrinoless double-beta-decay signal in near-future experiments is possible only for the inverted hierarchy. Milestone 2 makes precise the paper's parameter count (eleven parameters in Eq. (4) against seven light-neutrino observables): the two-right-handed-neutrino seesaw reproduces every rank- $\le 2$ light mass matrix. Milestones 3–6 pin down the closed-form content behind the inflationary predictions, the argument that baryogenesis is required, and the triviality behaviour of the singlet coupling.

These results are textbook-level linear algebra and calculus once stated; the contribution of the mission is a precise, machine-checked statement of exactly which claims of the paper are mathematical theorems and under which conventions.

Difficulty

The goal and Milestone 1 are linear-algebra facts, but they must be connected to the spectral-theorem definition of physical masses (eigenvalues of $A^\dagger A$ ), not merely to a determinant. Milestone 2 requires a Takagi-type decomposition of complex symmetric matrices (a rank- $r$ complex symmetric matrix is a sum of $r$ terms $w w^{\mathsf T}$ ), which is not available in Mathlib. Milestone 3 requires evaluating a parametric integral and derivatives of the potential. Milestone 6 is an ODE comparison argument from a differential inequality.

Formalization scope

All matrices are over $\mathbb C$ , indexed by Fin 2, Fin 3 and Fin 3 ⊕ Fin 2. Physical masses are defined as square roots of the eigenvalues of $A^\dagger A$ from Mathlib's spectral theorem for Hermitian matrices; their ordering is Mathlib's and no statement depends on it. Slow-roll quantities use Mathlib's deriv and interval integral; Lean's junk value $x/0=0$ cannot affect the stated results because the inflaton interval stays away from $\varphi=0$ . The phenomenological results (dark-matter relic abundance, the $130$ – $180$ GeV Higgs window, the $5.5$ GeV– $1.8$ TeV singlet window, direct-detection rates) rely on numerical integration and are out of scope. The one-loop beta functions are taken as given ODEs; their derivation from the Lagrangian is not formalized.

Selected references

H. Davoudiasl, R. Kitano, T. Li, H. Murayama, The new Minimal Standard Model, Phys. Lett. B 609 (2005) 117–123. https://doi.org/10.1016/j.physletb.2005.01.026
A. D. Linde, Phys. Lett. B 129 (1983) 177 (chaotic inflation; reference [18] of the paper).
J. R. Ellis, M. Raidal, T. Yanagida, Phys. Lett. B 581 (2004) 9 (source of the quoted values of $n_s$ and $r$ ; reference [21] of the paper).

8 thms2 active usersReviewed

Completed

Captain: Lucas

Astrophysical Fluid Dynamics I: Rankine–Hugoniot Shock RelationsTextbook

Motivation

Shock waves are ubiquitous in astrophysical gases: supernova remnants, stellar winds meeting the interstellar medium, accretion flows onto compact objects, and jets all contain them. Because astrophysical flows are typically highly supersonic and nearly inviscid, the internal structure of a shock is thin compared with the flow, and the shock is treated as a discontinuity. What connects the states on either side is not the detailed dissipative physics inside the shock but the conservation of mass, momentum and energy across it. For a perfect gas these conditions can be solved in closed form, giving the post-shock density, velocity and pressure as explicit functions of the pre-shock Mach number. These formulas are a standard tool, used for example as the boundary condition of the Sedov–Taylor blast-wave solution for supernova remnants.

The formulas go back to Rankine (1870) and Hugoniot (1887–1889). This mission follows the presentation in the Cambridge Part III lecture notes of G. I. Ogilvie, Astrophysical fluid dynamics, J. Plasma Phys. 82 (2016) 205820301 (doi:10.1017/S0022377816000489), §6.3.2 and Example A.13.

Setting

Consider a perfect gas with constant adiabatic exponent $\gamma > 1$ (for example $\gamma = 5/3$ for a fully ionized monatomic gas). A thermodynamic state is described by the density $\rho > 0$ and pressure $p > 0$ ; the specific enthalpy is $h = \frac{\gamma}{\gamma-1}\frac{p}{\rho}$ , the specific internal energy is $e = \frac{p}{(\gamma-1)\rho}$ , and the adiabatic sound speed is $v_s = (\gamma p/\rho)^{1/2}$ .

A normal shock is a planar discontinuity, here taken at rest at $x = 0$ , through which gas flows from left to right with velocity component $u > 0$ normal to the shock. The upstream (pre-shock) state is $(\rho_1, u_1, p_1)$ and the downstream (post-shock) state is $(\rho_2, u_2, p_2)$ . Writing $[Q]_1^2 = Q_2 - Q_1$ , the states satisfy the Rankine–Hugoniot relations

[\rho u]_1^2 = 0, \qquad [\rho u^2 + p]_1^2 = 0, \qquad \Big[\rho u\big(\tfrac12 u^2 + h\big)\Big]_1^2 = 0,

expressing continuity of the fluxes of mass, momentum and energy. The Mach numbers are $M_1 = u_1/v_{s1}$ and $M_2 = u_2/v_{s2}$ . A genuine shock is one in which the two states differ; the trivial solution $(\rho_2,u_2,p_2) = (\rho_1,u_1,p_1)$ always satisfies the relations.

The specific entropy of a perfect gas is $s = c_p(\gamma^{-1}\ln p - \ln \rho) + \text{const}$ , with $c_p = \gamma c_v$ , so the entropy jump across the shock is $[s]_1^2/c_v = \ln(p_2/p_1) - \gamma \ln(\rho_2/\rho_1)$ .

Formalization targets

Goal: the Rankine–Hugoniot jump formulas (eqs. 6.30–6.31)

For a genuine shock in a perfect gas,

\frac{\rho_2}{\rho_1} = \frac{u_1}{u_2} = \frac{(\gamma+1)M_1^2}{(\gamma-1)M_1^2+2}, \qquad \frac{p_2}{p_1} = \frac{2\gamma M_1^2-(\gamma-1)}{\gamma+1}, \qquad M_2^2 = \frac{2+(\gamma-1)M_1^2}{2\gamma M_1^2-(\gamma-1)}.

Milestones

The three jump formulas separately (eqs. 6.30a, 6.30b, 6.31).
The density and pressure ratios are strictly increasing functions of $M_1 > 0$ .
Classification: $M_1 \neq 1$ for a genuine shock; $M_1 > 1$ gives a compression shock ( $M_2<1$ , $\rho_2>\rho_1$ , $p_2>p_1$ ) and $M_1<1$ a rarefaction shock ( $M_2>1$ , $\rho_2<\rho_1$ , $p_2<p_1$ ).
The entropy jump in terms of the pressure ratio $P = p_2/p_1$ (eq. A 28):

\frac{[s]_1^2}{c_v} = \ln P - \gamma \ln\left[\frac{(\gamma+1)P+(\gamma-1)}{(\gamma-1)P+(\gamma+1)}\right].

The entropy jump is positive for compression shocks and negative for rarefaction shocks; hence the second law $[s]_1^2 \ge 0$ forces a compression shock with $M_1>1>M_2$ .
Strong-shock limits as $M_1 \to \infty$ (eqs. 6.32a–c): $\rho_2/\rho_1 \to \frac{\gamma+1}{\gamma-1}$ , $p_2/p_1 \to \infty$ , $M_2^2 \to \frac{\gamma-1}{2\gamma}$ .
The downstream state behind a strong shock (eqs. 6.33–6.34): at fixed $\rho_1$ and shock speed $u_{sh} = -u_1$ , as $p_1 \to 0^+$ ,

\rho_2 \to \frac{\gamma+1}{\gamma-1}\rho_1,\quad u_2-u_1 \to \frac{2u_{sh}}{\gamma+1},\quad p_2 \to \frac{2\rho_1u_{sh}^2}{\gamma+1},\quad e_2 \to \frac{2u_{sh}^2}{(\gamma+1)^2}.

Significance

The result itself. The jump formulas determine the post-shock state from the pre-shock state and a single number, the shock Mach number. They show that the compression ratio of a shock in a perfect gas is bounded (by $4$ for $\gamma = 5/3$ ) however strong the shock, that a strong shock converts a fixed fraction of the incoming kinetic energy into heat, and, through the entropy jump, that only compressive shocks are compatible with the second law of thermodynamics. The strong-shock downstream state is the input to the self-similar supernova blast-wave solution treated later in the same notes (§7).

Formalizing it. The results are classical and fully proved in the textbook sense; a search of the platform library found no existing formalization of them. The mission produces a reusable Lean vocabulary for one-dimensional perfect-gas shocks (enthalpy, sound speed, Mach number, Rankine–Hugoniot predicate, entropy jump) on which later missions on blast waves, oblique shocks or MHD shocks can build.

Difficulty

The individual steps are algebraic, but the Rankine–Hugoniot system is nonlinear and always has the trivial solution. Eliminating variables leads to a quadratic in the velocity ratio $u_2/u_1$ with roots $1$ and the shock root, so any derivation must use the hypothesis that the two states differ at exactly the right point; dividing by the trivial factor without that hypothesis is the standard mistake. The sign of the entropy jump is a genuinely analytic statement: it requires showing that a one-variable function of $P$ involving logarithms vanishes only at $P = 1$ and has a definite sign on each side. The strong-shock statements are limits and need uniform control of the downstream state as $p_1 \to 0$ .

Formalization scope

All quantities are real numbers. The gas is a perfect gas with $\gamma > 1$ ; every statement about gas states assumes strictly positive densities, pressures and normal velocities, which matches the source's convention $u_x > 0$ and makes all square roots, quotients and logarithms well-defined (Lean's total functions would otherwise return junk values, e.g. division by zero gives $0$ ). Only the normal, non-magnetic shock is treated; the shock is at rest, and the frame change to the upstream rest frame appears only through $u_{sh} = -u_1$ . The entropy is represented through its jump divided by $c_v$ . The genuine-shock hypothesis $(\rho_2,u_2,p_2) \neq (\rho_1,u_1,p_1)$ rules out the trivial solution, under which the jump formulas would be false for $M_1 \neq 1$ ; it is omitted only from the entropy-jump formula (A 28), which also holds for the trivial solution. The strong-shock limit " $M_1 \gg 1$ " is expressed as $p_1 \to 0^+$ at fixed $\rho_1$ and $u_1$ , and " $p_2/p_1 \gg 1$ " as divergence to $+\infty$ .

The definitions are collected in one shared file (namespace AstrophysicalFluidDynamics, intended to be reused by later missions on the same lecture notes). Only Mathlib's real analysis (logarithm, square root, limits) is needed. Contributions welcome: proofs of the milestones, and reusable lemmas such as the factorization of the Rankine–Hugoniot system through the trivial root.

Selected references

G. I. Ogilvie, Astrophysical fluid dynamics, Journal of Plasma Physics 82 (2016) 205820301. https://doi.org/10.1017/S0022377816000489
W. J. M. Rankine, On the thermodynamic theory of waves of finite longitudinal disturbance, Philosophical Transactions of the Royal Society of London 160 (1870) 277–288.
L. D. Landau and E. M. Lifshitz, Fluid Mechanics, 2nd ed., Pergamon (1987), Chapter IX.

12 thms2 active usersReviewed

Completed

Captain: Lucas

Giunti–Studenikin 2015: Neutrino Oscillations, Majorana Form Factors and Spin PrecessionResearch Paper

Motivation

Neutrinos are the only Standard Model fermions whose masses, mixing and electromagnetic properties are still largely unknown. The review of Giunti and Studenikin (Rev. Mod. Phys. 87, 531 (2015)) collects the theory of neutrino masses and mixing, the general structure of neutrino electromagnetic form factors for Dirac and Majorana neutrinos, and the dynamics of neutrino spin and flavor in electromagnetic fields and matter. Most of the review is phenomenology (experimental bounds, astrophysical estimates), but a core of it consists of exact mathematical statements about finite-dimensional unitary matrices, Hermitian matrices and two-level linear Schrödinger equations. Those exact statements are what this mission targets.

Timeline of the results formalized here:

1957–1968: Pontecorvo; Maki, Nakagawa and Sakata introduce neutrino mixing and oscillations.
1957: Case; Radicati and Touschek observe that Majorana neutrinos cannot have diagonal magnetic or electric dipole moments.
1971: Cisneros proposes spin precession $\nu_{eL}\to\nu_{eR}$ of solar neutrinos in a magnetic field.
1978: Wolfenstein writes the evolution equation of neutrino flavor in matter; 1985: Mikheev and Smirnov identify its resonance (MSW effect).
1986: Okun, Voloshin and Vysotsky; Voloshin and Vysotsky show that matter suppresses spin precession.

Setting

A mixing matrix is a unitary $n\times n$ complex matrix $U$ whose rows are labelled by flavors $\ell$ and whose columns are labelled by massive states $k$ with masses $m_k$ . For a neutrino of energy $E>0$ that has travelled a distance $L$ , the plane-wave transition probability (Eqs. (2.35)–(2.36)) is

P_{\nu_\ell\to\nu_{\ell'}}(L,E)=\Bigl|\sum_k U^*_{\ell k}\,e^{-i m_k^2 L/(2E)}\,U_{\ell' k}\Bigr|^2 .

In the Lean development this is oscProb U m L E l l'. The standard parametrization $U^{\mathrm D}(\vartheta_{12},\vartheta_{13},\vartheta_{23},\delta_{13})$ of Eq. (2.27) and the Majorana phase matrix $D^{\mathrm M}=\operatorname{diag}(1,e^{i\lambda_{21}},e^{i\lambda_{31}})$ of Eq. (2.28) are diracMixing and majoranaPhases; the two-neutrino rotation matrix of Eq. (2.38) is twoFlavorMixing.

In matter of constant electron density, the $\nu_e$ – $\nu_a$ amplitudes $(\varphi_e,\varphi_a)$ obey $i\,\tfrac{d}{dx}\varphi=\mathrm H\varphi$ with the effective Hamiltonian of Eq. (2.46) (mswHamiltonian), built from the vacuum squared-mass difference $\Delta m^2$ , the mixing angle $\vartheta$ and the charged-current potential $V_{\rm CC}$ with $A_{\rm CC}=2EV_{\rm CC}$ . The effective squared-mass difference $\Delta m^2_{\rm M}$ of Eq. (2.53) and effective angle $\vartheta_{\rm M}$ of Eq. (2.54) are mswDeltaM2 and mswMixingAngle.

Electromagnetic form-factor matrices $\mathbb f_\Omega$ ( $\Omega=Q,M,E,A$ : charge, magnetic, electric, anapole) are Hermitian $N\times N$ complex matrices in the space of massive neutrinos; for Majorana neutrinos they are in addition antisymmetric ( $\Omega=Q,M,E$ ) or symmetric ( $\Omega=A$ ), Eqs. (3.66)–(3.68).

Finally, the helicity amplitudes $(\psi_L,\psi_R)$ of an ultrarelativistic Dirac neutrino with magnetic moment $\mu$ in a transverse field $B_\perp$ and matter potential $V$ obey $i\,\tfrac{d}{dx}\psi=\begin{pmatrix}V&\mu B_\perp\\ \mu B_\perp&0\end{pmatrix}\psi$ (Eqs. (6.23), (6.28); spinFlavorHamiltonian), with energy splitting $\Delta E_{\rm M}=\sqrt{V^2+(2\mu B_\perp)^2}$ (Eq. (6.31); spinFlavorEnergySplitting).

Formalization targets

Goal: the general vacuum oscillation probability, Eq. (2.37)

For every unitary $U$ , all masses $m_k$ , every $L$ and every $E>0$ ,

P_{\nu_\ell\to\nu_{\ell'}}=\delta_{\ell\ell'}-4\sum_{k>j}\operatorname{Re}\bigl(U^*_{\ell k}U_{\ell' k}U_{\ell j}U^*_{\ell' j}\bigr)\sin^2\!\Bigl(\frac{\Delta m^2_{kj}L}{4E}\Bigr)-2\sum_{k>j}\operatorname{Im}\bigl(U_{\ell k}U^*_{\ell j}U^*_{\ell' k}U_{\ell' j}\bigr)\sin\!\Bigl(\frac{\Delta m^2_{kj}L}{2E}\Bigr),

with $\Delta m^2_{kj}=m_k^2-m_j^2$ . The number $n$ of massive states is left free (the paper uses $n=3$ , and $n>3$ with sterile neutrinos, Sec. II.F).

Milestones

Eqs. (2.26)–(2.28): $U^{\mathrm D}$ and $U^{\mathrm D}D^{\mathrm M}$ are unitary.
Eq. (2.39): two-neutrino transition probability $\sin^2 2\vartheta\,\sin^2(\Delta m^2L/4E)$ .
Eq. (2.40): two-neutrino survival probability $1-\sin^2 2\vartheta\,\sin^2(\Delta m^2L/4E)$ .
Eqs. (2.50)–(2.54): $U_{\rm M}^T\mathrm H U_{\rm M}=\operatorname{diag}(-\Delta m^2_{\rm M},\Delta m^2_{\rm M})/4E$ .
Eq. (2.57): MSW transition probability at constant density $\sin^2 2\vartheta_{\rm M}\sin^2(\Delta m^2_{\rm M}x/4E)$ .
Eqs. (3.66)–(3.70): Majorana form-factor matrices — antisymmetric Hermitian matrices are purely imaginary with vanishing diagonal; symmetric Hermitian matrices are real.
Eqs. (3.71)–(3.72): three-flavor antisymmetric Hermitian form factors are $i\sum_j\epsilon^{fij}\tilde{\mathbb f}^j$ with a real vector $\tilde{\mathbb f}$ .
Eq. (6.27): spin precession in a transverse field, $P_{\nu_L\to\nu_R}(x)=\sin^2\bigl(\int_0^x\mu B_\perp\bigr)$ .
Eq. (6.34): spin precession in matter, $P_{\nu_L\to\nu_R}(x)=\sin^2 2\xi\,\sin^2(\tfrac12\Delta E_{\rm M}x)$ with $\sin 2\xi=2\mu B_\perp/\Delta E_{\rm M}$ .

Significance

Eq. (2.37) is the formula used in essentially every analysis of oscillation data; its two-neutrino specializations (2.39)–(2.40) and the matter formula (2.57) are the standard fitting functions for reactor, accelerator and solar experiments. The Majorana constraints (3.67)–(3.70) are the precise statement behind the claim that a measured diagonal magnetic moment would rule out Majorana neutrinos (under CPT). The spin-precession formulas (6.27) and (6.34) underlie the astrophysical bounds on neutrino magnetic moments.

All targets are established results with textbook derivations; none is open. What the mission adds is machine-checked versions with every convention (sign of the phase, ordering $k>j$ , ranges of angles, boundary conditions of the Schrödinger equation) fixed explicitly. Related vacuum-oscillation statements from a different source already exist on the platform under the LipariNeutrino namespace; the present drafts are self-contained and follow this paper's notation and equation numbering.

Difficulty

The algebraic targets require careful bookkeeping of complex conjugation and of the unitarity relations $UU^\dagger=U^\dagger U=1$ inside double sums over $k>j$ . The dynamical targets (2.57), (6.27), (6.34) are statements about every solution of a linear ODE with a given initial value, so a solution in closed form is not enough: uniqueness of solutions of the (for (6.27), non-autonomous) linear system must also be established in Lean.

Formalization scope

Flavor and mass indices are Fin n; two-neutrino indices 0,1 stand for $(\nu_e,\nu_a)$ , $(\nu_L,\nu_R)$ or $(\nu_1,\nu_2)$ .
Masses $m_k$ are arbitrary reals and enter only through $m_k^2$ .
Unitarity is membership in Matrix.unitaryGroup.
The evolution equations are encoded as HasDerivAt φ (-(I • H.mulVec (φ x))) x for all real $x$ , i.e. $\varphi'=-i\mathrm H\varphi$ , with initial value $(1,0)$ .
$\vartheta_{\rm M}$ is defined as half the argument of $(\Delta m^2\cos2\vartheta-2EV_{\rm CC})+i\,\Delta m^2\sin2\vartheta$ , which realizes Eq. (2.54) without the division-by-zero at resonance; $\sin 2\xi=2\mu B_\perp/\Delta E_{\rm M}$ is inlined, with Lean's convention $0/0=0$ in the degenerate case $V=\mu B_\perp=0$ .
The source's angle ranges ( $0\le\vartheta\le\pi/2$ , $0\le\delta_{13}<2\pi$ ) and $E>0$ are kept as hypotheses.

Useful reusable infrastructure: uniqueness for linear ODEs in $\mathbb C^2$ , closed-form exponentials of $2\times2$ real symmetric matrices, and algebraic lemmas for unitary matrices.

Selected references

C. Giunti and A. Studenikin, Neutrino electromagnetic interactions: A window to new physics, Rev. Mod. Phys. 87, 531 (2015). https://doi.org/10.1103/RevModPhys.87.531
C. Giunti and C. W. Kim, Fundamentals of Neutrino Physics and Astrophysics, Oxford University Press (2007).
L. Wolfenstein, Neutrino oscillations in matter, Phys. Rev. D 17, 2369 (1978). https://doi.org/10.1103/PhysRevD.17.2369

11 thms2 active usersReviewed

Completed

Linear algebra·Captain: Lucas

Baumgarten 2018: How to (Un-) Quantum Mechanics — Phase-Space AlgebraResearch Paper

Motivation

C. Baumgarten's essay How to (Un-) Quantum Mechanics (arXiv:1810.06981, v2 2025) argues that much of the mathematical formalism usually presented as specifically "quantum" — Heisenberg's equation of motion, commutators, eigenvalue problems, the real Pauli and Dirac algebras — already follows from classical linear Hamiltonian mechanics on an abstract phase space. The physical and philosophical claims of the paper are outside the scope of a formalization, but its argument rests on a compact chain of linear-algebra facts stated in Sections IV–VI (pp. 13–20). This mission formalizes exactly that chain, so that the mathematical part of the argument can be checked independently of its interpretation.

Setting

Fix a number $n \ge 0$ of degrees of freedom. A phase-space vector is $\psi = (q_1,p_1,\dots,q_n,p_n)^T \in \mathbb R^{2n}$ . The symplectic unit matrix is the Kronecker product

\gamma_0 = \mathbf 1_n \otimes \eta_0, \qquad \eta_0 = \begin{pmatrix}0 & 1\\ -1 & 0\end{pmatrix}.

A real $2n\times 2n$ matrix is Hamiltonian if it equals $\gamma_0 A$ with $A$ symmetric, skew-Hamiltonian if it equals $\gamma_0 B$ with $B$ skew-symmetric, and symplectic if $M\gamma_0M^T = \gamma_0$ .

Linear Hamiltonian motion is $\dot\psi = H\psi$ with $H$ Hamiltonian (the paper's Eq. 35, coming from the quadratic Hamiltonian $\tfrac12\psi^TA\psi$ ). A matrix of second moments $\Sigma(\tau)$ (in the paper an average $\langle\psi\psi^T\rangle$ ) then evolves by

\dot\Sigma = H\Sigma + \Sigma H^T \qquad\text{(Eq. 40)},

and the autocorrelation matrix is $S = \Sigma\gamma_0^T$ .

Target

The goal theorem combines the conclusions drawn on pp. 16–17: for $H$ Hamiltonian and $\Sigma$ a symmetric solution of Eq. (40), the autocorrelation matrix satisfies, for every time $\tau$ ,

\chi_{S(\tau)} = \chi_{S(0)} \qquad\text{and}\qquad \operatorname{Tr}\big(S(\tau)^{2k+1}\big) = 0 \ \ (k \in \mathbb N),

where $\chi$ is the characteristic polynomial: "the eigenvalues are constants of motion" (after Eq. 51) together with Eq. (48).

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

pairing $\pm\lambda$ of eigenvalues of skew-symmetric matrices, and a vanishing eigenvalue in odd size (p. 13);
conservation of $H$ under $\dot\psi = J\nabla H$ with $J$ skew (Eqs. 26–28);
identities of $\gamma_0$ and the transpose rules for (skew-)Hamiltonian matrices (Eqs. 33, 36, 54);
$\exp(H\tau)\psi_0$ solves $\dot\psi = H\psi$ (Eq. 49);
Heisenberg's equation $\dot S = [H,S]$ for second moments (Eq. 42);
the Lax invariants $\operatorname{Tr}(S^k)$ (Eq. 47) and tracelessness of odd powers (Eq. 48);
symplecticity of $\exp(H\tau)$ and $S(\tau) = M(\tau)S(0)M(-\tau)$ (Eqs. 50–51);
the dimension counts $n(2n+1)$ and $n(2n-1)$ (Eqs. 55–56) and the (anti-)commutator table (Eq. 57);
the matrix Euler formulas for the real Pauli matrices (Eq. 66).

Significance

The result itself. Each statement is classical linear algebra or linear ODE theory; the paper uses them to argue that Heisenberg's equation and the spectral description of observables arise from second moments of a classical Hamiltonian ensemble. A checked version separates what is a theorem from what is interpretation, and pins down the hypotheses (for example, that only symmetry of $A$ is needed for Eq. 48, not positive definiteness).

Formalizing it. None of these statements is new mathematics; the work is to formalize them in the paper's notation ( $\gamma_0 = \mathbf 1_n\otimes\eta_0$ , entrywise matrix derivatives, the matrix exponential) so that they can be reused for later parts of the paper, such as the real Dirac algebra of Sec. VII–VIII.

Difficulty

Most milestones are short calculations. The two steps needing real infrastructure are (i) the uniqueness of solutions of the linear matrix ODE $\dot S = [H,S]$ , needed to identify $S(\tau)$ with $\exp(H\tau)S(0)\exp(-H\tau)$ , and (ii) the dimension counts, which require an explicit basis or an isomorphism with symmetric/skew-symmetric matrices. Going through the Lax invariants alone gives only the traces of powers of $S$ , and recovering the characteristic polynomial from them needs Newton's identities; the similarity form of Eq. (51) gives the conservation of the characteristic polynomial directly.

Formalization scope

Everything is over $\mathbb R$ . Matrices are indexed by pairs $(i,b)$ , $i<n$ , $b\in\{0,1\}$ , so that $\gamma_0$ is literally a Kronecker product; $n = 0$ is allowed. Time derivatives of matrix-valued functions are entrywise HasDerivAt; $\exp$ is Mathlib's power-series NormedSpace.exp. A Hamiltonian matrix is $\gamma_0A$ with $A$ symmetric (no definiteness); $\Sigma$ is any symmetric solution of Eq. (40) — positivity is not assumed because it is not used. Eigenvalues of real skew-symmetric matrices are taken over $\mathbb C$ . "Number of linearly independent elements" is the dimension of the real span. No statement is vacuous: all hypotheses are satisfied, for example, by $H = \gamma_0$ and $\Sigma \equiv \mathbf 1$ .

All statements share the definition file UnQM_phase_space and the namespace UnQuantumMechanics.

Selected references

C. Baumgarten, How to (Un-) Quantum Mechanics, arXiv:1810.06981v2 [physics.gen-ph], 2025. https://arxiv.org/abs/1810.06981
P. D. Lax, Integrals of nonlinear equations of evolution and solitary waves, Comm. Pure Appl. Math. 21 (1968), 467–490. https://doi.org/10.1002/cpa.3160210503

18 thms2 active usersReviewed

Completed

Captain: Lucas

Virial Theorem (Classical N-Particle Mechanics)Textbook

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

$\frac12\,\dot I=G$ .
$\dot G=2T+\sum_kF_k\cdot r_k$ .
With Newton's third law, $\sum_kF_k\cdot r_k=\sum_k\sum_{j<k}F_{jk}\cdot(r_k-r_j)$ .
Potential pair forces are central: $F_{jk}=-\frac{V_{jk}'(r_{jk})}{r_{jk}}(r_k-r_j)$ .
Potential pair forces satisfy $F_{jk}=-F_{kj}$ .
$\sum_kF_k\cdot r_k=-\sum_k\sum_{j<k}V'_{jk}(r_{jk})\,r_{jk}$ .
Power law: $\sum_kF_k\cdot r_k=-nV_{\mathrm{TOT}}$ .
Power law: $\dot G=2T-nV_{\mathrm{TOT}}$ .
Lagrange's identity ( $n=-1$ ): $\frac12\ddot I=2T+V_{\mathrm{TOT}}$ .
$\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$ .
Bounded motion: $\langle\dot G\rangle_\tau\to0$ .
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.

14 thms2 active usersReviewed

Completed

Statistics·Captain: Lucas

Methanol Limit on a Drifting Proton-to-Electron Mass Ratio (Bagdonaite et al. 2013)Research Paper

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

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

9 thms2 active usersReviewed

Completed

Differential Geometry·Captain: Lucas

Maldacena 1999 II: near-horizon geometries of M5-, M2- and D1-D5-branesResearch Paper

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:

Section 3.1: $N$ coincident M5-branes, with limit $\mathrm{AdS}_7\times S^4$ ;
Section 3.2: $N$ coincident M2-branes, with limit $\mathrm{AdS}_4\times S^7$ ;
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:

M5 (eq. (3.1)): $A=f^{-1/3}$ , $B=f^{2/3}$ , $f=1+\pi Nl_p^3/r^3$ , $n=4$ ;
M2 (eq. (3.3)): $A=f^{-2/3}$ , $B=f^{1/3}$ , $f=1+2^5\pi^2Nl_p^6/r^6$ , $n=7$ ;
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'}$ :

M5: $R_{\rm AdS}=2(\pi N)^{1/3}$ , $R_{\rm sph}=(\pi N)^{1/3}=R_{\rm AdS}/2$ ;
M2: $R_{\rm AdS}=(2^5\pi^2N)^{1/6}/2$ , $R_{\rm sph}=(2^5\pi^2N)^{1/6}=2R_{\rm AdS}$ ;
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

7 thms2 active usersReviewed

Completed

Differential Geometry·Captain: Lucas

Maldacena 1999: the near-horizon geometry of D3-branes is AdS5 × S5Research Paper

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

(A.1)–(A.2) $\Phi_R(U,x)\in\mathrm{AdS}_{p+2}(R)$ for $U>0$ .
Appendix $\Phi_R$ is a bijection from $\{U>0\}$ onto $\{X\in\mathrm{AdS}_{p+2}(R): X_{-1}+X_{p+1}>0\}$ .
(A.3) the induced metric is $\frac{U^2}{R^2}dx^2+R^2\frac{dU^2}{U^2}$ .
Appendix every $A$ with $A^{\mathsf T}\eta A=\eta$ preserves $\mathrm{AdS}_{p+2}(R)$ .
(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}$ .
(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

8 thms2 active usersReviewed

Completed

Quantum Information·Captain: Lucas

Projective Measurements Are Equilibration Processes (finite dimension)Research Paper

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

15 thms2 active usersReviewed

Completed

Analysis·Captain: Lucas

Feynman 1948: The Path-Integral Wave Function Satisfies Schrödinger's EquationResearch Paper

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

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$ .
Eqs. (27)–(28), zero-order agreement: $(U_\varepsilon\psi)(x)\to\psi(x)$ ; this is the condition that fixes $A$ .
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$ .
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).

8 thms2 active usersReviewed

Completed

Captain: Lucas

Sen 1998: Tachyon condensation on the brane–antibrane systemResearch Paper

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)

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

12 thms2 active usersReviewed

Completed

Combinatorics·Captain: Lucas

't Hooft 1993: Dimensional Reduction in Quantum GravityResearch Paper

Motivation

In the 1993 essay Dimensional Reduction in Quantum Gravity (arXiv:gr-qc/9310026), G. 't Hooft argued that, once gravitational collapse is taken into account, the number of quantum states available to a region of space grows with the area of its boundary rather than with its volume. The essay is the origin of what is now called the holographic principle (developed further by Susskind, arXiv:hep-th/9409089). Besides the physical counting argument, the essay contains a small, fully precise mathematical model: a cellular automaton on the cubic lattice $\mathbb Z^3$ whose data on a one-dimensional line determine the data everywhere. This mission formalizes the quantitative estimates and the automaton statements of the essay.

Setting

Entropy estimates (eqs. (4)–(11)). In natural units, a region bounded by a sphere of radius $R$ has volume $V=\tfrac43\pi R^3$ and area $A=4\pi R^2$ . A thermal gas of $Z$ particle species at temperature $T$ has energy $E=C_1 Z V T^4$ and entropy $S=C_2 Z V T^3$ with positive constants $C_1,C_2$ . It stays outside its own Schwarzschild radius if $2E<R$ . A black hole of mass $M$ has entropy $4\pi M^2$ (eq. (1), additive constant dropped).

Plaquette automaton (eqs. (12)–(19)). Data $f:\mathbb Z^3\to\mathbb Z/p$ live on lattice sites. An elementary plaquette has lowest corner $x$ and is spanned by two of the unit vectors $e^1,e^2,e^3$ ; its corners in cyclic order are $x,\;x+u,\;x+u+v,\;x+v$ . On every plaquette a relation $g(f_1,f_2,f_3,f_4)=0$ is imposed such that any three entries determine the fourth uniquely. The relations may differ from plaquette to plaquette. On the unit cube with corners $A=0$ , $B=e^1$ , $D=e^2$ , $E=e^3$ , $C=e^1+e^2$ , $F=e^1+e^3$ , $H=e^2+e^3$ , $G=e^1+e^2+e^3$ , the six face relations are (12a–f). The staircase (eq. (14)) is the sequence

x(3n+1)=x(3n)+e^1,\qquad x(3n+2)=x(3n+1)-e^2,\qquad x(3n+3)=x(3n+2)+e^3,\qquad n\in\mathbb Z .

A family of face relations is consistent (eq. (16)) if every choice of $f(A),f(B),f(D),f(E)$ extends to data on the cube satisfying all six relations; equivalently, the three values of $f(G)$ produced by (12b), (12d), (12f) agree. Linear relations (eq. (17)) have the form $\sum_j a_j f_j+b \equiv 0 \pmod p$ , with every $a_j$ invertible mod $p$ .

Formalization targets

Goal: the staircase determines everything

For any family of plaquette relations with the three-determine-the-fourth property, two solutions on $\mathbb Z^3$ that agree on the staircase agree everywhere:

\Big(\forall n\in\mathbb Z:\ f(x(n))=f'(x(n))\Big)\ \Longrightarrow\ f=f' .

Milestones

Eqs. (4)–(8): $T<C_3Z^{-1/4}V^{-1/6}$ and $S<C_4Z^{1/4}V^{1/2}=C_5Z^{1/4}A^{3/4}$ for the thermal gas.
Eqs. (9)–(11): black holes that fit inside the sphere have total entropy $<A/4$ , and $A/4$ is the supremum.
Discussion of Fig. 1: on one cube, the data at $D,H,E,F$ determine all eight corners.
Eqs. (17)–(19): consistent linear relations with invertible coefficients exist for every modulus $p\ge 2$ .
Eqs. (14), (17): for the linear relation $f_1-f_2+f_3-f_4\equiv0$ , any data on the staircase extend uniquely to a global solution. The staircase data are then exactly the free degrees of freedom.

Significance

The goal is the essay's concrete mathematical example of dimensional reduction: in a $2+1$ -dimensional lattice model, a one-dimensional set of data carries all the information. Milestone 5 shows that the reduction is sharp in the linear case: no data beyond the staircase are needed, and none of the staircase data are constrained. Milestones 1–2 are the scaling estimates behind the area law $S_{\max}=A/4$ . The physical argument around them (black-hole thermodynamics, the Schwarzschild criterion) is taken as modelling input, not formalized. The results are stated in the essay but, as far as is known, have not been machine-checked.

Difficulty

The local step (one cube, Milestone 3) is elementary. The goal needs a global propagation argument. The staircase is a thin zig-zag line, and each application of a plaquette relation fixes only one new site. So the proof has to show that repeated local determination starting from the line eventually reaches every site of $\mathbb Z^3$ , in both directions along the line and in both transverse directions. Layer-by-layer propagation in $t=x_1+x_2+x_3$ does not apply directly, because the staircase is not a full layer.

Formalization scope

Sites are ℤ × ℤ × ℤ. Data take values in ZMod p for an arbitrary natural number $p$ ; the uniqueness statements hold for every $p$ . The three-determine-the-fourth property is stated with unique existence ( $\exists!$ ) for each slot, which matches "uniquely determined" in the essay. Relations may depend on the plaquette, so no translation invariance is assumed. Consistency (16) is encoded as extendability of the four free values on the unit cube. In Milestones 1–2 the region is a round sphere of radius $R$ , so $V$ and $A$ are expressions in $R$ , and the constants are existentially quantified before all physical variables. Contributions welcome: proofs of each milestone, and further faithful statements from the triangular-lattice model (eqs. (20a–f)).

Selected references

G. 't Hooft, Dimensional Reduction in Quantum Gravity, essay in honour of A. Salam, 1993. https://arxiv.org/abs/gr-qc/9310026
L. Susskind, The World as a Hologram, J. Math. Phys. 36 (1995) 6377. https://arxiv.org/abs/hep-th/9409089

7 thms2 active usersReviewed

Completed

Captain: Lucas

Akhmedov Neutrino Physics I: MSW Oscillations at Constant DensityTextbook

Motivation

Neutrinos produced by weak interactions are created in flavour eigenstates ( $\nu_e$ , $\nu_\mu$ , $\nu_\tau$ ), while they propagate as mass eigenstates. When the two bases differ, the flavour content of a neutrino beam oscillates with distance. In ordinary matter this picture is modified: electron neutrinos scatter coherently forward on electrons via the charged current, which adds an extra potential energy $V_{CC}=\sqrt2\,G_F N_e$ to the $\nu_e$ component only (Wolfenstein 1978). Mikheyev and Smirnov observed that this potential can resonantly enhance the mixing, so that an almost complete flavour conversion is possible even for a tiny vacuum mixing angle — the MSW effect. It is the accepted explanation of the energy dependence of the solar $\nu_e$ deficit and is relevant for neutrinos crossing the Earth and for supernova neutrinos.

This mission formalizes the constant-density result of Section 8.2 of E. Kh. Akhmedov's lecture notes Neutrino physics (hep-ph/0001264): the two-flavour transition probability in matter of constant density, eq. (95), together with the statements that lead to it and follow from it, eqs. (91)–(98).

Setting

Fix the vacuum parameters: the mass-squared difference $\Delta m^2 = m_2^2-m_1^2\in\mathbb R$ , the neutrino energy $E>0$ , and the vacuum mixing angle $\theta_0\in\mathbb R$ . The matter is described by the Fermi constant $G_F$ and the electron number density $N_e$ , through the charged-current potential (eq. (87))

V_{CC}=\sqrt2\,G_F N_e .

Write $a=\Delta m^2/(2E)$ . After discarding all terms proportional to the identity (common phases), the vector $\nu(t)=(\nu_e(t),\nu_\mu(t))\in\mathbb C^2$ of flavour amplitudes evolves by the Schrödinger equation $i\,\dot\nu = H\nu$ with the real symmetric MSW Hamiltonian (eq. (91))

H=\begin{pmatrix}-\tfrac a2\cos2\theta_0+V_{CC} & \tfrac a2\sin2\theta_0\\[2pt] \tfrac a2\sin2\theta_0 & \tfrac a2\cos2\theta_0\end{pmatrix}.

The derived quantities are the energy gap in matter (eq. (94)), the oscillation length in matter (eq. (96)) and the oscillation amplitude in matter (eq. (97)):

\Delta_m=\sqrt{(a\cos2\theta_0-V_{CC})^2+a^2\sin^22\theta_0},\qquad l_m=\frac{2\pi}{\Delta_m},\qquad \sin^22\theta=\frac{a^2\sin^22\theta_0}{(a\cos2\theta_0-V_{CC})^2+a^2\sin^22\theta_0}.

The vacuum oscillation length is $l_{osc}=4\pi E/\Delta m^2$ (eq. (61)). Distance and time are identified ( $L\simeq t$ , units with $c=1$ ).

Formalization targets

Goal — transition probability at constant density (eq. (95))

If $\nu$ solves $i\dot\nu=H\nu$ for all $t$ with $\nu(0)=(1,0)$ (a pure $\nu_e$ is produced at $t=0$ ), then for every $L$

|\nu_\mu(L)|^2=\sin^22\theta\;\sin^2\!\Big(\frac{\pi L}{l_m}\Big).

Milestones

Common phases are unobservable (Sec. 8.1, below eq. (89)). Adding $c\,\mathbf 1$ ( $c\in\mathbb R$ ) to a Hamiltonian changes a solution only by a phase; multiplying back by $e^{ict}$ gives a solution for the reduced Hamiltonian with the same component moduli.
Mixing angle in matter (eq. (93)). There is an angle $\theta$ with $\Delta_m\cos2\theta=a\cos2\theta_0-V_{CC}$ and $\Delta_m\sin2\theta=a\sin2\theta_0$ ; in particular $\tan2\theta=a\sin2\theta_0/(a\cos2\theta_0-V_{CC})$ whenever the denominator is non-zero.
Matter eigenstates and eigenenergy difference (eqs. (92), (94)). For such $\theta$ , $(\cos\theta,-\sin\theta)$ and $(\sin\theta,\cos\theta)$ are eigenvectors of $H$ with eigenvalues $(V_{CC}\mp\Delta_m)/2$ , whose difference is $\Delta_m$ .
Oscillation amplitude (eq. (97)). For such $\theta$ and $\Delta_m\neq0$ , $\sin^2 2\theta$ equals the explicit resonance expression above.
MSW resonance (eq. (98)). The amplitude never exceeds $1$ , and when $a\sin2\theta_0\ne0$ it equals $1$ exactly when $\sqrt2\,G_FN_e=\frac{\Delta m^2}{2E}\cos2\theta_0$ .
Vacuum limit (text below eq. (96)). For $N_e=0$ and $\Delta m^2\ne0$ : $\sin^22\theta=\sin^22\theta_0$ and $l_m=|l_{osc}|$ .

Significance

Eq. (95) shows that at constant density the flavour transition has exactly the vacuum form with $\theta_0,l_{osc}$ replaced by $\theta,l_m$ ; together with the resonance condition (98) it underlies quantitative discussions of matter effects, from the solar neutrino problem to long-baseline experiments crossing the Earth. The milestones separate the linear-algebra content (diagonalizing a real symmetric $2\times2$ matrix) from the analytic content (solving a linear constant-coefficient ODE and the uniqueness of its solution).

The result is textbook material and is proved in the source. This mission adds a machine-checked derivation from the Schrödinger equation itself — including uniqueness of the solution of the initial-value problem, which the source leaves implicit — and reusable Lean definitions for later missions on the adiabatic (variable-density) regime of Section 8.3.

Difficulty

The algebra of eqs. (93)–(97) is elementary. The substantive step for a formal proof is the passage from "the Hamiltonian is diagonalized by a rotation" to "every solution of the ODE with the given initial datum has the stated $\nu_\mu$ component": this needs a uniqueness theorem for linear ODEs on $\mathbb C^2$ (or an equivalent argument). Degenerate parameter values ( $\Delta_m=0$ , $a\sin2\theta_0=0$ ) must be handled, since the Lean statements do not exclude them.

Formalization scope

All parameters are real numbers; the state is a function $\nu:\mathbb R\to\mathbb C^{2}$ (index $0=\nu_e$ , $1=\nu_\mu$ ) assumed differentiable everywhere with derivative $-i\,H\nu(t)$ , where $H$ is the real matrix above viewed as a complex matrix. The probability is the squared modulus $|\nu_\mu(L)|^2$ . $E>0$ is assumed throughout; the sign of $\Delta m^2$ , the value of $\theta_0$ and the density are unrestricted. Lean's division convention ( $x/0=0$ ) applies to $l_m$ and $\sin^22\theta$ when $\Delta_m=0$ ; in that degenerate case $H$ is a multiple of the identity and both sides of the goal are $0$ .

A statement that assumed the closed-form solution, or assumed the probability formula as a hypothesis, would be trivial; the goal instead quantifies over every solution of the initial-value problem. Proofs of any milestone, and reusable lemmas on uniqueness for linear constant-coefficient ODEs, are welcome.

Selected references

E. Kh. Akhmedov, Neutrino physics, Trieste Summer School lectures, 1999. https://arxiv.org/abs/hep-ph/0001264
L. Wolfenstein, Neutrino oscillations in matter, Phys. Rev. D 17 (1978) 2369. https://doi.org/10.1103/PhysRevD.17.2369
S. P. Mikheyev, A. Yu. Smirnov, Resonance enhancement of oscillations in matter and solar neutrino spectroscopy, Sov. J. Nucl. Phys. 42 (1985) 913.

8 thms2 active usersReviewed

Completed

Linear algebra·Captain: Lucas

Davidson–Nardi–Nir 2008 (Leptogenesis), Eq. (5.10): upper bound on the flavoured CP asymmetry in N1 decaysResearch Paper

Motivation

Leptogenesis is a class of scenarios in which the baryon asymmetry of the Universe is produced from a lepton asymmetry generated in the out-of-equilibrium decays of heavy singlet neutrinos $N_k$ , which also give the light neutrinos their small masses through the type I seesaw (Fukugita–Yanagida 1986). The review of Davidson, Nardi and Nir (Phys. Rep. 466 (2008) 105) collects the standard results of the field. One of its central quantitative facts is an upper bound on the CP asymmetry in the decays of the lightest singlet $N_1$ , in terms of $M_1$ and the light-neutrino masses. This bound is the origin of the familiar lower bound $M_1\gtrsim10^9\,$ GeV for thermal leptogenesis with hierarchical singlets (Eq. (5.12) of the review).

Timeline. Casas and Ibarra introduced the orthogonal-matrix parametrization of the seesaw in 2001 (hep-ph/0103065). Davidson and Ibarra derived the bound $|\varepsilon|\le 3M_1(m_3-m_1)/(16\pi v^2)$ on the total asymmetry in 2002 (hep-ph/0202239); Hamaguchi, Murayama and Yanagida gave a related bound (hep-ph/0109030). Once flavour effects were recognised (around 2006), attention moved to the flavoured asymmetries $\varepsilon_{\alpha\alpha}$ , whose bound (Eq. (5.10) of the review) is the goal of this mission.

Setting

There are three lepton flavours $\alpha$ and three singlets $N_k$ with Majorana masses $M_k>0$ . We work in the mass basis of the charged leptons and of the $N_k$ . The Yukawa matrix $\lambda$ is an arbitrary complex $3\times3$ matrix, and $v=v_u>0$ is the Higgs vev. The light-neutrino mass matrix (Eq. (2.5)) is

[m]_{\alpha\beta}=\sum_k\lambda_{\alpha k}M_k^{-1}\lambda_{\beta k}v^2 ,

a complex symmetric matrix. It is diagonalized as $m=U^*D_mU^\dagger$ with $U$ unitary and $D_m=\operatorname{diag}(m_1,m_2,m_3)$ , $m_i\ge0$ (Eq. (2.6)). The largest and smallest light masses are $m_{\max}$ and $m_{\min}$ . The Casas–Ibarra matrix is $R=D_m^{-1/2}U^T\lambda D_M^{-1/2}v$ (Eq. (2.11)).

At tree level $N_1$ decays into $\phi\ell_\alpha$ and $\bar\phi\bar\ell_\alpha$ with partial rate $\Gamma_{\alpha\alpha}=|\lambda_{\alpha1}|^2M_1/(8\pi)$ and total rate $\Gamma_D=[\lambda^\dagger\lambda]_{11}M_1/(8\pi)$ (Eq. (4.5)). So the branching fractions satisfy $B_{\phi\ell_\alpha}+B_{\bar\phi\bar\ell_\alpha}=\Gamma_{\alpha\alpha}/\Gamma_D$ . For hierarchical singlets the flavoured CP asymmetry is (Eq. (5.9))

\varepsilon_{\alpha\alpha}=\frac{3M_1}{16\pi v^2[\lambda^\dagger\lambda]_{11}}\operatorname{Im}\{[\lambda]_{\alpha1}[m^*\lambda]_{\alpha1}\}.

Formalization targets

Goal — Eq. (5.10)

|\varepsilon_{\alpha\alpha}|\le\frac{3M_1m_{\max}}{16\pi v^2}\sqrt{B_{\phi\ell_\alpha}+B_{\bar\phi\bar\ell_\alpha}}\qquad\text{for every flavour }\alpha.

Milestones

Eq. (2.6): the matrix $m$ admits a diagonalization $m=U^*D_mU^\dagger$ with $U$ unitary and $m_i\ge0$ .
Eq. (2.11): for $m_i>0$ , $R$ is complex orthogonal, $R^TR=RR^T=1$ .
Sec. 5.2: $|m\cdot x^*|\le m_{\max}|x|$ for all $x\in\mathbb C^3$ .
Sec. 5.2 / Eq. (5.17): the total asymmetry bound $|\sum_\alpha\varepsilon_{\alpha\alpha}|\le 3M_1(m_{\max}-m_{\min})/(16\pi v^2)$ .

Significance

Eq. (5.10) is the input to the lower bounds on $M_1$ and on the reheat temperature for hierarchical thermal leptogenesis (Eq. (5.12), Sec. 9.4.3), and it shows that flavoured asymmetries are not suppressed for degenerate light neutrinos, unlike the total one (Eq. (5.17)). These are established results. The work here is to formalize them: to state the seesaw quantities precisely and machine-check the linear-algebra steps (Takagi factorization, complex orthogonality, operator-norm bounds) that the physics literature takes for granted. To the captain's knowledge none of these statements has a machine-checked proof.

Difficulty

The goal reduces to an operator-norm estimate for the complex symmetric matrix $m$ . That estimate needs the diagonalization $m=U^*D_mU^\dagger$ , which is a Takagi (Autonne–Takagi) factorization, not a unitary eigen-decomposition: $m$ is symmetric, not Hermitian. The obvious move, applying the spectral theorem to $m$ , fails because $m$ is in general not normal. The milestone-1 existence statement therefore needs its own argument, for example through the Hermitian matrix $m^\dagger m$ . The total-asymmetry bound (milestone 4) needs a finer argument than the triangle inequality to produce the difference $m_{\max}-m_{\min}$ rather than $m_{\max}$ .

Formalization scope

Everything is $3\times3$ over $\mathbb C$ with index set $\{0,1,2\}$ (Fin 3); the singlet " $N_1$ " is index $0$ .
$m_{\max}$ and $m_{\min}$ are ⨆ i, masses i and ⨅ i, masses i over the three diagonal entries. No ordering of the $m_i$ is imposed.
The diagonalization is a hypothesis IsLightMassDiagonalization m U masses (unitary $U$ , $m_i\ge0$ , $m=\overline U\,\mathrm{diag}(m_i)\,U^\dagger$ ). It is always satisfiable by milestone 1, so it is not vacuous.
$\varepsilon_{\alpha\alpha}$ is the explicit hierarchical-limit expression (5.9), with $[\lambda^\dagger\lambda]_{11}$ written as $\sum_\beta|\lambda_{\beta1}|^2$ . The physical approximation $M_{2,3}\gg M_1$ is built into this formula and is not a hypothesis. The branching sum is the tree-level ratio $\Gamma_{\alpha\alpha}/\Gamma_D$ .
Division by zero returns $0$ in Lean. This only matters when the first column of $\lambda$ vanishes, where both sides of the goal are $0$ .
Needed infrastructure: Takagi factorization of complex symmetric matrices (reusable beyond this mission), and elementary Euclidean-norm estimates on $\mathbb C^3$ .

Selected references

S. Davidson, E. Nardi, Y. Nir, Leptogenesis, Physics Reports 466 (2008) 105–177. https://doi.org/10.1016/j.physrep.2008.06.002 · https://arxiv.org/abs/0802.2962
J. A. Casas, A. Ibarra, Oscillating neutrinos and μ → e γ, Nucl. Phys. B 618 (2001) 171. https://arxiv.org/abs/hep-ph/0103065
S. Davidson, A. Ibarra, A lower bound on the right-handed neutrino mass from leptogenesis, Phys. Lett. B 535 (2002) 25. https://arxiv.org/abs/hep-ph/0202239
M. Fukugita, T. Yanagida, Baryogenesis without grand unification, Phys. Lett. B 174 (1986) 45. https://doi.org/10.1016/0370-2693(86)91126-3

6 thms2 active usersReviewed

Completed

Captain: Lucas

Thorn 1991: String Bits and the 1/N Expansion — Discretized-String SpectrumResearch Paper

Motivation

In the note Reformulating String Theory with the 1/N Expansion (arXiv:hep-th/9405069), C. B. Thorn argues that stability and causality, which are manifest in quantum field theory but obscure in string theory, would become evident if strings were composite objects built from point-like constituents ("string bits"). The proposal combines the light-cone parametrization of the string with 't Hooft's $1/N$ expansion (G. 't Hooft, Nucl. Phys. B72 (1974) 461): bits are created by the entries of an $N\times N$ matrix field $\bar a(x)$ , closed strings by the singlet traces $\mathrm{tr}\{\bar a(x_1)\cdots\bar a(x_M)\}$ , and $1/N$ plays the role of the string coupling.

A load-bearing step of the proposal is that a long closed chain of $M$ bits behaves like a continuous string: in the continuum limit $M\to\infty$ with $P^+=M\epsilon T_0$ fixed, the finite-energy excitations must be string excitations. Thorn justifies this with the remark (p. 5) that "the low energy excitations of an $M$ particle discretized string are $O(1/M)\times$ the two-body level spacing". This mission formalizes that remark for the harmonic Hamiltonian written in the paper, together with the cyclic symmetry that ties the matrix traces to closed strings.

Setting

A discretized light-cone string with $M$ bits is described by transverse positions $x_1,\dots,x_M$ with cyclic identification $x_{M+1}=x_1$ and Hamiltonian (p. 4)

P^- = \frac1\epsilon\sum_{i=1}^{M}\frac{1}{2T_0}\Bigl(-\nabla_i^2 + T_0^2\,(x_{i+1}-x_i)^2\Bigr).

The potential term is the quadratic form of the cyclic Laplacian $L_M$ , $(L_Mx)_i=2x_i-x_{i+1}-x_{i-1}$ (indices mod $M$ ), and the equations of motion are $\ddot x=-\epsilon^{-2}L_Mx$ . A normal-mode frequency is an $\omega>0$ with $\epsilon^2\omega^2$ an eigenvalue of $L_M$ ; write $\Omega_{M,\epsilon}$ for the set of them. With $\hbar=1$ these are the excitation-level spacings of the chain.

The singlet creation operators are $\bar A(x_1,\dots,x_M)=(1/N)^{M/2}\mathrm{tr}\{\bar a(x_1)\cdots\bar a(x_M)\}$ ; since the $\bar a_{k\ell}$ commute with each other, cyclic invariance of the trace gives the cyclic symmetry $\psi_M(x_1,\dots,x_M)=\psi_M(x_2,\dots,x_M,x_1)$ of the string wave function.

Formalization targets

Goal

For all $M\ge2$ and $\epsilon>0$ ,

\min\Omega_{M,\epsilon}=\frac2\epsilon\sin\frac\pi M,\qquad \min\Omega_{2,\epsilon}=\frac2\epsilon,\qquad \min\Omega_{M,\epsilon}\le\frac\pi M\,\min\Omega_{2,\epsilon}.

Milestones

Cyclic symmetry: $\mathrm{tr}(a_0a_1\cdots a_M)=\mathrm{tr}(a_1\cdots a_Ma_0)$ for matrices over a commutative ring.
The bond potential is a quadratic form: $\sum_i(x_{i+1}-x_i)^2=x^{\mathsf T}L_Mx$ .
Each $4\sin^2(\pi k/M)$ is an eigenvalue of $L_M$ ( $M\ge1$ ).
Every eigenvalue of $L_M$ is $4\sin^2(\pi k/M)$ for some $0\le k<M$ .

Significance

The goal is the quantitative content of the paper's continuum-limit argument in the harmonic case: the gap of an $M$ -bit chain closes like $1/M$ relative to the two-body scale, so at fixed $P^+$ the low-lying spectrum approaches the equally spaced string spectrum. The same spectral facts about the cyclic Laplacian (the spectrum of the cycle graph) are used in lattice field theory and spectral graph theory, so the milestones are reusable outside this mission. The results are classical; the work here is their machine-checked formalization in a form tied to the string-bit Hamiltonian.

Difficulty

The trace and quadratic-form statements are finite algebra. The substance lies in the spectrum: exhibiting real eigenvectors for every $k$ needs trigonometric sum identities, and the completeness statement needs an argument that no other eigenvalues exist, which must handle the degenerate pairs $k\leftrightarrow M-k$ . Identifying the least positive value then requires the symmetry $\sin(\pi k/M)=\sin(\pi(M-k)/M)$ and monotonicity of $\sin$ on $[0,\pi/2]$ .

Formalization scope

$L_M$ is a real matrix indexed by $\mathrm{Fin}\,M$ ; eigenvalues are those of the real linear map $x\mapsto L_Mx$ (nonzero real eigenvector).
One transverse dimension is used; with $d-2$ transverse dimensions the modes decouple and the frequency set is the same. The tension $T_0$ drops out of the frequencies.
"Two-body level spacing" is formalized as the lowest frequency of the $M=2$ member of the same cyclic family. The paper's claim for a general attractive potential $V$ (and the quantum field theory, the $1/N$ expansion itself, and the postscript remarks) is outside the scope.
Edge cases: the goal assumes $M\ge2$ and $\epsilon>0$ , so $\Omega_{M,\epsilon}$ is nonempty and its minimum is attained; the definition of $\Omega$ requires $\omega>0$ , which excludes the zero mode.

Selected references

C. B. Thorn, Reformulating String Theory with the 1/N Expansion, invited talk, First Int. A. D. Sakharov Conference (1991); arXiv:hep-th/9405069 (1994). https://arxiv.org/abs/hep-th/9405069
G. 't Hooft, A planar diagram theory for strong interactions, Nucl. Phys. B72 (1974) 461.

6 thms2 active usersReviewed

Completed

Probability·Captain: Lucas

Douglas 2003: Statistics of String Vacua — Flux Counting and Gaussian EnsemblesResearch Paper

Motivation

String/M theory appears to admit a very large number of four-dimensional vacua, and M. R. Douglas's 2003 paper The statistics of string/M theory vacua proposes to study them statistically: instead of constructing vacua one at a time, one places a measure on a space of effective theories and computes expected numbers and distributions of vacua. Two concrete mathematical ingredients of that programme are the subject of this mission.

The first is the Bousso–Polchinski counting of flux vacua (Section 3.6 of the paper, following Bousso–Polchinski 2000). Quantized fluxes form an integer vector $N\in\mathbb Z^J$ , and the flux energy is a positive quadratic form in $N$ . The number of flux choices with energy below $V$ controls whether a small cosmological constant can be realised; the paper evaluates the number distribution (3.13) by replacing the lattice sum with an integral, obtaining a density proportional to $V^{J/2-1}\,dV$ .

The second is the Gaussian ensemble of superpotentials (Section 4 and 4.1): a random polynomial superpotential whose coefficients are independent complex Gaussians, with an explicit normalising constant and an explicit count of coefficients.

Setting

Fix an integer $J\ge 0$ (the number of independent flux quanta, $J=b_{p+1}$ in the paper) and a constant $c>0$ (in the paper $c=M_{pl}^2/(M^{2p}V_{p+1}^2)$ ). For a flux vector $N=(N_1,\dots,N_J)\in\mathbb Z^J$ the flux potential is

V(N)=c\sum_{i=1}^J N_i^2 ,

and the flux vacua count below level $V$ is

\mathcal N_J(c,V)=\#\{N\in\mathbb Z^J : V(N)\le V\}.

This is the cumulative distribution function of the measure $d\mu(V)=\sum_N\delta(V-V(N))$ of eq. (3.13). The unit ball in $\mathbb R^J$ has volume $\omega_J=\pi^{J/2}/\Gamma(J/2+1)$ , and the unit sphere has area $\mathrm{Vol}(S^{J-1})=2\pi^{J/2}/\Gamma(J/2)=J\omega_J$ .

For the superpotential ensemble, a polynomial in $n$ variables of degree at most $d$ has one coefficient per monomial $z^{I}=z_1^{I_1}\cdots z_n^{I_n}$ with $|I|\le d$ ; the paper states there are $c(d,n)=(d+n)!/(d!\,n!)$ of them. The coefficients $w_I\in\mathbb C$ are given the weight $(\alpha/\pi)^{c(d,n)}\prod_I d^2w_I\,e^{-\alpha|w_I|^2}$ , $\alpha>0$ , which the paper says is unit normalised.

Formalization targets

Goal: asymptotic count of flux vacua

\lim_{V\to\infty}\frac{\mathcal N_J(c,V)}{(V/c)^{J/2}}=\frac{\pi^{J/2}}{\Gamma(J/2+1)} .

This is the precise, integrated form of the approximation in (3.13): integrating $\tfrac12\mathrm{Vol}(S^{J-1})\,c^{-J/2}v^{J/2-1}$ from $0$ to $V$ gives exactly $\omega_J (V/c)^{J/2}$ .

Milestones

Finiteness: for every $V$ , only finitely many $N\in\mathbb Z^J$ satisfy $V(N)\le V$ (so $\mathcal N_J$ is a genuine count).
Continuum volume: the Lebesgue volume of $\{x\in\mathbb R^J : c\sum x_i^2\le V\}$ equals $\omega_J (V/c)^{J/2}$ for $V\ge 0$ .
Continuum density (3.13): for $0\le V_1\le V_2$ and $J\ge1$ , the volume of the shell $\{V_1<c\sum x_i^2\le V_2\}$ equals $\int_{V_1}^{V_2}\tfrac12\mathrm{Vol}(S^{J-1})\,c^{-J/2}\,v^{J/2-1}\,dv$ .
Coefficient count: $\#\{I\in\mathbb N^n : |I|\le d\}=\#\{I\in\mathbb N^{n+1} : |I|=d\}=(d+n)!/(d!\,n!)$ .
Normalisation of the complex Gaussian ensemble: $\int_{\mathbb C^m}(\alpha/\pi)^m e^{-\alpha\sum_I|w_I|^2}\,d^{2m}w=1$ for every $m$ and $\alpha>0$ .

Significance

The goal makes rigorous the step "replace the sum with an integral" that underlies the Bousso–Polchinski estimate of how many flux vacua lie below a given energy, with the exact constant appearing in (3.13). Milestones 4 and 5 certify the combinatorial and analytic constants of the Gaussian ensemble (4.6) on which the paper's densities (4.7)–(4.10) are built. None of these results is new mathematics: the goal is the $J$ -dimensional analogue of the Gauss circle problem at leading order, and the milestones are classical. What the mission adds is a machine-checked version of the precise constants used in the paper.

Difficulty

The goal requires comparing a lattice-point count with a volume. The naive bound, counting unit cubes centred at lattice points, must be controlled uniformly: cubes meeting the boundary of the ball contribute an error of order $R^{J-1}$ with $R=\sqrt{V/c}$ , and one has to show that this is $o(R^J)$ . The volume formula for Euclidean balls expressed through the Gamma function, and its transport to the product space $\mathbb R^J$ with the sum-of-squares form, is further required infrastructure.

Formalization scope

Flux vectors are functions Fin J → ℤ; the count uses Set.ncard, whose value on an infinite set would be $0$ — milestone 1 rules out that degenerate reading.
Continuum statements use the product Lebesgue measure on Fin J → ℝ (not EuclideanSpace), with the quadratic form $c\sum x_i^2$ written out explicitly.
The Gaussian ensemble is formalised only for complex coefficients (the "GUE" case). For real coefficients the paper's constant $(\alpha/\pi)^{c(d,n)}$ would not normalise the measure (the correct constant is $(\alpha/\pi)^{c(d,n)/2}$ ), so the real case is deliberately omitted.
The paper's finiteness conjecture (3.16) for full string compactifications, and the densities (4.7)–(4.10), are not formalised; they are not stated precisely enough in the source.
Definitions: DouglasVacua.fluxPotential, DouglasVacua.fluxVacuaCount.

Selected references

M. R. Douglas, The statistics of string/M theory vacua, JHEP 05 (2003) 046. https://doi.org/10.1088/1126-6708/2003/05/046 — arXiv:hep-th/0303194
R. Bousso, J. Polchinski, Quantization of four-form fluxes and dynamical neutralization of the cosmological constant, JHEP 06 (2000) 006. https://arxiv.org/abs/hep-th/0004134

7 thms2 active usersReviewed

Completed

Analysis·Captain: Lucas

Gambini–Pullin 2014, Appendix A: nonlocal weights make the Lorentz-violating model integral smallResearch Paper

Motivation

Gambini and Pullin (IJMPD 23 (2014) 1442023) study quantum fields living on the discrete quantum spacetimes of spherically symmetric loop quantum gravity. Discreteness makes the field equations lattice-like and hence breaks Lorentz invariance. Collins, Perez, Sudarsky, Urrutia and Vucetich (PRL 93 (2004) 191301) argued that in interacting theories such Planck-scale violations feed, through renormalized loop diagrams, into large low-energy violations: a difference of second derivatives of the self-energy that should vanish by Lorentz invariance stays bounded away from zero. Gambini and Pullin argue that two exponential weights — a Gaussian fuzziness factor from the spread of the ADM mass, and a Lorentz-invariant nonlocal interaction factor of the type found in string field theory — make this quantity arbitrarily small.

Because the full self-energy calculation is lengthy, the paper's Appendix A replaces it by a two-dimensional model integral in which rotations play the role of Lorentz transformations and a parameter $\sigma$ plays the role of lattice spacing. This mission formalizes the precise mathematical claims made about that model.

Setting

For real parameters $\sigma \ge 0$ define the denominator base and the model integrand

D_\sigma(x,y) = 1 + x^2 + \frac{y^2}{1+\sigma y^2}, \qquad f_\sigma(x,y) = \frac{x^2-y^2}{D_\sigma(x,y)^2}.

The paper's integral (A.1) is $I = \int_{\mathbb R^2} f_\sigma(x,y)\,dx\,dy$ . For $\sigma = 0$ one has $D_0 = 1 + x^2 + y^2$ , which is rotation invariant.

(A.1) is only a formal expression: $f_\sigma$ is not Lebesgue integrable on $\mathbb R^2$ (for $\sigma = 0$ it decays like $r^{-2}$ ; for $\sigma > 0$ it grows like $-y^2$ along the $y$ -axis). The mission therefore uses the disk-truncated integral

I^{\mathrm{disk}}_\sigma(R) = \int_{x^2+y^2 \le R^2} f_\sigma(x,y)\,dx\,dy,

which regularizes (A.1) in a rotation-invariant way.

The weighted model integral (A.2) is, for weights $\alpha, \beta$ ,

I(\alpha,\beta,\sigma) = \int_{\mathbb R^2} e^{-\alpha x^2}\, e^{-\beta(x^2+y^2)}\, f_\sigma(x,y)\,dx\,dy .

The first factor models the fuzziness (it acts on one direction only), and the second models the nonlocal interaction (rotation invariant here, Lorentz invariant in the physical case).

Formalization targets

Goal (Appendix A, sentence after (A.2))

"With suitable choices of $\alpha$ and $\beta$ one can make the integral as small as desired":

\forall \sigma > 0,\ \forall \varepsilon > 0,\ \exists \alpha > 0,\ \exists \beta > 0:\quad |I(\alpha,\beta,\sigma)| < \varepsilon .

Milestones

For $\sigma = 0$ the integral vanishes: $I^{\mathrm{disk}}_0(R) = 0$ for every $R$ .
For $\sigma > 0$ it "does not vanish by a significant amount": $I^{\mathrm{disk}}_\sigma(R) \to -\infty$ as $R \to \infty$ .
(A.2) is well defined: the weighted integrand is integrable for $\alpha \ge 0$ , $\beta > 0$ , $\sigma \ge 0$ .
With only the rotation-invariant weight and $\sigma = 0$ , (A.2) still vanishes: $I(0,\beta,0) = 0$ for $\beta > 0$ .
In the regime $\alpha \sim \beta$ large: $I(\beta,\beta,\sigma) \to 0$ as $\beta \to \infty$ , for each $\sigma > 0$ .

Significance

In the paper this model is the only precisely stated mathematical content backing the claim that the two exponential weights restore approximate Lorentz invariance. Formalizing it pins down exactly which statements hold (and in what sense the formal integral (A.1) "vanishes" or "does not vanish"), separating the rigorous content of the toy model from the physical argument it illustrates. The results are elementary real analysis; no machine-checked proofs of them are known to exist.

Difficulty

The main difficulty is that the unweighted integral (A.1) diverges, so both "vanishes" and "does not vanish" need a regularization. The weighted statements need integrability and dominated-convergence estimates on $\mathbb R^2$ and a change of variables (swapping $x$ and $y$ ) for the symmetry claims. The divergence to $-\infty$ in milestone 2 needs separate upper and lower estimates for the positive and negative parts of $f_\sigma$ on growing disks.

Formalization scope

All objects are real-valued functions on $\mathbb R \times \mathbb R$ with Lebesgue (product) measure. $I(\alpha,\beta,\sigma)$ is a Bochner integral over the whole plane; where the integrand is not integrable, the Lean integral is $0$ by convention, which is why milestone 3 is included and all weighted statements assume $\beta > 0$ . The disk is the closed Euclidean disk $\{x^2+y^2 \le R^2\}$ , not a sup-norm ball. The parameter $\sigma$ is restricted to $\sigma \ge 0$ (or $\sigma > 0$ ) wherever it matters, so that $1+\sigma y^2 > 0$ . The sentence in the paper "more precisely one needs $\alpha \sim \beta$ and both larger than $\sigma$ " is heuristic; only its sufficiency direction along $\alpha = \beta$ is formalized (milestone 5). No necessity claim is formalized, because a large $\beta$ alone already makes $I$ small.

Selected references

R. Gambini, J. Pullin, Emergence of stringlike physics from Lorentz invariance in loop quantum gravity, Int. J. Mod. Phys. D 23 (2014) 1442023. https://doi.org/10.1142/S0218271814420231
J. Collins, A. Perez, D. Sudarsky, L. Urrutia, H. Vucetich, Lorentz invariance and quantum gravity: an additional fine-tuning problem?, Phys. Rev. Lett. 93 (2004) 191301. https://doi.org/10.1103/PhysRevLett.93.191301

7 thms2 active usersReviewed

Completed

Probability·Captain: marwahaha

Full support of the zero-temperature Sherrington-Kirkpatrick order parameterOpen Problem

Motivation

A hierarchy of infinitely many overlap scales need not fill an interval. Full support asks whether an admissible zero-temperature SK minimizer leaves any gap below overlap one. The pinned manuscript supplies the research context.

Setting

An order parameter is a nonnegative, monotone, right-continuous integrable function on [0,1). The Parisi value is defined by a Brownian stochastic-control supremum. The Stieltjes measure μ lives on the subtype Time=[0,1); its support below is taken in that relative topology.

Formalization target

The selected goal is OAI.ZeroTemperatureSK.full_support. Its central assertion is

\operatorname{supp}\mu=[0,1),\qquad \mathbb E[u_x(t,X_t)^2]=t,\quad\mathbb E[u_{xx}(t,X_t)^2]=1.

The theorem states that, for any probability space carrying a real Brownian motion B (a BrownianSystem W) and any order parameter γ on [0,1), if γ minimizes the Parisi functional over all order parameters, then a five-part full-support conclusion holds. An order parameter γ:[0,1)→ℝ is nonnegative, monotone, right-continuous and integrable (extended by zero outside [0,1)). For a time t and position x, the value is the supremum, over controls α progressive for the filtration generated by the Brownian increments after t and bounded by 1 in absolute value, of the expected payoff |x + B₁ − B_t + ∫_t^1 γ(s)α(s−t)ds| − ½∫_t^1 γ(s)α(s−t)²ds. The gradient and curvature are its first and second derivatives in x, and the Parisi functional is value at (0,0) minus ½∫_0^1 tγ(t)dt. Being a minimizer means the functional at γ is at most its value at every order parameter η. The conclusion says: (1) there is a measure μ on [0,1) with μ((−∞,t]) = γ(t) for every t in [0,1); (2) there is a diffusion X, a process progressive for the Brownian filtration that almost surely is continuous on [0,1], starts at 0, and satisfies X_t = B_t + ∫_0^t γ(s)·gradient(s,X_s)ds; (3) every such measure μ has full support, equal to all of [0,1); (4) γ is strictly increasing, γ(a)<γ(b) whenever a<b; and (5) for every such diffusion X and every t in [0,1), the expected square of the gradient at X_t equals t, and the expected square of the curvature at X_t equals 1.

Significance and status

The main target is the five-part full-support conclusion for every encoded minimizer and Brownian system. The separate value-consequences bundle is retained as an additional formal target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The conclusion couples support, strict increase, diffusion existence and derivative identities. Minimization alone is not an assumption of those conclusions.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

OAI.SKValue.value_consequences (Open).

Selected references

OpenAI, Full support of the zero-temperature Sherrington-Kirkpatrick order parameter, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

6 thms2 active usersReviewed

Completed

Probability·Captain: marwahaha

Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive DisorderOpen Problem

Motivation

Random site energies change the spectral behavior of a lattice Schrödinger operator. Identifying its almost-sure spectrum is one part of the planar Anderson problem. The pinned manuscript supplies the research context.

Setting

The lattice is the integer plane. A state is a square-summable complex function on its sites, and the potential at each site is independently uniform on the interval from −h to h, with h positive.

Formalization target

The selected goal is OAI.PlanarAnderson.anderson_spectrum_ae. Its central assertion is

\sigma(H_v)=[-4-h,4+h].

The theorem states that for every real h>0, for almost every disorder configuration v under disorderLaw(h), there exists a bounded complex-linear operator H on the Hilbert space ℓ²(ℤ², ℂ) of square-summable complex functions on the planar lattice ℤ×ℤ such that H is an Anderson operator for v, H is self-adjoint, and the spectrum of H in ℂ equals the real interval [-4-h, 4+h] (embedded in ℂ as the points with imaginary part 0). Here a configuration is a real-valued function v on lattice sites, and disorderLaw(h) is the infinite product measure over sites of the uniform distribution (Lebesgue measure conditioned on the interval) on [-h,h], so the potential values are independent. H is an Anderson operator for v when, for every u in ℓ² and every site x=(a,b), (Hu)(a,b) = u(a+1,b)+u(a-1,b)+u(a,b+1)+u(a,b-1)+v(a,b)u(a,b), the sum of the four nearest-neighbour values plus the local potential times u at x. The statement is recorded as an admitted theorem.

Significance and status

The selected goal asserts existence, self-adjointness and the spectrum interval. Pure-point spectral type, a complete eigenbasis and dynamical localization are not conclusions of this published target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The interval must be identified almost surely for an infinite random operator, including both exclusion of spectrum outside the interval and inclusion of its interior.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

OpenAI, Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

2 thms2 active usersReviewed

Completed

Probability·Captain: marwahaha

Buffered comparison and stopping-band resolution in critical IsingOpen Problem

Motivation

Conditioning on an explored Ising interface fixes many spins and can create alternating signs. The source develops comparison estimates that remain valid with arbitrary common pinned spins. The source is OpenAI's September 2026 manuscript.

Setting

A ferromagnetic Ising law weights sign configurations by the exponential of nonnegative pair couplings plus real external fields. Two probability mixtures prescribe source spins on $J$ , while the same spins are pinned on $F$ and a target event is prescribed on $I$ .

Formalization targets

e^{-4\operatorname{artanh}q_0}\le\frac{\mu_{\mathrm{mix}}(\sigma_I=a\mid\sigma_F=\tau)}{\mu_{\mathrm{mix}'}(\\sigma_I=a\\mid\\sigma_F=\\tau)}\\le e^{4\\operatorname{artanh}q_0}.

A comparison bound for a ferromagnetic Ising model on a finite graph with n vertices and m separately indexed edges (parallel edges allowed, no loops, nonnegative couplings K_e) and an arbitrary real external field h. A configuration σ has energy equal to the sum over edges of K_e σ_u σ_v plus the sum over vertices of h_v σ_v, with spins ±1, and weight exp(energy). Take pairwise disjoint vertex sets I, J, F, and kept vertices i ∈ I and j ∈ J that lie outside F. Fix spin configurations a and τ. For a configuration b, the conditional probability of σ_I = a given σ_J = b and σ_F = τ is the ratio of the total weight of configurations satisfying all three agreements to the total weight of those agreeing with b on J and τ on F. For any two probability mixtures mix and mix' on configurations (nonnegative weights summing to 1), the mixture probability is the mix-weighted average of these conditional probabilities over b; only the restriction of b to J matters. Let q be the terminal connection probability in the zero-field random-cluster (FK) model with q=2 on the graph with F deleted (not pinned): edges e are open with probability 1-exp(-2K_e), the vertices of I are identified together and those of J are identified together, and q is the probability that i and j lie in the same cluster. Then the ratio of the mixture probability under mix to that under mix' lies between exp(-4 artanh q) and exp(4 artanh q), for every such pair of mixtures, uniformly in h, a and τ. The theorem is stated with its proof admitted (sorry).

The goal is OAI.BufferedIsing.finite_graph_comparison.

Significance

The estimate controls likelihood ratios uniformly over mixtures, fields, and common signs. It is the finite-graph comparison component of the manuscript. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Pinning a vertex changes neighboring fields; deleting it does something different. The comparison probability must come from the graph with the common pins deleted, with each terminal class contracted separately.

Formalization scope

The graph is finite with indexed edges, allowing parallel edges and excluding loops before contraction. The sets $I,J,F$ are pairwise disjoint and each terminal class contains a supplied vertex. The zero-field random-cluster weight has cluster parameter two. The stopping-band approximation theorem is not an attached target.

The shared definitions are supplied by BufferedIsing. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

OpenAI, Buffered comparison and stopping-band resolution in critical Ising, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

28 thms2 active usersReviewed

Analysis Partial Differential Equations·Captain: wurtle

Nonuniqueness for the periodic hard-sphere Boltzmann equationResearch Paper

Motivation: uniqueness of weak Boltzmann solutions

The Boltzmann equation describes a dilute gas through a density $F(t,x,v)$ of particles at position $x$ with velocity $v$ , evolving by free transport and binary collisions. For hard spheres, the collision rate is proportional to the normal relative speed. In 1989 DiPerna and Lions constructed global renormalized solutions for all initial data with finite mass, energy and entropy, and weak stability holds at the same level. Existence and stability do not give uniqueness, though: the physical bounds do not even make the quadratic collision term locally integrable, and the uniqueness of general renormalized solutions is a basic question in kinetic theory (Silvestre 2022, §2). Uniqueness is known only under much stronger assumptions, such as Maxwellian upper bounds or closeness to equilibrium.

Timeline

1974 — Ukai: global existence and uniqueness near a Maxwellian for periodic cutoff hard potentials (Proc. Japan Acad. 1974).
1978 — Kaniel and Shinbrot: uniqueness and local existence under Maxwellian upper bounds (CMP 1978).
1988 — Golse, Lions, Perthame and Sentis: velocity averaging lemmas (JFA 1988).
1989 — DiPerna and Lions: global renormalized solutions and weak stability (Ann. of Math. 1989); the entropy inequality follows in 1991 (ARMA 1991).
1999 — For the spatially homogeneous hard-sphere equation, Mischler and Wennberg prove uniqueness among conservative solutions with finite mass and energy (Ann. IHP C 1999); Wennberg gives homogeneous nonuniqueness examples in which the energy increases (J. Stat. Phys. 1999).
2010 — Levermore and Masmoudi give a periodic formulation of renormalized solutions relative to a Maxwellian (ARMA 2010).
2024–2026 — Ill-posedness results: Chen–Holmer for the constant kernel (Ann. PDE 2024), Chen–Guo–Shen–Zhang for hard spheres in Gaussian-weighted $L^2_vH^s_x$ (arXiv:2606.01331). Gismondi, Golding and Novack conjecture nonuniqueness of renormalized inhomogeneous Landau and Boltzmann solutions for a dense class of data (arXiv:2608.13758).
2026 — An OpenAI preprint, Nonuniqueness for the periodic hard-sphere Boltzmann equation (OpenAI Math Release, September 23, 2026), claims a single finite-entropy datum on $\mathbb T^3\times\mathbb R^3$ with two distinct admissible solutions. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Phase space is $\Omega=\mathbb T^3_x\times\mathbb R^3_v$ , with $\mathbb T^3=\mathbb R^3/\mathbb Z^3$ . For incoming velocities $v,v_*$ and a collision normal $\omega\in S^2$ , put $a=(v-v_*)\cdot\omega$ , $v'=v-a\omega$ , $v_*'=v_*+a\omega$ . The hard-sphere collision operator is

Q(F,F)(v)=\int_{\mathbb R^3\times S^2}|a|\,\big(F(v')F(v_*')-F(v)F(v_*)\big)\,dv_*\,d\omega ,

with ordinary surface measure on $S^2$ ; the two terms are the gain and the loss. The Cauchy problem is $(\partial_t+v\cdot\nabla_x)F=Q(F,F)$ , $F(0)=F_0$ . An initial datum has finite entropy if it is nonnegative and $\int_\Omega F_0(1+|v|^2+|\log F_0|)<\infty$ .

A solution is admissible (Definition 2.1 of the source) if, with $M(v)=(2\pi)^{-3/2}e^{-|v|^2/2}$ :

it is renormalized: the equation holds weakly for $M\beta(F/M)$ for every $C^1$ $\beta$ with $\beta(0)=0$ and $|\beta'(z)|\le C_\beta/(1+z)$ , and the separately renormalized gain and loss are integrable on bounded time intervals;
it is weakly continuous in $L^1$ against every bounded measurable test and takes the initial value $F_0$ ;
mass, energy and absolute entropy stay bounded on bounded time intervals;
it conserves local mass and total momentum, and satisfies the energy inequality and the relative-entropy inequality with the full entropy dissipation at every time.

Formalization targets

Goal: two admissible solutions from one datum (Theorem 1.1)

There is a nonnegative finite-entropy datum $F_0$ with bounded velocity support, two admissible global solutions $F,G$ with initial datum $F_0$ , and a time $T>0$ such that

F,G\in C([0,T];L^1(\Omega)),\qquad Q^\pm(F),\,Q^\pm(G)\in L^1([0,T]\times\Omega),\qquad F(t)\neq G(t)\ \text{in } L^1 \text{ for some } t\in[0,T].

This is Theorem 1.1 of the source (p. 3), with the difference placed in the common interval of strong continuity, which is where the source establishes it. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If the source's proof is correct, the theorem shows that the DiPerna–Lions framework, even with local mass conservation, momentum conservation and the energy and entropy inequalities retained, does not determine the evolution uniquely. The example is spatially inhomogeneous and periodic, and the two solutions start from exactly the same datum, unlike ill-posedness results that compare nearby data. On the interval where they differ, both solutions satisfy the unrenormalized equation. The datum has bounded velocities but unbounded amplitudes concentrated at smaller and smaller spatial scales, which points to the kind of extra control a uniqueness theorem has to impose.

Formalizing it. The statement fixes a long list of admissibility conditions. Its definitions are a useful contribution in their own right: renormalized solutions, entropy dissipation and kinetic test functions on the torus are not in Mathlib. The 65-page proof (colored decompositions, Carleman representation, velocity averaging, a dilation limit and a branching analysis) is a long-term target. Its propositions are natural milestones.

Difficulty

Constructing two different weak limits is not the hard part: approximations with and without a small "hot seed" give two candidate solutions. The difficulty is to show that they really differ. A vanishing seed can produce a hit on the a priori cap that carries arbitrarily little mass, and weak compactness can erase it in the limit. The source must rule out this loss of information uniformly as the cold velocity distributions collapse onto an axis, where the weight controlling the hot density is singular. At the same time every admissibility condition, including the entropy-dissipation inequality and local mass conservation, has to survive the limits. Energy-increasing constructions (Wennberg) and homogeneous examples do not meet these constraints.

Formalization scope

Velocities live in EuclideanSpace ℝ (Fin 3), positions in Fin 3 → AddCircle 1, and densities are real functions on phase space. The sphere carries (volume).toSphere, which is ordinary surface area, not a probability measure.
gain and loss are Bochner integrals. To prevent them from silently returning $0$ on non-integrable fibers, AdmissibleGlobal requires fiberwise integrability and space-time integrability of the renormalized gain and loss.
AdmissibleGlobal f₀ F encodes Definition 2.1: finite entropy at each time, a.e. initial value, weak continuity against bounded measurable tests, uniform moment bounds, the renormalized equation for all Renormalization $\beta$ and all smooth periodic KineticTest $\varphi$ , local mass conservation against MassTest, total momentum conservation, the energy inequality, and the entropy inequality in ℝ≥0∞ with the lower semicontinuous extension of $(A-B)\log(A/B)$ .
StrongEarly T F adds $T>0$ , strong $L^1$ continuity on $[0,T]$ via eLpNorm, and integrability of gain and loss on $[0,T]$ . Distinctness is ¬ (F t =ᵐ G t) for some $t\in[0,T]$ .
Infrastructure needed: averaging lemmas, renormalized-solution compactness, the Carleman representation, and estimates on free transport on the torus. Contributions to any of these are welcome.

Selected references

R. J. DiPerna and P.-L. Lions, On the Cauchy problem for Boltzmann equations: global existence and weak stability, Ann. of Math. 130 (1989), 321–366. https://doi.org/10.2307/1971423
R. J. DiPerna and P.-L. Lions, Global solutions of Boltzmann's equation and the entropy inequality, Arch. Ration. Mech. Anal. 114 (1991), 47–55. https://doi.org/10.1007/BF00375684
C. D. Levermore and N. Masmoudi, From the Boltzmann equation to an incompressible Navier–Stokes–Fourier system, Arch. Ration. Mech. Anal. 196 (2010), 753–809. https://doi.org/10.1007/s00205-009-0254-5
L. Silvestre, Regularity estimates and open problems in kinetic equations, arXiv:2204.06401 (2022). https://doi.org/10.48550/arXiv.2204.06401
S. Kaniel and M. Shinbrot, The Boltzmann equation. I. Uniqueness and local existence, Comm. Math. Phys. 58 (1978), 65–84. https://doi.org/10.1007/BF01624788
S. Ukai, On the existence of global solutions of mixed problem for non-linear Boltzmann equation, Proc. Japan Acad. 50 (1974), 179–184. https://doi.org/10.3792/pja/1195519027
S. Mischler and B. Wennberg, On the spatially homogeneous Boltzmann equation, Ann. Inst. H. Poincaré C 16 (1999), 467–501. https://doi.org/10.1016/S0294-1449(99)80025-0
B. Wennberg, An example of nonuniqueness for solutions to the homogeneous Boltzmann equation, J. Stat. Phys. 95 (1999), 469–477. https://doi.org/10.1023/A:1004546031908
F. Golse, P.-L. Lions, B. Perthame and R. Sentis, Regularity of the moments of the solution of a transport equation, J. Funct. Anal. 76 (1988), 110–125. https://doi.org/10.1016/0022-1236(88)90051-1
X. Chen and J. Holmer, Well/ill-posedness bifurcation for the Boltzmann equation with constant collision kernel, Ann. PDE 10 (2024), Art. 14. https://doi.org/10.1007/s40818-024-00177-w
X. Chen, Y. Guo, S. Shen and Z. Zhang, Sharp $H^s_x$ ill-posedness of the hard-sphere Boltzmann equation, arXiv:2606.01331 (2026). https://doi.org/10.48550/arXiv.2606.01331
N. Gismondi, W. Golding and M. Novack, A sharp rigidity/flexibility threshold for the isotropic Landau equation, arXiv:2608.13758 (2026). https://doi.org/10.48550/arXiv.2608.13758
OpenAI, Nonuniqueness for the periodic hard-sphere Boltzmann equation, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 3; Definition 2.1, p. 8). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Nonuniqueness-for-the-periodic-hard-sphere-Boltzmann-equation-September-23-2026/paper.pdf

4 thms2 active usersReviewed

Mathematical Physics

Missions

The Endpoint Distribution of Directed Polymers 1: In the Low-Temperature Phase the Endpoint Distribution Is Asymptotically Purely Atomic, and at High Temperature It Is NotResearch Paper

Motivation

Setting

Formalization targets

Asymptotic pure atomicity

Significance

Difficulty

Formalization scope

Selected references

Celestial w_{1+∞} wedge algebra and gluon S-algebra (Zhu review, §7.1)Research Paper

Motivation

Setting

Formalization targets

Goal: (7.8) is a Lie bracket

Milestones

Significance

Difficulty

Formalization scope

Selected references

Gubser-Klebanov-Polyakov 1998: dimensions of operators dual to massive string statesResearch Paper

Motivation

Setting

Formalization targets

Goal (Eqs. (41)–(46))

Milestones

Significance

Difficulty

Formalization scope

Selected references

Wall 2013: The generalized second law implies a quantum singularity theoremResearch Paper

Motivation

Setting

Formalization targets

Goal — Theorem 4 (quantum singularity theorem)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The new Minimal Standard ModelResearch Paper

Motivation

Setting

Formalization targets

Goal — an exactly massless neutrino

Milestones

Significance

Difficulty

Formalization scope

Selected references

Astrophysical Fluid Dynamics I: Rankine–Hugoniot Shock RelationsTextbook

Motivation

Setting

Formalization targets

Goal: the Rankine–Hugoniot jump formulas (eqs. 6.30–6.31)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Giunti–Studenikin 2015: Neutrino Oscillations, Majorana Form Factors and Spin PrecessionResearch Paper

Motivation

Setting

Formalization targets

Goal: the general vacuum oscillation probability, Eq. (2.37)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Baumgarten 2018: How to (Un-) Quantum Mechanics — Phase-Space AlgebraResearch Paper

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Virial Theorem (Classical N-Particle Mechanics)Textbook

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