BCS gap equation: gap integrals, $\Delta(0)$ , $T_c$ and $\Delta(T)$

Definition

BCSTheory_GapEquation

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

bcs-theoryintegral-equationsuperconductivity

Weak-coupling BCS model with Debye cutoff. Parameters: Boltzmann constant $k_B>0$ , Debye energy $\hbar\omega_D>0$ , coupling $\lambda = V_0Z(E_F)>0$ (attractive potential times half the density of states at the Fermi energy).

Fermi–Dirac distribution $f(E,T) = 1/(e^{E/k_BT}+1)$ .
Quasiparticle energy $E(\eta,\Delta) = \sqrt{\eta^2+\Delta^2}$ .
$I_0(\hbar\omega_D,\Delta) = \int_0^{\hbar\omega_D} d\eta/\sqrt{\eta^2+\Delta^2}$ (right-hand side of the $T=0$ gap equation).
$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}$ (right-hand side of the finite- $T$ gap equation; for $\Delta=0$ it is the $T_c$ integral).
$\Delta(0) = \sup\{\Delta>0 : I_0(\hbar\omega_D,\Delta) = 1/\lambda\}$ .
$T_c = \sup\{T>0 : I(k_B,\hbar\omega_D,0,T) = 1/\lambda\}$ .
$\Delta(T) = \sup\{\Delta>0 : I(k_B,\hbar\omega_D,\Delta,T) = 1/\lambda\}$ .

Conventions: suprema of empty sets (or sets unbounded above) are $0$ ; division by $0$ is $0$ . Uniqueness of the solutions is stated as separate milestones.

Definition code

import Mathlib

/-!
# BCS gap equation (weak-coupling BCS model with Debye cutoff)

Parameters used throughout:
* `kB > 0` — the Boltzmann constant,
* `hbarOmegaD > 0` — the Debye cutoff energy `ħ ω_D`,
* `coupling > 0` — the dimensionless coupling `V₀ · Z(E_F)` (attractive potential times
  half the density of states at the Fermi energy).
-/

namespace BCSTheory

/-- The Fermi–Dirac distribution `f(E, T) = 1 / (exp(E / (k_B T)) + 1)`. -/
noncomputable def fermiDirac (kB E T : ℝ) : ℝ :=
  1 / (Real.exp (E / (kB * T)) + 1)

/-- The quasiparticle energy `√(η² + Δ²)`. -/
noncomputable def quasiparticleEnergy (η Δ : ℝ) : ℝ :=
  Real.sqrt (η ^ 2 + Δ ^ 2)

/-- The right-hand side of the zero-temperature gap equation,
`∫₀^{ħω_D} dη / √(η² + Δ²)`. -/
noncomputable def gapIntegralZeroTemp (hbarOmegaD Δ : ℝ) : ℝ :=
  ∫ η in (0 : ℝ)..hbarOmegaD, 1 / quasiparticleEnergy η Δ

/-- The right-hand side of the finite-temperature BCS gap equation,
`∫₀^{ħω_D} dη · tanh(√(η² + Δ²) / (2 k_B T)) / √(η² + Δ²)`.
For `Δ = 0` the integrand is `tanh(η / (2 k_B T)) / η` (the critical-temperature equation). -/
noncomputable def gapIntegral (kB hbarOmegaD Δ T : ℝ) : ℝ :=
  ∫ η in (0 : ℝ)..hbarOmegaD,
    Real.tanh (quasiparticleEnergy η Δ / (2 * kB * T)) / quasiparticleEnergy η Δ

/-- The zero-temperature gap `Δ(0)`: the supremum of all `Δ > 0` solving
`1 / (V₀ Z(E_F)) = ∫₀^{ħω_D} dη / √(η² + Δ²)`. -/
noncomputable def zeroTemperatureGap (hbarOmegaD coupling : ℝ) : ℝ :=
  sSup {Δ : ℝ | 0 < Δ ∧ gapIntegralZeroTemp hbarOmegaD Δ = 1 / coupling}

/-- The critical (transition) temperature `T_c`: the supremum of all `T > 0` solving
`1 / (V₀ Z(E_F)) = ∫₀^{ħω_D} (dη / η) tanh(η / (2 k_B T))`. -/
noncomputable def criticalTemperature (kB hbarOmegaD coupling : ℝ) : ℝ :=
  sSup {T : ℝ | 0 < T ∧ gapIntegral kB hbarOmegaD 0 T = 1 / coupling}

/-- The temperature-dependent gap `Δ(T)`: the supremum of all `Δ > 0` solving the
finite-temperature gap equation `1 / (V₀ Z(E_F)) = gapIntegral kB ħω_D Δ T`
(this is `0` when no positive solution exists, e.g. for `T ≥ T_c`). -/
noncomputable def gap (kB hbarOmegaD coupling T : ℝ) : ℝ :=
  sSup {Δ : ℝ | 0 < Δ ∧ gapIntegral kB hbarOmegaD Δ T = 1 / coupling}

end BCSTheory

Source

Wikipedia (de), Artikel „BCS-Theorie“ (PDF-Ausdruck vom 05.10.2026), Abschnitt „Erfolge der BCS-Theorie“, Unterabschnitte „Existenz einer Energielücke“ und „Isotopeneffekt“.

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.

The definition file (namespace BCSTheory) introduces, for real parameters, the following real-valued functions. No hypotheses are attached to any of them; all inputs range over all of $\mathbb R$ .

Fermi–Dirac function $f(k_B,E,T) = \dfrac{1}{e^{E/(k_B T)}+1}$ . If $k_BT = 0$ the exponent $E/(k_BT)$ is taken to be $0$ (division by zero returns $0$ ), so then $f = 1/2$ .
Quasiparticle energy $E(\eta,\Delta) = \sqrt{\eta^2+\Delta^2}$ (non-negative square root).
Zero-temperature gap integral

I_0(\hbar\omega_D,\Delta) = \int_0^{\hbar\omega_D}\frac{d\eta}{\sqrt{\eta^2+\Delta^2}},

an oriented interval integral (negative of $\int_{\hbar\omega_D}^0$ if $\hbar\omega_D<0$ ). Where the integrand is undefined ( $\eta = \Delta = 0$ ) it equals $0$ ; if the integrand is not integrable (e.g. $\Delta = 0$ , $\hbar\omega_D\neq0$ , where $1/|\eta|$ is not integrable at $0$ ) the integral is defined to be $0$ .

Finite-temperature gap integral

I(k_B,\hbar\omega_D,\Delta,T) = \int_0^{\hbar\omega_D}\frac{\tanh\bigl(\sqrt{\eta^2+\Delta^2}/(2k_BT)\bigr)}{\sqrt{\eta^2+\Delta^2}}\,d\eta,

with the same conventions (a quotient with zero denominator is $0$ ; a non-integrable integrand gives integral $0$ ). For $\Delta=0$ the integrand is $\tanh(|\eta|/(2k_BT))/|\eta|$ .

Zero-temperature gap $\Delta_0(\hbar\omega_D,\lambda) = \sup\{\Delta\in\mathbb R : \Delta>0,\ I_0(\hbar\omega_D,\Delta) = 1/\lambda\}$ .
Critical temperature $T_c(k_B,\hbar\omega_D,\lambda) = \sup\{T\in\mathbb R : T>0,\ I(k_B,\hbar\omega_D,0,T) = 1/\lambda\}$ .
Temperature-dependent gap $\Delta(k_B,\hbar\omega_D,\lambda,T) = \sup\{\Delta\in\mathbb R : \Delta>0,\ I(k_B,\hbar\omega_D,\Delta,T) = 1/\lambda\}$ .

In the last three, $1/\lambda$ is $0$ when $\lambda = 0$ , and the supremum is the real-number supremum, which by convention equals $0$ when the set is empty or unbounded above. In particular, nothing in the definitions asserts that these sets are nonempty, bounded, or singletons; these facts are separate theorems. Note also that $\Delta(k_B,\hbar\omega_D,\lambda,T)$ at $T=0$ is not $\Delta_0$ : at $T=0$ the argument of $\tanh$ is $0$ by the division convention, so $I(\cdot,\cdot,\Delta,0)=0$ .

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 gap equation: gap integrals, Δ(0)\Delta(0)Δ(0), TcT_cTc​ and Δ(T)\Delta(T)Δ(T)

BCS gap equation: gap integrals, $\Delta(0)$ , $T_c$ and $\Delta(T)$