meissner_effect_structural

formal source

 112
 113    In RS: the ledger phase θ is the U(1) gauge degree of freedom,
 114    and the London equation is its minimization condition. -/
 115theorem meissner_effect_structural
 116    (n_s e m c : ℝ) (hns : 0 < n_s) (he : 0 < e) (hm : 0 < m) (hc : 0 < c)
 117    (A : ℝ) :
 118    -- Supercurrent is proportional to vector potential (London equation)
 119    ∃ lL_sq : ℝ, lL_sq = m * c ^ 2 / (4 * Real.pi * n_s * e ^ 2) ∧
 120    ∃ j : ℝ, j = -A / lL_sq := by
 121  refine ⟨m * c ^ 2 / (4 * Real.pi * n_s * e ^ 2), rfl, ?_⟩
 122  exact ⟨-A / (m * c ^ 2 / (4 * Real.pi * n_s * e ^ 2)), rfl⟩
 123
 124/-- London penetration depth is positive. -/
 125noncomputable def london_depth (n_s e m c : ℝ) : ℝ :=
 126  Real.sqrt (m * c ^ 2 / (4 * Real.pi * n_s * e ^ 2))
 127
 128theorem london_depth_positive (n_s e m c : ℝ)
 129    (hns : 0 < n_s) (he : 0 < e) (hm : 0 < m) (hc : 0 < c) :
 130    0 < london_depth n_s e m c := by
 131  unfold london_depth
 132  apply Real.sqrt_pos_of_pos
 133  positivity
 134
 135/-! ## Isotope Effect -/
 136
 137/-- **BCS ISOTOPE EFFECT**: T_c ∝ M^(-1/2)
 138    Since ω_D ∝ M^(-1/2) (Debye frequency from lattice dynamics),
 139    and T_c ∝ ω_D, we get T_c ∝ M^(-1/2). -/
 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
 144  unfold bcs_Tc
 145  have h_exp_pos : (0 : ℝ) < Real.exp (-1 / (N₀ * V)) := Real.exp_pos _