Specific-heat jump at $T_c$ : $(C_{es}-C_{en})/C_{en} \approx 1.43$

Proved

BCSTheory.specific_heat_jump_weak_coupling

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

bcs-theorysuperconductivity

For fixed $k_B,\hbar\omega_D>0$ : for every coupling $\lambda>0$ the left derivative $D(\lambda) = \frac{d\Delta^2}{dT}\big|_{T_c^-}$ exists, and the BCS specific-heat jump

\frac{C_{es}-C_{en}}{C_{en}} = \frac{1}{\frac{\pi^2}{3}k_B^2T_cZ}\cdot\frac{Z}{2}\Bigl(-\frac{d\Delta^2}{dT}\Bigr)\Big|_{T_c} = \frac{-D(\lambda)}{\frac{2\pi^2}{3}k_B^2T_c}

tends to $\frac{12}{7\zeta(3)} = 1.426\ldots$ as $\lambda\to0^+$ .

Preamble

import Mathlib
import Definitions.Def_BCSTheory_GapEquation
open Filter Topology

Formal statement

namespace BCSTheory

theorem specific_heat_jump_weak_coupling (kB hbarOmegaD : ℝ) (hkB : 0 < kB)
    (hω : 0 < hbarOmegaD) :
    ∃ D : ℝ → ℝ,
      (∀ coupling : ℝ, 0 < coupling →
        HasDerivWithinAt (fun T : ℝ => gap kB hbarOmegaD coupling T ^ 2) (D coupling)
          (Set.Iic (criticalTemperature kB hbarOmegaD coupling))
          (criticalTemperature kB hbarOmegaD coupling)) ∧
      Tendsto (fun coupling : ℝ => -D coupling /
          (2 * Real.pi ^ 2 / 3 * kB ^ 2 * criticalTemperature kB hbarOmegaD coupling))
        (𝓝[>] 0) (𝓝 (12 / (7 * (riemannZeta 3).re))) := by sorry

end BCSTheory

Source

Wikipedia (de), Artikel „BCS-Theorie“ (PDF-Ausdruck vom 05.10.2026), Abschnitt „Erfolge der BCS-Theorie“, Unterabschnitt „Wärmekapazitätssprung bei der Sprungtemperatur“, Sprungformel

\approx 1{,}43

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$ , $\hbar\omega_D>0$ , and write $T_c(\lambda)$ , $\Delta_\lambda(T)$ for the supremum-based critical temperature and temperature-dependent gap of the definition file. The statement asserts that there is a function $D:\mathbb R\to\mathbb R$ such that

for every $\lambda>0$ , the function $T\mapsto\Delta_\lambda(T)^2$ , restricted to $T\le T_c(\lambda)$ , has derivative $D(\lambda)$ at the point $T_c(\lambda)$ (a one-sided, left derivative within the set $(-\infty,T_c(\lambda)]$ ; this uses the value $\Delta_\lambda(T_c(\lambda))^2$ given by the supremum definition);

\lim_{\lambda\to0^+}\ \frac{-D(\lambda)}{\frac{2\pi^2}{3}\,k_B^2\,T_c(\lambda)} = \frac{12}{7\,\zeta(3)},

with $\zeta(3)$ the real part of the Riemann zeta function at $3$ .

Numerically $12/(7\zeta(3))\approx1.426$ . Division by zero is read as $0$ . The values of $D$ at $\lambda\le0$ are unconstrained. No heat capacities appear in the code; only the expression in (2) built from $D$ , $k_B$ and $T_c$ .

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

Specific-heat jump at TcT_cTc​: (Ces−Cen)/Cen≈1.43(C_{es}-C_{en})/C_{en} \approx 1.43(Ces​−Cen​)/Cen​≈1.43

Specific-heat jump at $T_c$ : $(C_{es}-C_{en})/C_{en} \approx 1.43$