Explicit zero-temperature gap $\Delta(0) = \hbar\omega_D / \sinh(1/V_0 Z(E_F))$

Proved

BCSTheory.zeroTemperatureGap_eq

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

bcs-theorysuperconductivity

Let $\hbar\omega_D>0$ and $\lambda = V_0 Z(E_F) > 0$ . A number $\Delta>0$ solves the zero-temperature gap equation $\frac{1}{\lambda} = \int_0^{\hbar\omega_D} \frac{d\eta}{\sqrt{\eta^2+\Delta^2}}$ if and only if $\Delta = \hbar\omega_D/\sinh(1/\lambda)$ ; consequently $\Delta(0) = \hbar\omega_D/\sinh(1/\lambda)$ .

Preamble

import Mathlib
import Definitions.Def_BCSTheory_GapEquation
open Filter Topology

Formal statement

namespace BCSTheory

theorem zeroTemperatureGap_eq (hbarOmegaD coupling : ℝ) (hω : 0 < hbarOmegaD)
    (hc : 0 < coupling) :
    (∀ Δ : ℝ, 0 < Δ →
      (gapIntegralZeroTemp hbarOmegaD Δ = 1 / coupling ↔
        Δ = hbarOmegaD / Real.sinh (1 / coupling))) ∧
    zeroTemperatureGap hbarOmegaD coupling = hbarOmegaD / Real.sinh (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“, zweite Formel; wiederholt im Unterabschnitt „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.

Let $\hbar\omega_D$ and $\lambda$ be real numbers with $\hbar\omega_D>0$ and $\lambda>0$ . The statement asserts the conjunction of two claims:

For every real $\Delta>0$ :

\int_0^{\hbar\omega_D}\frac{d\eta}{\sqrt{\eta^2+\Delta^2}} = \frac1\lambda \iff \Delta = \frac{\hbar\omega_D}{\sinh(1/\lambda)}.

The zero-temperature gap $\Delta_0(\hbar\omega_D,\lambda)$ , defined as the supremum of the set of all $\Delta>0$ satisfying the equation in (1) (with the convention $\sup = 0$ for empty or unbounded sets), equals $\hbar\omega_D/\sinh(1/\lambda)$ .

Since $\lambda>0$ , $\sinh(1/\lambda)>0$ , so the right-hand side is a positive number and no division by zero occurs.

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

Explicit zero-temperature gap Δ(0)=ℏωD/sinh⁡(1/V0Z(EF))\Delta(0) = \hbar\omega_D / \sinh(1/V_0 Z(E_F))Δ(0)=ℏωD​/sinh(1/V0​Z(EF​))

Explicit zero-temperature gap $\Delta(0) = \hbar\omega_D / \sinh(1/V_0 Z(E_F))$