bcs_gap

formal source

  64
  65    In RS: the gap is the recognition cost barrier for pair breaking.
  66    The exponential form follows from the saddle-point of the J-cost landscape. -/
  67noncomputable def bcs_gap (ω_D N₀ V : ℝ) : ℝ :=
  68  2 * ω_D * Real.exp (-1 / (N₀ * V))
  69
  70/-- The gap is positive for positive parameters. -/
  71theorem bcs_gap_positive (ω_D N₀ V : ℝ) (hω : 0 < ω_D) (hN : 0 < N₀) (hV : 0 < V) :
  72    0 < bcs_gap ω_D N₀ V := by
  73  unfold bcs_gap
  74  positivity
  75
  76/-- **CRITICAL TEMPERATURE**:
  77    k_B T_c = 1.134 ℏω_D exp(-1/[N(0)V])
  78
  79    The prefactor 1.134 = 2e^γ/π where γ = Euler-Mascheroni constant.
  80    We use the approximation 1.134 ≈ 2e^(0.5772)/π. -/
  81noncomputable def bcs_Tc (ω_D N₀ V : ℝ) : ℝ :=
  82  1.134 * ω_D * Real.exp (-1 / (N₀ * V))
  83
  84/-- T_c is positive for positive parameters. -/
  85theorem bcs_Tc_positive (ω_D N₀ V : ℝ) (hω : 0 < ω_D) (hN : 0 < N₀) (hV : 0 < V) :
  86    0 < bcs_Tc ω_D N₀ V := by
  87  unfold bcs_Tc
  88  positivity
  89
  90/-- **UNIVERSAL BCS RATIO**: 2Δ(0) / (k_B T_c) = 4/1.134 ≈ 3.528.
  91    Note: Δ(0) = 2ω_D exp(-1/NV) (bcs_gap), k_BT_c = 1.134 ω_D exp (bcs_Tc).
  92    So 2Δ/(k_BT_c) = 2×bcs_gap/bcs_Tc = 4/1.134 ≈ 3.528. ✓ -/
  93theorem universal_bcs_ratio (ω_D N₀ V : ℝ) (hω : 0 < ω_D) (hN : 0 < N₀) (hV : 0 < V) :
  94    2 * bcs_gap ω_D N₀ V / bcs_Tc ω_D N₀ V = 4 / 1.134 := by
  95  unfold bcs_gap bcs_Tc
  96  have hω' : ω_D ≠ 0 := ne_of_gt hω
  97  have hexp' : Real.exp (-1 / (N₀ * V)) ≠ 0 := ne_of_gt (Real.exp_pos _)