phi_ladder_tc_monotone

formal source

  85
  86/-- **THEOREM EN-002.5**: Higher rungs give higher critical temperatures.
  87    T_c(n+1) = φ · T_c(n) > T_c(n) since φ > 1. -/
  88theorem phi_ladder_tc_monotone (n : ℤ) : T_c_rung n < T_c_rung (n + 1) := by
  89  unfold T_c_rung
  90  rw [zpow_add_one₀ phi_ne_zero]
  91  have hphi_gt1 : 1 < phi := one_lt_phi
  92  have hpos : 0 < phi ^ n := zpow_pos phi_pos n
  93  exact lt_mul_of_one_lt_right hpos hphi_gt1
  94
  95/-- **THEOREM EN-002.6**: The φ-ladder spans all temperature scales.
  96    For any temperature T > 0, there exists a rung n such that T_c(n) > T. -/
  97theorem phi_ladder_unbounded (T : ℝ) (hT : 0 < T) :
  98    ∃ n : ℤ, T < T_c_rung n := by
  99  unfold T_c_rung
 100  -- phi⁻¹ < 1 since phi > 1, so phi⁻¹^k → 0 as k → ∞
 101  -- equivalently phi^k → ∞
 102  obtain ⟨n, hn⟩ := pow_unbounded_of_one_lt T one_lt_phi
 103  exact ⟨(n : ℤ), by rw [zpow_natCast]; exact hn⟩
 104
 105/-! ## §III. Superconducting Gap -/
 106
 107/-- The superconducting gap function Δ in RS.
 108    Δ is proportional to E_coh reduced by the thermal competition ratio.
 109    When T < T_c, gap Δ > 0 (superconducting); when T ≥ T_c, Δ = 0 (normal). -/
 110def superconducting_gap (T : ℝ) (T_c : ℝ) (hTc : 0 < T_c) : ℝ :=
 111  if T < T_c then E_coh * (1 - T / T_c) else 0
 112
 113/-- **THEOREM EN-002.7**: The superconducting gap is positive when T < T_c. -/
 114theorem superconducting_gap_positive (T T_c : ℝ) (hTc_pos : 0 < T_c)
 115    (hT_pos : 0 ≤ T) (hT_lt : T < T_c) :
 116    superconducting_gap T T_c hTc_pos > 0 := by
 117  unfold superconducting_gap
 118  simp [hT_lt]