For $0<T<T_c$ the gap equation has a unique positive solution; none for $T\ge T_c$

Proved

BCSTheory.gap_existsUnique_below_Tc

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

bcs-theorysuperconductivity

For $k_B,\hbar\omega_D,\lambda>0$ : for every $0<T<T_c$ the finite-temperature gap equation $\frac1\lambda = \int_0^{\hbar\omega_D}\frac{d\eta}{\sqrt{\eta^2+\Delta^2}}\tanh\frac{\sqrt{\eta^2+\Delta^2}}{2k_BT}$ has exactly one solution $\Delta>0$ (namely $\Delta(T)$ ), and for every $T\ge T_c$ it has no solution $\Delta>0$ (the gap vanishes).

Preamble

import Mathlib
import Definitions.Def_BCSTheory_GapEquation
open Filter Topology

Formal statement

namespace BCSTheory

theorem gap_existsUnique_below_Tc (kB hbarOmegaD coupling : ℝ) (hkB : 0 < kB)
    (hω : 0 < hbarOmegaD) (hc : 0 < coupling) :
    (∀ T : ℝ, 0 < T → T < criticalTemperature kB hbarOmegaD coupling →
      ∃! Δ : ℝ, 0 < Δ ∧ gapIntegral kB hbarOmegaD Δ T = 1 / coupling) ∧
    (∀ T : ℝ, criticalTemperature kB hbarOmegaD coupling ≤ T →
      ¬ ∃ Δ : ℝ, 0 < Δ ∧ gapIntegral kB hbarOmegaD Δ T = 1 / coupling) := 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“ (

\Delta(T)

als implizite Lösung;

\Delta(T_c)=0

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, \lambda$ be real numbers with $k_B>0$ , $\hbar\omega_D>0$ , $\lambda>0$ , and let $T_c = T_c(k_B,\hbar\omega_D,\lambda)$ be the critical temperature of the definition file (supremum of all $T>0$ with $I(k_B,\hbar\omega_D,0,T) = 1/\lambda$ ; $0$ if that set is empty or unbounded). With

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,

the statement asserts both:

for every real $T$ with $0<T<T_c$ there is exactly one real $\Delta>0$ with $I(k_B,\hbar\omega_D,\Delta,T) = 1/\lambda$ ;
for every real $T$ with $T\ge T_c$ there is no real $\Delta>0$ with $I(k_B,\hbar\omega_D,\Delta,T) = 1/\lambda$ .

Part 2 covers all $T\ge T_c$ , including $T\le 0$ in case $T_c\le 0$ . If $T_c$ were $0$ , part 1 would be vacuous and part 2 would include all $T\ge0$ .

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

For 0<T<Tc0<T<T_c0<T<Tc​ the gap equation has a unique positive solution; none for T≥TcT\ge T_cT≥Tc​

For $0<T<T_c$ the gap equation has a unique positive solution; none for $T\ge T_c$