The critical-temperature equation has a unique solution $T_c>0$

Proved

BCSTheory.criticalTemperature_existsUnique

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

bcs-theorysuperconductivity

For $k_B>0$ , $\hbar\omega_D>0$ and $\lambda=V_0Z(E_F)>0$ there is exactly one $T>0$ with

\frac{1}{\lambda} = \int_0^{\hbar\omega_D}\frac{d\eta}{\eta}\tanh\frac{\eta}{2k_BT};

this is the critical temperature $T_c$ .

Preamble

import Mathlib
import Definitions.Def_BCSTheory_GapEquation
open Filter Topology

Formal statement

namespace BCSTheory

theorem criticalTemperature_existsUnique (kB hbarOmegaD coupling : ℝ) (hkB : 0 < kB)
    (hω : 0 < hbarOmegaD) (hc : 0 < coupling) :
    ∃! T : ℝ, 0 < T ∧ gapIntegral kB hbarOmegaD 0 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“, Gleichung bei der Übergangstemperatur

T_c

(

\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$ . Then there exists exactly one real number $T$ such that $T>0$ and

\int_0^{\hbar\omega_D}\frac{\tanh\bigl(\sqrt{\eta^2}/(2k_BT)\bigr)}{\sqrt{\eta^2}}\,d\eta = \frac1\lambda,

i.e. $I(k_B,\hbar\omega_D,0,T) = 1/\lambda$ with the gap integral $I$ of the definition file at $\Delta=0$ (on $(0,\hbar\omega_D)$ the integrand is $\tanh(\eta/(2k_BT))/\eta$ ; at $\eta = 0$ it is $0$ by the division convention). Existence and uniqueness are both asserted, uniqueness among positive $T$ only.

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

The critical-temperature equation has a unique solution Tc>0T_c>0Tc​>0

The critical-temperature equation has a unique solution $T_c>0$