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