Isotope effect: $T_c \propto M^{-1/2}$ when $\omega_D \propto M^{-1/2}$

Proved

BCSTheory.criticalTemperature_isotope_effect

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

bcs-theorysuperconductivity

Let $k_B>0$ , $\lambda=V_0Z(E_F)>0$ , $C>0$ and an ionic mass $M>0$ . If the Debye energy is $\hbar\omega_D = C/\sqrt{M}$ , then

T_c\bigl(C/\sqrt M\bigr) = T_c(C)\cdot M^{-1/2},

i.e. $T_c \propto M^{-\alpha}$ with $\alpha = 1/2$ .

Preamble

import Mathlib
import Definitions.Def_BCSTheory_GapEquation
open Filter Topology

Formal statement

namespace BCSTheory

theorem criticalTemperature_isotope_effect (kB C coupling M : ℝ) (hkB : 0 < kB)
    (hC : 0 < C) (hc : 0 < coupling) (hM : 0 < M) :
    criticalTemperature kB (C / Real.sqrt M) coupling =
      criticalTemperature kB C coupling * M ^ (-(1 / 2 : ℝ)) := by sorry

end BCSTheory

Source

Wikipedia (de), Artikel „BCS-Theorie“ (PDF-Ausdruck vom 05.10.2026), Abschnitt „Erfolge der BCS-Theorie“, Unterabschnitt „Isotopeneffekt“ (

T_c\propto M^{-\alpha}

\alpha\approx0{,}5

, mit

\omega_D \propto 1/\sqrt M

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, C, \lambda, M$ be real numbers with $k_B>0$ , $C>0$ , $\lambda>0$ , $M>0$ . Then

T_c\Bigl(k_B,\ \frac{C}{\sqrt M},\ \lambda\Bigr) = T_c(k_B, C, \lambda)\cdot M^{-1/2},

where $T_c(k_B,\hbar\omega_D,\lambda)$ is the critical temperature of the definition file (supremum of all $T>0$ solving $\int_0^{\hbar\omega_D}\tanh(|\eta|/(2k_BT))/|\eta|\,d\eta = 1/\lambda$ , with supremum $=0$ for empty or unbounded sets), evaluated once with Debye energy $\hbar\omega_D = C/\sqrt M$ and once with $\hbar\omega_D = C$ ; $M^{-1/2}$ is the real power, equal to $1/\sqrt M$ . The statement does not itself assert that the solution sets are nonempty: as written it would also hold if both sides were $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

Isotope effect: Tc∝M−1/2T_c \propto M^{-1/2}Tc​∝M−1/2 when ωD∝M−1/2\omega_D \propto M^{-1/2}ωD​∝M−1/2

Isotope effect: $T_c \propto M^{-1/2}$ when $\omega_D \propto M^{-1/2}$