Prove2Me

Weak coupling: Δ(0)≈2ℏωD e−1/V0Z(EF)\Delta(0) \approx 2\hbar\omega_D\, e^{-1/V_0 Z(E_F)}

Proved
BCSTheory.zeroTemperatureGap_weak_coupling

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

bcs-theorysuperconductivity

For fixed ℏωD>0\hbar\omega_D>0, as the coupling λ=V0Z(EF)→0+\lambda = V_0Z(E_F) \to 0^+,

Δ(0)2ℏωD e−1/λ→1.\frac{\Delta(0)}{2\hbar\omega_D\, e^{-1/\lambda}} \to 1.
Preamble
import Mathlib
import Definitions.Def_BCSTheory_GapEquation
open Filter Topology
Formal statement
namespace BCSTheory

theorem zeroTemperatureGap_weak_coupling (hbarOmegaD : ℝ) (hω : 0 < hbarOmegaD) :
    Tendsto (fun coupling : ℝ =>
        zeroTemperatureGap hbarOmegaD coupling / (2 * hbarOmegaD * Real.exp (-1 / coupling)))
      (𝓝[>] 0) (𝓝 1) := 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 (Näherung für V0Z(EF)≪1V_0 Z(E_F) \ll 1).
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 ℏωD\hbar\omega_D be a real number with ℏωD>0\hbar\omega_D>0. Then, as λ\lambda tends to 00 through strictly positive values (λ→0+\lambda\to0^+),

Δ0(ℏωD,λ)2 ℏωD e−1/λ⟶1,\frac{\Delta_0(\hbar\omega_D,\lambda)}{2\,\hbar\omega_D\,e^{-1/\lambda}} \longrightarrow 1,

where Δ0(ℏωD,λ)\Delta_0(\hbar\omega_D,\lambda) is the zero-temperature gap of the definition file, i.e. sup⁡{Δ>0:∫0ℏωDdη/η2+Δ2=1/λ}\sup\{\Delta>0 : \int_0^{\hbar\omega_D}d\eta/\sqrt{\eta^2+\Delta^2} = 1/\lambda\} (supremum =0=0 if the set is empty or unbounded). Only the limit along λ>0\lambda>0 is asserted; nothing is said about λ≤0\lambda\le 0. The denominator is positive for every λ>0\lambda>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