Mathematical Physics

Completed

Analysis Probability·Captain: wurtle

A radial continuum phase transition with algebraic decayResearch Paper

Motivation: continuum phase transitions with a power-law tail

Whether identical classical particles in $\mathbb R^3$ , interacting only through a stable radial pair potential, can undergo a phase transition is a classical existence problem of rigorous statistical mechanics, highlighted in Simon's list of problems in mathematical physics (Simon 1984). A transition shows up as a singularity of the thermodynamic free energy. Earlier rigorous continuum transitions rely on extra structure — two species, many-body terms, hard cores, or interactions defined through a fixed partition into boxes — or on a mean-field limit in which the potential itself changes. A natural requirement for a satisfactory answer is a single fixed pair potential with a bounded core and an explicit integrable power-law tail.

Timeline

1965 — Motzkin and Straus's weighted-graph maximization, later used for occupation bounds (Motzkin–Straus 1965).
1966 — Lebowitz and Penrose: rigorous van der Waals–Maxwell theory in the Kac limit (Lebowitz–Penrose 1966).
1970 — Ruelle's superstability framework (Ruelle 1970).
1971 — Ruelle: transition for a symmetric two-species continuum system (Ruelle 1971).
1973 — Gerardi, Marchioro, Olivieri and Presutti extend the Lebowitz–Penrose limit to superstable references (GMOP 1973).
1984 — Simon lists the problem among fifteen problems in mathematical physics.
1998–1999 — Lebowitz, Mazel and Presutti: liquid–vapor transition with attractive pair and repulsive four-body interactions (PRL 1998, J. Stat. Phys. 1999).
2026 — He, Jauslin, Lebowitz and Peled: transition for a finite-range box-modified Kac pair interaction (CMP 2026); Dereudre and Renaud-Chan: density coexistence for saturated many-body interactions (arXiv:2602.11078).
2026 — Two OpenAI preprints (OpenAI Math Release, September 24, 2026): a radial potential with divergent core and $o(r^{-3})$ tail with a temperature singularity, and the present A radial continuum phase transition with algebraic decay, which claims a bounded continuous potential with $|\phi(r)|\le Cr^{-3-1/32}$ . Neither is peer reviewed, and the theorem is not formally verified.

Setting

Particles live in $\mathbb R^3$ ; a radial pair potential is a function $\phi:[0,\infty)\to\mathbb R$ (in Lean, ℝ≥0 → ℝ) applied to pair distances. For the cube $\Lambda_L=[0,L]^3$ and $N\ge0$ ,

U^\phi(x_1,\dots,x_N)=\sum_{i<j}\phi(|x_i-x_j|),\qquad Z_{L,N}(\beta)=\frac1{N!}\int_{\Lambda_L^N}e^{-\beta U^\phi}\,dx,\qquad Z_{L,0}=1 .

The potential is stable if $U^\phi\ge -BN$ for all configurations. The canonical free energy at density $\rho$ is

f(\beta,\rho)=-\lim_{L\to\infty}\frac1{\beta L^3}\log Z_{L,\lfloor\rho L^3\rfloor}(\beta).

The packing constant is $p=\lim_{L\to\infty}M_L/L^3$ , where $M_L$ is the largest number of points in $[0,L]^3$ at mutual distance $\ge1$ ; in Lean IsPackingDensity p asserts this limit. StrictTemperatureCorner f βc asserts finite left and right derivatives at $\beta_c$ with the right one strictly smaller, and non-differentiability.

Formalization targets

Milestone: the corner at the central density

At the single density $\rho=5p/3$ : there are a bounded continuous stable $\phi$ with $|\phi(r)|\le Cr^{-3-1/32}$ for $r\ge1$ and $\beta_c\in[7/8,9/8]$ such that $f(\cdot,5p/3)$ exists for all $\beta>0$ and

f'_-(\beta_c,5p/3)>f'_+(\beta_c,5p/3).

Goal: a common corner on a density interval

There are a bounded continuous $\phi$ , constants $B,C>0$ with

\sum_{i<j}\phi(|x_i-x_j|)\ge -BN,\qquad |\phi(r)|\le C\,r^{-3-1/32}\ (r\ge1),

an open interval $I=(5p/3-\eta,\,5p/3+\eta)\subset(0,\infty)$ and one $\beta_c\in[7/8,9/8]$ such that for every $\rho\in I$ the free energy $f(\beta,\rho)$ exists and is finite for every $\beta>0$ , and

f'_-(\beta_c,\rho)>f'_+(\beta_c,\rho).

This is Theorem 1.1 of the source. Both statements are published on the platform with status Open.

Significance

The result itself. The theorem gives a single-species, bounded, continuous radial pair potential with an explicit integrable power-law tail whose canonical free energy has a strict temperature corner at one critical inverse temperature for a whole interval of densities. The interaction is a genuine radial function of separations with all long-range terms kept; boxes appear only in the estimates. It does not treat Lennard–Jones-type potentials and does not identify the phases as conventional fluids. The companion preprint has a divergent core but only an $o(r^{-3})$ tail; the fixed power margin $1/32$ here needs a quantitative range estimate not present there.

Formalizing it. The statement fixes the model completely (free boundary conditions on $[0,L]^3$ , Lebesgue measure without temperature normalization, $1/N!$ , $\lfloor\rho L^3\rfloor$ particles), so a formal proof would settle exactly which version of the problem is solved. The infrastructure (thermodynamic limits, convex duality for pressures, Kac comparisons) is reusable for the companion mission.

Difficulty

The Lebowitz–Penrose theory produces non-convex mean-field free energies only in the limit where the attraction range tends to infinity, and that limiting object is not the free energy of any fixed potential. A single potential must therefore contain infinitely many attractions at growing ranges, and the required singularity must survive all of them. Density coexistence at fixed temperature does not by itself give a temperature corner at a fixed density: two supporting slopes with equal density coordinate and different energy coordinates are needed. A pointwise power bound constrains how strong the successive attractions may be relative to their ranges, which is why a quantitative comparison with an explicit error is required.

Formalization scope

Positions are EuclideanSpace ℝ (Fin 3); distances enter through nndist, so the potential is a function on ℝ≥0. Boundedness, continuity, stability with $B>0$ , and decay with $C>0$ are separate conjuncts.
$p$ is existentially quantified but pinned by IsPackingDensity p (a limit), and $p>0$ is required; packingNumber is a sSup over a bounded set of naturals.
IsCanonicalFreeEnergy φ ρ f asserts $-\log Z/(\beta L^3)\to f(\beta)$ for every $\beta>0$ , so $f$ is determined on $(0,\infty)$ ; one-sided derivatives use HasDerivWithinAt on Iic βc and Ici βc.
The goal requires the interval to lie in $(0,\infty)$ and $\beta_c$ to be independent of $\rho$ .
Needed infrastructure: superstability and occupation moments, existence of thermodynamic limits and their convex duality, a Motzkin–Straus bound, quantitative Kac comparison, and subdifferential persistence arguments.

Selected references

B. Simon, Fifteen problems in mathematical physics, in Perspectives in Mathematics, Birkhäuser, 1984, 423–454. https://math.caltech.edu/SimonPapers/R27.pdf
T. S. Motzkin and E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canad. J. Math. 17 (1965), 533–540. https://doi.org/10.4153/CJM-1965-053-6
J. L. Lebowitz and O. Penrose, Rigorous treatment of the van der Waals–Maxwell theory of the liquid-vapor transition, J. Math. Phys. 7 (1966), 98–113. https://doi.org/10.1063/1.1704821
D. Ruelle, Superstable interactions in classical statistical mechanics, Comm. Math. Phys. 18 (1970), 127–159. https://doi.org/10.1007/BF01646091
D. Ruelle, Existence of a phase transition in a continuous classical system, Phys. Rev. Lett. 27 (1971), 1040–1041. https://doi.org/10.1103/PhysRevLett.27.1040
A. Gerardi, C. Marchioro, E. Olivieri and E. Presutti, Van der Waals–Maxwell theory, Lebowitz–Penrose limit and superstable interactions, Comm. Math. Phys. 29 (1973), 219–231. https://doi.org/10.1007/BF01645248
J. L. Lebowitz, A. E. Mazel and E. Presutti, Liquid–vapor phase transitions for systems with finite-range interactions, J. Stat. Phys. 94 (1999), 955–1025. https://doi.org/10.1023/A:1004591218510
Q. He, I. Jauslin, J. Lebowitz and R. Peled, Liquid-vapor transition in a model of a continuum particle system with finite-range modified Kac pair potential, Comm. Math. Phys. 407 (2026), 240. https://doi.org/10.1007/s00220-026-05735-w
D. Dereudre and C. Renaud-Chan, First-order phase transition for Gibbs point processes with saturated interactions, arXiv:2602.11078 (2026). https://arxiv.org/abs/2602.11078v1
R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
OpenAI, A continuum temperature singularity for a radial pair potential, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026/paper.pdf
OpenAI, A radial continuum phase transition with algebraic decay, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026/paper.pdf

14 thms2 active usersReviewed

Completed

Analysis Probability·Captain: wurtle

A continuum temperature singularity for a radial pair potentialResearch Paper

Motivation: phase transitions for continuum particles

Whether a single species of classical particles in $\mathbb R^3$ , interacting only through a stable radial pair potential, can undergo a phase transition is one of the long-standing existence questions of rigorous statistical mechanics; it appears in Simon's list of problems in mathematical physics (Simon 1984). A phase transition is detected as a loss of regularity of the thermodynamic free energy. Lattice models and continuum models with extra structure (several species, many-body terms, hard cores, box-restricted interactions) were handled long ago; ordinary pair potentials finite at every positive separation remained the difficult case.

Timeline

1966 — Lebowitz and Penrose give the rigorous van der Waals–Maxwell theory in the Kac (long-range) limit (Lebowitz–Penrose 1966).
1970 — Ruelle's superstability framework for classical continuum systems (Ruelle 1970).
1971 — Ruelle proves a transition for the two-species Widom–Rowlinson model (Ruelle 1971).
1975 — Israel's convex construction gives coexistence for hard-core continuum particles with a spherically symmetric pair perturbation (Israel 1975).
1984 — Simon lists the continuum phase-transition problem among fifteen problems in mathematical physics.
1998–1999 — Lebowitz, Mazel and Presutti prove a liquid–vapor transition for attractive pair plus repulsive four-body interactions (PRL 1998, J. Stat. Phys. 1999).
2025–2026 — He, Jauslin, Lebowitz and Peled: coexistence for a box-modified Kac pair interaction (CMP 2026); Dereudre and Renaud-Chan: low-temperature coexistence for saturated (many-body) interactions (arXiv:2602.11078).
2026 — An OpenAI preprint, A continuum temperature singularity for a radial pair potential (OpenAI Math Release, September 24, 2026), claims an admissible radial pair potential in $\mathbb R^3$ whose canonical free energy has a temperature corner at one critical inverse temperature for every density in an open interval. It has not been peer reviewed and the theorem is not formally verified.

Setting

A radial pair potential is $\Phi(x)=\phi(|x|)$ on $\mathbb R^3$ with $\Phi(0)=+\infty$ . It is admissible if $\Phi$ is Borel measurable, $\phi$ is finite and locally bounded on $(0,\infty)$ , and

$\phi(r)\to+\infty$ as $r\downarrow0$ ;
$\phi\le-a<0$ on some interval $[r_1,r_2]$ with $0<r_1<r_2$ ;
$\int_R^\infty r^2|\phi(r)|\,dr<\infty$ for some $R$ ;
(stability) $U_N(x_1,\dots,x_N)=\sum_{i<j}\Phi(x_i-x_j)\ge -BN$ for all $N$ and all configurations.

With $\Lambda_L=[-L/2,L/2]^3$ and free boundary conditions, the canonical partition function is

Z_{\Lambda_L,N}(\beta)=\frac1{N!}\int_{\Lambda_L^N}e^{-\beta U_N}\,dx,\qquad Z_{\Lambda_L,0}=1,\quad e^{-\beta\cdot\infty}=0,

and the canonical free-energy density at density $\rho>0$ is

f(\beta,\rho)=-\frac1\beta\lim_{L\to\infty}L^{-3}\log Z_{\Lambda_L,\lfloor\rho L^3\rfloor}(\beta).

In Lean, radialPotential φ takes values in EReal (value ⊤ at the origin), energy is the pair sum, partition φ β L N is the integral above, and HasCanonicalFreeEnergy φ f says $L^{-3}\log Z\to-\beta f(\beta,\rho)$ for all $\beta,\rho>0$ .

Formalization targets

Goal: a strict temperature corner throughout a density interval

There exist an admissible $\phi$ with $\phi(r)=o(r^{-3})$ as $r\to\infty$ , a free-energy function $f$ realizing the canonical limit for every $\beta>0,\rho>0$ , a nonempty open interval $I\subset(0,\infty)$ and one $\beta_c\in(1/2,3/2)$ such that for every $\rho\in I$ the one-sided $\beta$ -derivatives exist and

D^-_\beta f(\beta_c,\rho)\;>\;D^+_\beta f(\beta_c,\rho).

This is Theorem 1.1 of the source (MainStatement). The goal is published on the platform with status Open.

Significance

The result itself. The theorem exhibits a genuine one-species pair potential, finite at every positive separation and with all cross-cube interactions retained, whose canonical free energy is not $C^1$ in temperature at a fixed density, with one critical temperature for an entire interval of densities. It does not concern the Lennard–Jones potential, does not identify the coexisting states as liquid/vapor/solid, and does not give a power-law tail $|\phi(r)|\le Cr^{-3-\varepsilon}$ ; formulations of the historical problem that require such a margin are not resolved by it. A companion preprint (A radial continuum phase transition with algebraic decay) gives a bounded potential with tail $r^{-3-1/32}$ .

Formalizing it. The statement is fully explicit about the model, normalization, and boundary conditions, so a formal proof would remove any ambiguity about which version of the problem is solved. It requires thermodynamic limits for superstable continuum systems, convex-analytic facts about pressures, and a Kac/Lebowitz–Penrose comparison with uniform estimates, none of which is currently in Mathlib.

Difficulty

Density coexistence for a grand-canonical system does not by itself produce a temperature corner at a fixed density; one needs two supporting slopes of the pressure with the same density coordinate and different energy coordinates. Classical tools for transitions (Peierls arguments, reflection positivity, Kac limits) either need lattice structure, many-body terms, or a limit in which the potential itself changes. Here a single fixed potential must be built through infinitely many attractions at growing ranges, and the convex supporting-slope information must survive every approximation step while preserving stability and integrable tails.

Formalization scope

Space is EuclideanSpace ℝ (Fin 3); the potential is EReal-valued with ⊤ at the origin, and the Boltzmann weight is $0$ when the energy is ⊤. Stability is stated in EReal, which also rules out ⊥.
Free boundary conditions on the closed cube $[-L/2,L/2]^3$ , Lebesgue measure without temperature normalization, $1/N!$ , and $N=\lfloor\rho L^3\rfloor$ via Nat.floor; the limit is over real $L\to\infty$ .
One-sided derivatives are HasDerivWithinAt on Iic βc and Ici βc, so both are finite real numbers; $f$ is pinned by HasCanonicalFreeEnergy for every $\beta>0,\rho>0$ , so it cannot be chosen freely near $\beta_c$ .
$I$ is open, order-connected, nonempty and contained in $(0,\infty)$ ; $\beta_c$ is independent of $\rho$ .
Needed infrastructure: superstability estimates, existence of canonical and grand-canonical thermodynamic limits, Legendre duality for pressures, the Lebowitz–Penrose limit. These are reusable for the companion mission.

Selected references

B. Simon, Fifteen problems in mathematical physics, in Perspectives in Mathematics, Birkhäuser, 1984, 423–454. https://math.caltech.edu/SimonPapers/R27.pdf
J. L. Lebowitz and O. Penrose, Rigorous treatment of the van der Waals–Maxwell theory of the liquid-vapor transition, J. Math. Phys. 7 (1966), 98–113. https://doi.org/10.1063/1.1704821
D. Ruelle, Superstable interactions in classical statistical mechanics, Comm. Math. Phys. 18 (1970), 127–159. https://doi.org/10.1007/BF01646091
D. Ruelle, Existence of a phase transition in a continuous classical system, Phys. Rev. Lett. 27 (1971), 1040–1041. https://doi.org/10.1103/PhysRevLett.27.1040
R. B. Israel, Existence of phase transitions for long-range interactions, Comm. Math. Phys. 43 (1975), 59–68. https://doi.org/10.1007/BF01609141
J. L. Lebowitz, A. E. Mazel and E. Presutti, Liquid–vapor phase transitions for systems with finite-range interactions, J. Stat. Phys. 94 (1999), 955–1025. https://doi.org/10.1023/A:1004591218510
Q. He, I. Jauslin, J. Lebowitz and R. Peled, Liquid–vapor transition in a model of a continuum particle system with finite-range modified Kac pair potential, Comm. Math. Phys. 407 (2026), 240. https://doi.org/10.1007/s00220-026-05735-w
D. Dereudre and C. Renaud-Chan, First-order phase transition for Gibbs point processes with saturated interactions, arXiv:2602.11078 (2026). https://arxiv.org/abs/2602.11078v1
OpenAI, A radial continuum phase transition with algebraic decay, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026/paper.pdf
OpenAI, A continuum temperature singularity for a radial pair potential, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026/paper.pdf

5 thms2 active usersReviewed

Completed

Markov Chain Probability·Captain: wurtle

Critical slowing down in the Sherrington–Kirkpatrick modelResearch Paper

Motivation

The Sherrington–Kirkpatrick (SK) model is the mean-field spin glass, and $\beta=1$ is its equilibrium critical point. Physicists expect critical slowing down: at a phase transition, local dynamics needs time growing polynomially in the system size to relax. For the SK model this was studied through linearized mean-field theory, dynamical equations for correlation and response, and simulations of equilibrium autocorrelations on an $n^{2/3}$ time scale. Rigorous results on Glauber dynamics had concentrated on high temperature, where mixing is fast. This mission asks for a rigorous total-variation obstruction at $\beta=1$ : most equilibrium configurations, used as starting states, are still far from equilibrium after $o(n^{2/3})$ time.

Timeline

1975, 1978. Sherrington and Kirkpatrick introduce the model and study Glauber autocorrelations above the critical temperature (doi:10.1103/PhysRevLett.35.1792, doi:10.1103/PhysRevB.17.4384).
1976. Kosterlitz, Thouless and Jones analyze the spherical spin glass, with its transition at the spectral edge (doi:10.1103/PhysRevLett.36.1217).
1981–1982. Sompolinsky and Zippelius develop dynamical equations for correlation and response (doi:10.1103/PhysRevLett.47.359, doi:10.1103/PhysRevB.25.6860).
1996. Comets relates the Ising and spherical partition functions via a Haar-averaging identity (doi:10.24033/ast.331).
2011. Billoire and Campbell numerically examine critical autocorrelations on the $n^{2/3}$ scale (doi:10.1103/PhysRevB.84.054442).
2016, 2022. Baik and Lee, and Landon, prove free-energy fluctuation limits for the spherical model, including criticality (doi:10.1007/s10955-016-1610-0, doi:10.1063/5.0054298).
2019, 2022. Bauerschmidt–Bodineau and Eldan–Koehler–Zeitouni prove functional inequalities at high temperature (doi:10.1016/j.jfa.2019.01.007, doi:10.1007/s00440-021-01085-x).
2026. Du and Huang prove critical free-energy and overlap results (arXiv:2607.02172, arXiv:2608.08752); Wang and Boban–Li–Oveis Gharan prove fast mixing for $\beta<1/2$ and $\beta<1/2+\varepsilon_0$ (arXiv:2608.22159, arXiv:2609.13138).

The source of this mission is an OpenAI preprint dated September 24, 2026.

Setting

At $\beta=1$ and zero field, let $W_{ij}\sim N(0,1/n)$ be independent for $i<j$ and

\mu_W(x)\propto\exp\Bigl(\sum_{i<j}W_{ij}x_ix_j\Bigr),\qquad x\in\{-1,1\}^n .

A heat-bath update at site $i$ resamples $x_i$ from its conditional law given the other spins. In continuous time every site has an independent rate-one clock (generator $\sum_i(K_i-I)$ ); in discrete time each step updates a uniformly chosen site (kernel $n^{-1}\sum_iK_i$ ). For a fixed start $x$ , $d^{\rm ct}_t(W,x)$ and $d^{\rm dt}_k(W,x)$ are the total-variation distances to $\mu_W$ .

Formalization targets

Goal: Theorem 1.1 (realized equilibrium initial states)

For every deterministic $t_n\ge0$ with $t_n=o(n^{2/3})$ and every deterministic integer $k_n=o(n^{5/3})$ ,

\mu_W\{x:\ d^{\rm ct}_{t_n}(W,x)>1/4\}\ \xrightarrow{\ \mathbb P\ }\ 1,\qquad \mu_W\{x:\ d^{\rm dt}_{k_n}(W,x)>1/4\}\ \xrightarrow{\ \mathbb P\ }\ 1 .

Lean: OAI.CriticalSK.realized_equilibrium_initial_states, open on the platform.

Milestone: Theorem 1.2 (covariance and linear tests)

With $\Sigma=\operatorname{Cov}_{\mu_W}(x)$ , $\mathcal D(f)=\sum_i\mu_W[\operatorname{Var}(f\mid x_{-i})]$ and $R_{\rm lin}=\sup_{a\ne0}\operatorname{Var}(a^{\mathsf T}x)/\mathcal D(a^{\mathsf T}x)$ : for every $M_n\to\infty$ , with probability tending to one,

\|\Sigma\|,\ R_{\rm lin}\ \in\ \bigl[n^{2/3}/M_n,\ M_nn^{2/3}\bigr].

Milestones: Theorem 1.3 (critical mixing bounds)

For every fixed $\epsilon>0$ ,

\mathbb P\{n^{2/3-\epsilon}\le t_{\rm mix}\le e^{\epsilon n}\}\to1,\qquad \mathbb P\{n^{5/3-\epsilon}\le k_{\rm mix}\le e^{\epsilon n}\}\to1,

with a separate Lean target for the lower bounds alone.

Significance

The theorem shows that at criticality the slow direction is visible from typical equilibrium starts, not only from adversarial ones, and pins the time scale $n^{2/3}$ to the spectral edge of the coupling matrix. Theorem 1.2 identifies the covariance scale $n^{2/3}$ , contrasting with bounded covariance at every $\beta<1$ . A companion OpenAI preprint uses Theorems 1.1 and 1.2 as inputs for matching upper bounds $n^{2/3+o(1)}$ .

The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists.

Difficulty

Averaging over the starting state gives back the stationary law, so the obstruction must be proved start by start. The slow observable is the projection $v^{\mathsf T}x$ on the top eigenvector of the coupling matrix; the difficulty is the static estimate that this projection is rarely small on the $n^{1/3}$ scale under the Ising Gibbs law. This requires edge-of-spectrum random matrix estimates, a precise comparison between the Ising law and a tilted spherical law, and control of the conditioning on the sphere.

Formalization scope

hamiltonian W x = ∑_{i<j} W_{ij} x_i x_j; disorderLaw n is the product of gaussianReal 0 (1/n) over pairs $i<j$ .
siteKernel W i is the heat-bath kernel on configurations agreeing off $i$ ; discreteKernel = n^{-1}∑_i siteKernel; continuousKernel W t = exp(t ∑_i (siteKernel W i - 1)).
continuousGoodMass/discreteGoodMass are the Gibbs masses of starts with distance $>1/4$ ; convergence in probability is written as $\mathbb P(|\text{mass}-1|\ge\delta)\to0$ for all $\delta>0$ .
covarianceNorm is the Euclidean operator norm; linearRayleigh is a real sSup over nonzero $a$ (the quotient is bounded and the set nonempty).
Mixing times are sInf over times at which all starts are within $1/4$ .

Infrastructure: finite continuous-time Markov chains (matrix exponentials), GOE edge estimates, tridiagonal models, spherical integrals. The intermediate results Proposition 3.1, Theorem 5.3 and Proposition 5.4 are natural further milestones.

Selected references

OpenAI, Critical slowing down in the Sherrington–Kirkpatrick model, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Critical-slowing-down-in-the-Sherrington-Kirkpatrick-model-September-24-2026/paper.pdf
D. Sherrington, S. Kirkpatrick, Solvable model of a spin-glass, Phys. Rev. Lett., 1975. https://doi.org/10.1103/PhysRevLett.35.1792
H. Sompolinsky, A. Zippelius, Dynamic theory of the spin-glass phase, Phys. Rev. Lett., 1981. https://doi.org/10.1103/PhysRevLett.47.359
F. Comets, A spherical bound for the Sherrington–Kirkpatrick model, Astérisque, 1996. https://doi.org/10.24033/ast.331
H. Du, B. Huang, Fluctuations of the Sherrington–Kirkpatrick free energy at critical temperature, preprint, 2026. https://arxiv.org/abs/2607.02172
H. Du, B. Huang, Overlap distribution of the critical Sherrington–Kirkpatrick model, preprint, 2026. https://arxiv.org/abs/2608.08752
J. Baik, J. O. Lee, Fluctuations of the free energy of the spherical Sherrington–Kirkpatrick model, J. Stat. Phys., 2016. https://doi.org/10.1007/s10955-016-1610-0
B. Landon, Free energy fluctuations of the two-spin spherical SK model at critical temperature, J. Math. Phys., 2022. https://doi.org/10.1063/5.0054298
A. Billoire, I. A. Campbell, Dynamics in the Sherrington–Kirkpatrick Ising spin glass at and above $T_g$ , Phys. Rev. B, 2011. https://doi.org/10.1103/PhysRevB.84.054442

8 thms2 active usersReviewed

Completed

Probability·Captain: wurtle

Exponential decay in two-dimensional classical O(n) modelsResearch Paper

Motivation: mass generation in two-dimensional spin systems

The classical $O(n)$ model (for $n=3$ , the classical Heisenberg model) places a unit vector $\sigma_x\in S^{n-1}$ at each site of the square lattice and favours alignment of neighbouring spins. It is the basic lattice model of a system with continuous symmetry. In two dimensions the Mermin–Wagner theorem rules out spontaneous magnetization at every positive temperature, but it does not say how fast spins decorrelate. For $n=2$ (the plane rotator) correlations decay only polynomially at low temperature — the Berezinskii–Kosterlitz–Thouless phase. For $n\ge3$ , Polyakov's 1975 renormalization-group argument predicts mass generation: exponential decay of correlations at every positive temperature, the lattice analogue of asymptotic freedom in four-dimensional non-Abelian gauge theory. A rigorous proof at low temperature has long been a central question of rigorous statistical mechanics.

Timeline

1966–1967 — Mermin and Wagner prove absence of order for quantum Heisenberg models (PRL 1966); Mermin gives a classical argument (J. Math. Phys. 1967).
1971–1973 — Berezinskii (Sov. Phys. JETP 1971) and Kosterlitz–Thouless (J. Phys. C 1973) describe the slow-decay phase for two-component spins.
1975 — Polyakov predicts mass generation for $n\ge3$ at every positive temperature (Phys. Lett. B 1975).
1977 — McBryan and Spencer prove algebraic upper bounds on two-dimensional correlations by complex spin rotations (CMP 1977); extended by Gagnebin and Velenik (CMP 2014).
1980 — Aizenman and Simon prove exponential decay at high temperature from local Ward identities and a finite-size criterion (CMP 1980); Kupiainen proves a mass gap in the large- $n$ regime via the $1/n$ expansion (CMP 1980).
1981 — Fröhlich and Spencer prove the Kosterlitz–Thouless transition: polynomial lower bounds for the plane rotator at low temperature (CMP 1981), so no all-temperature exponential decay is possible for $n=2$ .
2002 — Patrascioiu and Seiler study percolation of spin regions as a route to a possible massless phase for $n=3$ (J. Stat. Phys. 106, 2002).
2025 — Aru, Garban and Sepúlveda record the all-temperature exponential-decay assertion as an open conjecture (CMP 2025).
2026 — An OpenAI preprint, Exponential decay in two-dimensional classical O(n) models (OpenAI Math Release, September 23, 2026), claims exponential decay for every $n\ge3$ and every finite $\beta$ , uniformly over finite free-boundary subgraphs. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Let $G=(V,E)$ be a finite subgraph of the nearest-neighbour square lattice $\mathbb Z^2$ , and let $b=(b_e)_{e\in E}$ be edge strengths with $0\le b_e\le\beta$ . Put a spin $\sigma_x\in S^{n-1}$ at each vertex. The free-boundary Gibbs measure is

d\mu^{(n)}_{G,b}(\sigma)=\frac{1}{Z^{(n)}_{G,b}}\exp\Bigl(\sum_{\{x,y\}\in E}b_{xy}\,\sigma_x\cdot\sigma_y\Bigr)\prod_{x\in V}d\omega_{n-1}(\sigma_x),

where $\omega_{n-1}$ is the uniform probability measure on the unit sphere and $Z^{(n)}_{G,b}$ is the normalizing integral. There are no boundary spins and no external field. The two-point function is $\langle\sigma_x\cdot\sigma_y\rangle^{(n)}_{G,b}$ , and $\|x-y\|_2$ is Euclidean distance.

Formalization targets

Goal: all-temperature exponential decay (Theorem 1.1)

For every integer $n\ge3$ and every $\beta>0$ there are $A<\infty$ and $m>0$ such that, for every finite nearest-neighbour subgraph $G$ of $\mathbb Z^2$ , every $b\in[0,\beta]^E$ and all $x,y\in V$ ,

0\ \le\ \langle\sigma_x\cdot\sigma_y\rangle^{(n)}_{G,b}\ \le\ A\,e^{-m\|x-y\|_2}.

The constants depend only on $n$ and $\beta$ and may deteriorate as $\beta\to\infty$ . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Uniformity over all finite subgraphs and strengths gives the same bound for free-boundary limits on boxes (Corollary 1.2 of the source) and for their subsequential infinite-volume limits, hence finite susceptibility. It confirms rigorously, for the spin two-point function, the mass-generation prediction for $n\ge3$ at arbitrarily low temperature, the regime left open by high-temperature and large- $n$ results, and contrasts sharply with the $n=2$ case. The source does not claim a transfer-matrix gap for all local observables, correlation-length asymptotics, or uniqueness of Gibbs states.

Formalizing it. The statement is a uniform estimate on explicit finite-dimensional integrals; a formal proof would certify a result the physics literature has expected since 1975. Groundwork includes Gibbs measures on products of spheres, rotation (Ward) identities, and random-cluster/sign-cluster representations, reusable for other lattice spin models.

Difficulty

Mermin–Wagner and McBryan–Spencer type arguments only show that order is destroyed and give polynomial bounds; they allow a zero decay rate and cannot distinguish $n\ge3$ from $n=2$ . Any proof must use the non-Abelian nature of the symmetry group, since the conclusion fails for $n=2$ . Exponential decay at high temperature (small $\beta$ ) follows from expansions, but at large $\beta$ spins are strongly aligned over long distances and no small parameter is available. Reducing to three components by conditioning produces random, dependent couplings, so the three-component estimate must hold uniformly over all strength arrays.

Formalization scope

Sites are ℤ × ℤ; a LatticeGraph is a finite vertex set with a finite set of positively oriented nearest-neighbour edges (each undirected edge represented once). Strengths are functions G.edges → ℝ with $0\le b_e\le\beta$ , so deleting edges and weakening couplings are covered.
Spins live in Metric.sphere 0 1 of EuclideanSpace ℝ (Fin n); the single-site law is the normalized sphere measure (toSphere of Lebesgue measure); the configuration law is the product measure.
correlation is the ratio of integrals $\int\sigma_x\cdot\sigma_y\,e^{H}\big/\int e^{H}$ ; the partition function is strictly positive, so the division is genuine.
The quantifier order is $\forall n\ge3,\ \forall\beta>0,\ \exists A,m$ with $m>0$ , then $\forall G,b,x,y$ : constants may not depend on the graph, the strengths or the points. Distance is the Euclidean norm on $\mathbb Z^2\subset\mathbb R^2$ .
Infrastructure needed: integration on spheres, differentiation of partition functions under spin rotations, FKG/Ginibre inequalities, Edwards–Sokal type couplings and percolation crossing estimates.

Selected references

N. D. Mermin and H. Wagner, Absence of ferromagnetism or antiferromagnetism in one- or two-dimensional isotropic Heisenberg models, Phys. Rev. Lett. 17 (1966), 1133–1136. https://doi.org/10.1103/PhysRevLett.17.1133
A. M. Polyakov, Interaction of Goldstone particles in two dimensions, Phys. Lett. B 59 (1975), 79–81. https://doi.org/10.1016/0370-2693(75)90161-6
O. A. McBryan and T. Spencer, On the decay of correlations in SO(n)-symmetric ferromagnets, Comm. Math. Phys. 53 (1977), 299–302. https://doi.org/10.1007/BF01609854
M. Aizenman and B. Simon, Local Ward identities and the decay of correlations in ferromagnets, Comm. Math. Phys. 77 (1980), 137–143. https://doi.org/10.1007/BF01982713
A. J. Kupiainen, On the 1/n expansion, Comm. Math. Phys. 73 (1980), 273–294. https://doi.org/10.1007/BF01197703
J. Fröhlich and T. Spencer, The Kosterlitz–Thouless transition in two-dimensional Abelian spin systems and the Coulomb gas, Comm. Math. Phys. 81 (1981), 527–602. https://doi.org/10.1007/BF01208273
M. Gagnebin and Y. Velenik, Upper bound on the decay of correlations in a general class of O(N)-symmetric models, Comm. Math. Phys. 332 (2014), 1235–1255. https://doi.org/10.1007/s00220-014-2075-0
J. Aru, C. Garban and A. Sepúlveda, Percolation for 2D classical Heisenberg model and exit sets of vector valued GFF, Comm. Math. Phys. 406 (2025). https://doi.org/10.1007/s00220-024-05208-y
OpenAI, Exponential decay in two-dimensional classical O(n) models, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Exponential-decay-in-two-dimensional-classical-On-models-September-23-2026/paper.pdf

7 thms2 active usersReviewed

Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XIII: The Sherrington–Kirkpatrick Model at High Temperature — Deviations of log Z_N from β²N/4Textbook

Motivation

The Sherrington–Kirkpatrick model assigns random interactions to every pair of spins in a system. Its partition function aggregates the weights of all spin configurations, and the logarithm of that partition function is the free energy. For a finite system, the free energy is a random quantity because the interactions are random. A useful question is therefore how far it can move from a deterministic high-temperature scale. Aizenman, Lebowitz and Ruelle (1987), and Comets and Neveu (1995) for Gaussian couplings, proved that for $\beta<1$ the variable $\log Z_N-\beta^2N/4$ converges in law to a normal random variable ALR 1987; Talagrand asks instead for tail estimates valid for every $N$ . Talagrand's Chapter 12 gives a finite-size tail bound and a bound on the expected free energy per site under explicit moment conditions on the interaction law Talagrand 1995.

The chapter belongs to a larger study of concentration inequalities on product spaces. Its relevance to the spin model is concrete: each pair interaction is an independent coordinate, while every spin configuration uses all those coordinates. The number of coordinates grows quadratically with the number of spins. A uniform estimate must respect both this growing dimension and the normalization in the energy Talagrand 1995, pp. 191–195.

Setting

Fix an integer $N\ge1$ . A spin configuration is a vector $\varepsilon=(\varepsilon_i)_{1\le i\le N}$ with each $\varepsilon_i\in\{-1,1\}$ . Each unordered pair of sites $i<j$ has a real coupling $h_{ij}$ . For an inverse temperature $\beta>0$ , the normalized partition function is

Z_N(h)=2^{-N}\sum_{\varepsilon\in\{-1,1\}^N} \exp\left(\frac{\beta}{\sqrt N}\sum_{1\le i<j\le N} h_{ij}\varepsilon_i\varepsilon_j\right).

Write $F_N(h)=\log Z_N(h)$ . The factor $2^{-N}$ averages over configurations. Since every summand is positive, $Z_N(h)>0$ for every array $h$ , so this logarithm is defined without excluding any coupling array.

The couplings are independent with a common probability law $\nu$ on $\mathbb R$ ; their joint law is $P_N=\nu^{\otimes\binom N2}$ . Under $\nu$ , a single coupling $H$ satisfies $\mathbb EH=\mathbb EH^3=0$ and $\mathbb EH^2=1$ . The chapter also assumes $\mathbb E e^{\alpha|H|}<\infty$ for some $\alpha>0$ . Its main theorem adds $\mathbb Ee^H<2$ and $\mathbb Ee^{-H}<2$ . These inequalities describe a class of interaction laws rather than one chosen distribution. A median $M_N$ of $F_N$ means that both $P_N(F_N\le M_N)$ and $P_N(F_N\ge M_N)$ are at least $1/2$ Talagrand 1995, pp. 191–193.

Formalization targets

The goal is Theorem 12.1. There is one absolute constant $K>0$ such that, for $0<\beta<1$ and $0<t<N/K$ ,

P_N\left(\left|F_N-\frac{\beta^2N}{4}\right|\ge K\left(t+\sqrt{\log\frac K{1-\beta^2}}\right)\sqrt N\right) \le 2e^{-t^2},

and the same constant satisfies

-\frac K{\sqrt N}\sqrt{\log\frac2{1-\beta^2}} \le \frac1N\mathbb EF_N-\frac{\beta^2}{4} \le \frac KN.

The first formula controls deviations at finite $N$ ; the second locates the expected free energy per site. The theorem leaves the absolute value of $K$ unspecified, as the source does Talagrand 1995, Theorem 12.1.

Four numbered displays form the supporting targets. Equation (12.6) bounds the change in $F_N$ when all couplings are changed. Equation (12.5) bounds deviations about any median. Equations (12.7) and (12.8) give first- and second-moment estimates for $Z_N$ . Together these specify the deterministic regularity and probabilistic estimates used by the chapter Talagrand 1995, pp. 192–195.

Significance

The theorem gives a nonasymptotic probability estimate, valid for each finite size and each law meeting the stated conditions. It also bounds the difference between the mean free energy per site and $\beta^2/4$ as $N$ grows, for fixed $\beta<1$ . The moment estimates separately describe the scale of the partition function and limit its relative second moment. These conclusions keep the coupling law general within the stated moment class Talagrand 1995, Theorem 12.1 and Eqs. (12.7)–(12.8).

The result is proved in the cited paper; the open work here is its Lean formalization. A completed development would connect product-measure concentration, finite spin sums, exponential-moment bounds, and real-valued expectations in one reusable interface. The coupling product space and median conventions can also serve other finite random-interaction models. No machine-checked proof of this chapter's target is claimed by this proposal.

Difficulty

A direct bounded-differences estimate cannot be applied to this model as stated: the couplings are real and may be unbounded. An estimate that handles each coordinate must account for the law's exponential moments while still retaining the $N$ and $\beta$ factors in the chapter's explicit bounds. The normalization by $\sqrt N$ makes a single coupling's influence small, but there are $\binom N2$ couplings, so treating the total sensitivity as dimension-free would lose the scale of the theorem. The first moment alone also does not control the lower tail of $Z_N$ ; this is why the second-moment target is present Talagrand 1995, pp. 192–195.

Formalization scope

Lean indexes sites by Fin N and interactions by pairs with $i<j$ . A spin is a Boolean choice interpreted as $-1$ or $1$ , and the configuration sum is normalized by $2^N$ . The coupling array is a function on the pair type, carrying the finite product measure of the common law $\nu$ . The theorem uses $N\ge1$ , $0<\beta<1$ , and exactly the common-law moment assumptions above; the median deviation milestone uses $N\ge2$ because its denominator contains $N-1$ . The main theorem places its single universal $K$ before every size, temperature, law, and deviation level.

Expectations are Bochner integrals, so integrability is explicit in the law predicates or in each conclusion that needs it. Probability expressions are real values of measurable events under the product measure. This avoids relying on Lean's default value for a nonintegrable integral. The model retains the entire real coupling law and does not replace it with a finite alphabet or a Gaussian special case. The partition function is built from the couplings and spins, rather than supplied as an unconstrained variable.

The source's displayed (12.5) omits $\beta$ , whereas the derivation following (12.6) gives, for each tail separately, the range $0<t\le4\beta\sqrt N(N-1)$ and the exponent $-t^2/(32\beta^2(N-1))$ with the factor $2$ . The formal milestone states exactly these two one-sided bounds, while its milestone text preserves the printed display verbatim. The first- and second-moment displays are kept with an absolute constant; the second-moment target uses the proof's $N\ge8$ range, since for smaller sizes the chapter's interaction-law assumptions do not ensure that $Z_N^2$ is integrable. Integrability of $F_N$ is a conclusion of the main theorem, never a hypothesis, and the median is quantified universally, so neither the expectation in (12.4) nor the deviation bound can hold by a default value of an undefined integral or by an unsatisfiable hypothesis; the Rademacher law $\nu=\frac12(\delta_{-1}+\delta_1)$ satisfies every assumption. Reusable contributions include integrability and measurability of $Z_N$ and $F_N$ , product-law estimates, and the source's numbered inequalities.

Selected references

Michel Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. DOI: 10.1007/BF02699376.
Michael Aizenman, Joel L. Lebowitz, David Ruelle, Some rigorous results on the Sherrington–Kirkpatrick spin glass model, Communications in Mathematical Physics 112 (1987), 3–20. DOI: 10.1007/BF01217677.
Francis Comets, Jacques Neveu, The Sherrington–Kirkpatrick model of spin glasses and stochastic calculus: the high temperature case, Communications in Mathematical Physics 166 (1995), 549–564. DOI: 10.1007/BF02099887.

6 thms2 active usersReviewed

Completed

Quantum Information·Captain: Lucas

Peres-Terno: the no-communication theorem for commuting Kraus operatorsResearch Paper

Motivation

Two observers, Alice and Bob, share a quantum system. Alice performs some intervention (a measurement, possibly followed by discarding part of her apparatus) and Bob, somewhere else, performs his own. If the statistics of Bob's outcomes could depend on what Alice chose to do, Alice could send Bob a message through the shared system alone, and if the two interventions are spacelike separated this would be a signal faster than light. Quantum mechanics and special relativity coexist peacefully only because this does not happen: the no-communication theorem guarantees that Bob's marginal statistics are independent of Alice's intervention whenever the two interventions are "local" to different parts of the system.

The review article of Peres and Terno, Quantum information and relativity theory (Rev. Mod. Phys. 76, 2004), develops the operational toolkit of quantum information (Kraus matrices, positive-operator-valued measures, completely positive maps) in Sec. II.D and then derives, in Sec. II.E, a sufficient algebraic condition for the absence of instantaneous information transfer: all of Alice's Kraus matrices commute with all of Bob's (their Eq. (9)). This mission formalizes that derivation together with the facts about Kraus matrices and complete positivity that the same pages state.

Setting

A quantum state on a finite-dimensional Hilbert space $\mathbb C^d$ is a density matrix $\rho$ : a positive semidefinite $d\times d$ complex matrix with $\operatorname{tr}\rho = 1$ .

An intervention with outcomes $\mu$ is described by Kraus matrices $A_{\mu m}$ , where the label $m$ ranges over a finite set indexing the subsystems discarded at the end of the interaction. When outcome $\mu$ occurs, the state is updated (Eq. (6)) to the unnormalized matrix

\rho'_\mu = \sum_m A_{\mu m}\,\rho\,A_{\mu m}^\dagger ,

and the probability of outcome $\mu$ is $p_\mu = \operatorname{tr}\rho'_\mu$ . The matrices

E_\mu = \sum_m A_{\mu m}^\dagger A_{\mu m}

(Eq. (8)) are the POVM elements; the intervention is complete when $\sum_\mu E_\mu = \mathbb 1$ .

A map $T$ on matrices is positive if it sends positive semidefinite matrices to positive semidefinite matrices, and completely positive if $T\otimes\mathbb 1$ , acting blockwise on matrices over $\mathbb C^d\otimes\mathbb C^n$ , is positive for every ancilla dimension $n$ .

For the no-communication theorem, Alice's Kraus matrices $A_{\mu m}$ and Bob's Kraus matrices $B_{\nu n}$ act on the same finite-dimensional space. The probability that Bob obtains $\nu$ , irrespective of Alice's outcome, is (Eq. (10))

p_\nu = \sum_\mu \operatorname{tr}\Big(\sum_{m,n} B_{\nu n} A_{\mu m}\,\rho\,A_{\mu m}^\dagger B_{\nu n}^\dagger\Big).

Formalization targets

Goal: no-communication (Sec. II.E, Eqs. (9)-(11))

If $[A_{\mu m}, B_{\nu n}] = 0$ for all $\mu, m, \nu, n$ , Alice's POVM is complete, and $\rho$ is a density matrix, then for every outcome $\nu$ of Bob

\sum_\mu \operatorname{tr}\Big(\sum_{m,n} B_{\nu n} A_{\mu m}\,\rho\,A_{\mu m}^\dagger B_{\nu n}^\dagger\Big) = \operatorname{tr}\Big(\sum_n B_{\nu n}\,\rho\,B_{\nu n}^\dagger\Big),

so all of Alice's operators disappear from Bob's statistics.

Milestones (Sec. II.D-II.E)

Eq. (7): $\sum_m \operatorname{tr}(A_{\mu m}\rho A_{\mu m}^\dagger) = \operatorname{tr}(\rho E_\mu)$ .
Eq. (8): every $E_\mu$ is positive semidefinite.
Eqs. (7)-(8): for a density matrix and a complete POVM, the $p_\mu$ are nonnegative reals summing to $1$ .
Eq. (6) defines a completely positive map.
Eq. (6) is the most general completely positive linear map: every completely positive linear map between matrix algebras has a finite Kraus representation.
Time reversal (transposition, i.e. complex conjugation of a Hermitian $\rho$ ) is a positive map,
but it is not completely positive.
The exchange step of Sec. II.E: under the commutation hypothesis, $\operatorname{tr}\sum_{m,n} B_{\nu n}A_{\mu m}\rho A_{\mu m}^\dagger B_{\nu n}^\dagger = \operatorname{tr}\big(E_\mu \sum_n B_{\nu n}\rho B_{\nu n}^\dagger\big)$ .

Significance

The no-communication theorem is the consistency check between quantum measurement theory and relativistic causality, and it is the starting point of the relativistic measurement theory developed in Sec. III of the review. The commutation condition (9) is exactly what local quantum field theory provides for spacelike separated regions, so this algebraic form is the one later used for microcausality arguments. The Kraus representation (milestones 4-5) is a basic structural theorem of quantum information theory, and the failure of complete positivity for transposition (milestones 6-7) underlies the partial-transpose entanglement criterion.

The results are classical and their proofs are known; the mission produces machine-checked versions on top of Mathlib's matrix library. The finite Kraus representation theorem (milestone 5) requires Choi-matrix machinery that is not, to the knowledge of this proposal, available in Mathlib in this form; it is reusable well beyond this mission.

Difficulty

The goal and milestones 1-3 and 8 are finite-dimensional trace manipulations; the care needed is in keeping the order of products right, using the adjoint of the commutation relation, and summing over indices in the correct order. Milestone 7 needs an explicit entangled witness on $\mathbb C^2\otimes\mathbb C^n$ . Milestone 5 is the substantial one: the obvious approach of writing $T(\rho)$ in a basis does not produce Kraus operators directly; a positivity argument (via the Choi matrix of $T$ and its spectral decomposition) is needed.

Formalization scope

All Hilbert spaces are finite dimensional: matrices are indexed by arbitrary finite types with complex entries. Outcome sets and discarded-subsystem label sets are finite types; Alice's and Bob's label sets may depend on the outcome. Kraus matrices for the single-intervention milestones may be rectangular ( $e\times d$ ), reflecting that the system after the intervention may differ from the original one; in the no-communication theorem both observers' matrices are square on a common space. The order on $\mathbb C$ used for "nonnegative probability" is the standard partial order ( $z\ge 0$ iff $z$ is real and nonnegative). Complete positivity quantifies over ancillas $\mathbb C^n$ for every $n\in\mathbb N$ , with $T\otimes\mathbb 1$ acting blockwise. Time reversal is encoded by the linear map $\rho\mapsto\rho^{T}$ ; on Hermitian matrices this coincides with complex conjugation, and only the linear extension gives a meaningful complete-positivity statement.

The goal keeps the hypotheses of the source setting (both POVMs complete, $\rho$ a density matrix); none of them can be dropped silently by a degenerate encoding, and the conclusion is an identity of complex numbers, so no hypothesis is vacuous: for instance, single-outcome trivial interventions with $A = B = \mathbb 1$ satisfy all of them.

Note: the sentence on p. 100 of the source claiming that commuting POVM elements are necessarily orthogonal projections is not included; as stated it fails (e.g. $E_1 = E_2 = \tfrac12\mathbb 1$ ).

Selected references

A. Peres and D. R. Terno, Quantum information and relativity theory, Rev. Mod. Phys. 76, 93-123 (2004). https://doi.org/10.1103/RevModPhys.76.93
K. Kraus, States, Effects, and Operations, Lecture Notes in Physics 190, Springer (1983). https://doi.org/10.1007/3-540-12732-1
M.-D. Choi, Completely positive linear maps on complex matrices, Linear Algebra Appl. 10, 285-290 (1975). https://doi.org/10.1016/0024-3795(75)90075-0

10 thms2 active usersReviewed

Probability·Captain: mikedeng1

The Intermediate Disorder Regime for Directed Polymers in Dimension 1+1: The Rescaled Partition Function Converges in Law to a Wiener ChaosResearch Paper

Motivation

A directed polymer in a random environment is a simple random walk whose paths are reweighted by a random field of energies. It is a basic model of disordered statistical mechanics, and in dimension $1+1$ it belongs to the Kardar–Parisi–Zhang (KPZ) universality class: at fixed temperature the free energy fluctuates on the scale $n^{1/3}$ and is expected to follow Tracy–Widom laws. Comets and Yoshida (Ann. Probab. 34 (2006)) showed that in dimension $1+1$ every positive inverse temperature $\beta$ lies in the strong disorder regime, where the normalised partition function tends to zero. At $\beta=0$ the polymer is simply the random walk.

Alberts, Khanin and Quastel (arXiv:1202.4398, Ann. Probab. 42 (2014)) identified the regime in between. If the inverse temperature is scaled as $\beta n^{-1/4}$ , the partition function neither concentrates nor vanishes: it converges in law to a universal random variable, a Wiener chaos in a space–time white noise. That variable is the solution at time $1$ , integrated in space, of the stochastic heat equation with multiplicative noise, whose logarithm is the Hopf–Cole solution of the KPZ equation. The theorem therefore connects discrete polymers to the continuum KPZ equation under weak, $n$ -dependent disorder, with no assumption on the environment beyond exponential moments.

Setting

The environment is a family $\omega=(\omega(i,x))_{i\ge1,\,x\in\mathbb Z}$ of i.i.d. real random variables on a probability space $(\Omega,Q)$ , with mean $0$ and variance $1$ . Write $\lambda(\beta)=\log Q\,e^{\beta\omega}$ . The polymer is the symmetric simple random walk $S$ on $\mathbb Z$ started at $0$ , independent of $\omega$ , under the uniform measure $\mathbf P$ on the $2^n$ step sequences. The energy of an $n$ -step path is $H_n^\omega(S)=\sum_{i=1}^n\omega(i,S_i)$ , and the point-to-line partition function is

Z_n^\omega(\beta)=\mathbf P\big[e^{\beta H_n^\omega(S)}\big].

The modified partition function replaces $e^{\beta\omega}$ by $1+\beta\omega$ : $\mathfrak z_n^\omega(\beta)=\mathbf P\big[\prod_{i=1}^n(1+\beta\,\omega(i,S_i))\big]$ .

On the continuum side, a white noise on $[0,1]\times\mathbb R$ is a centred Gaussian family $\{W(A)\}$ , indexed by the Borel sets of finite Lebesgue measure, with $E[W(A)W(B)]=|A\cap B|$ . Its multiple stochastic integrals are continuous linear maps $I_k:L^2([0,1]^k\times\mathbb R^k)\to L^2$ with $I_k(\mathbf 1_{A_1\times\dots\times A_k})=\prod_jW(A_j)$ for pairwise disjoint $A_j$ . Let $\varrho(t,x)=e^{-x^2/2t}/\sqrt{2\pi t}$ be the heat kernel and $\Delta_k=\{0=t_0<t_1<\dots<t_k\le1\}$ . Put $\varrho_k(\mathbf t,\mathbf x)=\prod_{j=1}^k\varrho(t_j-t_{j-1},x_j-x_{j-1})$ on $\Delta_k\times\mathbb R^k$ , with $x_0=0$ , and zero elsewhere. The Wiener chaos (7) is

\mathcal Z_\beta=\sum_{k\ge0}\beta^kI_k(\varrho_k)=1+\sum_{k\ge1}\beta^k\int_{\Delta_k}\int_{\mathbb R^k}\prod_{i=1}^kW(t_i,x_i)\,\varrho(t_i-t_{i-1},x_i-x_{i-1})\,dx_i\,dt_i .

The discrete counterpart of $I_k$ is the weighted U-statistic $\mathcal S_k^n(g)$ of (29): a sum of products $\prod_j\omega(i_j,x_j)$ over distinct times, weighted by averages of $g$ over space–time rectangles of size $\frac1n\times\frac2{\sqrt n}$ .

Formalization targets

Goal: Theorem 2.1 (second bullet), proved as Proposition 5.4

If, in addition, $\lambda(b)<\infty$ for all $0<b<\beta_0$ for some $\beta_0>0$ , then for every $\beta>0$

e^{-n\lambda(\beta n^{-1/4})}\,Z_n^\omega(\beta n^{-1/4})\xrightarrow{(d)}\mathcal Z_{\sqrt2\beta}\qquad(n\to\infty).

Modified partition function: Proposition 5.3 (Theorem 2.1, first bullet)

Under mean zero and variance one alone, $\mathfrak z_n^\omega(\beta n^{-1/4})\xrightarrow{(d)}\mathcal Z_{\sqrt2\beta}$ .

Milestones

In the order the proof uses them:

the norm $\|\varrho_k\|^2_{L^2}=1/(2^k\Gamma(k/2+1))$ and the convergence of the chaos series (§3.4, Lemma 3.1);
the $L^2$ structure of $\mathcal S_k^n$ (Lemma 4.1);
an approximation lemma for convergence in law (Lemma 4.2);
convergence of $n^{-3k/4}\mathcal S_k^n(g)$ to $I_k(g)$ , jointly over finitely many orders (Theorem 4.3);
convergence of whole discrete chaos expansions (Lemma 4.4);
the exact expansion $\mathfrak z_n^\omega(\beta)=\sum_{k\le n}2^{k/2}\beta^k\mathcal S_k^n(p_k^n)$ (Lemma 5.2);
a uniform $L^2$ bound on the discretised random walk kernels $n^{k/2}p_k^n$ (Lemma A.1);
Proposition 5.3.

Significance

The theorem gives a universal scaling limit for the partition function in a regime where the polymer still moves diffusively but feels the disorder. As a corollary, $\log Z_n^\omega(\beta n^{-1/4})-n\lambda(\beta n^{-1/4})$ converges in law, so the fluctuation exponent of the free energy is $0$ in this regime. The companion results (point-to-point partition functions, Theorem 2.2) show that the rescaled polymer path measure converges to a continuum directed random polymer. Letting $\beta$ grow then interpolates between Gaussian behaviour and the Tracy–Widom GUE fluctuations of the KPZ class. The U-statistic machinery of Section 4 (discrete chaos expansions in an i.i.d. space–time field converging to multiple Wiener–Itô integrals) applies to other discrete models with polynomial chaos expansions.

The theorem is proved in the paper. To our knowledge it has no machine-checked proof, and Mathlib has no space–time white noise, no multiple Wiener integrals, no Wiener chaos, no Lindeberg–Feller theorem for triangular arrays and no local limit theorem for the simple random walk. A complete formalization would build each of these and check the paper's argument, including two statements that are false as printed (see Formalization scope).

Difficulty

The obvious route is to expand $Z_n^\omega(\beta n^{-1/4})$ in powers of $\beta$ and pass to the limit term by term. Two steps of that route do not go through as stated. First, the $k$ -th term is a degenerate U-statistic of order $k$ in the environment. Its convergence to $I_k$ is not a classical central limit theorem: it needs joint control of all orders and a density argument in $L^2([0,1]^k\times\mathbb R^k)$ , and the space–time discretisation must respect the parity of the walk, which is why the rectangles have spatial length $2/\sqrt n$ . Second, exchanging the limit with the infinite sum over $k$ needs bounds on the discrete kernels $n^{k/2}p_k^n$ that are uniform in $n$ and summable in $k$ . Pointwise convergence from the local limit theorem is not enough. Passing from $\mathfrak z_n$ to $Z_n$ also requires a central limit theorem for a triangular array whose law depends on $n$ .

Formalization scope

The environment is ω : ℕ × ℤ → Ω → ℝ, independent and identically distributed, square integrable, with mean $0$ and variance $1$ . Times $i\ge1$ are read. $Z_n$ and $\mathfrak z_n$ are explicit averages over the $2^n$ step sequences. The white noise lives on $[0,1]\times\mathbb R$ , since only $t\le1$ enters (7). $I_k$ is a family of continuous linear maps on $L^2$ characterised by its values on indicators of products of disjoint sets. Every limit theorem quantifies over all white noises and all such families, and a separate item asserts that one exists. $\mathcal Z_\beta$ and $\mathcal S_k^n$ are sums in $L^2$ ; real powers $n^{-1/4}$ , $n^{-3k/4}$ are Real.rpow; $\lambda$ is Mathlib's cgf; convergence in law is TendstoInDistribution.

Normalisation of $I_k$ . The paper's normalisation of multiple integrals is not consistent (§3.2 and the remark on p. 19 differ by $k!$ ). The formalization follows (7) and the variance computation on p. 6: for $g$ supported on $\Delta_k\times\mathbb R^k$ , $E[I_k(g)^2]=\|g\|^2$ .

Corrected statements. Two milestones are stated in the corrected form that the paper's proof establishes:

Lemma 4.1. The bound $Q[\mathcal S_k^n(g)^2]\le n^{3k/2}\|g\|^2$ is false for general $g$ when $k\ge2$ , because permuted index vectors give the same product of environment variables. It is stated for $g$ vanishing outside $\Delta_k\times\mathbb R^k$ , the only case Section 5 uses. "Mean zero" is stated for $k\ge1$ , since $\mathcal S_0^n(g_0)=g_0$ .
Lemma 4.4. It is stated for Fock vectors whose components vanish outside the simplices, with square-summable norms, so that $\sum_kI_k(g_k)$ converges.

Theorem 4.5 and Lemma 4.6 (perturbed environments) are not part of the milestone list. Theorem 4.5 is false as printed: mean zero and a variance tending to $1$ do not give a central limit theorem for a triangular array, and the Lindeberg condition named in its proof must be added. Lemma A.1 is stated for the point-to-line kernels only.

Trivializations ruled out. The limit is the chaos (7) built from a genuine white noise and its multiple integrals, not any random variable with a prescribed property. $I$ is pinned down by $W$ . Every infinite sum comes with a milestone proving its summability, and the partition function averages over all $2^n$ walk paths.

Infrastructure that would be reusable beyond this mission: space–time white noise and multiple Wiener–Itô integrals with their isometry, a Lindeberg–Feller central limit theorem, the local limit theorem for the simple random walk, and the Cramér–Wold device. Contributions of any of these, or of proofs of the milestones in any order, are welcome.

Selected references

T. Alberts, K. Khanin, J. Quastel, The intermediate disorder regime for directed polymers in dimension 1+1, Ann. Probab. 42 (2014), 1212–1256. arXiv:1202.4398
T. Alberts, K. Khanin, J. Quastel, The continuum directed random polymer, J. Stat. Phys. 154 (2014), 305–326. MR3162542
F. Comets, N. Yoshida, Directed polymers in random environment are diffusive at weak disorder, Ann. Probab. 34 (2006), 1746–1770. MR2271480
S. Janson, Gaussian Hilbert Spaces, Cambridge Tracts in Mathematics 129, Cambridge University Press, 1997. MR1474726
P. Billingsley, Convergence of Probability Measures, Wiley, 1968. MR0233396

12 thms2 active usersReviewed

Optimization Partial Differential Equations Probability·Captain: mikedeng1

Optimization of Mean-field Spin Glasses I: Every Minimizer of the Extended Parisi Functional Has Full SupportResearch Paper

Motivation

The Ising mixed $p$ -spin model assigns to each configuration $\sigma \in \{-1,+1\}^N$ the energy of a random polynomial whose covariance is $\mathbb E\{H_N(\sigma)H_N(\sigma')\} = N\xi(\langle\sigma,\sigma'\rangle/N)$ . Its ground-state energy $\max_\sigma H_N(\sigma)/N$ converges to the value of a variational problem, the zero-temperature Parisi formula (Auffinger–Chen 2017), in which a functional $\mathsf P$ is minimized over non-decreasing order parameters $\gamma$ . El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) ask how close a polynomial-time algorithm can get to this maximum. Their answer is an extended variational principle: the best value reachable by incremental approximate message passing is $\inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$ , where the space $\mathscr L$ drops the monotonicity constraint.

The algorithm that reaches this value is built from a minimizer $\gamma_*$ of $\mathsf P$ over $\mathscr L$ , and it runs along the set of times where $\gamma_*$ is positive. Theorem 5 of the paper (p. 30) shows that this set is dense: a minimizer has full support. This mission formalizes that theorem and the first- and second-order optimality conditions it rests on (Section 6.1, pp. 22–31).

Timeline. Parisi proposed the variational formula in 1979. Talagrand (2006) and Panchenko (2013) proved it at positive temperature. Auffinger and Chen (2017) established the zero-temperature version with $\Phi(1,x)=|x|$ and proved that a minimizer over the monotone space exists. Jagannath and Tobasco (2016) developed the PDE and SDE tools for the Parisi functional that Section 6.1 of the present paper adapts to non-monotone order parameters. Montanari (2019) gave the first message passing algorithm for the Sherrington–Kirkpatrick case; the present paper (2020) extended it to general mixtures and introduced $\mathscr L$ .

Setting

A mixture is $\xi(t) = \sum_{k\ge2} c_k^2 t^k$ with $\xi(1+\varepsilon) < \infty$ for some $\varepsilon > 0$ ; its derivatives $\xi'$ , $\xi''$ are the termwise differentiated power series, non-negative and non-decreasing on $[0,1]$ .

An order parameter is a function $\gamma : [0,1) \to \mathbb R_{\ge0}$ . The extended space is

\mathscr L = \Bigl\{\gamma : [0,1)\to\mathbb R_{\ge0} : \|\xi''\gamma\|_{\mathrm{TV}[0,t]}<\infty\ \forall t\in[0,1),\ \int_0^1\xi''(t)\gamma(t)\,dt<\infty\Bigr\},

with the weighted distance $\|\gamma_1-\gamma_2\|_{1,\xi''} = \int_0^1\xi''(t)|\gamma_1(t)-\gamma_2(t)|\,dt$ . The non-negative step functions $\mathsf{SF}_+$ are the finite sums $\sum_i a_i\mathbb I_{[t_{i-1},t_i)}$ with $0=t_0<\dots<t_m=1$ and $a_i\ge0$ .

For a terminal condition $f_0$ (convex, continuous, even, non-negative, differentiable off $0$ with $0\le f_0'\le1$ on $(0,\infty)$ ) and $\gamma\in\mathsf{SF}_+$ , the Parisi PDE

\partial_t\Phi + \tfrac12\xi''(t)\bigl(\partial_x^2\Phi + \gamma(t)(\partial_x\Phi)^2\bigr) = 0,\qquad \Phi(1,x) = f_0(x),

has the explicit Cole–Hopf solution $\Phi^\gamma$ : on $[t_{i-1},t_i)$ , $\Phi(t,x) = \gamma_i^{-1}\log\mathbb E\exp\{\gamma_i\Phi(t_i, x+\sqrt{\xi'(t_i)-\xi'(t)}\,G)\}$ with $G\sim\mathsf N(0,1)$ . For $\gamma\in\mathscr L$ , $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n\to\gamma$ in the weighted distance. The Parisi functional is

\mathsf P(\gamma) = \Phi^\gamma(0,0) - \frac12\int_0^1 t\,\xi''(t)\gamma(t)\,dt .

Given a Brownian motion $B$ , the process $X$ solves $dX_t = \xi''(t)\gamma(t)\,\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$ , $X_0 = 0$ . The support of $\gamma$ is $S(\gamma) = \{t\in[0,1):\gamma(t)>0\}$ , and $\overline S(\gamma)$ is its closure in $[0,1)$ .

Formalization targets

Goal: Theorem 5

With $f_0(x) = |x|$ , if $\gamma_*\in\mathscr L$ satisfies $\mathsf P(\gamma_*) = \inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$ , then

\overline S(\gamma_*) = [0,1).

Milestones

The path to the goal, in attack order:

Proposition 6.1(b),(c): on step functions, $\partial_x\Phi$ is non-decreasing with $|\partial_x\Phi|\le1$ , and $\|\Phi^{\gamma_1}-\Phi^{\gamma_2}\|_\infty\le\|\xi''(\gamma_1-\gamma_2)\|_1$ .
Lemma 6.2: these properties pass to $\gamma\in\mathscr L$ .
Lemma 6.5: the SDE has a unique strong solution on $[0,1]$ .
Corollary 6.6: $\mathbb E\{\partial_x\Phi(t_2,X_{t_2})^2\}-\mathbb E\{\partial_x\Phi(t_1,X_{t_1})^2\}=\int_{t_1}^{t_2}\xi''(s)\,\mathbb E\{(\partial_x^2\Phi(s,X_s))^2\}\,ds$ .
Lemma 6.7: the map $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$ .
Proposition 6.8: the first variation $\frac{d}{ds}\mathsf P(\gamma+s\delta)|_{s=0+}=\frac12\int_0^1\xi''\delta\,(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t)\,dt$ .
Lemma 6.9: $S(\gamma)$ is a countable disjoint union of intervals.
Corollary 6.10: $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\}=t$ on $\overline S(\gamma_*)$ and $\ge t$ off it.
Corollary 6.11: $\xi''(t)\,\mathbb E\{\partial_x^2\Phi^{\gamma_*}(t,X_t)^2\}=1$ on $\overline S(\gamma_*)$ .
Lemma 6.12: the law of $X_t$ has a density, bounded below on compact sets, once $\gamma$ vanishes.

Significance

The result. Full support identifies the extended variational principle as one whose minimizers are "nowhere flat". The algorithm of Theorem 3 in the paper follows $\gamma_*$ through incremental steps whose size is set by $\gamma_*$ , and it needs no special treatment of gaps where $\gamma_* = 0$ . The stationarity conditions (Corollaries 6.10–6.11) also characterize minimizers over $\mathscr L$ the way the Auffinger–Chen conditions characterize minimizers over the monotone space. They are the starting point for comparing $\inf_{\mathscr L}\mathsf P$ with the Parisi value.

Formalizing it. The theorem is proved in the paper; nothing here is open mathematics. The paper's proofs rely on cited PDE regularity (Jagannath–Tobasco 2016) and on standard SDE theory, often in one line. The mission produces a machine-checked chain from the explicit Cole–Hopf formula to the support theorem. Along the way it builds the Parisi PDE solution on a non-monotone class, a first-variation formula, and stationarity conditions, none of which have a formal counterpart. No formal statement of the Parisi functional or the Parisi PDE exists on Prove2Me (index search, 2026-10-03).

Difficulty

Two steps resist a direct argument. The first is the first variation (Proposition 6.8): differentiating $\Phi^\gamma(0,0)$ in $\gamma$ requires comparing the SDE for $\gamma$ with the SDE for the perturbed parameter and controlling their difference uniformly, which needs bounds on $\partial_x^2\Phi$ that degenerate as $t\to1$ . The second is the exclusion of gaps: on an interval where $\gamma_*=0$ the PDE is a time-changed heat equation, and the contradiction comes from a strict inequality, which requires the law of $X_t$ to charge every interval (Lemma 6.12). The obvious idea of perturbing $\gamma_*$ upward on a gap only yields the inequality (6.14), which is consistent with a gap; the second-order identity at the gap's endpoints is what closes the argument.

Formalization scope

Conventions committed to in Lean:

The mixture is a coefficient sequence $c$ with $c_0=c_1=0$ ; $\xi,\xi',\xi''$ are explicit series.
Order parameters are functions $\mathbb R\to\mathbb R$ read only on $[0,1)$ . Membership in $\mathscr L$ uses eVariationOn for the total variation and IntegrableOn for the integral; the latter includes the a.e.-measurability that the paper takes for granted.
$\Phi^\gamma$ for step functions is the Cole–Hopf recursion (7.3). For a piece with $\gamma_i = 0$ the formula's limit, the heat semigroup, is used instead of a division by zero. $\mathbb E$ over $G$ is integration against gaussianReal 0 1. For $\gamma\in\mathscr L$ , $\Phi^\gamma$ is a limit along the filter of step functions converging in the weighted $L^1$ distance; it is never "some solution of the PDE".
$\partial_x\Phi$ and $\partial_x^2\Phi$ are iterated derivs in $x$ . Lemma 6.2's weak-derivative claim is stated as "convex and 1-Lipschitz", its equivalent.
The SDE uses the published strong-solution concept EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by zero after time $1$ . The driver is assumed to be a standard Brownian motion (IsBrownianReal). Statements about $X$ hold for every strong solution, which by Lemma 6.5 is unique.
Section 6.1's results are stated for every admissible $f_0$ ; $\mathsf P$ is parametrized by $f_0$ , and Theorem 5 fixes $f_0=|\cdot|$ .
Minimality is " $\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma\in\mathscr L$ ", never a real infimum. $\overline S(\gamma)$ is closure (S γ) ∩ Ico 0 1. Right-continuity of $\gamma_*$ , the paper's convention from p. 28, is a hypothesis.
Disclosed hypothesis $\xi\not\equiv0$ (some $c_k\neq0$ ) on Theorem 5, Corollaries 6.10–6.11 and Lemma 6.12. For $\xi\equiv0$ every $\gamma$ minimizes $\mathsf P$ and $X\equiv0$ , so $\gamma_*\equiv0$ has empty support and each of those statements fails. When $c_2=0$ no minimizer exists (Corollary 6.11 at $t=0$ ), and Theorem 5 is vacuous, as in the paper.
Lemma 6.12's density bound is stated without choosing density versions: $\varepsilon\,\mathrm{Leb}(A)\le\mathbb P(X_t\in A)$ for measurable $A\subseteq[-M,M]$ .

A trivializing formalization is excluded: $\Phi^\gamma$ and $X$ are the paper's objects, built from the data, so the goal cannot be met by choosing a convenient solution, and minimality over $\mathscr L$ cannot be satisfied by a junk infimum.

Not formalized: the weak formulation (6.4) of Lemma 6.2, printed with a wrong boundary term; the stochastic-integral identity (6.7) of Lemma 6.5; the regularity Lemmas 6.3–6.4; Proposition 6.1(a). The paper's algorithmic Theorems 2–4 are out of scope, because they concern algorithms in an informal model of computation and an AMP state-evolution theory that is not part of this mission.

Useful infrastructure beyond this mission: the Cole–Hopf solution and its Lipschitz dependence on $\gamma$ , the Parisi functional on $\mathscr L$ , and the SDE (6.3). Contributions that formalize Itô's formula for these processes or the regularity of $\Phi^\gamma$ are welcome as supporting lemmas.

Selected references

A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904
A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Annals of Probability, 2017. https://arxiv.org/abs/1606.05335
A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proceedings of the AMS, 2016. https://arxiv.org/abs/1502.04398
A. Montanari, Optimization of the Sherrington–Kirkpatrick Hamiltonian, FOCS 2019. https://arxiv.org/abs/1812.10897
M. Talagrand, The Parisi formula, Annals of Mathematics 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
D. Panchenko, The Parisi ultrametricity conjecture, Annals of Mathematics 177(1), 2013. https://doi.org/10.4007/annals.2013.177.1.8

22 thms2 active usersReviewed

Completed

Topology·Captain: Lucas

Assumptions of Physics III: Properties, Quantities and Natural OrdersTextbook

Motivation

This is the third mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing the order-theoretic core of Part II, Chapter 3, "Properties and quantities". The chapter explains when the possibilities of an experiment can be labelled by numbers: a domain can be described by a quantity exactly when its possibilities already carry a linear order whose order topology is the natural topology. It then shows that integer-valued quantities correspond to sparse orders and decidable domains, and real-valued quantities to dense, complete, separable orders. The mission imports the definitions of mission I (Assumptions of Physics I), which must be launched first.

Setting

For an experimental domain $\mathcal D$ with possibilities $X$ and natural topology $\mathcal T_X$ (mission I), a property with values in a topological space $Q$ fully characterizes $\mathcal D$ if it is a homeomorphism $q:X\to Q$ . A quantity is a property whose value space $(Q,\le)$ is linearly ordered and carries the order topology. A linear order on $X$ is a natural order if its order topology equals $\mathcal T_X$ . A linear order is sparse if every chain between two elements is finite and dense if between any two elements there is an infinite chain; it is complete if every non-empty bounded subset has a supremum.

Formalization targets

Goal (Theorem 3.9, Property ordering theorem)

\mathcal D \text{ fully characterized by } (Q,\le,q) \iff \exists \text{ natural order } \preceq \text{ on } X \text{ with } (X,\preceq)\cong(Q,\le).

Milestones

Proposition 3.14: for a natural order, each " $x<x_1$ " is verifiable and $x_1\le x_2\iff$ " $x<x_1$ " $\preccurlyeq$ " $x<x_2$ ".
Proposition 3.42: sparse linear orders are exactly the contiguous subsets of $\mathbb Z$ (up to isomorphism).
Corollary 3.48: dense in the book's sense iff between two elements there is always a third.
Theorem 3.51: dense, complete linear orders with a countable dense subset are exactly the contiguous subsets of $\mathbb R$ .
Theorem 3.44 (1⇔2): natural sparse order iff fully characterized by a discrete quantity.
Proposition 3.46: decidable iff fully characterized by a discrete quantity.
Theorem 3.53 (1⇔2): natural dense complete separable order iff fully characterized by a continuous quantity.
Propositions 3.55, 3.56: the order topology on $\mathbb R$ is generated by rational open intervals, and its open sets are countable unions of open intervals.

Significance

These results say that numerical labels are not added to experimental domains from outside: an integer or real quantity can be assigned only when the domain already has the corresponding order structure, and that order is fixed by narrowness of verifiable statements. Theorem 3.51 is a classical characterization of real intervals that the book takes without proof. The results are proved informally in the book (3.51 is only sketched there); no machine-checked formalization of the domain-level statements is known to the drafters.

Difficulty

Theorem 3.9 needs transport of a linear order along a homeomorphism and the fact that order isomorphisms are homeomorphisms of order topologies. Theorem 3.51 needs the uniqueness of Dedekind completions of a countable dense order and must handle every kind of endpoint behaviour of a contiguous subset of $\mathbb R$ . Proposition 3.46 must cover finite as well as infinite domains: the book's proof uses a bijection with $\mathbb Z$ , which exists only for countably infinite possibility sets.

Formalization scope

Quantities are types Q with Mathlib's LinearOrder, TopologicalSpace and OrderTopology; full characterization is Nonempty (D.Possibility ≃ₜ Q); a natural order is a LinearOrder structure on D.Possibility whose Preorder.topology equals the natural topology. "Contiguous subset" is Set.OrdConnected. For continuous quantities the subset $U\subseteq\mathbb R$ carries its own order topology, as in Definitions 3.6 and 3.52. In Theorems 3.44 and 3.46 the value type ranges over Type, which is enough because sparse orders are countable. Sections 3.3 and 3.6 (references and their ordering, statement (3) of Theorems 3.44 and 3.53, Theorem 3.38) are left for a later mission: they need a separate formal theory of references.

Selected references

G. Carcassi, C. A. Aidala, Assumptions of Physics, Ver. 3.0, December 31, 2025. https://assumptionsofphysics.org/book — Part II, Chapter 3 "Properties and quantities", pp. 169–195.

11 thms2 active usersReviewed

Completed

Topology·Captain: Lucas

Assumptions of Physics II: Inference and Causal Relationships Between Experimental DomainsTextbook

Motivation

This is the second mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing Part II, Chapter 2, "Domain combination and relationships". The chapter asks when the outcome of one experiment can be inferred from another (e.g. temperature from the height of a mercury column), and shows that such inference relationships between verifiable statements correspond to causal relationships between possibilities, which are continuous maps of the natural topologies. It builds on the definitions of the first mission (Assumptions of Physics I), which must be launched first because this mission imports its definition file.

Setting

Statements are truth sets $s\subseteq\Omega$ over the possible assignments $\Omega$ of a fixed logical context; an experimental domain $\mathcal D$ , its possibilities $X$ , verifiable sets $U(s)$ and natural topology are as in mission I. An inference relationship from $\mathcal D_Y$ to $\mathcal D_X$ is a map $r:\mathcal D_Y\to\mathcal D_X$ with $r(s)\equiv s$ ; $\mathcal D_Y$ depends on $\mathcal D_X$ if one exists, and two domains are equivalent if each depends on the other. A causal relationship is a function $f:X\to Y$ between possibilities with $x\preccurlyeq f(x)$ . The combined domain of a countable family of domains is generated by all their statements under finite conjunction and countable disjunction.

Formalization targets

Goal (Theorem 2.10, Experimental Relationship Theorem, with continuity made explicit)

\mathcal D_Y\subseteq\mathcal D_X \iff \exists\, f:X\to Y \text{ continuous with } x\preccurlyeq f(x)\ \forall x\in X.

Milestones

Corollary 2.3: a sub-domain depends on the domain.
Corollary 2.5: domain equivalence is an equivalence relation.
Corollary 2.9: a causal relationship is unique if it exists.
Corollary 2.11: $\mathcal D_X\equiv\mathcal D_Y$ iff there is a homeomorphism $f:X\to Y$ with $x\equiv f(x)$ .
Proposition 2.14: the possibilities of a combined domain are the non-impossible conjunctions $\bigwedge_i x_i$ of possibilities $x_i\in X_i$ .

Significance

Theorem 2.10 is what justifies describing experimental relationships by functions between possibilities rather than by maps between all finite-precision statements, and Corollary 2.11 identifies equivalence of experimental domains with homeomorphisms that respect the statements. Later chapters use these to transport structure between equivalent domains. The results are proved informally in the book; no machine-checked formalization is known to the drafters.

Difficulty

The forward direction requires showing that each possibility of $\mathcal D_X$ lies inside exactly one possibility of $\mathcal D_Y$ and that preimages of verifiable sets are verifiable. The converse is subtler: Definition 2.7 does not require continuity, and the book's Corollary 2.8 ("all causal relationships are continuous") does not hold in general. For example, with $\Omega=\{0,1\}$ , $\mathcal D_X=\{\emptyset,\{1\},\Omega\}$ and $\mathcal D_Y=\{\emptyset,\{0\},\Omega\}$ , the identity on possibilities is a causal relationship but $\mathcal D_Y\not\subseteq\mathcal D_X$ . The goal therefore includes continuity of $f$ explicitly. That is the hypothesis the book's proof of the converse actually uses.

Formalization scope

Domains are ExperimentalDomain Ω on a common type Ω; dependence is ExperimentalDomain.DependsOn (existence of an equivalence-preserving map, which here is the inclusion $\mathcal D_Y\subseteq\mathcal D_X$ ), causal relationships are predicates IsCausalRel on functions between the possibility types, and topological notions are Mathlib's (Continuous, ≃ₜ). The combined domain ExperimentalDomain.combined takes a family over an arbitrary countable index type. Theorem 2.12 (transport of structure) is informal in the source and is not formalized here. Propositions 2.15–2.28 are left out: the residual possibility depends on the choice of basis, and Proposition 2.18 appears to need a stronger independence hypothesis than Definition 2.17 provides. They are candidates for a later mission.

Selected references

G. Carcassi, C. A. Aidala, Assumptions of Physics, Ver. 3.0, December 31, 2025. https://assumptionsofphysics.org/book — Part II, Chapter 2 "Domain combination and relationships", pp. 149–168.

7 thms2 active usersReviewed

Completed

Topology·Captain: Lucas

Assumptions of Physics I: Experimental Domains and Their Natural TopologyTextbook

Motivation

Assumptions of Physics by Gabriele Carcassi and Christine A. Aidala (book, v3.0, 2025) is a programme to derive the mathematical structures of physical theories from explicit physical requirements. Part II, "Physical Mathematics", begins (Chapter 1) by making precise what it means for a statement to be experimentally verifiable, and shows that a single physical requirement (only countably many tests can be run in an indefinite amount of time) is enough to force the familiar structures of point-set topology onto the space of outcomes of any experiment. This mission formalizes that chapter. It is the first mission of a series on the book; all declarations live in the namespace AssumptionsOfPhysics so that later missions can build on them.

Setting

A logical context is represented by its set $\Omega$ of possible truth assignments, and a statement (up to logical equivalence) by its truth set $s\subseteq\Omega$ . Negation, conjunction and disjunction are complement, intersection and union; the certainty is $\Omega$ and the impossibility is $\emptyset$ ; " $s_1$ is narrower than $s_2$ " means $s_1\subseteq s_2$ , and $s_1,s_2$ are compatible when $s_1\cap s_2\neq\emptyset$ .

An experimental domain $\mathcal D$ is a family of statements that contains $\Omega$ and $\emptyset$ , is closed under finite conjunction and countable disjunction, and has a countable basis $B\subseteq\mathcal D$ : every element of $\mathcal D$ is obtained from $B$ by finite conjunctions and countable disjunctions. Its theoretical domain $\bar{\mathcal D}$ is the closure of $\mathcal D$ under negation, finite conjunction and countable disjunction. A possibility is a non-impossible $x\in\bar{\mathcal D}$ that, for every $s\in\bar{\mathcal D}$ , is either narrower than $s$ or incompatible with it; $X$ denotes the set of possibilities. The verifiable set of a statement $s$ is $U(s)=\{x\in X: x\cap s\neq\emptyset\}$ , and the natural topology on $X$ is the topology generated by $\{U(s): s\in\mathcal D\}$ . A domain is decidable if it is closed under negation.

Formalization targets

Goal (Propositions 1.57, 1.61, 1.65)

\mathcal T_X = \{U(s) : s\in\mathcal D\},\qquad (X,\mathcal T_X)\ \text{is second-countable and } T_0 .

Milestones

Proposition 1.37: $\bar{\mathcal D}$ is closed under countable conjunction.
Proposition 1.46: any basis of $\mathcal D$ generates $\bar{\mathcal D}$ by negation and countable operations.
Proposition 1.48: the possibilities are exactly the non-impossible minterms of a basis.
Theorem 1.52: $|X|\le 2^{\aleph_0}$ .
Proposition 1.53: $X$ finite $\iff$ $\mathcal D$ finite $\iff$ $\mathcal D$ has a finite basis.
Proposition 1.56: $s=\bigvee_{x\in U(s)}x$ for $s\in\mathcal D$ .
Propositions 1.57, 1.60, 1.61, 1.65: the verifiable sets are exactly the open sets; $U(B)\cup\{X\}$ is a sub-basis; second countability; $T_0$ .
Proposition 1.66: $T_1$ $\iff$ every possibility is approximately verifiable.
Proposition 1.74 and Theorem 1.76: equivalent characterizations of decidable domains, and decidability $\iff$ discreteness of the natural topology.

Significance

The chapter's results identify the open sets of a topology with verifiable statements and its points with complete experimental answers (possibilities). Second countability and the $T_0$ axiom are thereby derived rather than assumed, and the cardinality bound $|X|\le 2^{\aleph_0}$ limits which mathematical objects can carry experimental meaning. Later chapters of the book (domain combination, properties and quantities, ensemble spaces) rely on these facts. The results are proved informally in the book; no machine-checked formalization of them is known to the drafters. A formalization fixes the precise hypotheses under which they hold (for instance, whether a basis must be countable in Propositions 1.46, 1.48 and 1.60) and provides a reusable library for the rest of the series.

Difficulty

The individual statements are elementary, but several of the book's proofs are informal about two points that a formal proof must handle. First, the possibilities must be shown to cover the space of assignments and to be atoms of $\bar{\mathcal D}$ ; the book argues through minterms of a countable basis, which needs a "disjunctive normal form" for countably generated families. Second, the natural topology is defined via arbitrary unions while experimental domains are only closed under countable disjunction; showing that every open set is still of the form $U(s)$ (Proposition 1.57) requires a second-countability / Lindelöf-type argument rather than direct closure.

Formalization scope

Statements are subsets s : Set Ω of an arbitrary type Ω (possibly empty); the experimental domain is the structure ExperimentalDomain Ω, whose field stmts is the family $\mathcal D$ . Generation by finite conjunction and countable disjunction (FinConjCountDisj) includes the empty conjunction $\Omega$ and the empty disjunction $\emptyset$ ; generation with negation (NegFinConjCountDisj) includes $\Omega$ . Possibilities form the type D.Possibility, which carries the natural topology as an instance; topological notions (SecondCountableTopology, T0Space, T1Space, DiscreteTopology) are Mathlib's. The primitive notion of verifiability (Axiom 1.27) is not modelled separately: membership in $\mathcal D$ is what all results of the chapter use. Statements involving "a basis" quantify over every basis (countable or not), as in the source. Contributions of reusable lemmas, in particular a disjunctive-normal-form lemma for countably generated families of sets, are welcome.

Selected references

G. Carcassi, C. A. Aidala, Assumptions of Physics, Ver. 3.0, December 31, 2025. https://assumptionsofphysics.org/book — Part II, Chapter 1 "Verifiable statements and experimental domains", pp. 101–146.

15 thms2 active usersReviewed

Completed

Captain: Lucas

Assumptions of Physics IV: Ensemble Spaces Are CancellativeTextbook

Motivation

This is the fourth mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing the axiomatic core of Part II, Chapter 4, "Ensemble spaces". The chapter proposes three physically motivated axioms (ensemble, mixture, entropy) that every space of statistical states should satisfy, covering classical probability distributions and quantum density operators alike, and derives from them structure that is usually postulated, for example that mixtures can be "un-mixed" (cancellativity). That is the first step towards embedding ensembles in a vector space. Unlike missions II and III, this mission does not depend on earlier missions.

Setting

An ensemble space is a $T_0$ , second countable topological space $E$ with a continuous mixing operation $(p,a,b)\mapsto pa+\bar pb$ ( $p\in[0,1]$ , $\bar p=1-p$ ) that is idempotent, commutative and associative, and a continuous entropy $S:E\to\mathbb R$ . The entropy is strictly concave, $S(pa+\bar pb)\ge pS(a)+\bar pS(b)$ with equality iff $a=b$ , and bounded above by $I(p,\bar p)+pS(a)+\bar pS(b)$ for a universal function $I$ . Two ensembles are orthogonal, $a\perp b$ , when this bound is saturated, and mixtures preserve orthogonality. An ensemble $c$ is a component of $a$ if $a=pc+\bar pd$ with $p\in(0,1]$ ; two ensembles are separate if they have no common component. The mixing entropy is $MS(a,b)=S(\tfrac12a+\tfrac12b)-\tfrac12S(a)-\tfrac12S(b)$ .

Formalization targets

Goal (Theorem 4.73, Ensemble spaces are cancellative)

pa+\bar pe=pb+\bar pe \text{ for some } p\in(0,1)\implies a=b.

Milestones

Proposition 4.67: orthogonality is irreflexive and symmetric, components are not orthogonal, and orthogonality implies separateness.
Corollary 4.102: $pa+\bar pb=b$ for some $p\in(0,1]$ implies $a=b$ .
Proposition 4.116 (items 1, 2, 3, 5): $MS(a,b)\ge0$ , $MS(a,b)=0\iff a=b$ , $MS(a,b)\le I(\tfrac12,\tfrac12)$ , $MS(a,b)=MS(b,a)$ .

Significance

Cancellativity is what allows affine combinations with negative coefficients, the origin, in this framework, of the vector-space embedding of ensembles (Theorem 4.94) and of negative quasi-probabilities such as Wigner functions. It holds in classical and quantum statistics, and here it is derived from continuity and strict concavity of the entropy instead of being postulated. The results are proved informally in the book; no machine-checked formalization is known to the drafters.

Difficulty

The convex-space axioms are stated in a two-sided associativity form, so every rearrangement of mixtures must be derived from it. The book's proof of cancellativity first propagates the equality $pa+\bar pe=pb+\bar pe$ from one coefficient to all of $(0,1)$ by an iteration $p\mapsto 2p/(1+p)$ , and then uses a limit $p\to1$ together with continuity of mixing and of the entropy. Strict concavity has to be applied only to non-trivial coefficients.

Formalization scope

The structure EnsembleSpace I E bundles Axioms 4.4, 4.7 and 4.55 for a topological space E; mixing coefficients are elements of Mathlib's unitInterval. Real coefficient expressions in the associativity axiom pass through clampI, the projection $\mathbb R\to[0,1]$ , and lie in $[0,1]$ on the stated domain. The universal function $I$ is a parameter. Orthogonality is saturation of the upper bound for every $p\in(0,1)$ . Strict concavity is required for $p\in(0,1)$ only, since at $p\in\{0,1\}$ equality is automatic. The book's Proposition 4.67 uses $I(p,\bar p)>0$ for $p\in(0,1)$ , which follows from universality of $I$ (any space with two distinct ensembles forces it); the milestone carries this as an explicit hypothesis. Items 3 and 4 of Proposition 4.116 in the book use the normalization $I(\tfrac12,\tfrac12)=1$ from Theorem 4.59; item 3 is stated with $I(\tfrac12,\tfrac12)$ and item 4 is omitted. Hull operators, the vector-space embedding (Theorem 4.94), boundedness of lines (Theorem 4.105), the entropic geometry and the standard classical/quantum models (Propositions 4.5, 4.9, 4.56) are left for later missions.

Selected references

G. Carcassi, C. A. Aidala, Assumptions of Physics, Ver. 3.0, December 31, 2025. https://assumptionsofphysics.org/book — Part II, Chapter 4 "Ensemble spaces", pp. 197–284.

5 thms2 active usersReviewed

Completed

Discrete Geometry·Captain: Lucas

Thomson Problem: Seven Electrons and the Known Exact SolutionsOpen Problem

Motivation

The Thomson problem asks for the configuration of $N$ electrons, constrained to the surface of the unit sphere and repelling each other according to Coulomb's law, that minimises the total electrostatic potential energy. J. J. Thomson posed it in 1904 in connection with his "plum pudding" atomic model. The same energy-minimisation question reappears in the arrangement of protein subunits in spherical virus shells, in colloidosomes, in fullerene patterns and in multi-electron bubbles, and it is a special case ( $s=1$ ) of the Riesz $s$ -energy problem on the sphere; the logarithmic variant is Smale's 7th problem.

Despite its elementary statement, the minimum is rigorously known only for a handful of values of $N$ .

Timeline of exact solutions (as reported in the source).

$N=1,2$ : trivial; for $N=2$ the optimum is an antipodal pair with $U=1/2$ .
$N=3$ : equilateral triangle on a great circle — L. Föppl (1912).
$N=4$ : regular tetrahedron (listed in the source without a citation).
$N=6$ : regular octahedron — V. A. Yudin (1992).
$N=12$ : regular icosahedron — N. N. Andreev (1996).
$N=5$ : triangular bipyramid — R. Schwartz (2013), computer-assisted.
$N=7$ : pentagonal bipyramid — long observed numerically; in September 2026 an exact, Lean-kernel-checked proof was claimed (H. Tran, Vals AI).
$N=8$ and $N=20$ : numerically, the optimum is not the cube, resp. the dodecahedron.

Setting

A configuration of $N$ points is a map $x:\{0,\dots,N-1\}\to\mathbb R^3$ . It is admissible if every point lies on the unit sphere, $\|x_i\|=1$ , and the points are pairwise distinct. In units with $e=1$ and $k_e=1$ its Coulomb energy is

U(x)=\sum_{0\le i<j\le N-1}\frac{1}{\|x_i-x_j\|}.

An admissible $x$ is an energy minimiser (solves the Thomson problem for $N$ ) if $U(x)\le U(y)$ for every admissible $N$ -point configuration $y$ .

Explicit candidate configurations are fixed in the definitions file: the antipodal pair ( $N=2$ ), an equatorial equilateral triangle ( $N=3$ ), the regular tetrahedron ( $N=4$ ), the triangular bipyramid ( $N=5$ ), the regular octahedron ( $N=6$ ), the pentagonal bipyramid ( $N=7$ : the two poles plus a regular pentagon $(\cos\tfrac{2\pi k}5,\sin\tfrac{2\pi k}5,0)$ on the equator) and the regular icosahedron ( $N=12$ ).

Formalization targets

Goal: $N=7$

\text{the pentagonal bipyramid is an energy minimiser for } N=7 .

This asserts admissibility of the seven points and the inequality $U(P_7)\le U(y)$ against every admissible seven-point configuration $y$ . It fixes no numerical value of the minimum and does not assert uniqueness.

Milestones: the other known exact solutions

N=1:\ U\equiv 0;\qquad N=2:\ \text{antipodal pair optimal},\ U=\tfrac12;

N=3,4,5,6,12:\ \text{triangle, tetrahedron, triangular bipyramid, octahedron, icosahedron are energy minimisers.}

Significance

The result. Among the values of $N$ listed in the source, $N=7$ is the smallest one whose optimum was, until the 2026 claim, supported only by numerical computation; the cases $N\le 6$ and $N=12$ were settled earlier. Settling $N=7$ extends the short list of rigorously known Thomson minimisers.

Formalizing it. The $N=7$ result reported in the source is recent and described there as a claimed Lean-kernel-checked proof; a formalization on this platform against a public, reviewed statement would corroborate it independently. For the milestones, the source attributes the $N=3,5,6,12$ cases to published proofs (Föppl 1912, Schwartz 2013, Yudin 1992, Andreev 1996); the source does not describe machine-checked proofs of these, and each is a self-contained formalization target.

Difficulty

The energy is a non-convex function on the configuration space $(S^2)^N$ with many critical points, so numerical minimisation — which is how most entries of the source's table of smallest known energies were obtained — does not certify global optimality. The $N=5$ case, the most recent classical entry before $N=7$ , was resolved only with a computer-assisted proof (Schwartz 2013).

Formalization scope

Points live in EuclideanSpace ℝ (Fin 3); configurations are functions Fin N → EuclideanSpace ℝ (Fin 3). Admissibility requires unit norm and injectivity (distinct points), matching the source's " $N$ distinct points". The energy sums $1/\mathrm{dist}(x_i,x_j)$ over $i<j$ ; Lean's $1/0=0$ convention is harmless because coincident points are excluded by admissibility. The candidate configurations are fixed in one particular orientation; since the energy is invariant under orthogonal maps and relabelling, this is no loss of generality. The statement " $x$ is an energy minimiser" includes admissibility of $x$ itself, so the goal cannot be satisfied by a degenerate candidate.

Reusable infrastructure welcome: energy invariance under isometries and permutations, existence of minimisers by compactness, linear-programming (Delsarte–Yudin) bounds on the sphere, and interval-arithmetic tooling for certified numerical bounds.

Selected references

Wikipedia, Thomson problem (source of this mission). https://en.wikipedia.org/wiki/Thomson_problem
J. J. Thomson, On the Structure of the Atom…, Philosophical Magazine 7 (1904), 237–265.
L. Föppl, Stabile Anordnungen von Elektronen im Atom, J. Reine Angew. Math. 141 (1912), 251–301. https://doi.org/10.1515/crll.1912.141.251
V. A. Yudin, The minimum of potential energy of a system of point charges, Discrete Math. Appl. 3 (1993), 75–81. https://doi.org/10.1515/dma.1993.3.1.75
N. N. Andreev, An extremal property of the icosahedron, East J. Approx. 2 (1996), 459–462.
R. Schwartz, The five-electron case of Thomson's problem, Experimental Mathematics 22 (2013), 157–186. https://arxiv.org/abs/1001.3702
S. Smale, Mathematical Problems for the Next Century, Math. Intelligencer 20 (1998), 7–15. https://doi.org/10.1007/bf03025291
Vals AI, A Lean Proof of the Thomson Problem for Seven Electrons (2026). https://www.vals.ai/blogs/thomson-n7-lean-proof

23 thms2 active usersReviewed

Analysis Functional Analysis Partial Differential Equations·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics XII: Self-Adjointness and Essential Spectrum of One-Particle Schrödinger OperatorsTextbook

Motivation

The Hamiltonian of a single nonrelativistic particle in $\mathbb R^n$ moving in a potential $V$ is the Schrödinger operator $H = -\Delta + V$ acting in $L^2(\mathbb R^n)$ . Before anything can be said about the dynamics or the energy levels of such a particle, one must know that $H$ is a genuine observable: a self-adjoint operator on a specified domain. For potentials that decay at infinity one also wants the coarse structure of the spectrum, namely that it is bounded below and that everything below the continuum threshold $0$ consists of isolated eigenvalues of finite multiplicity. The hydrogen atom, with the Coulomb potential $-\gamma/|x|$ in three dimensions, is the central example.

The self-adjointness results go back to T. Kato's 1951 paper on the Hamiltonians of atoms; the identification of the essential spectrum through relatively compact perturbations is due to H. Weyl's theorem and its later extensions. This mission follows Chapter 10 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), Sections 10.1, 10.2, 10.4 and 10.5.

Setting

$L^2(\mathbb R^n)$ is the complex Hilbert space of square integrable functions with respect to Lebesgue measure. The free Schrödinger operator is $H_0 = -\Delta$ with domain the Sobolev space $H^2(\mathbb R^n) = \{ f \in L^2 \mid |p|^2 \hat f(p) \in L^2 \}$ ; equivalently, $H_0$ is the inverse Fourier transform of the maximally defined multiplication by $p^2$ . Units are $\hbar = 1$ and mass $m = 1/2$ .

A real function $V$ acts by the multiplication operator $(Vf)(x) = V(x) f(x)$ on its maximal domain $\{f \in L^2 \mid Vf \in L^2\}$ . The sum $H_0 + V$ is defined on $\mathfrak D(H_0) \cap \mathfrak D(V)$ . $L^\infty_\infty(\mathbb R^n)$ denotes the bounded Borel functions vanishing at infinity, and $C_c^\infty(\mathbb R^n)$ the smooth compactly supported functions.

For a linear operator $A$ , the resolvent $R_A(z) = (A - z)^{-1}$ exists when $A - z$ maps $\mathfrak D(A)$ bijectively onto $L^2$ with bounded inverse; the resolvent set $\rho(A)$ collects such $z$ and $\sigma(A) = \mathbb C \setminus \rho(A)$ . The point spectrum $\sigma_p(A)$ is the set of eigenvalues; the discrete spectrum $\sigma_d(A)$ consists of the eigenvalues that are isolated in $\sigma(A)$ and have finite-dimensional eigenspace; the essential spectrum is $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$ . An operator $K$ is relatively compact with respect to $A$ if $\mathfrak D(A) \subseteq \mathfrak D(K)$ and $K R_A(z)$ is compact for one $z \in \rho(A)$ . $A$ is bounded from below if $\langle \psi, A\psi\rangle \ge \gamma\|\psi\|^2$ on $\mathfrak D(A)$ for some real $\gamma$ , and a subspace is a core of a closed operator if the closure of the restriction to it is the operator itself.

The hydrogen Hamiltonian is $H^{(1)} = -\Delta - \gamma/|x|$ on $L^2(\mathbb R^3)$ . A function in $L^2(\mathbb R^n)$ is positive if it is $\ge 0$ a.e. and not a.e. zero, and strictly positive if it is $> 0$ a.e.; a bounded operator is positivity improving if it maps positive functions to strictly positive ones.

Formalization targets

Goal: self-adjointness and essential spectrum (Theorem 10.2)

Let $n \ge 1$ and $V$ real with $V \in L^\infty_\infty(\mathbb R^n)$ if $n > 3$ and $V \in L^\infty_\infty(\mathbb R^n) + L^2(\mathbb R^n)$ if $n \le 3$ . Then $V$ is relatively compact with respect to $H_0$ , and $H = H_0 + V$ has domain $H^2(\mathbb R^n)$ , is self-adjoint and bounded from below, satisfies

\sigma_{ess}(H) = [0,\infty),

and has $C_c^\infty(\mathbb R^n)$ as a core.

Milestones

Sobolev bound (Lemma 10.1). For $n \le 3$ , every $\psi \in H^2(\mathbb R^n)$ is continuous and vanishes at infinity, and for every $a > 0$ there is $b > 0$ with $\|\psi\|_\infty \le a\|H_0\psi\| + b\|\psi\|$ on $H^2(\mathbb R^n)$ .
Virial theorem (Theorem 10.3). If $V$ is homogeneous of degree $-1$ under dilations, every normalized eigenfunction of $H_0 + V$ with eigenvalue $\lambda$ satisfies $\lambda = -\langle\psi, H_0\psi\rangle = \frac12\langle\psi, V\psi\rangle$ ; in particular $\lambda < 0$ .
Hydrogen spectrum (Corollary 10.4). For $\gamma > 0$ , $\sigma_p(H^{(1)}) = \sigma_d(H^{(1)})$ is a strictly increasing sequence of negative numbers converging to $0$ .
Hydrogen eigenvalues (Theorem 10.9, eigenvalue part). For $\gamma > 0$ the eigenvalues of $H^{(1)}$ are $E_n = -(\gamma/(2(n+1)))^2$ , $n \in \mathbb N_0$ .
Perron–Frobenius for positivity improving operators (Theorem 10.11). If $A$ is bounded, self-adjoint, real and positivity improving and $\|A\|$ is an eigenvalue, it is simple with a strictly positive eigenfunction.
Nondegenerate ground state (Theorem 10.12). If $H_0 + V$ is self-adjoint, bounded below, has $C_c^\infty$ as a core, and $E_0 = \min\sigma(H)$ is an eigenvalue, then $E_0$ is simple with a strictly positive eigenfunction.

Significance

The result. Theorem 10.2 is the existence theorem for one-particle quantum mechanics with decaying potentials. It makes $H_0 + V$ an observable on the natural domain $H^2$ , guarantees a lowest energy, and places the continuum exactly at $[0,\infty)$ , so that all spectral information below zero is carried by bound states. Its three-dimensional case covers the Coulomb potential, and the same scheme (relative boundedness, Kato–Rellich, relative compactness, Weyl) is the template for the $N$ -body HVZ theorem. The virial theorem, the qualitative and the explicit hydrogen spectrum, and the nondegeneracy of ground states are the standard first applications.

Formalizing it. None of these statements is formalized. Mathlib has the $L^2$ Fourier transform, tempered distributions and Sobolev spaces on the distribution side, and LinearPMap with adjoints and closures, but no free Schrödinger operator as an unbounded operator on $L^2$ , no resolvent set or essential spectrum for unbounded operators, and no self-adjointness theorem for $-\Delta + V$ . The mission asks for proofs of Teschl's statements and, with them, a reusable definition of $H_0$ on $H^2(\mathbb R^n)$ and of maximally defined multiplication operators.

Difficulty

The goal combines several chapters of the book. A proof needs self-adjointness of $H_0$ on $H^2$ via the Fourier transform, the Sobolev bound of Lemma 10.1 to get $\mathfrak D(H_0) \subseteq \mathfrak D(V)$ with relative bound zero, the Kato–Rellich theorem, compactness of operators of the form $g(x)f(p)$ (Lemma 7.11) to obtain relative compactness, Weyl's theorem on the invariance of the essential spectrum, $\sigma(H_0) = [0,\infty)$ with no eigenvalues, and the fact that $C_c^\infty$ is a core for $H_0$ . None of these intermediate results is in Mathlib for unbounded operators.

The milestones add their own difficulties: the virial theorem requires the dilation group and a derivative argument on domains; Corollary 10.4 requires a variational argument producing infinitely many negative eigenvalues; Theorem 10.9 requires separation of variables in spherical coordinates and the Laguerre polynomials; and Theorem 10.12 uses the Trotter product formula and strong resolvent convergence to transfer positivity from $e^{-tH_0}$ to $e^{-tH}$ .

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure and $L^2(\mathbb R^n)$ is Mathlib's Lp ℂ 2 volume, a separable complex Hilbert space. Unbounded operators are Mathlib LinearPMaps, sums of unbounded operators are LinearPMap sums on the intersection of domains, self-adjointness is Mathlib's IsSelfAdjoint, and "core" is LinearPMap.HasCore. The resolvent is the bounded two-sided inverse of $A - z$ ; $\rho(A)$ , $\sigma(A)$ , $\sigma_p$ , $\sigma_d$ and $\sigma_{ess}$ are defined from it, and Mathlib's Banach-algebra spectrum is not used. Compactness is IsCompactOperator.

The Fourier transform is Mathlib's unitary $L^2$ transform with kernel $e^{-2\pi i\langle x,\xi\rangle}$ , not Teschl's $(2\pi)^{-n/2}e^{-ipx}$ . $H_0$ is defined as $\mathcal F^{-1}(2\pi|\xi|)^2\mathcal F$ and $H^2$ as $\{f \mid (2\pi|\xi|)^2 \mathcal F f \in L^2\}$ ; both coincide with the book's objects, independently of the normalization. No projection-valued measure or functional calculus is taken as data. $C_\infty(\mathbb R^n)$ is Mathlib's space of continuous functions vanishing at infinity, and positivity of complex values is taken in ComplexOrder.

The virial hypothesis $U(-s)VU(s) = e^{-s}V$ is stated as $V(e^s x) = e^{-s}V(x)$ for almost every $x$ , for every $s$ , which is what the operator identity means for a multiplication operator. Corollary 10.4's index set $\{E_{j-1}\}_{j\in\mathbb N_0}$ is read as the sequence $E_0, E_1, \dots$ . Only the eigenvalue formula of Theorem 10.9 is included, not its explicit eigenbasis.

A trivializing formalization is ruled out: the only hypotheses of the goal are the function-space conditions on $V$ and $n \ge 1$ . Neither $\mathfrak D(H_0) \subseteq \mathfrak D(V)$ , a relative bound below one, nor closedness of $H_0 + V$ is assumed; the equality of the domain with $H^2(\mathbb R^n)$ and the relative compactness of $V$ are conclusions. The essential spectrum requires all three of "eigenvalue", "isolated" and "finite multiplicity" in its complement, so $[0,\infty)$ is a genuine identification.

Selected references

G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009, Chapter 10. https://doi.org/10.1090/gsm/099
T. Kato, Fundamental properties of Hamiltonian operators of Schrödinger type, Transactions of the AMS 70 (1951), 195–211. https://doi.org/10.1090/S0002-9947-1951-0041010-X
M. Reed and B. Simon, Methods of Modern Mathematical Physics II: Fourier Analysis, Self-Adjointness (Section X.2) and IV: Analysis of Operators (Sections XIII.4, XIII.12), Academic Press, 1975, 1978.
H. L. Cycon, R. G. Froese, W. Kirsch and B. Simon, Schrödinger Operators, Springer, 1987.

20 thms2 active usersReviewed

Completed

Analysis Functional Analysis·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics IV: The Min-Max Principle and Temple's InequalityTextbook

Motivation

In quantum mechanics the energy levels of a system are the eigenvalues of a self-adjoint Hamiltonian $A$ , and for almost every Hamiltonian of interest (atoms with more than one electron, molecules) they cannot be computed in closed form. What can be computed are expectation values $\langle \psi, A\psi\rangle$ of explicit trial functions $\psi$ . The min-max principle turns such numbers into rigorous statements about the eigenvalues: every trial computation gives an upper bound, and the optimal choices reproduce the eigenvalues exactly. It goes back to Fischer (1905) for quadratic forms in finitely many variables and to Courant (1920) for differential operators; Temple (1928) added the matching lower bound. This mission formalizes the version for unbounded self-adjoint operators with essential spectrum, as stated in Chapter 4 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), where eigenvalues below the essential spectrum are characterized and estimated.

Setting

Let $\mathfrak H$ be a complex Hilbert space, with inner product $\langle\cdot,\cdot\rangle$ conjugate linear in the first argument. An operator $A$ is a linear map defined on a subspace $\mathfrak D(A) \subseteq \mathfrak H$ , its domain; $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A$ equals its adjoint. The resolvent set $\rho(A)$ is the set of $z \in \mathbb C$ for which $A - z : \mathfrak D(A) \to \mathfrak H$ is a bijection with bounded inverse, and the spectrum is $\sigma(A) = \mathbb C \setminus \rho(A)$ . For self-adjoint $A$ , $\sigma(A) \subseteq \mathbb R$ .

For $z \in \mathbb C$ the eigenspace is $\operatorname{Ker}(A - z) = \{\psi \in \mathfrak D(A) \mid A\psi = z\psi\}$ ; $z$ is an eigenvalue when it is nonzero, and its dimension is the multiplicity. The discrete spectrum $\sigma_d(A)$ consists of the eigenvalues that are isolated points of $\sigma(A)$ and have finite multiplicity, and the essential spectrum is $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$ .

Let $\Sigma = \inf \sigma_{ess}(A) \in [-\infty, +\infty]$ ( $+\infty$ if $\sigma_{ess}(A)$ is empty). The numbers $E_1 \le E_2 \le E_3 \le \cdots$ are the eigenvalues of $A$ below $\Sigma$ , listed in increasing order and repeated according to multiplicity; if there are only $N$ of them, $E_n = \Sigma$ for $n > N$ . For vectors $\psi_1, \dots, \psi_m \in \mathfrak H$ let

U(\psi_1, \dots, \psi_m) = \{\psi \in \mathfrak D(A) \mid \|\psi\| = 1,\ \psi \perp \psi_1, \dots, \psi_m\}.

Some statements involve the spectral projections $P_A(\Omega)$ of $A$ , for Borel sets $\Omega \subseteq \mathbb R$ : the projection-valued measure with $A = \int \lambda\, dP_A(\lambda)$ . With the spectral measures $\mu_\psi(\Omega) = \langle \psi, P_A(\Omega)\psi\rangle$ , the form domain is $\mathfrak Q(A) = \{\psi \mid \int |\lambda|\, d\mu_\psi(\lambda) < \infty\}$ , and on it $\langle \psi, A\psi\rangle$ means $\int \lambda\, d\mu_\psi(\lambda)$ .

Formalization targets

Goal: the min-max principle (Theorem 4.10)

For self-adjoint $A$ and every $n \ge 1$ ,

E_n = \sup_{\psi_1, \dots, \psi_{n-1} \in \mathfrak H} \ \inf_{\psi \in U(\psi_1, \dots, \psi_{n-1})} \langle \psi, A\psi\rangle .

Both sides are extended real numbers; the infimum over an empty set is $+\infty$ .

Milestones

Theorem 2.19 (the case $n = 1$ and its mirror image): $\inf \sigma(A) = \inf_{\psi \in \mathfrak D(A), \|\psi\| = 1} \langle\psi, A\psi\rangle$ and $\sup \sigma(A) = \sup_{\psi \in \mathfrak D(A), \|\psi\| = 1} \langle\psi, A\psi\rangle$ .
Theorem 4.12 (i): if $\psi_1, \dots, \psi_k \in \mathfrak Q(A)$ are linearly independent and $\langle \psi, A\psi\rangle < \lambda\|\psi\|^2$ for every nonzero $\psi \in \operatorname{span}\{\psi_j\}$ , then $\dim \operatorname{Ran} P_A((-\infty,\lambda)) \ge k$ ; with $>$ , $\dim \operatorname{Ran} P_A((\lambda,\infty)) \ge k$ .
Theorem 4.12 (ii): if $\psi_1, \dots, \psi_k \in \mathfrak D(A)$ are linearly independent, $\lambda_1 < \lambda_2$ , and $\|(A - \tfrac{\lambda_2+\lambda_1}{2})\psi\| < \tfrac{\lambda_2-\lambda_1}{2}\|\psi\|$ for every nonzero $\psi$ in their span, then $\dim \operatorname{Ran} P_A((\lambda_1,\lambda_2)) \ge k$ .
Corollary 4.11: if $A, B$ are self-adjoint, $\mathfrak D(A) \subseteq \mathfrak D(B)$ and $\langle \psi, (A - B)\psi\rangle \ge 0$ on $\mathfrak D(A)$ , then $E_n(A) \ge E_n(B)$ for all $n \ge 1$ .
Theorem 4.13 (Temple's inequality): if $\lambda_1 < \lambda_2$ , $\psi \in \mathfrak D(A)$ , $\|\psi\| = 1$ , $\lambda = \langle \psi, A\psi\rangle \in (\lambda_1, \lambda_2)$ and $\sigma(A) \cap (\lambda_1, \lambda_2) = \{E\}$ , then

\lambda - \frac{\|(A-\lambda)\psi\|^2}{\lambda_2 - \lambda} \le E \le \lambda + \frac{\|(A-\lambda)\psi\|^2}{\lambda - \lambda_1}.

Significance

The min-max principle is the standard tool for comparing eigenvalues of different operators: Corollary 4.11 (monotonicity under operator inequalities) follows from it, and with it the stability of eigenvalues under perturbations, Dirichlet–Neumann bracketing and the Rayleigh–Ritz method used in computational quantum chemistry. Theorem 4.12 converts a finite-dimensional computation into a lower bound for the number of eigenvalues in an interval, and Temple's inequality supplies lower bounds on an eigenvalue to complement the variational upper bounds, which is what makes numerical eigenvalue enclosures rigorous.

All of these results are classical and proved in the literature. What is not available is a machine-checked version for unbounded operators: Mathlib has the Courant–Fischer characterization only for finite-dimensional or compact self-adjoint operators, and existing formal developments of Temple's inequality and min-max levels treat bounded operators. This mission formalizes the unbounded case, with the essential spectrum and the counting of eigenvalues by multiplicity made explicit, and with the edge cases (operators unbounded below, empty essential spectrum) covered by extended-real values.

Difficulty

The central difficulty is that $E_n$ is defined by spectral data (which points of the spectrum are isolated eigenvalues of finite multiplicity, and how many there are below a given level), while the right-hand side is defined by expectation values on the domain. Relating the two needs the spectral theorem for unbounded operators: for every level below $\Sigma$ the spectral subspace must be shown to be finite dimensional and spanned by eigenvectors, and for the level $\Sigma$ itself one needs infinite-dimensional spectral subspaces in every neighbourhood, which is where the essential spectrum enters. When $E_n = \Sigma$ the supremum and infimum need not be attained, so the finite-dimensional argument with eigenvectors does not transfer. For Corollary 4.11 and Temple's inequality the hypotheses concern only the operator and one vector, while the conclusions concern the spectrum.

Formalization scope

The formalization uses Lean 4 with Mathlib. Operators are partially defined linear maps (LinearPMap, H →ₗ.[ℂ] H) on a complex Hilbert space; self-adjointness is Mathlib's IsSelfAdjoint, which includes a dense domain. The Hilbert space is not assumed separable. The spectrum is the resolvent spectrum defined above, not Mathlib's Banach-algebra spectrum, and for self-adjoint operators it enters through its real points. Eigenspace dimensions are cardinals (Module.rank). $E_n$ is defined from the spectrum, the essential spectrum and these dimensions, as an element of EReal, indexed from $n = 1$ ; if $A$ is unbounded below its value is $-\infty$ , and if the essential spectrum is empty and the eigenvalues run out it is $+\infty$ . The min-max identity is stated in EReal, with $\langle\psi, A\psi\rangle$ entering through its real part.

A formalization that defines $E_n$ as the min-max expression itself would make the goal true by definition. This is ruled out: $E_n$ is defined only from the spectrum, the essential spectrum and the dimensions of eigenspaces.

The spectral theorem is not part of this mission. Theorem 4.12 takes a projection-valued measure $P$ on the Borel sets of $\mathbb R$ as data, together with the hypothesis that $A = \int \lambda\, dP(\lambda)$ (domain $\{\psi \mid \int \lambda^2 d\mu_\psi < \infty\}$ and $\langle\psi, A\psi\rangle = \int \lambda\, d\mu_\psi$ ), which is the form the spectral theorem guarantees; $P_A$ is then $P$ , and $\mathfrak Q(A)$ and the quadratic form are defined from it. Nothing else the book derives is taken as a hypothesis. The goal, Theorem 2.19, Corollary 4.11 and Temple's inequality use no projection-valued measure. Corollary 4.11 states the domain inclusion $\mathfrak D(A) \subseteq \mathfrak D(B)$ explicitly, as the meaning of $A - B \ge 0$ .

A complete development needs the spectral theorem for unbounded self-adjoint operators (or an equivalent functional calculus), the identification of $\sigma_{ess}$ with the points where spectral projections have infinite rank, and the orthogonality of eigenspaces. These are reusable across the rest of the book. Proofs of any milestone, and of lemmas connecting the resolvent spectrum with spectral projections, are welcome.

Selected references

G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009. doi:10.1090/gsm/099. Theorem 2.19 (p. 77), Section 4.3–4.4 (pp. 117–120), essential spectrum (p. 145).
E. Fischer, Über quadratische Formen mit reellen Koeffizienten, Monatshefte für Mathematik und Physik 16 (1905), 234–249. doi:10.1007/BF01693781.
R. Courant, Über die Eigenwerte bei den Differentialgleichungen der mathematischen Physik, Mathematische Zeitschrift 7 (1920), 1–57. doi:10.1007/BF01199396.
G. Temple, The theory of Rayleigh's principle as applied to continuous systems, Proceedings of the Royal Society of London A 119 (1928), 276–293. doi:10.1098/rspa.1928.0098.

15 thms2 active usersReviewed

Completed

Analysis Functional Analysis·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics XI: Weyl's Limit Circle / Limit Point AlternativeTextbook

Why the endpoint behaviour of Sturm–Liouville operators matters

A quantum particle on a line or half-line, and the radial part of a particle in a spherically symmetric potential, are described by a Sturm–Liouville expression

\tau f = \frac{1}{r}\big(-(pf')' + qf\big)

on an interval $I = (a, b)$ . The expression alone does not define a Hamiltonian: a self-adjoint operator needs a domain, and on a general interval the choice of domain is a choice of boundary conditions at $a$ and $b$ . Whether a boundary condition is needed at all depends on the behaviour of $\tau$ near the endpoint. H. Weyl settled this in 1910 (Math. Ann. 68, 220–269) with his limit circle / limit point dichotomy: at each endpoint either all solutions of $\tau u = z u$ are square integrable near it and a boundary condition must be imposed, or they are not and no condition is possible. This mission formalizes Sections 9.1–9.2 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), which develop the theory for coefficients that are only locally integrable, and culminate in Theorem 9.9, the Weyl alternative.

Setting

Let $-\infty \le a < b \le \infty$ and $I = (a,b)$ . The coefficients satisfy: $p^{-1} \in L^1_{loc}(I)$ with $p > 0$ ; $q \in L^1_{loc}(I)$ real-valued; $r \in L^1_{loc}(I)$ with $r > 0$ . The Hilbert space is $L^2(I, r\,dx)$ with $\langle f, g\rangle = \int_a^b f^* g\, r\,dx$ .

A function $f$ is locally absolutely continuous, $f \in AC_{loc}(I)$ , if it is an indefinite integral of a locally integrable function on $I$ . The equation $\tau f = g$ means that $f$ and its quasi-derivative $pf'$ both lie in $AC_{loc}(I)$ and $-(pf')' + qf = rg$ almost everywhere. A solution of $(\tau - z)u = 0$ , $z \in \mathbb{C}$ , is a complex-valued $u$ with $\tau u = z u$ in this sense. The maximal domain is

\mathfrak{D}(\tau) = \{ f \in L^2(I, r\,dx) \mid f, pf' \in AC_{loc}(I),\ \tau f \in L^2(I, r\,dx) \}.

The modified Wronskian is $W_x(f_1, f_2) = f_1(x)(pf_2')(x) - (pf_1')(x) f_2(x)$ , with no complex conjugation, and $W_a(f_1, f_2) = \lim_{x \to a} W_x(f_1, f_2)$ , $W_b$ likewise.

$\tau$ is limit circle (l.c.) at $a$ if there is a $v \in \mathfrak{D}(\tau)$ with $W_a(v^*, v) = 0$ and $W_a(v, f) \ne 0$ for some $f \in \mathfrak{D}(\tau)$ ; otherwise it is limit point (l.p.) at $a$ . The same holds at $b$ . A function $u$ is square integrable near $a$ if $\int_a^c |u|^2 r\,dx < \infty$ for some $c \in I$ .

Formalization targets

Goal: the Weyl alternative (Theorem 9.9)

For every Sturm–Liouville expression as above,

\tau \text{ is l.c. at } a \iff \text{for one } z_0 \in \mathbb{C}, \text{ all solutions of } (\tau - z_0)u = 0 \text{ are square integrable near } a,

and if $\tau$ is l.c. at $a$ , then for every $z \in \mathbb{C}$ all solutions of $(\tau - z)u = 0$ are square integrable near $a$ . The same two statements hold at $b$ .

Milestones

Theorem 9.1. For $rg \in L^1_{loc}(I)$ , $c \in I$ , $\alpha, \beta \in \mathbb{C}$ , the problem $(\tau - z) f = g$ , $f(c) = \alpha$ , $(pf')(c) = \beta$ has a unique solution, entire in $z$ .
Lemma 9.2. If $u_1, u_2$ solve $(\tau - z)u = 0$ with $W(u_1, u_2) = 1$ , every solution of $(\tau - z)f = g$ is given by the variation-of-constants formula (9.10).
Eq. (9.7). For $f, g \in \mathfrak{D}(\tau)$ the limits $W_a(g^*, f)$ , $W_b(g^*, f)$ exist and $\langle g, \tau f\rangle = W_a(g^*, f) - W_b(g^*, f) + \langle \tau g, f\rangle$ (the printed $W_b - W_a$ has the wrong sign for the Wronskian (9.5)).
Lemma 9.5. If $v \in \mathfrak{D}(\tau)$ , $W_a(v^*, v) = 0$ and $W_a(v^*, \hat f) \ne 0$ for some $\hat f \in \mathfrak{D}(\tau)$ , then $W_a(v, f) = 0 \Leftrightarrow W_a(v, f^*) = 0$ , and $W_a(v, f) = W_a(v, g) = 0 \Rightarrow W_a(g^*, f) = 0$ .
Theorem 9.6. The operator $Af = \tau f$ on $\mathfrak{D}(A) = \{ f \in \mathfrak{D}(\tau) \mid W_a(v, f) = 0 \text{ if l.c. at } a,\ W_b(w, f) = 0 \text{ if l.c. at } b\}$ is self-adjoint, and the set $\mathfrak{D}_1$ of (9.21) is a core.
Lemma 9.7. For $z \in \rho(A)$ there are solutions $u_a$ , $u_b$ of $(\tau - z)u = 0$ , square integrable near $a$ resp. $b$ and satisfying the boundary condition there, and $(A - z)^{-1}$ is the integral operator with the Green function (9.28).

Significance

The Weyl alternative turns a question about operators into a question about an ordinary differential equation. Whether a Schrödinger operator $-d^2/dx^2 + q$ on a half-line needs a boundary condition at infinity, or whether $-\Delta + V$ with a radial potential is essentially self-adjoint on smooth functions, reduces to checking square integrability of solutions for a single value of $z$ . Combined with Theorem 9.6 it classifies the self-adjoint realizations with separated boundary conditions: none at an l.p. endpoint, a one-parameter family at an l.c. endpoint. The Green function of Lemma 9.7 is the starting point of the spectral theory of one-dimensional Schrödinger operators: Weyl–Titchmarsh $m$ -functions, spectral transformations, and oscillation theory in the rest of Teschl's Chapter 9.

The results are classical and proved in many textbooks. The formal content is new: Mathlib has unbounded operators (LinearPMap) and their adjoints, but no Sturm–Liouville theory, no quasi-derivatives, no ODE existence theorem for measurable, locally integrable coefficients (its Picard–Lindelöf theorem needs Lipschitz right-hand sides), and no self-adjoint realizations of differential operators on general intervals.

Difficulty

The definition of limit circle refers only to $\mathfrak{D}(\tau)$ and boundary limits of Wronskians, while the conclusion is about all solutions of an ODE for all $z \in \mathbb{C}$ . The two sides are linked only through self-adjoint operators: the passage from boundary Wronskians to square integrable solutions goes through the resolvent of a self-adjoint realization, which exists only for $z \in \rho(A)$ , and so only for nonreal $z$ in general. Extending the conclusion to real $z$ , where no resolvent is available, needs an argument of a different kind. On the ODE side, the coefficients are only locally integrable, so solutions are merely locally absolutely continuous, equations hold only almost everywhere, and every boundary quantity is a limit whose existence must itself be established.

Formalization scope

Interval and coefficients. The structure SLData bundles $a, b \in$ EReal with $a < b$ (infinite endpoints allowed), $p, q, r : \mathbb{R} \to \mathbb{R}$ , and the standing hypotheses (i)–(iii) of p. 181; $p, r > 0$ pointwise on $I$ . $L^2(I, r\,dx)$ is Lp ℂ 2 for the measure $r\,dx$ on $I$ .
Regularity. $AC_{loc}(I)$ is encoded by its integral characterization. The quasi-derivative $pf'$ is the continuous function $f^{[1]} \in AC_{loc}(I)$ with $f(y) - f(x) = \int_x^y f^{[1]}/p$ , chosen by Classical.choose (it is unique on $I$ ). $\tau f = g$ is $(pf')(y) - (pf')(x) = \int_x^y (qf - rg)$ with a local integrability clause. No smoothness of the coefficients and no $C^2$ solutions are assumed.
Boundary Wronskians $W_a$ , $W_b$ are Filter.limUnder along $x \to a$ , $x \to b$ inside $I$ . They are used only on $\mathfrak{D}(\tau)$ , where milestone (9.7) states that the limits exist. In Lemma 9.7, where $u_a$ need not lie in $\mathfrak{D}(\tau)$ , the boundary condition is stated as a convergence.
Operators. Operators in $L^2(I, r\,dx)$ are LinearPMaps; self-adjointness is Mathlib's IsSelfAdjoint. Theorem 9.6 asserts that an operator with graph $\{(f, \tau f) \mid f \in \mathfrak{D}(A)\}$ exists (i.e. is well defined) and is self-adjoint. $\rho(A)$ and $(A - z)^{-1}$ follow Teschl (2.66): a bounded two-sided inverse of $A - z$ . No projection-valued measure or functional calculus is used.
Corrections to the printed text. Lemma 9.7 says "a solution $u_a$ of $(\tau - z)u = g$ "; the proof and (9.28) need $(\tau - z)u = 0$ , which is what is stated. The condition at an endpoint in (9.21) is imposed only where $\tau$ is l.c., as in (9.20). The second line of (9.10) is stated for quasi-derivatives. The boundary term of (9.7) is printed as $W_b(g^*, f) - W_a(g^*, f)$ ; integration by parts with (9.5) gives $W_a(g^*, f) - W_b(g^*, f)$ (check: $p = r = 1$ , $q = 0$ on $(0,1)$ , $f = x^2$ , $g = 1$ ), and the corrected identity is stated.
Ruling out trivialization. Limit circle is the Wronskian notion of p. 187, never "all solutions are square integrable", which would make the goal circular. The goal has no hypothesis beyond the standing assumptions on $p, q, r$ .

A complete development needs a Carathéodory-type existence theorem for linear first-order systems with $L^1_{loc}$ coefficients, the Lagrange identity with its boundary limits, Lemma 9.3 (a linear-algebra fact about functionals) and the computation of the closure and adjoint of the minimal operator (Lemma 9.4). The ODE layer and the $L^2(I, r\,dx)$ operator layer can be reused for the Weyl–Titchmarsh theory, oscillation theory (Sec. 9.7) and one-particle Schrödinger operators (Ch. 10). Contributions that build them as general lemmas are welcome.

Selected references

G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, AMS Graduate Studies in Mathematics 99, 2009, Sections 9.1–9.2. https://doi.org/10.1090/gsm/099
H. Weyl, "Über gewöhnliche Differentialgleichungen mit Singularitäten und die zugehörigen Entwicklungen willkürlicher Funktionen", Math. Ann. 68 (1910), 220–269. https://doi.org/10.1007/BF01474161
J. Weidmann, Spectral Theory of Ordinary Differential Operators, Lecture Notes in Mathematics 1258, Springer, 1987. https://doi.org/10.1007/BFb0077960
A. Zettl, Sturm–Liouville Theory, Mathematical Surveys and Monographs 121, AMS, 2005. https://doi.org/10.1090/surv/121

20 thms2 active usersReviewed

Completed

Analysis Functional Analysis·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics II: The Spectral Theorem for Unbounded Self-Adjoint OperatorsTextbook

Motivation

In quantum mechanics an observable is a self-adjoint operator $A$ on a complex Hilbert space $\mathfrak H$ , and the dynamics is the Schrödinger equation $i\,\tfrac{d}{dt}\psi(t) = H\psi(t)$ . In finite dimensions the solution is the matrix exponential $e^{-itH}\psi(0)$ , computed by diagonalizing $H$ . The operators of physics (the Laplacian, Schrödinger operators with Coulomb potentials, position and momentum) are unbounded, defined only on a dense subspace, and have no eigenbasis in general. The spectral theorem is the substitute for diagonalization in this setting: it expresses every self-adjoint operator as an integral of the identity function against a family of orthogonal projections, and so gives meaning to $f(A)$ for every Borel function $f$ , in particular to $e^{-itA}$ and to the spectral projections $\chi_\Omega(A)$ .

The theorem goes back to Hilbert (bounded symmetric forms, 1906) and was extended to unbounded self-adjoint operators by von Neumann (1929/30), Stone (1932) and Riesz. This mission follows the treatment in G. Teschl, Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), Section 3.1: projection-valued measures, their functional calculus for bounded and unbounded functions, and the spectral theorem obtained from resolvents through the Herglotz representation of Borel transforms.

Setting

Let $\mathfrak H$ be a complex Hilbert space, with inner product $\langle\cdot,\cdot\rangle$ conjugate linear in the first argument, and let $\mathfrak L(\mathfrak H)$ be the bounded operators on it. An (unbounded) operator $A$ is a linear map defined on a subspace $\mathfrak D(A) \subseteq \mathfrak H$ ; $A \subseteq B$ means $B$ extends $A$ . $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A^* = A$ , domains included.

The resolvent set of $A$ is the set of $z \in \mathbb{C}$ for which $A - z : \mathfrak D(A) \to \mathfrak H$ is a bijection with bounded inverse, and the spectrum is its complement, $\sigma(A) = \mathbb{C} \setminus \rho(A)$ .

A projection-valued measure assigns to every Borel set $\Omega \subseteq \mathbb{R}$ an orthogonal projection $P(\Omega) = P(\Omega)^* = P(\Omega)^2$ such that $P(\mathbb{R}) = \mathbb{I}$ and, for pairwise disjoint Borel sets $\Omega_n$ , $\sum_n P(\Omega_n)\psi = P(\bigcup_n \Omega_n)\psi$ for every vector $\psi$ (strong, not norm, $\sigma$ -additivity). Each $\psi$ gives the spectral measure $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle = \|P(\Omega)\psi\|^2$ , a finite Borel measure of total mass $\|\psi\|^2$ , and by polarization the complex measures $\mu_{\varphi,\psi}(\Omega) = \langle\varphi, P(\Omega)\psi\rangle$ .

For a bounded Borel function $f$ the operator $P(f) = \int f(\lambda)\,dP(\lambda) \in \mathfrak L(\mathfrak H)$ is the bounded operator with $\langle\psi, P(f)\psi\rangle = \int f\,d\mu_\psi$ for all $\psi$ . For an arbitrary Borel function $f$ it is the operator with domain

\mathfrak D_f = \Big\{\psi \in \mathfrak H \;\Big|\; \int_{\mathbb{R}} |f(\lambda)|^2\, d\mu_\psi(\lambda) < \infty\Big\}

and $\langle\psi, P(f)\psi\rangle = \int f\,d\mu_\psi$ for $\psi \in \mathfrak D_f$ . An operator $T$ is normal if it is densely defined, $\mathfrak D(T) = \mathfrak D(T^*)$ and $\|T\psi\| = \|T^*\psi\|$ on $\mathfrak D(T)$ .

Formalization targets

Goal: the spectral theorem (Theorem 3.7)

For every self-adjoint operator $A$ in $\mathfrak H$ there is a unique projection-valued measure $P_A$ with

A = \int_{\mathbb{R}} \lambda\, dP_A(\lambda),

an equality of operators including their domains. Uniqueness is among projection-valued measures, compared on Borel sets.

Milestones

Theorem 3.1. For a projection-valued measure $P$ , the map $f \mapsto P(f)$ from bounded Borel functions (sup norm) to $\mathfrak L(\mathfrak H)$ is a unital $C^*$ -algebra homomorphism of norm one, $\langle P(g)\varphi, P(f)\psi\rangle = \int g^* f\, d\mu_{\varphi,\psi}$ , and $P(f_n) \to P(f)$ strongly when $f_n \to f$ pointwise with $\sup_\lambda |f_n(\lambda)|$ bounded.
Theorem 3.2. For every Borel $f$ , the operator $P(f)$ with $\mathfrak D(P(f)) = \mathfrak D_f$ exists, is normal, and $P(f)^* = P(f^*)$ .
Lemma 3.5. $\alpha P(f) + \beta P(g) \subseteq P(\alpha f + \beta g)$ with domain $\mathfrak D_{|f|+|g|}$ , and $P(f)P(g) \subseteq P(fg)$ with domain $\mathfrak D_g \cap \mathfrak D_{fg}$ .
Theorem 3.8. For self-adjoint $A$ , $\sigma(A) = \{\lambda \in \mathbb{R} \mid P_A((\lambda-\varepsilon, \lambda+\varepsilon)) \ne 0 \text{ for all } \varepsilon > 0\}$ .
Corollary 3.9. $P_A(\sigma(A)) = \mathbb{I}$ and $P_A(\mathbb{R} \cap \rho(A)) = 0$ .

A further supporting statement (not a milestone) records that $\mu_\psi$ is a finite measure with $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle = \|P(\Omega)\psi\|^2$ .

Significance

The result itself. The spectral theorem is the foundation of the rest of the book and of mathematical quantum mechanics generally. Stone's theorem and the time evolution $e^{-itA}$ , the min-max principle, the RAGE theorem, the decomposition of the spectrum into absolutely continuous, singular continuous and pure point parts, Weyl's theorem on essential spectra and scattering theory are all statements about $f(A)$ or $P_A(\Omega)$ . Theorem 3.8 identifies the spectrum with the support of $P_A$ , which is what makes spectral questions accessible to measure theory.

Formalizing it. The result is classical and fully proved in the literature. Mathlib has the continuous functional calculus for bounded normal elements of $C^*$ -algebras and the finite-dimensional spectral theorem, but no projection-valued measures, no spectral integral of unbounded functions, and no spectral theorem for unbounded operators (LinearPMap). On Prove2Me the related published material is bounded or finite-dimensional (for example diagonalization of self-adjoint endomorphisms and the Fuglede–Putnam theorem). A formal proof here supplies the object $f(A)$ that every later mission of this series currently has to take as data.

Difficulty

The obvious route through the bounded case fails. For bounded self-adjoint $A$ one can build $f(A)$ from polynomials by the sup norm on $\sigma(A)$ and extend by monotone limits; for unbounded $A$ there are no polynomials in $A$ defined on a common useful domain and no sup-norm estimate. The standard reductions (the Cayley transform $(A-i)(A+i)^{-1}$ , or the bounded resolvent $(A-z)^{-1}$ ) produce bounded normal operators whose spectral measures must then be transported back, and the domain $\mathfrak D(A)$ must be recovered exactly as $\mathfrak D_\lambda$ ; getting the domains right, not just the formulas on a core, is where unbounded arguments usually break. Beyond the domain issue, the projections $P_A(\Omega)$ are not given by any formula in $A$ that Mathlib can evaluate: they have to be recovered from resolvent data, which in the book's development requires the Herglotz representation of Borel transforms and the Stieltjes inversion formula for finite measures, neither of which is in Mathlib. Uniqueness is also not automatic: it requires that a projection-valued measure is determined by the operator $\int \lambda\, dP(\lambda)$ alone.

Formalization scope

$\mathfrak H$ is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since none of the stated results or their proofs in the book need it. Operators are LinearPMaps H →ₗ.[ℂ] H; self-adjointness is Mathlib's IsSelfAdjoint, which includes density. A projection-valued measure is a function Set ℝ → (H →L[ℂ] H) constrained on Borel sets only (IsProjValuedMeasure); uniqueness in the goal compares values on Borel sets. The spectral measure spectralMeasure P ψ is built with Measure.ofMeasurable from $\Omega \mapsto \|P(\Omega)\psi\|^2$ . The spectral integral spectralIntegral P f is the operator with domain $\mathfrak D_f$ and quadratic form $\int f\,d\mu_\psi$ (the predicate IsSpectralIntegral), selected by choice; its existence for Borel $f$ is part of the milestone for Theorem 3.2, not an assumption. The bounded calculus boundedSpectralIntegral is characterized the same way in $\mathfrak L(\mathfrak H)$ . The spectrum is the resolvent-based TeschlQM.Spectral.spectrum of Section 2.4, not Mathlib's spectrum ℂ of a Banach algebra element. In Theorems 3.8 and 3.9, $P_A$ enters as a projection-valued measure P with the hypothesis A = spectralIntegral P (fun x => x), which by the goal's uniqueness is exactly $P_A$ .

Nothing is taken as data that the book derives. In particular the goal is not stated for "a projection-valued measure with $A = \int\lambda\,dP$ " given as a hypothesis, and $P_A$ is not defined by choosing such a measure: the goal quantifies existentially and uniquely over projection-valued measures, with self-adjointness of $A$ as the only hypothesis.

Lemma 3.4 (spectral bases), Lemma 3.6 (the family $P_A(\Omega)$ built from the Herglotz representation) and the results of Sections 3.2–3.3 are not stated. A complete development needs finite Borel measures and $L^2$ spaces (in Mathlib), the Herglotz representation and Stieltjes inversion (the subject of the next mission of this series), and the adjoint theory of LinearPMap. The projection-valued measure and spectral-integral layer is reusable by every later mission of the series. Contributions of any milestone, of general lemmas about IsProjValuedMeasure (finite additivity, $P(\Omega_1)P(\Omega_2) = P(\Omega_1 \cap \Omega_2)$ , monotonicity), and of alternative proofs of the goal are welcome.

Selected references

G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009, Chapter 3. https://doi.org/10.1090/gsm/099
J. von Neumann, Allgemeine Eigenwerttheorie Hermitescher Funktionaloperatoren, Mathematische Annalen 102 (1930), 49–131. https://doi.org/10.1007/BF01782338
M. H. Stone, Linear Transformations in Hilbert Space and Their Applications to Analysis, AMS Colloquium Publications 15, 1932. https://doi.org/10.1090/coll/015
M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Academic Press, 1980, Chapters VII–VIII. https://doi.org/10.1016/B978-0-12-585050-6.X5001-4

12 thms2 active usersReviewed

Completed

Captain: Lucas

Microstate counting in dS₃: eigenvalue count vs. sphere partition functionResearch Paper

Motivation

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

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

Setting

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

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

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

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

Formalization targets

Goal (eq. (4.35))

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

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

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

Milestones

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

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

6 thms2 active usersReviewed

Completed

Functional Analysis·Captain: Lucas

Uma Breve Introdução à Matemática da Mecânica Quântica I: Princípio da Incerteza de HeisenbergTextbook

Motivation

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

Setting

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

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

Formalization targets

Goal — Teorema 8.2 (Heisenberg)

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

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

Milestones

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

7 thms2 active usersReviewed

Completed

Differential Geometry·Captain: Lucas

A No-Nonsense Introduction to General Relativity I: Birkhoff's theorem and the Schwarzschild solutionTextbook

Motivation

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

Setting

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

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

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

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

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

Target

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

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

The milestones follow the notes in order:

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

16 thms2 active usersReviewed

Differential Geometry·Captain: Lucas

Teleparallel Gravity: Equivalence with General Relativity (Aldrovandi-Pereira-Vu 2004)Research Paper

Motivation

General relativity describes gravitation through the curvature of the Levi-Civita (Christoffel) connection of a spacetime metric. An alternative description, going back to Einstein's 1928-1930 papers on distant parallelism and developed in modern form as the teleparallel equivalent of general relativity, uses instead a tetrad field $h^a{}_\mu$ and the Weitzenböck connection it defines, a connection with vanishing curvature but non-zero torsion. The paper of Aldrovandi, Pereira and Vu (Braz. J. Phys. 34 (2004) 1374) reviews this formulation as a gauge theory of the translation group, and uses it to discuss the weak equivalence principle and a global (phase-factor) formulation of gravitation.

The claim that both descriptions are physically equivalent rests on a small number of exact tensor identities: the Weitzenböck connection splits as the Christoffel connection plus the contortion tensor, its curvature vanishes identically, and the teleparallel Lagrangian differs from the Einstein-Hilbert Lagrangian only by a total divergence. This mission asks for machine-checked proofs of these identities, in coordinates, exactly as used in Sections 2-3 of the paper.

Timeline (for orientation): Einstein introduced distant parallelism in 1928 (translations in the Delphenich collection Selected Papers on Teleparallelism); Weitzenböck studied the differential invariants of the theory the same year; the modern teleparallel equivalent of general relativity was developed from the 1960s-1970s onward, and the gauge-theoretic reading used here is the one reviewed by Aldrovandi-Pereira-Vu (2004).

Setting

Work in a single global chart $x=(x^0,x^1,x^2,x^3)\in\mathbb R^4$ and write $\partial_\nu$ for coordinate partial derivatives. Tangent-space (Latin) indices are raised and lowered with the Minkowski metric $\eta_{ab}=\mathrm{diag}(+1,-1,-1,-1)$ .

A tetrad is a smooth field of invertible $4\times 4$ matrices $h^a{}_\mu(x)$ , with inverse $h_a{}^\mu$ and determinant $h=\det(h^a{}_\mu)$ .
The metric is $g_{\mu\nu}=\eta_{ab}h^a{}_\mu h^b{}_\nu$ (Eq. (4)); $g^{\mu\nu}$ is its inverse.
The Weitzenböck connection is $\Gamma^\rho{}_{\mu\nu}=h_a{}^\rho\,\partial_\nu h^a{}_\mu$ (Eq. (5)), its torsion $T^\rho{}_{\mu\nu}=\Gamma^\rho{}_{\nu\mu}-\Gamma^\rho{}_{\mu\nu}$ (Eq. (6)).
The Christoffel connection is $\mathring\Gamma^\rho{}_{\mu\nu}=\tfrac12 g^{\rho\sigma}(\partial_\mu g_{\sigma\nu}+\partial_\nu g_{\sigma\mu}-\partial_\sigma g_{\mu\nu})$ ; the contortion is $K^\rho{}_{\mu\nu}=\tfrac12(T_\mu{}^\rho{}_\nu+T_\nu{}^\rho{}_\mu-T^\rho{}_{\mu\nu})$ (Eq. (9)).
The superpotential is $S^{\rho\mu\nu}=\tfrac12\big[K^{\mu\nu\rho}-g^{\rho\nu}T^{\sigma\mu}{}_\sigma+g^{\rho\mu}T^{\sigma\nu}{}_\sigma\big]$ (Eq. (11)), and the teleparallel Lagrangian density is $\mathcal L_G=\frac{c^4 h}{16\pi G}S^{\rho\mu\nu}T_{\rho\mu\nu}$ (Eq. (10)).
In the gauge picture the tetrad is $h^a{}_\mu=\partial_\mu x^a+B^a{}_\mu$ (Eq. (3)), with translational gauge potential $B^a{}_\mu$ and field strength $F^a{}_{\mu\nu}=\partial_\mu B^a{}_\nu-\partial_\nu B^a{}_\mu$ (Eq. (7)).

Curvature of a connection is $R^\rho{}_{\theta\mu\nu}=\partial_\mu\Gamma^\rho{}_{\theta\nu}-\partial_\nu\Gamma^\rho{}_{\theta\mu}+\Gamma^\rho{}_{\sigma\mu}\Gamma^\sigma{}_{\theta\nu}-\Gamma^\rho{}_{\sigma\nu}\Gamma^\sigma{}_{\theta\mu}$ , Ricci $\mathring R_{\theta\nu}=\mathring R^\rho{}_{\theta\rho\nu}$ , scalar $\mathring R=g^{\theta\nu}\mathring R_{\theta\nu}$ (Landau-Lifshitz conventions, consistent with the paper's Eq. (15)). The Einstein-Hilbert density is $\mathcal L_{EH}=-\frac{c^4}{16\pi G}\sqrt{-g}\,\mathring R$ .

Formalization targets

Goal: equivalence of Lagrangians up to a divergence (Section 2, after Eq. (14))

For a smooth, positively oriented tetrad ( $h>0$ , so $h=\sqrt{-g}$ ):

\mathcal L_G=\mathcal L_{EH}+\partial_\mu\Big(-\frac{c^4}{8\pi G}\,h\,T^{\nu\mu}{}_\nu\Big).

The paper states only "up to a divergence"; the divergence term is written explicitly because an unspecified divergence would make the statement empty (every function on $\mathbb R^4$ is a divergence).

Milestones

Eqs. (2)-(3): the tetrad and $F^a{}_{\mu\nu}$ are invariant under $x^a\mapsto x^a+\varepsilon^a$ , $B^a{}_\mu\mapsto B^a{}_\mu-\partial_\mu\varepsilon^a$ .
Eq. (7): $F^a{}_{\mu\nu}=h^a{}_\rho T^\rho{}_{\mu\nu}$ .
Text after Eq. (5): the Weitzenböck connection has zero curvature.
Eq. (8): $\Gamma^\rho{}_{\mu\nu}=\mathring\Gamma^\rho{}_{\mu\nu}+K^\rho{}_{\mu\nu}$ .
Eq. (11): $S^{\rho\mu\nu}=-S^{\rho\nu\mu}$ .
Eq. (19): $T^\lambda{}_{\mu\rho}u_\lambda u^\rho=-K^\lambda{}_{\mu\rho}u_\lambda u^\rho$ .

Significance

The goal identity is the precise sense in which teleparallel gravity is "equivalent" to general relativity: the two actions differ by a boundary term, so they give the same field equations (the paper's Eqs. (12) and (15)). Milestone 4 is what turns the teleparallel force equation into the geodesic equation (Eq. (20)), and milestone 2 is the dictionary between the gauge field strength and torsion used throughout Sections 3-4. The results are classical and proved on paper; to our knowledge they are not formalized in Mathlib, which has no coordinate tensor calculus of this kind. A formal development would provide reusable coordinate lemmas (derivative of an inverse matrix field, symmetry of second derivatives in index form, Christoffel symbols of $g=h^{\mathsf T}\eta h$ ).

Difficulty

Each identity is elementary on paper, but the index computations are long, and in Lean every derivative carries differentiability side conditions: derivatives of inverse matrices and of determinants, and symmetry of mixed partial derivatives, must be justified from smoothness and invertibility of the tetrad. The goal identity involves second derivatives of the inverse metric and a careful bookkeeping of about a hundred index contractions.

Formalization scope

Spacetime is $\mathbb R^4$ as Fin 4 → ℝ with one global chart; partial derivatives are Fréchet derivatives applied to coordinate basis vectors. A tetrad is a family of real functions h a μ, assumed $C^\infty$ with invertible matrix at every point (IsTetrad). Inverses are matrix inverses (which would be $0$ for singular matrices; the invertibility hypothesis excludes this). The physical constants $c,G$ are arbitrary reals. All definitions live in the single definition file of the mission, namespace TeleparallelGravity.

Selected references

R. Aldrovandi, J. G. Pereira, K. H. Vu, Selected Topics in Teleparallel Gravity, Braz. J. Phys. 34 (2004) 1374. https://doi.org/10.1590/S0103-97332004000700009
D. H. Delphenich (ed., transl.), Selected Papers on Teleparallelism (translations of Einstein, Weitzenböck, Cartan and others, 1928-1935).
L. D. Landau, E. M. Lifshitz, The Classical Theory of Fields, 4th ed., Pergamon, 1975 (sign conventions).

8 thms2 active usersReviewed

Completed

Captain: Lucas

String Theory (Tong) I: The Critical Dimension D = 26Textbook

Motivation

The bosonic string can be quantized consistently only in $D=26$ spacetime dimensions. In lightcone quantization this appears in two ways in David Tong's Cambridge Part III lecture notes. First (Sections 2.2.2–2.3), the normal-ordering constant $a$ in the mass formula $M^2=\frac{4}{\alpha'}(N-a)$ is identified with a regularized Casimir energy $a=\frac{D-2}{24}$ , using $\sum_{n\ge1}n$ " $=$ " $-\frac1{12}$ ; Lorentz invariance then forces the first excited states to be massless, which happens only for $D=26$ . Second (Section 2.4), the commutator $[M^{i-},M^{j-}]$ of lightcone Lorentz generators, which must vanish for the quantum theory to be Lorentz invariant, is proportional to a coefficient that vanishes for all oscillator levels $n$ exactly when $D=26$ and $a=1$ (Goddard–Goldstone–Rebbi–Thorn 1973).

Setting

Let $D\ge2$ be the number of spacetime dimensions, so there are $D-2$ transverse oscillator directions, and let $\alpha'>0$ be the Regge slope. In lightcone gauge the mass of a closed-string state at level $N=\tilde N$ is (2.25)

M^2=\frac{4}{\alpha'}(N-a),

with an undetermined normal-ordering constant $a$ . The heuristic evaluation of $a$ replaces the divergent zero-point sum $\frac{D-2}2\sum_{n\ge1}n$ by its cut-off regularization $\sum_{n\ge1}ne^{-\epsilon n}$ , or by the Riemann zeta function value $\zeta(-1)$ , giving $a=\frac{D-2}{24}$ (2.26). The first excited states $\tilde\alpha^i_{-1}\alpha^j_{-1}|0;p\rangle$ (2.28) are $(D-2)^2$ in number and have $M^2=\frac4{\alpha'}\bigl(1-\frac{D-2}{24}\bigr)$ . In one sector the level-2 states are $\alpha^i_{-1}\alpha^j_{-1}|0\rangle$ (unordered pairs $\{i,j\}$ , since the oscillators commute) and $\alpha^i_{-2}|0\rangle$ . Finally, Section 2.4 states that

[M^{i-},M^{j-}]=\frac{2}{(p^+)^2}\sum_{n>0}\left(\Big[\frac{D-2}{24}-1\Big]n+\frac1n\Big[a-\frac{D-2}{24}\Big]\right)\bigl(\alpha^i_{-n}\alpha^j_n-\alpha^j_{-n}\alpha^i_n\bigr)+(\alpha\leftrightarrow\tilde\alpha).

Formalization targets

Goal: the anomaly coefficient vanishes iff $D=26$ , $a=1$

For $D\in\mathbb N$ and $a\in\mathbb R$ ,

\Big(\forall n\ge1:\ \Big[\frac{D-2}{24}-1\Big]n+\frac1n\Big[a-\frac{D-2}{24}\Big]=0\Big)\iff\bigl(D=26\ \text{and}\ a=1\bigr).

Milestones (in the order of the notes)

Cut-off regularization: $\sum_{n\ge1}ne^{-\epsilon n}=\frac1{\epsilon^2}-\frac1{12}+O(\epsilon)$ as $\epsilon\to0^+$ .
Zeta-function regularization: $\zeta(-1)=-\frac1{12}$ .
First excited states are massless iff $D=26$ .
Level-2 counting: $\frac12(D-2)(D-1)+(D-2)=\frac12D(D-1)-1$ , the dimension of the traceless symmetric tensor representation of $SO(D-1)$ .

Significance

The result. The critical dimension is the single most-quoted prediction of the bosonic string, and the pair $(D,a)=(26,1)$ fixes the entire lightcone spectrum: the tachyon $M^2=-4/\alpha'$ , the massless graviton, $B$ -field and dilaton, and the massive tower $M^2=4(N-1)/\alpha'$ .

Formalizing it. This mission formalizes the mathematical steps of Tong's lightcone derivation: the two regularizations of $\sum n$ , the mass-shell and state-counting arithmetic, and the final algebraic step of the Lorentz-algebra argument. It does not formalize the operator computation of $[M^{i-},M^{j-}]$ in the lightcone Fock space, which Tong quotes ("After a tedious computation, one finds ...") without derivation; that computation is a natural follow-up mission. The value $\zeta(-1)=-1/12$ is already available in Mathlib through the Bernoulli-number formula for $\zeta$ at negative integers.

Difficulty

The individual statements are elementary once formalized; the difficulty is faithfulness rather than proof. The regularized sum is an asymptotic statement whose leading term diverges, so it has to be stated as an $O(\epsilon)$ remainder along $\epsilon\to0^+$ rather than as an equation; and the goal is a statement for all levels $n\ge1$ , where a single level ( $n=1$ ) only forces $a=1$ and two levels are needed to force $D=26$ .

Formalization scope

The dimension $D$ is a natural number and the normal-ordering constant $a$ a real number. The regularized sum is Mathlib's tsum of $n e^{-\epsilon n}$ over $n\in\mathbb N$ (the $n=0$ term vanishes), and the asymptotic claim uses Mathlib's big-O along the right neighbourhood filter of $0$ . Level-2 states of one sector are counted as unordered pairs with repetition of transverse indices (Mathlib's Sym2 (Fin (D-2))) plus the $D-2$ states $\alpha^i_{-2}|0\rangle$ ; natural-number subtraction and division are safe because $D\ge2$ is assumed and $D(D-1)$ is even. The zeta function is Mathlib's riemannZeta, i.e. the analytic continuation.

Selected references

D. Tong, String Theory, Cambridge Part III lecture notes, 2009, Sections 2.2.2–2.4. http://www.damtp.cam.ac.uk/user/tong/string.html (arXiv:0908.0333)
P. Goddard, J. Goldstone, C. Rebbi, C. B. Thorn, Quantum dynamics of a massless relativistic string, Nucl. Phys. B 56 (1973) 109. https://doi.org/10.1016/0550-3213(73)90223-X
J. Polchinski, String Theory, Vol. 1, Cambridge University Press, 1998, Section 1.3.
B. Zwiebach, A First Course in String Theory, 2nd ed., Cambridge University Press, 2009, Chapter 12.

5 thms2 active usersReviewed

Completed

Captain: Lucas

Termodinâmica de Buracos Negros (Menezes 2021): the first law for Kerr black holesResearch Paper

Motivation

In 1973 Bardeen, Carter and Hawking showed that stationary black holes in general relativity obey four laws with the same structure as the laws of thermodynamics, with the surface gravity $\kappa$ of the horizon playing the role of temperature and the horizon area $A$ the role of entropy (Bardeen–Carter–Hawking 1973). Two years later Hawking showed that quantum fields near a black hole produce thermal radiation at temperature $T_{BH}=\kappa/2\pi$ (Hawking 1975), which turned the analogy into an identification, with entropy $S_{BH}=A/4$ .

The M.Sc. dissertation Termodinâmica de Buracos Negros (F. H. de C. Menezes, UFMG, 2021) presents this construction for the Kerr black hole, the rotating stationary solution of Einstein's vacuum equations. The first law, eq. (3.79), is its central quantitative statement:

\delta M = \frac{\kappa}{8\pi}\,\delta A + \Omega_H\,\delta J,

relating first-order changes of mass $M$ , horizon area $A$ and angular momentum $J$ between neighbouring Kerr black holes, where $\Omega_H$ is the angular velocity of the horizon.

Timeline: Kerr found the rotating solution (1963); Smarr derived the mass formula $M = \kappa A/4\pi + 2\Omega_H J$ (1973); Bardeen, Carter and Hawking stated the four laws (1973); Hawking derived the thermal emission (1974–75).

Setting

Units are geometrized, $G=c=1$ (and $\hbar=k_B=1$ for quantum quantities). A Kerr black hole has mass $M>0$ and rotation parameter $a$ with $a^2\le M^2$ ; its angular momentum is $J=Ma$ . In Boyer–Lindquist coordinates $(t,r,\theta,\varphi)$ the metric involves

\Delta = r^2-2Mr+a^2,\qquad \Sigma = r^2+a^2\cos^2\theta,

with angular components $g_{\theta\theta}=\Sigma$ and $g_{\varphi\varphi} = \dfrac{(r^2+a^2)^2-\Delta a^2\sin^2\theta}{\Sigma}\sin^2\theta$ . The zeros of $\Delta$ are $r_\pm = M\pm\sqrt{M^2-a^2}$ ; the event horizon is $r=r_+$ .

The horizon area $A$ is the area of the cross-section $t=\text{const}$ , $r=r_+$ , computed from the induced metric: $A=\int_0^\pi\int_0^{2\pi}\sqrt{g_{\theta\theta}g_{\varphi\varphi}}\,d\varphi\,d\theta$ at $r=r_+$ .
The surface gravity is $\kappa = \dfrac{\sqrt{M^2-a^2}}{2M(M+\sqrt{M^2-a^2})}$ (eq. (3.3)).
The angular velocity of the horizon is $\Omega_H = \dfrac{a}{2M(M+\sqrt{M^2-a^2})}$ (eq. (2.42)).

A Kerr black hole is non-extremal when $a^2<M^2$ , equivalently $|J|<M^2$ .

Formalization targets

Goal — the first law (eq. (3.79))

Regard $A,\kappa,\Omega_H$ as functions of $(M,J)$ with $a=J/M$ . For $M>0$ and $J^2<M^4$ , the area is differentiable at $(M,J)$ and, as linear forms in $(\delta M,\delta J)$ ,

\delta M = \frac{\kappa}{8\pi}\,\delta A + \Omega_H\,\delta J .

Milestones, in the dissertation's order

Eq. (2.42): $\Omega_H = a/(r_+^2+a^2)$ .
Eq. (3.4): $\kappa = (r_+-r_-)/(2(r_+^2+a^2))$ .
Eq. (3.44): $A = 8\pi M\left(M+\sqrt{M^2-a^2}\right)$ .
Eq. (3.43), Smarr formula: $M = \kappa A/4\pi + 2\Omega_H J$ .
Eq. (3.78), variation of $\kappa$ : $\delta M = -\frac{A}{4\pi}\delta\kappa - 2J\,\delta\Omega_H$ .
Eq. (3.81) and the following remark: $\kappa=0 \iff |J|=M^2$ .
Eq. (4.137): $M(t) = (M_0^3-t/256\pi)^{1/3}$ solves $\dot M = -(768\pi)^{-1}M^{-2}$ , $M(0)=M_0$ .

In the dissertation the first law is the sum of the variation (3.45) of the Smarr formula and the relation (3.78).

Significance

The first law is the identity behind the identification $T_{BH}=\kappa/2\pi$ , $S_{BH}=A/4$ : with these values it becomes $\delta M = T_{BH}\,\delta S_{BH} + \Omega_H\,\delta J$ , the ordinary first law of thermodynamics for a rotating body. The Smarr formula is its integrated (Euler-relation) form, and the vanishing of $\kappa$ at extremality underlies the dissertation's formulation of the third law.

All results are classical and proved in the literature. The contribution of the mission is a machine-checked version of the explicit Kerr relations, with the horizon area computed from the metric rather than taken as given, and a check of the dissertation's formulas. One such check is already recorded: the coefficient $-2\pi J$ printed in eq. (3.78) conflicts with the dissertation's own eqs. (3.70) and (3.77), which give $-2J$ , the value required for (3.79); the milestone uses $-2J$ .

Difficulty

The dissertation derives the first law geometrically, from Komar integrals and a perturbation of the horizon Killing field. That route needs Lorentzian geometry, Killing horizons and Stokes' theorem on manifolds, which the Lean library does not provide. The explicit route through the Kerr formulas avoids this, but has its own obstacles: the horizon area is a double integral of a square root of a rational trigonometric expression that simplifies only on the horizon, where $\Delta(r_+)=0$ ; and the differentials involve $\sqrt{M^2-J^2/M^2}$ , which is not differentiable at extremality, so the non-extremal hypothesis must be used when differentiating.

Formalization scope

All quantities are real-valued functions of real arguments, defined in one definition file in the namespace KerrBlackHoleThermo. Every theorem restricts to the physical range explicitly ( $M>0$ and $a^2\le M^2$ , or $M>0$ and $J^2<M^4$ for statements involving derivatives), so Lean's conventions for $\sqrt{\cdot}$ of negative numbers and division by zero do not enter the physical content. First-order variations "between two neighbouring Kerr configurations" are formalized as Fréchet derivatives (HasFDerivAt) of the explicit family in the coordinates $(M,J)$ ; the first law is an identity of linear forms on $\mathbb R^2$ . The horizon area is defined as a metric integral, not as the closed form (3.44), so the goal cannot be reduced to a pure algebraic identity by definition.

Out of scope: the general-spacetime versions of the zeroth, second (area theorem) and third laws, which need a theory of Lorentzian manifolds, event horizons and energy conditions, and the quantum field theory derivation of Hawking radiation in Chapter 4. Contributions building that infrastructure are welcome as separate missions.

Selected references

F. H. de C. Menezes, Termodinâmica de Buracos Negros, M.Sc. dissertation, Universidade Federal de Minas Gerais, 2021 (the source of this mission).
J. M. Bardeen, B. Carter, S. W. Hawking, The four laws of black hole mechanics, Commun. Math. Phys. 31 (1973) 161–170. https://doi.org/10.1007/BF01645742
S. W. Hawking, Particle creation by black holes, Commun. Math. Phys. 43 (1975) 199–220. https://doi.org/10.1007/BF02345020
L. Smarr, Mass formula for Kerr black holes, Phys. Rev. Lett. 30 (1973) 71–73. https://doi.org/10.1103/PhysRevLett.30.71
R. P. Kerr, Gravitational field of a spinning mass as an example of algebraically special metrics, Phys. Rev. Lett. 11 (1963) 237–238. https://doi.org/10.1103/PhysRevLett.11.237
R. M. Wald, General Relativity, University of Chicago Press, 1984.

9 thms2 active usersReviewed

Completed

Captain: Lucas

The International System of Units (SI Brochure, 9th ed.) I: base units from the seven defining constantsTextbook

Motivation

Since 20 May 2019 the International System of Units (SI) is no longer defined through material artefacts or particular experiments. Instead, the 26th General Conference on Weights and Measures fixed the exact numerical values of seven defining constants and declared that the SI is the system of units in which these constants take these values. The reference text is the BIPM's SI Brochure, 9th edition (2019), bipm.org. Every calibration certificate, every value in the CODATA tables and every textbook formula expressed in SI units rests on this definition.

The mathematical content of the new definition is small but exact: from the seven fixed values, the Brochure derives, for each of the seven base units, an explicit formula expressing that unit as a rational multiple of a product of integer powers of the defining constants (Section 2.3.1), and it asserts that any SI unit can be written through products and quotients of the defining constants (Section 2.2). These are statements about a free abelian group of unit monomials together with exact rational coefficients, so they can be checked completely.

Timeline. 1960: the 11th CGPM establishes the SI with six base units (the mole is added in 1971). 1983: the metre is redefined by fixing the speed of light $c$ . 2018–2019: the 26th CGPM (Resolution 1) redefines the kilogram, ampere, kelvin and mole by fixing $h$ , $e$ , $k$ and $N_A$ ; the new definitions enter into force on 20 May 2019 and are published in the 9th edition of the SI Brochure.

Setting

A quantity value is written as a number times a unit. In this mission a quantity value is a pair $(x, u)$ , written $x\,u$ , where $x\in\mathbb R$ is the numerical value and

u = \mathrm{s}^{a_1}\,\mathrm{m}^{a_2}\,\mathrm{kg}^{a_3}\,\mathrm{A}^{a_4}\,\mathrm{K}^{a_5}\,\mathrm{mol}^{a_6}\,\mathrm{cd}^{a_7},\qquad a_i\in\mathbb Z,

is a unit monomial in the seven base units second, metre, kilogram, ampere, kelvin, mole and candela (Table 2 of the Brochure). Products multiply numerical values and add exponents; quotients and integer powers are defined accordingly; a real number $r$ acts by $r\cdot(x\,u) = (rx)\,u$ . Two quantity values are equal exactly when they have the same numerical value and the same seven exponents.

The derived units needed in Section 2.2 are $\mathrm{Hz}=\mathrm s^{-1}$ , $\mathrm J=\mathrm{kg\,m^2\,s^{-2}}$ , $\mathrm C=\mathrm{A\,s}$ , $\mathrm W=\mathrm{kg\,m^2\,s^{-3}}$ , $\mathrm{sr}=\mathrm{m^2\,m^{-2}}$ and $\mathrm{lm}=\mathrm{cd\,sr}$ . The seven defining constants (Section 2.2, Table 1) are

\Delta\nu_{\mathrm{Cs}} = 9\,192\,631\,770\ \mathrm{Hz},\quad c = 299\,792\,458\ \mathrm{m\,s^{-1}},\quad h = 6.626\,070\,15\times10^{-34}\ \mathrm{J\,s},

e = 1.602\,176\,634\times10^{-19}\ \mathrm C,\quad k = 1.380\,649\times10^{-23}\ \mathrm{J\,K^{-1}},\quad N_A = 6.022\,140\,76\times10^{23}\ \mathrm{mol^{-1}},\quad K_{\mathrm{cd}} = 683\ \mathrm{lm\,W^{-1}}.

Formalization targets

Goal (Section 2.2, p. 127)

"The seven constants are chosen in such a way that any unit of the SI can be written either through a defining constant itself or through products or quotients of defining constants." Formally: for every exponent vector $u\in\mathbb Z^7$ there are a real number $a$ and integers $n_1,\dots,n_7$ with

\mathrm{s}^{u_1}\cdots\mathrm{cd}^{u_7} \;=\; a\cdot \Delta\nu_{\mathrm{Cs}}^{\,n_1}\, c^{\,n_2}\, h^{\,n_3}\, e^{\,n_4}\, k^{\,n_5}\, N_A^{\,n_6}\, K_{\mathrm{cd}}^{\,n_7}.

Milestones (Section 2.3.1, pp. 130–135)

The seven exact expressions of the base units in terms of the defining constants, each in both forms displayed by the Brochure:

1\ \mathrm s = \frac{9\,192\,631\,770}{\Delta\nu_{\mathrm{Cs}}},\qquad 1\ \mathrm m = \frac{9\,192\,631\,770}{299\,792\,458}\,\frac{c}{\Delta\nu_{\mathrm{Cs}}},\qquad 1\ \mathrm{kg} = \frac{(299\,792\,458)^2}{(6.626\,070\,15\times10^{-34})(9\,192\,631\,770)}\,\frac{h\,\Delta\nu_{\mathrm{Cs}}}{c^2},

1\ \mathrm A = \frac{\Delta\nu_{\mathrm{Cs}}\,e}{(9\,192\,631\,770)(1.602\,176\,634\times10^{-19})},\quad 1\ \mathrm K = \frac{1.380\,649\times10^{-23}}{(6.626\,070\,15\times10^{-34})(9\,192\,631\,770)}\,\frac{\Delta\nu_{\mathrm{Cs}}\,h}{k},

1\ \mathrm{mol} = \frac{6.022\,140\,76\times10^{23}}{N_A},\qquad 1\ \mathrm{cd} = \frac{(\Delta\nu_{\mathrm{Cs}})^2\,h\,K_{\mathrm{cd}}}{(6.626\,070\,15\times10^{-34})(9\,192\,631\,770)^2\,683},

together with the rounded decimal values quoted for the five non-trivial numerical factors ( $\approx 30.663\,319$ , $1.475\,5214\times10^{40}$ , $6.789\,687\times10^{8}$ , $2.266\,6653$ , $2.614\,830\times10^{10}$ ).

Significance

The result itself. The milestones are the operational content of the 2019 redefinition: they say how each base unit is recovered from the fixed constants, and together they show that the matrix of exponents of the seven defining constants with respect to the seven base units is invertible over $\mathbb Z$ , which is exactly what the goal asserts. Every derived unit is a monomial in base units, so the goal also covers the derived units.

Formalizing it. The platform already has purely numerical checks of these formulas (rational identities of the form "coefficient $\times$ constant values $=1$ "). This mission adds a model with units as first-class data: equalities are between quantity values, so a wrong exponent or a missing factor of $c^2$ is a type-level failure, not a silent numerical coincidence. The definition file is reusable for later missions in this series (derived units, Tables 4–8, prefixes).

Difficulty

The individual milestones are exact finite computations; the only care needed is bookkeeping of exponents and of large decimal constants. The goal requires choosing the integer exponents $n_i$ as functions of $u$ and showing that the unit monomials match componentwise — an argument that the exponent matrix is unimodular, not merely invertible over $\mathbb Q$ . Solving the system over the rationals is not enough.

Formalization scope

Numerical values are real numbers; exponents are integers; base units form a seven-element type. Equality of quantity values is equality of the numerical value and of all seven exponents.
The steradian is modelled as $\mathrm m^2\,\mathrm m^{-2}$ , i.e. the unit of dimension one, as in the Brochure (Table 4); consequently $\mathrm{lm} = \mathrm{cd}$ in this model.
Real division and inversion follow Mathlib's conventions ( $0^{-1}=0$ ); all constants used here are non-zero, so this convention never enters the milestones.
The goal allows an arbitrary real coefficient $a$ ; since unit monomials have numerical value $1$ , $a$ is forced to be non-zero, so the statement cannot be satisfied trivially.
Out of scope: the physical realization of units (Section 2.3.2 onward), uncertainties, and the definitions of the non-coherent and non-SI units.

Selected references

BIPM, The International System of Units (SI), 9th edition, 2019. ISBN 978-92-822-2272-0. https://www.bipm.org/en/publications/si-brochure
CGPM, Resolution 1 of the 26th meeting (2018), On the revision of the International System of Units (SI). https://www.bipm.org/en/committees/cg/cgpm/26-2018/resolution-1

10 thms2 active usersReviewed

Completed

Quantum Information·Captain: Lucas

Decoherence in Two-Flavour Neutrino Oscillations (Alves 2020)Research Paper

Motivation

Neutrino oscillations are an interference phenomenon, so they are sensitive to any mechanism that degrades quantum coherence during propagation. The open quantum system description models such effects without specifying their microscopic origin: the neutrino is treated as a subsystem whose reduced density matrix evolves under a Markovian master equation. The dissertation of G. F. S. Alves (Instituto de Física, Universidade de São Paulo, 2020) develops this framework for two and three neutrino generations and uses public IceCube atmospheric data to constrain the new parameters. Its two-generation chapter derives closed-form oscillation probabilities under several choices of the dissipative term; this mission formalizes that chapter's mathematical content.

Setting

A density matrix is a positive semidefinite complex matrix of unit trace. For a two-level system (two neutrino mass eigenstates) the reduced state $\rho(t)\in\mathbb C^{2\times2}$ obeys the Lindblad equation with constant coefficients,

\dot\rho=-i[H,\rho]+D[\rho],\qquad D[\rho]=\tfrac12\sum_{i,j=1}^3 a_{ij}\bigl(2\sigma_i\rho\sigma_j-\{\sigma_j\sigma_i,\rho\}\bigr),

where $\sigma_1,\sigma_2,\sigma_3$ are the Pauli matrices and the $3\times3$ Kossakowski matrix $a=(a_{ij})$ is Hermitian positive semidefinite (the condition for complete positivity). In the mass basis the vacuum Hamiltonian is $H=\operatorname{diag}(0,\Delta m^2/2E)$ , and the mixing matrix with Majorana phase $\alpha$ is

U=\begin{pmatrix}\cos\theta&e^{i\alpha}\sin\theta\\-e^{-i\alpha}\sin\theta&\cos\theta\end{pmatrix}.

The muon neutrino is produced in the state $\rho_\mu(0)=U^\dagger|\nu_1\rangle\langle\nu_1|U$ , and the survival probability after a baseline $L$ is $P_{\nu_\mu\to\nu_\mu}=\operatorname{Tr}\{\rho(L)\rho_\mu(0)\}$ . The linear entropy $S_l(\rho)=1-\operatorname{Tr}\rho^2$ and the von Neumann entropy $S(\rho)=-\operatorname{Tr}\rho\ln\rho$ measure the loss of purity.

Formalization targets

Goal: decoherent survival probability, eq. (3.24)

For the pure-decoherence Kossakowski matrix $a=\operatorname{diag}(0,0,\gamma)$ , $\gamma\ge0$ , every solution with $\rho(0)=\rho_\mu(0)$ satisfies, for all $L\ge0$ ,

P_{\nu_\mu\to\nu_\mu}=\frac14\Bigl(3+\cos4\theta+2e^{-2\gamma L}\cos\Bigl(\frac{\Delta m^2}{2E}L\Bigr)\sin^22\theta\Bigr).

Milestones

Range of the linear entropy, eq. (2.45), and of the von Neumann entropy, eqs. (2.40)–(2.41).
Non-negativity of the relative entropy, eq. (2.43).
Entropy increase whenever the maximally mixed state is a fixed point of $D$ (Appendix B.1, two-level case).
Pauli-basis form of the Dissipator, eq. (3.5).
Average-energy conservation holds iff $a=\operatorname{diag}(0,0,\gamma)$ , eqs. (3.19)–(3.22).
The evolved state in case (1), eq. (3.23), and the population in case (4), eq. (3.26).

Significance

The goal is the formula used in the dissertation to show how decoherence damps oscillations: it reduces to the standard vacuum formula at $\gamma=0$ , it tends to $\tfrac14(3+\cos4\theta)$ at large $L$ instead of oscillating, and it does not depend on $\alpha$ . The milestones connect the formula to the structure of the Lindblad generator (energy conservation singles out this Dissipator) and to entropy growth. A formal development yields a checked two-level Lindblad toolkit (Pauli expansion of dissipators, explicit solutions, entropy bounds) reusable in other open-system missions. The results are proved informally in the source; none is known to be machine-checked.

Difficulty

The ODE part requires a uniqueness argument for a linear matrix ODE on $[0,\infty)$ given only one-sided derivatives at $t=0$ , plus exact trigonometric bookkeeping. The entropy milestones need spectral calculus for Hermitian matrices (Klein's inequality, concavity of $-x\ln x$ ) and, for Appendix B.1, the monotonicity of relative entropy under completely positive trace-preserving maps together with complete positivity of Lindblad semigroups, neither of which is expected to be available off the shelf.

Formalization scope

Matrices are Matrix (Fin 2) (Fin 2) ℂ; the Kossakowski matrix is Matrix (Fin 3) (Fin 3) ℂ with indices $0,1,2$ for the thesis' $1,2,3$ . Solutions are curves $\mathbb R\to\mathbb C^{2\times2}$ satisfying the Lindblad equation entrywise for $t\ge0$ (derivatives within $[0,\infty)$ ); the exponential $e^{\mathcal Lt}$ is not used. Entropies use the continuous functional calculus. Two printed formulas are corrected in the drafts: the sign of the $\rho_0\,\mathrm{Im}(a_{ij})$ terms in eq. (3.5), and the overall sign of the off-diagonal entries in eq. (3.23); both corrections are explained in the corresponding items. The two-generation cases (4) and (5) survival probabilities, eqs. (3.25) and (3.27), and the three-generation and IceCube analyses are out of scope.

Selected references

G. F. S. Alves, Decoherence in Neutrino Oscillations in the IceCube Experiment, MSc dissertation, Instituto de Física, Universidade de São Paulo, 2020.
G. Lindblad, On the generators of quantum dynamical semigroups, Commun. Math. Phys. 48 (1976) 119–130, https://doi.org/10.1007/BF01608499
V. Gorini, A. Kossakowski, E. C. G. Sudarshan, Completely positive dynamical semigroups of N-level systems, J. Math. Phys. 17 (1976) 821–825, https://doi.org/10.1063/1.522979

10 thms2 active usersReviewed

Mathematical Physics

Missions

A radial continuum phase transition with algebraic decayResearch Paper

Motivation: continuum phase transitions with a power-law tail

Timeline

Setting

Formalization targets

Milestone: the corner at the central density

Goal: a common corner on a density interval

Significance

Difficulty

Formalization scope

Selected references

A continuum temperature singularity for a radial pair potentialResearch Paper

Motivation: phase transitions for continuum particles

Timeline

Setting

Formalization targets

Goal: a strict temperature corner throughout a density interval

Significance

Difficulty

Formalization scope

Selected references

Critical slowing down in the Sherrington–Kirkpatrick modelResearch Paper

Motivation

Timeline

Setting

Formalization targets

Goal: Theorem 1.1 (realized equilibrium initial states)

Milestone: Theorem 1.2 (covariance and linear tests)

Milestones: Theorem 1.3 (critical mixing bounds)

Significance

Difficulty

Formalization scope

Selected references

Exponential decay in two-dimensional classical O(n) modelsResearch Paper

Motivation: mass generation in two-dimensional spin systems

Timeline

Setting

Formalization targets

Goal: all-temperature exponential decay (Theorem 1.1)

Significance

Difficulty

Formalization scope

Selected references

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XIII: The Sherrington–Kirkpatrick Model at High Temperature — Deviations of log Z_N from β²N/4Textbook

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Peres-Terno: the no-communication theorem for commuting Kraus operatorsResearch Paper

Motivation

Setting

Formalization targets

Goal: no-communication (Sec. II.E, Eqs. (9)-(11))

Milestones (Sec. II.D-II.E)

Significance

Difficulty

Formalization scope

Selected references

The Intermediate Disorder Regime for Directed Polymers in Dimension 1+1: The Rescaled Partition Function Converges in Law to a Wiener ChaosResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.1 (second bullet), proved as Proposition 5.4

Modified partition function: Proposition 5.3 (Theorem 2.1, first bullet)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimization of Mean-field Spin Glasses I: Every Minimizer of the Extended Parisi Functional Has Full SupportResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5

Milestones

Goal: $N=7$