isotope_effect
The isotope effect theorem shows that the BCS critical temperature decreases when isotope mass increases, because the Debye frequency scales as the inverse square root of mass and Tc is proportional to that frequency. Condensed-matter theorists comparing Tc across isotopic variants of conventional superconductors would cite the result. The argument unfolds the explicit Tc formula, establishes the required power inequalities, and finishes with a linear-arithmetic comparison.
claimLet positive reals satisfy $M_1 < M_2$, $N_0 > 0$, $V > 0$. Then the BCS critical temperature obeys $1.134 M_2^{-1/2} e^{-1/(N_0 V)} < 1.134 M_1^{-1/2} e^{-1/(N_0 V)}$.
background
The module derives Cooper-pair stability from J-cost submultiplicativity and states the standard BCS critical-temperature formula as a definition: bcs_Tc(ω_D, N_0, V) equals 1.134 ω_D exp(−1/(N_0 V)), where the prefactor approximates 2e^γ/π. The isotope-effect statement assumes this formula together with the lattice-dynamics relation ω_D ∝ M^{−1/2}. Upstream results supply the explicit bcs_Tc definition and the RecognitionStructure M used elsewhere in the module.
proof idea
The tactic proof unfolds bcs_Tc, proves positivity of the exponential and of the relevant real powers, establishes the strict inequality between the two inverse-square-root frequencies via rpow_lt_rpow and inv_lt_inv, and closes with nlinarith.
why it matters in Recognition Science
The declaration supplies the isotopic dependence required by the BCS model inside the Recognition Science derivation of superconductivity. It belongs to the CooperPair module that also contains bcs_Tc, bcs_gap and the universal ratio 3.52, all supporting the paper RS_BCS_Superconductivity.tex. No downstream theorems are recorded.
scope and limits
- Does not derive the BCS gap equation or the numerical prefactor 1.134.
- Does not address high-Tc or unconventional pairing mechanisms.
- Does not incorporate anharmonic lattice corrections to the Debye frequency.
formal statement (Lean)
140theorem isotope_effect (M₁ M₂ N₀ V : ℝ)
141 (hM₁ : 0 < M₁) (hM₂ : 0 < M₂) (hN : 0 < N₀) (hV : 0 < V) (h : M₁ < M₂) :
142 -- Heavier isotope has lower T_c (since ω_D ∝ M^(-1/2))
143 bcs_Tc (M₂ ^ (-(1/2 : ℝ))) N₀ V < bcs_Tc (M₁ ^ (-(1/2 : ℝ))) N₀ V := by
proof body
Tactic-mode proof.
144 unfold bcs_Tc
145 have h_exp_pos : (0 : ℝ) < Real.exp (-1 / (N₀ * V)) := Real.exp_pos _
146 have hM1r : (0 : ℝ) < M₁ ^ ((1/2 : ℝ)) := Real.rpow_pos_of_pos hM₁ _
147 have hsqrt : M₁ ^ ((1/2 : ℝ)) < M₂ ^ ((1/2 : ℝ)) :=
148 Real.rpow_lt_rpow (le_of_lt hM₁) h (by norm_num)
149 have h12 : M₂ ^ (-(1/2 : ℝ)) < M₁ ^ (-(1/2 : ℝ)) := by
150 rw [Real.rpow_neg (le_of_lt hM₁), Real.rpow_neg (le_of_lt hM₂)]
151 have hM2r : (0 : ℝ) < M₂ ^ ((1/2 : ℝ)) := Real.rpow_pos_of_pos hM₂ _
152 rw [inv_lt_inv₀ (Real.rpow_pos_of_pos hM₂ _) hM1r]
153 exact hsqrt
154 have hM1neg : (0 : ℝ) < M₁ ^ (-(1/2 : ℝ)) := by
155 rw [Real.rpow_neg (le_of_lt hM₁)]; positivity
156 nlinarith [mul_pos (by norm_num : (0:ℝ) < 1.134) h_exp_pos]
157
158end BCS
159end Physics
160end IndisputableMonolith