isotope_effect
plain-language theorem explainer
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.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.