Mathematical Physics

Motivation

The cosmological constant problem is the mismatch between the vacuum energy density predicted by quantum field theory in flat space–time and the small value of the cosmological term inferred from observations (Weinberg 1989). One line of work replaces the constant by a decaying vacuum: a time-dependent cosmological term $\Lambda(t)$ that falls as the universe expands, while the energy it loses is transferred to matter so that total energy is conserved.

S. Carneiro's essay From de Sitter to de Sitter: a non-singular inflationary universe driven by vacuum (Int. J. Mod. Phys. D 15 (2006) 2241–2247, honorable mention in the 2006 Gravity Research Foundation essay competition) derives such a law from a semi-classical argument, $\Lambda\approx(m+H)^4-m^4$, and studies the cosmologies it produces. In the early-time regime $\Lambda\approx H^4$ it finds a universe with no initial singularity: an eternal quasi-de Sitter phase at the Planck scale, followed by a fast transition to a radiation era. In the late-time regime $\Lambda\approx m^3H$ it finds a dust era that tends again to a de Sitter universe. The calculations in the paper are explicit closed-form computations, which makes them a good target for a complete machine-checked development.

Setting

All quantities are in Planck units, and space is flat. The expansion is described by the Hubble parameter $H(t)=\dot a(t)/a(t)$ of a scale factor $a(t)$. The cosmic fluid has total energy density $\rho_T=\rho_m+\Lambda$ and total pressure $p_T=p_m-\Lambda$, where $\rho_m,p_m$ are the matter density and pressure and $\Lambda$ is the vacuum term. The Friedmann equation is $\rho_T=3H^2$ and the conservation equation is

$$\dot\rho_T+3H(\rho_T+p_T)=0 .$$

Radiation has $p_m=\rho_m/3$ and dust has $p_m=0$. The relative energy densities are $\Omega_m=\rho_m/\rho_T$ and $\Omega_\Lambda=\Lambda/\rho_T$, and the deceleration parameter is $q=-1-\dot H/H^2$.

The vacuum term comes from a massless scalar field $\phi$ obeying $\ddot\phi+3H\dot\phi-\nabla^2\phi=0$. For slowly varying $H$ this has the damped radial plane-wave solution $\phi=\phi_0e^{-br}e^{-i(\omega t-kr)}$, with $k(\omega,H)$ and $b(\omega,H)$ given by explicit square-root formulas (Eqs. (7)–(8)), and energy density $(\omega^2+b^2)|\phi|^2$. Shifting the cutoff $m$ of the thermally regularized vacuum integral $\int_0^\infty\omega^3\,d\omega/(e^{\omega/m}-1)$ by $b\approx H$ and subtracting the flat-space value gives the vacuum term $\Lambda(m,H)=(m+H)^4-m^4$. In the mission's Lean development these objects are waveNumber, dampingRate, planeWave, vacuumTerm, dustScaleFactor and decelerationParameter, all in the namespace CarneiroDeSitter.

Formalization targets

Goal: the non-singular early universe

With radiation and $\Lambda=3H^4$, the evolution equation is $\dot H+2H^2-2H^4=0$ (Eq. (12)). The goal asserts that it has a solution defined for all times, given implicitly by Eq. (13):

$$\exists\,H:\mathbb R\to(0,1),\quad 2t=\frac1{H(t)}-\operatorname{artanh}H(t),\quad \dot H=-2H^2+2H^4,\quad H\xrightarrow[t\to-\infty]{}1,\quad H\xrightarrow[t\to+\infty]{}0 .$$

Milestones (in the order of the paper)

1. Eq. (2): $\int_0^\infty\frac{\omega^3\,d\omega}{e^{\omega/m}-1}=\frac{\pi^4}{15}m^4$.
2. Eqs. (5)–(8): the damped plane wave solves $\ddot\phi+3H\dot\phi-\partial_r^2\phi=0$ for constant $H$.
3. Eqs. (9)–(10): its energy density is $(\omega^2+b^2)|\phi|^2$.
4. Eq. (11): $(m+H)^4-m^4\sim H^4$ as $H\to\infty$ and $\sim4m^3H$ as $H\to0^+$.
5. Eq. (12): the conservation equation with $\rho_T=3H^2$, $\Lambda=3H^4$, $p_m=\rho_m/3$ gives $\dot H+2H^2-2H^4=0$.
6. Eq. (13): every solution on $\mathbb R$ with $0<H<1$ satisfies $2(t-t_0)=1/H-\operatorname{artanh}H$.
7. p. 2245: $\Omega_m=1-H^2$, $\Omega_\Lambda=H^2$, $q=1-2H^2$.
8. Eq. (14): $a=C(e^{\sigma t/2}-1)^{2/3}$ solves the dust era with $\Lambda=\sigma H$.
9. Limits of (14): $a\sim C(\sigma/2)^{2/3}t^{2/3}$ as $t\to0^+$ and $H\to\sigma/3$ as $t\to\infty$.
10. Eq. (15): $\int_0^\infty\frac{\omega^2\,d\omega}{e^{\omega/(m+H)}-1}=2\zeta(3)(m+H)^3$.

Significance

The goal is the paper's central claim: under the stated vacuum law the universe has existed for an infinite past, in a quasi-de Sitter phase with $H\approx1$, and leaves it through a transition in which $H$ and $\Lambda$ fall towards zero, producing radiation. The milestones cover the steps the paper uses to reach it (the vacuum law, the evolution equation and its integration) and the late-time picture (the dust solution and its de Sitter limit, which the paper links to the Eddington–Dirac large-number relation $H\approx m^3$).

The results are proved by hand calculation in the paper. The same evolution equation and implicit solution reappear in Carneiro's later paper Cosmological Concordance Model with Particle Creation (2012), whose statements are also on the platform (namespace CarneiroParticleCreation); this mission formalizes the 2006 paper, its vacuum law and its late-time dust solution. Formalizing them produces a verified account of which statements are exact identities and which are approximations. Where the paper writes "$\approx$", the milestones state the exact identity or asymptotic equivalence behind it.

Difficulty

The algebraic milestones (5, 7) are routine. The goal concerns a function known only implicitly: the solution is the inverse of $H\mapsto\frac12\big(1/H-\operatorname{artanh}H\big)$ on $(0,1)$, and its existence on the whole line, its differentiability and its end behaviour all have to be established for an inverse function, not read off a formula. Milestone 6 is a uniqueness statement on all of $\mathbb R$, so it cannot be checked by substitution. Milestones 1 and 10 are improper integrals whose values involve $\zeta(4)=\pi^4/90$ and $\zeta(3)$, and they need integrability arguments near $0$ and $\infty$. Milestones 2, 3, 8 and 9 involve derivatives of complex exponentials, square roots and real powers, where Lean's conventions for $\sqrt{\cdot}$ and $x^{2/3}$ at non-positive arguments must be handled.

Formalization scope

• Real numbers throughout; the scalar field is complex-valued, and derivatives are one-variable derivatives in $t$ or $r$.
• In milestones 2–3 the Hubble parameter is a constant and the Laplacian of the radial plane wave is $\partial_r^2$, which is the paper's approximation.
• $\operatorname{artanh}$ is Mathlib's Real.artanh, the real power $x^{2/3}$ is Real.rpow, $\sim$ is Asymptotics.IsEquivalent, and $\zeta(3)$ is written as $\sum_{n\ge0}1/(n+1)^3$.
• Every statement that divides by $\omega$ or $H$ assumes $\omega>0$ or $H(t)\neq0$. The goal requires the solution on the whole real line and states both limits, so a solution on a half-line or a constant function does not satisfy it.
• Approximate steps of the paper that are not exact statements (the identification $b\approx H$, the radiation law $a\propto t^{1/2}$ quoted from earlier work, and the holographic entropy estimates) are not formalized.

Contributions are welcome on all milestones. The inverse-function and Bose-integral arguments can be reused outside this mission.

Selected references

• S. Carneiro, From de Sitter to de Sitter: a non-singular inflationary universe driven by vacuum, Int. J. Mod. Phys. D 15 (2006) 2241–2247. https://doi.org/10.1142/S0218271806009510
• S. Weinberg, The cosmological constant problem, Rev. Mod. Phys. 61 (1989) 1–23. https://doi.org/10.1103/RevModPhys.61.1

Motivation

Kramers–Wannier duality was found in 1941 as a map between the high- and low-temperature phases of the two-dimensional Ising model (Kramers–Wannier 1941). In its quantum form it exchanges the transverse field $X_j$ and the nearest-neighbour coupling $Z_{j-1}Z_j$ of the transverse-field Ising chain, and it fixes the critical point. In conformal field theory it is implemented by a topological defect line (Fröhlich–Fuchs–Runkel–Schweigert 2004), the prototypical non-invertible symmetry: its fusion with itself is a sum of operators, not a single invertible one (Shao, TASI lectures 2023).

On a finite periodic chain the duality cannot be a unitary operator, because it maps the $\mathbb Z_2$-even sector to itself and annihilates the odd sector. Seiberg–Shao 2023 and Seiberg–Seifnashri–Shao 2024 wrote the exact lattice operator $\mathsf D$ on the tensor-product Hilbert space $(\mathbb C^2)^{\otimes L}$. They showed that its algebra closes only after the lattice translation is included: $\mathsf D^2=(1+\eta)T^{-1}$. This is a lattice relation that a fusion category does not describe, since the continuum fusion rule $\mathcal N^2=1+\eta$ appears only at low energy. The same identity drives the LSM-type constraint proved in that paper.

Timeline. 1941: Kramers and Wannier find the duality of the 2D Ising model. 2004: Fröhlich, Fuchs, Runkel and Schweigert realise it as a conformal defect. 2016: Aasen–Mong–Fendley construct the lattice defects. 2023–2024: Seiberg, Seifnashri and Shao find the exact operator algebra on the tensor-product Hilbert space, including the translation factor.

Setting

Fix $L\ge1$ qubits on a ring, with site indices in $\mathbb Z/L$ (Fin L with modular arithmetic). A computational-basis state is labelled by a configuration $s=(s_0,\dots,s_{L-1})\in(\mathbb Z/2)^L$ (Config L). Operators are complex $2^L\times2^L$ matrices indexed by configurations (Op L). Write $\operatorname{sgn}(a)=(-1)^a$.

• Pauli operators. $X_j|s\rangle=|s+e_j\rangle$ flips spin $j$ (pauliX), and $Z_j|s\rangle=(-1)^{s_j}|s\rangle$ (pauliZ).
• $\mathbb Z_2$ symmetry. $\eta=\prod_j X_j$ flips every spin (eta).
• Translation. $T|s\rangle=|s'\rangle$ with $s'_k=s_{k-1}$ (transl), so that $TX_jT^{-1}=X_{j+1}$.
• Kramers–Wannier operator (kwD):

$$\langle t|\,\mathsf D\,|s\rangle \;=\; 2^{-L/2}\,(-1)^{\sum_{k} t_k\,(s_k+s_{k+1})}.$$

This explicit formula is the definition used throughout. Relations (1.5) together with $\mathsf D\eta=\mathsf D$ determine $\mathsf D$ up to a scalar, and (1.4) fixes the scalar up to a sign. Every statement below is invariant under $\mathsf D\mapsto-\mathsf D$, so this is the operator of Seiberg–Seifnashri–Shao in that paper's normalisation (footnote 1). Its equality with their matrix-product presentation (2.64) is not formalised here.

Formalization targets

Goal: the non-invertible fusion rule (eqs. (1.4), (2.65), (F.18))

$$\mathsf D^2=(1+\eta)\,T^{-1}\qquad\text{for every }L\ge1 .$$

Milestones

1. Invertible algebra (eqs. (1.1)–(1.3), (2.10), (2.65)): $\eta^2=1$, $T\eta=\eta T$, $T^L=1$, $TX_jT^{-1}=X_{j+1}$, $TZ_jT^{-1}=Z_{j+1}$, $\eta X_j=X_j\eta$, $\eta Z_j=-Z_j\eta$.
2. Duality on $X$ (eq. (1.5)): $\mathsf D X_j=Z_{j-1}Z_j\,\mathsf D$.
3. Duality on $ZZ$ (eq. (1.5)): $\mathsf D Z_{j-1}Z_j=X_{j-1}\,\mathsf D$.
4. Absorbing $\eta$ (eqs. (1.4), (2.65)): $\mathsf D\eta=\eta\mathsf D=\mathsf D$.
5. Translation and adjoint (eq. (2.65), Table 1): $T\mathsf D=\mathsf DT$ and $\mathsf D^\dagger=\mathsf DT$.
6. Non-invertibility (§1.1): $\mathsf D$ is not a unit, and $\ker\mathsf D\neq0$.

Significance

The result. The goal identity is the defining relation of the lattice Kramers–Wannier symmetry. Together with milestones 4–5 it shows that $\mathsf D/\sqrt2$ restricted to the $\eta$-even sector squares to a translation, so $\mathsf D$ is a square root of $T^{-1}$ there. The paper uses this to derive its LSM-type constraint, and also to show that the lattice symmetry is not a fusion category, because the continuum rule $\mathcal N^2=1+\eta$ only emerges at low energy. Milestones 2–3 are the lattice Kramers–Wannier map on $\mathbb Z_2$-invariant operators, so $\mathsf D$ commutes with the critical Ising Hamiltonian $H=-\sum_j(Z_{j-1}Z_j+X_j)$.

Formalizing it. The identities are proved in the physics literature by tensor-network manipulations ((F.14)–(F.18)) and checked numerically, but none of this is machine-checked. This mission produces a reusable Lean setup for qubit chains: Pauli strings on $(\mathbb Z/2)^L$, $\mathbb Z_2$ and translation symmetries, and an exact non-invertible operator with its full operator algebra for every chain length. No mission on the platform or file in Mathlib currently formalizes a non-invertible lattice symmetry.

Difficulty

Each identity is easy to check for a fixed small $L$ by brute force. The content is that it holds for all $L$ at once, on a $2^L$-dimensional space. The difficulty is bookkeeping with periodic indices: sums over $(\mathbb Z/2)^L$ of characters $(-1)^{\langle t,\,\cdot\rangle}$, reindexing $k\mapsto k\pm1$ in Fin L (including $L=1$, where $k+1=k$, and $L=2$, where $k+1=k-1$), and the exact normalisation $2^{-L/2}$, so that the right-hand side carries no stray factor $2^L$. The goal also involves the matrix inverse $T^{-1}$, so a proof must establish that $T$ is invertible rather than rely on Lean's junk value.

Formalization scope

• Representation. Operators are Matrix (Fin L → ZMod 2) (Fin L → ZMod 2) ℂ; products are matrix products; $T^{-1}$ is Mathlib's matrix inverse (transl L)⁻¹; $\dagger$ is conjTranspose. Every theorem assumes [NeZero L], i.e. $L\ge1$.
• Conventions committed to. $Z_j=(-1)^{s_j}$ on basis states, translation to the right ($s'_k=s_{k-1}$), and $\mathsf D$ normalised by $2^{-L/2}$ as in eqs. (1.4)/(2.65). Other conventions (left translation, unnormalised $\mathsf D$) change the statements to $T$ instead of $T^{-1}$ or add a factor $2^L$; the conventions here reproduce the paper's equations verbatim.
• No trivialisation. kwD is an explicit formula, not a hypothesis. The goal fixes both sides completely, and milestone 1 pins the translation convention against eq. (2.10).
• Out of scope. The defect Hamiltonians, the MPO presentation (2.64) itself, the $\mathbb Z_2$- and duality-twisted operators of §§2.3.3–2.3.4, and the LSM constraint of §4.
• Reusable. Pauli operators, translation and $\eta$ on qubit chains; character-sum lemmas over $(\mathbb Z/2)^L$. Contributions of general Mathlib lemmas on Walsh–Hadamard-type sums are welcome.

Selected references

• H. A. Kramers, G. H. Wannier, Statistics of the Two-Dimensional Ferromagnet. Part I, Phys. Rev. 60, 252–262 (1941). doi:10.1103/PhysRev.60.252
• J. Fröhlich, J. Fuchs, I. Runkel, C. Schweigert, Kramers–Wannier duality from conformal defects, Phys. Rev. Lett. 93, 070601 (2004). arXiv:cond-mat/0404051
• D. Aasen, R. S. K. Mong, P. Fendley, Topological Defects on the Lattice I: The Ising model, J. Phys. A 49, 354001 (2016). arXiv:1601.07185
• N. Seiberg, S.-H. Shao, Majorana chain and Ising model – (non-invertible) translations, anomalies, and emanant symmetries, SciPost Phys. 16, 064 (2024). arXiv:2307.02534
• S.-H. Shao, What's Done Cannot Be Undone: TASI Lectures on Non-Invertible Symmetries (2023). arXiv:2308.00747
• Source: N. Seiberg, S. Seifnashri, S.-H. Shao, Non-invertible symmetries and LSM-type constraints on a tensor product Hilbert space, SciPost Phys. 16, 154 (2024). arXiv:2401.12281

Motivation

Near thermodynamic equilibrium, flows of extensive quantities (heat, matter, charge) depend linearly on the thermodynamic forces (gradients of the conjugate intensive variables). Some of the coefficients in these linear laws describe cross effects: a temperature gradient driving an electric current (Seebeck effect), a voltage driving a heat flow (Peltier effect), a temperature gradient driving diffusion (Soret effect) and its converse (Dufour effect). In 1931 Lars Onsager showed that, as a consequence of the time-reversibility of microscopic dynamics, the matrix of these coefficients is symmetric (Onsager 1931). These reciprocal relations were confirmed experimentally across many classes of irreversible processes (Miller 1960), and Onsager received the 1968 Nobel Prize in Chemistry for them.

This mission formalizes the abstract, finite-dimensional version of Onsager's principle as presented by Landau and Lifshitz (Statistical Physics, Part 1, 1975) and reproduced in the Wikipedia article Onsager reciprocal relations, sections "Abstract formulation" and "Proof".

Setting

Let $x=(x_1,\dots,x_n)\in\mathbb R^n$ be the fluctuations of $n$ thermodynamic quantities from their equilibrium values. For small fluctuations the entropy is quadratic, and Boltzmann's formula gives the Gaussian fluctuation distribution

$$w(x)=\tilde A\,e^{-\frac12\beta_{ik}x_ix_k},$$

where $\beta$ is a positive definite symmetric real $n\times n$ matrix and summation over repeated indices is understood. Write $\langle f\rangle$ for the average of $f(x)$ with respect to $w$.

The thermodynamic conjugate quantities are $X_i=\beta_{ik}x_k$. In the quasi-stationary regime the fluctuations relax according to $\dot x_i=-\lambda_{ik}x_k$ for a real matrix $\lambda$, so that $\dot x_i=-\gamma_{ik}X_k$ with the kinetic coefficients

$$\gamma_{ik}=\lambda_{il}\,(\beta^{-1})_{lk}.$$

The mean value at time $t$ of a fluctuation which takes the value $x$ at $t=0$ is $\xi(t)=e^{-t\lambda}x$, and $\Xi(t)=\beta\xi(t)$. The time correlation is $\langle x_i(t)x_k(0)\rangle=\langle\xi_i(t)x_k\rangle$.

Formalization targets

Goal: Onsager's principle

If fluctuations are symmetric under time reversal,

$$\langle \xi_i(t)\,x_k\rangle=\langle x_i\,\xi_k(t)\rangle\qquad(t\ge0,\ 1\le i,k\le n),$$

then the kinetic coefficients are symmetric:

$$\gamma_{ik}=\gamma_{ki}.$$

Milestones (in the order of the source's argument)

1. $\dot x_i=-\lambda_{ik}x_k=-\gamma_{ik}X_k$ (definition of kinetic coefficients).
2. $\xi(0)=x$ and $\dot\xi_i(t)=-\gamma_{ik}\Xi_k(t)$.
3. $\frac{d}{dt}\langle\xi_i(t)x_k\rangle=-\gamma_{il}\langle\Xi_l(t)x_k\rangle$.
4. $\langle X_ix_k\rangle=\delta_{ik}$.
5. Under time-reversal symmetry, $\gamma_{il}\langle X_lx_k\rangle=\gamma_{kl}\langle X_lx_i\rangle$.

Significance

The symmetry $\gamma_{ik}=\gamma_{ki}$ is the mathematical content of the reciprocal relations: it reduces the number of independent transport coefficients from $n^2$ to $n(n+1)/2$ and yields the equality of measurable cross-coefficients such as the Peltier and Seebeck coefficients. Together with the positive semi-definiteness of the coefficient matrix (from non-negative entropy production), it is the basic structural input of linear irreversible thermodynamics.

The result is classical and its proof is standard in physics textbooks; this mission produces a machine-checked version of the finite-dimensional argument, including the Gaussian moment identity $\langle X_ix_k\rangle=\delta_{ik}$ and the differentiation of the time-correlation function under the integral sign. No machine-checked formalization of this statement is known to the proposer.

Difficulty

The algebraic core is short, but the formal argument needs analytic input that the textbook treats as routine: Gaussian integrals over $\mathbb R^n$ for a general positive definite $\beta$ (integrability of polynomial moments against $e^{-\frac12x^{\mathsf T}\beta x}$ and the value of the second moments), differentiation of a parameter-dependent integral involving a matrix exponential, and the passage from an identity valid for $t\ge0$ to an identity between derivatives at the boundary point $t=0$, where only a one-sided derivative is available from the hypothesis.

Formalization scope

Vectors are functions Fin n → ℝ with Lebesgue measure; matrices are Matrix (Fin n) (Fin n) ℝ, and β.PosDef (which includes symmetry) is assumed in every theorem. The average $\langle f\rangle$ is the ratio $\int f\,w\,dx/\int w\,dx$ of Bochner integrals, so the normalizing constant $\tilde A$ cancels. The mean relaxation is the matrix exponential $\xi(t)=e^{-t\lambda}x$. The time-reversal hypothesis is assumed only for $t\ge0$. The entropy $S$ and Boltzmann's constant are not modelled; $\beta$ is the primitive datum, as in the source's statement of the principle. The hypothesis is non-vacuous (e.g. $\lambda=\beta$ satisfies it), and the conclusion concerns $\gamma=\lambda\beta^{-1}$, not $\lambda$.

All definitions are collected in Definitions.Def_OnsagerReciprocal_basic (namespace OnsagerReciprocal). Reusable Gaussian-moment lemmas for positive definite quadratic forms are welcome contributions.

Selected references

• L. Onsager, Reciprocal Relations in Irreversible Processes. I, Physical Review 37 (1931) 405–426. doi:10.1103/physrev.37.405
• D. G. Miller, Thermodynamics of Irreversible Processes. The Experimental Verification of the Onsager Reciprocal Relations, Chemical Reviews 60 (1960) 15–37. doi:10.1021/cr60203a003
• L. D. Landau, E. M. Lifshitz, Statistical Physics, Part 1, Butterworth-Heinemann (1975).
• Wikipedia, Onsager reciprocal relations, oldid 1355014688.

Motivation

In 1913 Albert Einstein and the mathematician Marcel Grossmann published the Entwurf ("outline") of a generalized theory of relativity and a theory of gravitation. It is the first theory in which the gravitational field is described by the ten components $g_{\mu\nu}$ of a space-time metric, $ds^2=\sum_{\mu\nu}g_{\mu\nu}\,dx_\mu dx_\nu$, and in which Ricci and Levi-Civita's absolute differential calculus (Grossmann's mathematical part) is brought into physics. Its gravitational field equations were superseded by the generally covariant field equations of November 1915, but the framework of the Entwurf — metric as gravitational potential, the energy-momentum law of matter in a gravitational field, a stress-energy expression for the gravitational field itself — carried over to general relativity.

The physical part (Part I, by Einstein) derives the field equations from one requirement: the energy-momentum law must hold for matter and gravitational field together. The derivation runs through an explicit differential identity, eq. (12), whose rewritten form (12a) yields the field equations (18) and the total conservation law (19). This mission formalizes that chain of statements.

Timeline.

• 1912: Einstein's theory of the static gravitational field, with a single scalar potential $c(x)$ (Ann. d. Physik 38).
• 1913: Einstein–Grossmann, Entwurf: metric tensor $g_{\mu\nu}$, energy-momentum law (10), field equations (18), conservation law (19).
• 1915: Einstein, Die Feldgleichungen der Gravitation (Sitzungsber. Preuss. Akad. Wiss.): generally covariant field equations replace (18).

Setting

All objects live in one coordinate chart, $x=(x_1,x_2,x_3,x_4)\in\mathbb R^4$, with $x_4$ the time coordinate. The fundamental tensor $g_{\mu\nu}(x)$ is a symmetric $4\times4$ matrix field with negative determinant $g=\det(g_{\mu\nu})$; $\gamma_{\mu\nu}$ is the reciprocal (contravariant) tensor, the inverse matrix, and $\sqrt{-g}$ is the density factor. All sums run over $1,\dots,4$.

A material process is described by its contravariant stress-energy tensor $\Theta_{\mu\nu}$ (for incoherent dust, $\Theta_{\mu\nu}=\varrho_0\frac{dx_\mu}{ds}\frac{dx_\nu}{ds}$). Its energy-momentum law in the gravitational field is eq. (10):

$$\sum_{\mu\nu}\frac{\partial}{\partial x_\nu}\big(\sqrt{-g}\,g_{\sigma\mu}\Theta_{\mu\nu}\big)-\tfrac12\sum_{\mu\nu}\sqrt{-g}\,\frac{\partial g_{\mu\nu}}{\partial x_\sigma}\Theta_{\mu\nu}=0\qquad(\sigma=1,2,3,4).$$

The second sum is the momentum (for $\sigma=4$, the energy) transferred per unit volume from the gravitational field to matter.

The gravitational field carries its own stress-energy tensor $\vartheta_{\mu\nu}$, eq. (13):

$$-2\kappa\,\vartheta_{\mu\nu}=\sum_{\alpha\beta\tau\rho}\Big(\gamma_{\alpha\mu}\gamma_{\beta\nu}\frac{\partial g_{\tau\rho}}{\partial x_\alpha}\frac{\partial\gamma_{\tau\rho}}{\partial x_\beta}-\tfrac12\gamma_{\mu\nu}\gamma_{\alpha\beta}\frac{\partial g_{\tau\rho}}{\partial x_\alpha}\frac{\partial\gamma_{\tau\rho}}{\partial x_\beta}\Big),$$

and the field equations involve the second-order operator of eq. (15),

$$\Delta_{\mu\nu}(\gamma)=\sum_{\alpha\beta}\frac{1}{\sqrt{-g}}\frac{\partial}{\partial x_\alpha}\Big(\gamma_{\alpha\beta}\sqrt{-g}\,\frac{\partial\gamma_{\mu\nu}}{\partial x_\beta}\Big)-\sum_{\alpha\beta\tau\rho}\gamma_{\alpha\beta}g_{\tau\rho}\frac{\partial\gamma_{\mu\tau}}{\partial x_\alpha}\frac{\partial\gamma_{\nu\rho}}{\partial x_\beta}.$$

The Entwurf field equations (18) read $\Delta_{\mu\nu}(\gamma)=\kappa(\Theta_{\mu\nu}+\vartheta_{\mu\nu})$, with $\kappa$ a constant. Lowering indices with $g$ gives the covariant objects $T_{\mu\nu}=\sum g_{\mu\alpha}g_{\nu\beta}\Theta_{\alpha\beta}$, $t_{\mu\nu}$ (eq. (14)) and the operator $D_{\mu\nu}(g)$ (eq. (16)).

Formalization targets

Goal: eq. (19)

If the energy-momentum law (10) and the field equations (18) hold, then for $\sigma=1,2,3,4$

$$\sum_{\mu\nu}\frac{\partial}{\partial x_\nu}\Big\{\sqrt{-g}\,g_{\sigma\mu}(\Theta_{\mu\nu}+\vartheta_{\mu\nu})\Big\}=0.$$

Milestones

1. The electrostatic model identity of p. 14, which illustrates the method.
2. Identity (12a): $\sum_{\mu\nu}\frac{\partial}{\partial x_\nu}\{\sqrt{-g}\,g_{\sigma\mu}\kappa\vartheta_{\mu\nu}\}=\tfrac12\sum_{\mu\nu}\sqrt{-g}\,\frac{\partial g_{\mu\nu}}{\partial x_\sigma}\{-\Delta_{\mu\nu}(\gamma)+\kappa\vartheta_{\mu\nu}\}$, for every metric.
3. Identity (12b), the covariant counterpart, with $t_{\mu\nu}$ and $D_{\mu\nu}(g)$.
4. Eq. (10) $\Leftrightarrow$ eq. (20), the covariant energy-momentum law.
5. Eq. (18) $\Rightarrow$ eq. (21), $-D_{\mu\nu}(g)=\kappa(t_{\mu\nu}+T_{\mu\nu})$.
6. Eq. (22), the covariant conservation law for matter plus field.

Significance

The result itself. Eq. (19) is the property Einstein required of any relativistic theory of gravitation: the energy of the gravitational field acts as a source in the same way as every other form of energy, and matter together with field obeys conservation laws of divergence form. Identity (12a) is what makes this work for the Entwurf operator $\Delta_{\mu\nu}(\gamma)$; together with the matter law (10), the field equations (18) and the gravitational stress-energy $\vartheta_{\mu\nu}$ are fixed by it.

Formalizing it. These statements are proved in the source by explicit computation, and the steps (12) → (12a) and the covariant forms (20)–(22) are given without the intermediate algebra. A machine-checked development provides the full index computations: derivatives of $\gamma_{\mu\nu}$ and $\sqrt{-g}$ in terms of those of $g_{\mu\nu}$, the contractions in (12a) and (12b), and the lowering identities linking $\Delta_{\mu\nu}(\gamma)$ to $D_{\mu\nu}(g)$ and $\vartheta_{\mu\nu}$ to $t_{\mu\nu}$. A search of the platform library found no existing formalization of these statements.

Difficulty

There is no conceptual obstacle, but the identities are long. Identity (12a) involves second derivatives of $\gamma_{\mu\nu}$, the derivative of $\sqrt{-g}$, and contractions over up to six indices. The source gives only the final form of (12) and says the identity is obtained "nach dem angedeuteten Verfahren"; the intermediate algebra, and the analytic facts behind it (differentiability of matrix inversion and of $\sqrt{-\det g}$ under the standing assumptions), are not written out. A naive expansion of all sums produces thousands of terms.

Formalization scope

• Space-time is $\mathbb R^4$ as one global chart, with points $x:\mathrm{Fin}\,4\to\mathbb R$; two-index fields are matrix-valued functions. Partial derivatives are Fréchet derivatives along coordinate directions.
• Standing assumptions on the metric: entries $C^2$, symmetric, $\det g<0$ everywhere. No signature condition beyond the sign of the determinant; $\gamma$ is the matrix inverse, $\sqrt{-g}$ the real square root of $-\det g$.
• $\kappa\neq0$ is assumed wherever $\vartheta_{\mu\nu}$ or $t_{\mu\nu}$ (defined with the factor $1/(2\kappa)$) appears. Matter tensors are assumed $C^1$, and symmetric where the source's manipulation needs it (eq. (20)).
• In eq. (14) the sum over $\alpha,\beta$ is taken only in the term containing them, following the paper's convention. The printed eq. (22) has an inconsistent index placement; milestone 6 uses the placement of (20) and (12b).
• The goal must not be trivialized: the field equations and the matter law are hypotheses about the same $\Theta_{\mu\nu}$, and the hypotheses are satisfiable (e.g. constant metric, $\Theta=0$) but not degenerate in general.
• Reusable infrastructure: derivative formulas for the inverse and determinant of a $C^k$ matrix field, coordinate tensor calculus on $\mathbb R^4$. Contributions of these as separate lemmas are welcome.

Selected references

• A. Einstein and M. Grossmann, Entwurf einer verallgemeinerten Relativitätstheorie und einer Theorie der Gravitation, B. G. Teubner, Leipzig und Berlin, 1913; reprinted in Zeitschrift für Mathematik und Physik 62 (1914). The source of all statements of this mission (Part I, §§4–5, pp. 10–17).
• A. Einstein, Die Feldgleichungen der Gravitation, Sitzungsberichte der Preußischen Akademie der Wissenschaften, 1915, pp. 844–847.

Motivation

The first law of thermodynamics is the form the law of conservation of energy takes for thermodynamic processes. For a closed system (no transfer of matter) it is usually written, in the sign convention of Clausius, as

$$\Delta U = Q - W,$$

where $Q$ is the heat supplied to the system, $W$ is the work done by the system on its surroundings, and $U$ is the internal energy. Heat and work describe a process and depend on the path; the internal energy is a property of the state, and its change depends only on the initial and final states.

The Wikipedia article First law of thermodynamics (revision oldid=1366986255) describes two ways of reaching this statement. In the original "thermodynamic approach" (Clausius 1850, Rankine), heat, defined by calorimetry, and work are primitive notions. In the "mechanical approach" (Bryan 1907, Carathéodory 1909, Born 1921), only adiabatic work is primitive. The law then asserts that adiabatic work is independent of the path, and that this work defines a state function $U$, fixed up to an additive constant. Heat becomes a derived quantity, the residual $Q = \Delta U + W$. This mission formalizes the logical core of the mechanical approach.

Setting

A closed system has a set $\sigma$ of states. A process $p$ has an initial state $p_{\mathrm{start}}$, a final state $p_{\mathrm{finish}}$, a net work $W(p)\in\mathbb R$ done by the system on its surroundings, and a label recording whether it is adiabatic (carried out inside an adiabatic enclosure, so that energy is transferred only as work). A set $\mathcal P$ of processes stands for the processes that can actually be carried out. It is assumed to satisfy:

1. Composition: if $p,q\in\mathcal P$ and $p_{\mathrm{finish}}=q_{\mathrm{start}}$, then the composite "first $p$, then $q$" lies in $\mathcal P$. Its work is $W(p)+W(q)$, and it is adiabatic exactly when both stages are.
2. Null processes: for every state $A$, leaving the system in state $A$ (with no work and no exchange) is in $\mathcal P$.
3. Path independence of adiabatic work: any two adiabatic processes in $\mathcal P$ with the same initial and final states involve the same work.
4. Adiabatic accessibility: there is a reference state $O$ such that every state $A$ is reached from $O$, or reaches $O$, by some adiabatic process in $\mathcal P$.

A function $U:\sigma\to\mathbb R$ is an internal energy for $\mathcal P$ if $U(p_{\mathrm{finish}})-U(p_{\mathrm{start}})=-W(p)$ for every adiabatic $p\in\mathcal P$. For a given $U$, the heat supplied in a process is the residual

$$Q_U(p)=U(p_{\mathrm{finish}})-U(p_{\mathrm{start}})+W(p).$$

Formalization targets

Goal: existence and uniqueness of internal energy

Under assumptions 1 to 4,

$$\exists\,U \text{ internal energy for } \mathcal P,\qquad\text{and}\qquad U,U' \text{ internal energies} \implies \exists c\in\mathbb R\ \forall A,\ U'(A)=U(A)+c.$$

This is the article's statement: "For all adiabatic processes between two specified states of a closed system of any nature, the net work done is the same regardless the details of the process, and determines a state function called internal energy, $U$", together with its remark that the internal energy "is defined only up to an arbitrary additive constant of integration".

Milestones

1. Formula (1) and the chain through the reference state. If quasi-static adiabatic work $W_{A\to B}$ satisfies $W_{A\to O}=-W_{O\to A}$ and $W_{A\to B}=W_{A\to O}+W_{O\to B}$, and $U(A)=U(O)-W_{O\to A}$, then $-W_{A\to B}=U(B)-U(A)$.
2. Shifting an internal energy by a constant gives an internal energy.
3. Under adiabatic accessibility, two internal energies differ by a constant.
4. Under assumptions 1 to 4, an internal energy exists (normalized by $U(O)=0$).
5. The Clausius form $\Delta U=Q-W$ holds for the residual heat.
6. Adiabatic processes involve no heat.
7. In an adynamic process (no work), $Q=\Delta U$.
8. Heat does not depend on the additive constant in $U$.
9. In a cyclic process, the net work done equals the net heat taken in.
10. No adiabatic cyclic process produces net work (no perpetual motion machine of the first kind).

Significance

The goal makes precise the step in the mechanical approach where internal energy is defined from adiabatic work instead of being postulated. It shows which properties of the set of realizable processes are needed for the definition to make sense. Once $U$ exists, the familiar consequences follow at once: the Clausius equation for every process, the heat-free character of adiabatic processes, $Q=\Delta U$ for adynamic processes, the equality of work and heat over a cycle, and the impossibility of perpetual motion of the first kind. Milestones 5 to 10 record these.

The mathematics is elementary and the results are classical. The value of the formalization is that it states exactly the hypotheses under which "path-independent adiabatic work defines a state function" holds. The article itself notes the gaps: experimental evidence for independence from the order of stages is thin (Bailyn), and Münster observes that one cannot always go adiabatically in both directions between two states. Assumption 4 therefore asks only for one direction.

Difficulty

The only non-routine step is existence when accessibility holds in just one direction per state. One defines $U(A)=-W(O\to A)$ or $U(A)=W(A\to O)$, depending on which link exists. Showing that this choice is consistent, and that it gives $\Delta U=-W$ for an arbitrary adiabatic process $A\to B$, requires splitting into four cases according to how $A$ and $B$ are linked to $O$. In some of these cases the composite process is an adiabatic cycle, which must be compared with a null process. Without null processes, or without closure under composition, the naive definition is not well-defined.

Formalization scope

• States form an arbitrary type $\sigma$. Work is real-valued and is work done by the system (Clausius convention), so that $\Delta U=-W$ for adiabatic processes and $\Delta U=Q-W$ in general.
• "Adiabatic" is a primitive label on processes, as adiabatic walls are primitive in the mechanical approach. Heat is not primitive: it is defined as the residual $Q_U(p)=\Delta U+W$.
• The physically realizable processes form a set $\mathcal P$. All hypotheses are stated about $\mathcal P$, never about every conceivable process.
• The goal is not vacuous: assumptions 1 to 4 can all hold at once (for example, states $\mathbb R$, with adiabatic work from $a$ to $b$ equal to $a-b$).
• Open systems, matter transfer, the extensivity statement $U_0=U_1+U_2$, and the differential form $dU=\delta Q-\delta W$ are out of scope for this first mission.

Selected references

• Wikipedia, First law of thermodynamics, revision oldid=1366986255. https://en.wikipedia.org/w/index.php?title=First_law_of_thermodynamics&oldid=1366986255
• C. Carathéodory, Untersuchungen über die Grundlagen der Thermodynamik, Mathematische Annalen 67 (1909), 355–386. https://ui.adsabs.harvard.edu/abs/1909MatAn..67..355C
• M. Born, Kritische Betrachtungen zur traditionellen Darstellung der Thermodynamik, Physikalische Zeitschrift 22 (1921), 218–224.

Motivation

Why is general relativity not a renormalizable quantum field theory? The textbook answer is perturbative: Newton's constant has negative mass dimension, so the gravitational coupling is irrelevant and loop divergences cannot be absorbed into finitely many counterterms. That argument can in principle be evaded (Weinberg's asymptotic safety). Shomer's note (arXiv:0709.3555), following Banks and Aharony–Banks, gives a non-perturbative, thermodynamic argument instead: the very-high-energy spectrum of any renormalizable $d$-dimensional QFT is that of a $d$-dimensional conformal field theory (CFT), whereas the high-energy spectrum of gravity is dominated by black holes, whose Bekenstein–Hawking entropy grows with energy in a way no CFT can match.

Setting

• CFT side (Sec. IV, Eqs. 29–30). For a $d$-dimensional CFT on $\mathbb R_{\text{time}}\times S^{d-1}$ (sphere radius $R$) at temperature $T$, dimensional analysis and extensivity give $S=a\,(RT)^{d-1}$ and $E=b\,R^{d-1}T^{d}$ with constants $a,b>0$. Eliminating $T$ gives the entropy as a function of energy, $S_{\rm CFT}(E)=a\,\bigl(R\,(E/(bR^{d-1}))^{1/d}\bigr)^{d-1}\sim E^{(d-1)/d}$.
• Flat gravity (Sec. V.1, Eqs. 31–32). The $d$-dimensional Schwarzschild metric has $f(r)=1-\omega_{d-2}G_N M/r^{d-3}$ with $\omega_n=16\pi/(n\,\mathrm{Vol}(S^n))$. The horizon $r_H$ is the zero of $f$, and the Bekenstein–Hawking entropy is $S=A/(4G_N)$ with $A=\mathrm{Vol}(S^{d-2})\,r_H^{d-2}$, giving $S\sim M^{(d-2)/(d-3)}$.
• AdS gravity (Sec. V.2, Eqs. 33–34). With $f(r)=1-\omega_{d-2}G_NM/r^{d-3}+r^2/R_{\rm AdS}^2$ the horizon is the largest zero of $f$ and $S\sim M^{(d-2)/(d-1)}$ — the CFT law of one dimension lower (a shadow of AdS/CFT).

Formalization targets

Goal — black-hole entropy is not CFT entropy (flat space, Sec. V.1)

For every spacetime dimension $d\ge 4$, every $G_N>0$ and every CFT datum $a,b,R>0$,

$$S_{\rm BH}(E)\ \text{is not}\ \Theta\bigl(S_{\rm CFT}(E)\bigr)\quad\text{as }E\to\infty .$$

Here $\Theta$ means bounded above and below by positive multiples of each other for all large $E$; this is how the paper's "$\sim$" is read.

Milestones

Eq. (29) (the elimination of $T$), Eq. (30), Eq. (32) exactly, footnote 26 (exponent comparison), Eq. (34) asymptotically, the AdS mismatch with a $d$-dimensional CFT, and the AdS match with a $(d-1)$-dimensional CFT.

Significance

The goal is the precise mathematical content of the paper's one-line argument: once the black-hole entropy formula and the CFT scaling law are fixed, their large-energy growth exponents $(d-2)/(d-3)>1>(d-1)/d$ are incompatible. The physics inputs (that a renormalizable QFT flows to a CFT in the UV, that black holes dominate the gravitational density of states, the Bekenstein–Hawking formula) are modelling assumptions, encoded as definitions; the mission formalizes the asymptotic analysis that turns them into a contradiction, not the physics itself.

Difficulty

Mathematically elementary but fiddly: the horizon radius is defined implicitly as the largest positive zero of $f$, so one must solve $f(r_H)=0$ (exactly in flat space, asymptotically in AdS, where $r_H^{d-3}(1+r_H^2/R_{\rm AdS}^2)=\omega_{d-2}G_NM$), handle real powers, and compare asymptotic classes with distinct exponents.

Formalization scope

All statements live in namespace GravityNonRenorm and import one definition file. The unit-sphere volume is the closed form $\mathrm{Vol}(S^n)=2\pi^{(n+1)/2}/\Gamma((n+1)/2)$. Horizon radii are sSup of the set of positive zeros of $f$ (junk value $0$ when that set is empty, e.g. for $M\le 0$); all claims are asymptotic as $E\to\infty$ or assume $M>0$, so the junk value is never used. Dimensions are natural numbers; $d\ge 4$ for flat-space statements, $d\ge3$ for AdS, $d\ge2$ for CFT statements.

Selected references

• A. Shomer, A pedagogical explanation for the non-renormalizability of gravity, arXiv:0709.3555 (2007). https://arxiv.org/abs/0709.3555
• O. Aharony and T. Banks, Note on the quantum mechanics of M theory, JHEP 9903:016 (1999), arXiv:hep-th/9812237.

Motivation

Fick's laws of diffusion, posited by Adolf Fick in 1855, are the basic constitutive and evolution laws for the transport of mass by diffusion. The first law states that the diffusive flux is proportional to minus the concentration gradient, $J=-D\,\partial_x\varphi$; the second law is the resulting evolution equation for the concentration,

$$\frac{\partial\varphi}{\partial t}=D\,\frac{\partial^2\varphi}{\partial x^2}.$$

They are the standard model for diffusion in solids, liquids and gases (in the absence of bulk flow), and are used to model transport in foods, neurons, biopolymers, pharmaceuticals, porous soils, nuclear materials and semiconductor doping. Mathematically, the second law is the heat equation with the thermal diffusivity replaced by the diffusion coefficient $D>0$.

This mission formalizes the mathematical content of the Wikipedia article Fick's laws of diffusion: the derivation of the second law from the first, the steady state, the fundamental solution, the error-function solutions for a constant source, and the mean-squared-displacement law.

Setting

A concentration is a real function $\varphi(x,t)$ of position $x$ and time $t$; a flux is a real function $J(x,t)$. The diffusion coefficient is a constant $D>0$. For $t>0$ the diffusion kernel is

$$\varphi_D(x,t)=\frac{1}{\sqrt{4\pi Dt}}\exp\Big(-\frac{x^2}{4Dt}\Big),$$

and in $n$ space dimensions

$$\varphi^{(n)}_D(x,t)=(4\pi Dt)^{-n/2}\exp\Big(-\frac{\|x\|^2}{4Dt}\Big),\qquad x\in\mathbb R^n.$$

The complementary error function is $\operatorname{erfc}(u)=\frac{2}{\sqrt\pi}\int_u^\infty e^{-s^2}\,ds$.

Formalization targets

Goal: the fundamental solution

For $D>0$, $\varphi_D$ solves $\partial_t\varphi=D\partial_x^2\varphi$ for $t>0$, has $\int_{\mathbb R}\varphi_D(x,t)\,dx=1$ for every $t>0$, and satisfies

$$\lim_{t\to0^+}\int_{\mathbb R}\varphi_D(x-y,t)f(y)\,dy=f(x)$$

for every bounded continuous $f$ and every $x$.

Milestones

1. Fick's second law follows from Fick's first law and mass conservation $\partial_t\varphi+\partial_xJ=0$ (constant $D$).
2. A $C^2$ steady state in one dimension is linear: $c(x)=ax+b$.
3. The three components of the goal, separately (PDE, unit mass, initial point source).
4. $n(x,t)=n_0\operatorname{erfc}\big(x/(2\sqrt{Dt})\big)$ solves the second law with $n(0,t)=n_0$ and $n(x,0^+)=0$ for $x>0$.
5. $n(x,t)=\frac{n_0}{2}\operatorname{erfc}\big(x/(2\sqrt{Dt})\big)$ solves the second law with initial profile $n_0$ on $x<0$ and $0$ on $x>0$.
6. Mean squared displacement in $\mathbb R^n$: $\int\|x\|^2\varphi^{(n)}_D(x,t)\,dx=2nDt$.

Significance

The fundamental solution is what makes the second law usable: the solution of the one-dimensional diffusion problem with bounded continuous initial data is the convolution of the data with $\varphi_D$, and the erfc profiles and diffusion length $2\sqrt{Dt}$ quoted throughout applications are derived from it. The mean-squared-displacement law $2nDt$ connects the macroscopic diffusion coefficient to the microscopic Brownian motion of particles.

All statements are classical and proved in the literature; the task here is to formalize them. Mathlib provides the Gaussian integral but has no error function and no development of the one-dimensional diffusion equation, so the mission also produces reusable infrastructure (erfc and its derivative and limits, Gaussian moments in $\mathbb R^n$, the approximate-identity property).

Difficulty

The individual computations are routine on paper; the formal difficulty lies in rigor that the article leaves implicit: differentiating the kernel in both variables only on $t>0$, justifying limits of parameter-dependent integrals as $t\to0^+$ (dominated convergence for the point-source property), computing the second moment of an $n$-dimensional Gaussian on Euclidean space, and building erfc from scratch, including its derivative $-\frac{2}{\sqrt\pi}e^{-u^2}$ and its limits at $\pm\infty$.

Formalization scope

All objects are real-valued; derivatives are Mathlib's deriv (which is $0$ at non-differentiable points), integrals are Lebesgue integrals, and limits as $t\to0^+$ use the right-neighbourhood filter. Every statement about the kernel or erfc profiles assumes $D>0$ and evaluates the PDE only at $t>0$, so junk values of square root and division never matter. The steady-state milestone assumes $C^2$ regularity, without which deriv would admit non-smooth "solutions" such as $|x|$. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Physical parts of the article (Stokes–Einstein relation, Maxwell–Stefan, sorption kinetics, approximations) are out of scope.

Selected references

• Wikipedia contributors, Fick's laws of diffusion. https://en.wikipedia.org/wiki/Fick%27s_laws_of_diffusion
• A. Fick, Ueber Diffusion, Annalen der Physik 170 (1855) 59–86. https://doi.org/10.1002/andp.18551700105
• J. Crank, The Mathematics of Diffusion, 2nd ed., Oxford University Press, 1975.

Motivation

The BCS theory of Bardeen, Cooper and Schrieffer (1957) is the microscopic theory of conventional superconductivity in metals; its authors received the 1972 Nobel Prize in Physics. Its most quoted quantitative predictions are universal numbers: in the weak-coupling limit the zero-temperature energy gap and the transition temperature are related by $\Delta(0) = (\pi/e^{\gamma})\,k_BT_c \approx 1.764\,k_BT_c$, the gap closes as $\Delta(T)/\Delta(0)\approx 1.74\sqrt{1-T/T_c}$, and the specific heat jumps by $(C_{es}-C_{en})/C_{en}\approx 1.43$ at $T_c$. These numbers are what experiments compare against, and they follow from a single scalar integral equation, the BCS gap equation. This mission formalizes that mathematical core, following the section Erfolge der BCS-Theorie of the German Wikipedia article BCS-Theorie.

Timeline (as summarized in the source):

• 1950 — isotope effect observed (Lock et al.; Maxwell; Serin et al.): $T_c$ depends on the ionic mass $M$.
• 1956 — Cooper shows that an arbitrarily weak attraction binds two electrons above a filled Fermi sea.
• 1957 — Bardeen, Cooper and Schrieffer publish Theory of Superconductivity, including the gap equation and its consequences.

Setting

Fix the Boltzmann constant $k_B>0$, the Debye energy $\hbar\omega_D>0$ (called hbarOmegaD in Lean) and the dimensionless coupling $\lambda = V_0\,Z(E_F)>0$ (called coupling), where $V_0$ is the attractive pairing potential and $Z(E_F)$ is half the electronic density of states at the Fermi energy. With the quasiparticle energy $E(\eta,\Delta)=\sqrt{\eta^2+\Delta^2}$ define

$$I_0(\hbar\omega_D,\Delta)=\int_0^{\hbar\omega_D}\frac{d\eta}{\sqrt{\eta^2+\Delta^2}},\qquad I(k_B,\hbar\omega_D,\Delta,T)=\int_0^{\hbar\omega_D}\frac{d\eta}{\sqrt{\eta^2+\Delta^2}}\tanh\frac{\sqrt{\eta^2+\Delta^2}}{2k_BT}.$$

The zero-temperature gap $\Delta(0)$ is the positive solution of $1/\lambda = I_0(\hbar\omega_D,\Delta)$; the critical temperature $T_c$ is the positive solution of $1/\lambda = I(k_B,\hbar\omega_D,0,T)$; and for $0<T<T_c$ the gap $\Delta(T)$ is the positive solution of $1/\lambda = I(k_B,\hbar\omega_D,\Delta,T)$. The Fermi–Dirac function is $f(E,T) = 1/(e^{E/k_BT}+1)$, and $1-2f(E,T) = \tanh(E/2k_BT)$.

Formalization targets

Goal: the universal gap ratio

$$\lim_{\lambda\to0^+}\frac{\Delta(0)}{k_BT_c}=\frac{\pi}{e^{\gamma}}=1.764\ldots$$

with $\gamma$ the Euler–Mascheroni constant. The source writes $\Delta(T=0)=2\hbar\omega_D e^{-1/V_0Z(E_F)}=\frac{\pi}{e^\gamma}k_BT_c$; both equalities are weak-coupling asymptotics, so the goal is stated as a limit $\lambda\to0^+$ at fixed $k_B$, $\hbar\omega_D$.

Milestones

1. $I_0(\hbar\omega_D,\Delta) = \operatorname{arsinh}(\hbar\omega_D/\Delta)$.
2. $\Delta(0)=\hbar\omega_D/\sinh(1/\lambda)$, the unique positive solution of the $T=0$ gap equation.
3. $\Delta(0)\sim 2\hbar\omega_D e^{-1/\lambda}$ as $\lambda\to0^+$.
4. The Fermi–Dirac and $\tanh$ forms of the finite-temperature gap equation agree.
5. The $T_c$ equation has exactly one positive solution.
6. $k_BT_c\sim\frac{2e^\gamma}{\pi}\hbar\omega_D e^{-1/\lambda}$ (the source's $1{,}14$).
7. Isotope effect: with $\hbar\omega_D = C/\sqrt M$, $T_c\propto M^{-1/2}$.
8. $\Delta(T)$ exists uniquely for $0<T<T_c$, and the gap equation has no positive solution for $T\ge T_c$.
9. Near $T_c$: $\Delta(T)^2/(1-T/T_c)$ has a limit $L(\lambda)$ as $T\to T_c^-$, and $L(\lambda)/\Delta(0)^2\to 8e^{2\gamma}/(7\zeta(3)) = 1.7367^2$ as $\lambda\to0^+$.
10. Specific-heat jump: the left derivative $D(\lambda)$ of $\Delta(T)^2$ at $T_c$ exists, and $-D(\lambda)/(\tfrac{2\pi^2}{3}k_B^2T_c)\to 12/(7\zeta(3)) = 1.426\ldots$.

Significance

The universal ratios are the standard quantitative test that separates weak-coupling (BCS-like) superconductors from strong-coupling ones; deviations from $1.764$ and $1.43$ are used to diagnose strong electron–phonon coupling. Mathematically, each statement is an assertion about a parameter-dependent integral equation and its asymptotics as $\lambda\to0^+$, with the Euler–Mascheroni constant and $\zeta(3)$ arising from the asymptotics of $\int_0^X\tanh(x)/x\,dx$ and from a Sommerfeld-type expansion near $T_c$. These results are classical in the physics literature; the mission aims at a machine-checked derivation of the textbook constants from the gap equation, together with reusable lemmas on monotone parameter-dependent integrals.

Difficulty

The $T=0$ statements reduce to an explicit antiderivative. The finite-temperature statements do not: $T_c$ and $\Delta(T)$ are defined only implicitly, so the asymptotics require a uniform expansion $\int_0^X\tanh(x)/x\,dx=\log X+\log(4e^\gamma/\pi)+o(1)$. The near-$T_c$ and specific-heat statements additionally concern the behaviour of $\Delta(T)^2$ at the boundary point $T_c$, where $\Delta$ itself is not differentiable, and the evaluation of the resulting coefficient in the limit $\hbar\omega_D/k_BT_c\to\infty$.

Formalization scope

• All quantities are real numbers. $\Delta(0)$, $T_c$ and $\Delta(T)$ are defined as real suprema (sSup) of the corresponding positive solution sets, so they equal $0$ when no positive solution exists; existence and uniqueness are separate milestones. In particular $\Delta(T)=0$ for $T\ge T_c$.
• The zero-temperature gap is a separate definition: at $T=0$ the finite-temperature integrand is not used.
• The coupling enters only through $\lambda = V_0Z(E_F)$; asymptotic claims are limits $\lambda\to0^+$ at fixed $k_B,\hbar\omega_D>0$, with the exact constants $2e^\gamma/\pi$, $8e^{2\gamma}/(7\zeta(3))$ and $12/(7\zeta(3))$ in place of the rounded $1{,}14$, $1{,}74^2$ and $1{,}43$. $\zeta(3)$ is written as the real part of riemannZeta 3.
• The specific heat is not modeled thermodynamically; the jump milestone formalizes the source's closed-form expression in terms of $-d\Delta^2/dT$ at $T_c$.
• Needed infrastructure: monotonicity and continuity of parameter-dependent interval integrals, the integral identity for $\operatorname{arsinh}$, asymptotics of $\int_0^X\tanh x/x\,dx$, and Mathlib's Euler–Mascheroni constant and $\zeta(3)$.

Selected references

• J. Bardeen, L. N. Cooper, J. R. Schrieffer, Theory of Superconductivity, Phys. Rev. 108, 1175 (1957). https://doi.org/10.1103/PhysRev.108.1175
• L. N. Cooper, Bound Electron Pairs in a Degenerate Fermi Gas, Phys. Rev. 104, 1189 (1956). https://doi.org/10.1103/PhysRev.104.1189
• Wikipedia (de), BCS-Theorie, section Erfolge der BCS-Theorie (source used for all statements). https://de.wikipedia.org/wiki/BCS-Theorie