BCS universal ratio $\Delta(0) = \frac{\pi}{e^\gamma}k_BT_c = 1.764\,k_BT_c$

Proved

BCSTheory.gap_ratio_weak_coupling

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

bcs-theorysuperconductivity

In the weak-coupling BCS model with Debye cutoff $\hbar\omega_D>0$ and Boltzmann constant $k_B>0$ , the ratio of the zero-temperature gap $\Delta(0)$ (positive solution of $\frac1\lambda=\int_0^{\hbar\omega_D}\frac{d\eta}{\sqrt{\eta^2+\Delta^2}}$ ) to $k_BT_c$ (where $T_c>0$ solves $\frac1\lambda=\int_0^{\hbar\omega_D}\frac{d\eta}{\eta}\tanh\frac{\eta}{2k_BT_c}$ ) satisfies

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

where $\lambda = V_0Z(E_F)$ and $\gamma$ is the Euler–Mascheroni constant.

Preamble

import Mathlib
import Definitions.Def_BCSTheory_GapEquation
open Filter Topology

Formal statement

namespace BCSTheory

theorem gap_ratio_weak_coupling (kB hbarOmegaD : ℝ) (hkB : 0 < kB) (hω : 0 < hbarOmegaD) :
    Tendsto (fun coupling : ℝ =>
        zeroTemperatureGap hbarOmegaD coupling /
          (kB * criticalTemperature kB hbarOmegaD coupling))
      (𝓝[>] 0) (𝓝 (Real.pi / Real.exp Real.eulerMascheroniConstant)) := by sorry

end BCSTheory

Source

Wikipedia (de), Artikel „BCS-Theorie“ (PDF-Ausdruck vom 05.10.2026), Abschnitt „Erfolge der BCS-Theorie“, Unterabschnitt „Existenz einer Energielücke“, Formel

\Delta(T=0) = 2\hbar\omega_D e^{-1/V_0Z(E_F)} = \frac{\pi}{e^\gamma}k_BT_c = 1{,}764\,k_BT_c

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor and must not be mistaken for independent testimony; an independent read-back is still advisable before launch.

Let $k_B, \hbar\omega_D$ be real numbers with $k_B>0$ and $\hbar\omega_D>0$ . Then, as $\lambda\to0^+$ (through strictly positive values),

\frac{\Delta_0(\hbar\omega_D,\lambda)}{k_B\,T_c(k_B,\hbar\omega_D,\lambda)} \longrightarrow \frac{\pi}{e^{\gamma}}\approx1.764,

where $\gamma$ is the Euler–Mascheroni constant and, from the definition file,

$\Delta_0(\hbar\omega_D,\lambda) = \sup\{\Delta>0 : \int_0^{\hbar\omega_D}d\eta/\sqrt{\eta^2+\Delta^2} = 1/\lambda\}$ ,
$T_c(k_B,\hbar\omega_D,\lambda) = \sup\{T>0 : \int_0^{\hbar\omega_D}\tanh(|\eta|/(2k_BT))/|\eta|\,d\eta = 1/\lambda\}$ ,

each supremum being $0$ if its set is empty or unbounded above, and a quotient by $0$ being $0$ . Only the limit is asserted; there is no claim about any fixed $\lambda$ .

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

BCS universal ratio Δ(0)=πeγkBTc=1.764 kBTc\Delta(0) = \frac{\pi}{e^\gamma}k_BT_c = 1.764\,k_BT_cΔ(0)=eγπ​kB​Tc​=1.764kB​Tc​

BCS universal ratio $\Delta(0) = \frac{\pi}{e^\gamma}k_BT_c = 1.764\,k_BT_c$