superconducting_gap

formal source

 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]
 119  apply mul_pos rs_coherence_quantum_pos
 120  rw [sub_pos, div_lt_one hTc_pos]
 121  exact hT_lt
 122
 123/-- **THEOREM EN-002.8**: The gap vanishes at and above T_c. -/
 124theorem gap_zero_above_tc (T T_c : ℝ) (hTc_pos : 0 < T_c)
 125    (hT_ge : T_c ≤ T) :
 126    superconducting_gap T T_c hTc_pos = 0 := by
 127  unfold superconducting_gap
 128  simp [not_lt.mpr hT_ge]
 129
 130/-- **THEOREM EN-002.9**: The gap is maximized at T = 0. -/
 131theorem gap_max_at_zero (T_c : ℝ) (hTc_pos : 0 < T_c) :
 132    superconducting_gap 0 T_c hTc_pos = E_coh := by
 133  unfold superconducting_gap
 134  simp [hTc_pos]
 135
 136/-! ## §IV. Room-Temperature Superconductivity Condition -/
 137
 138/-- The condition for ambient (room temperature) superconductivity:
 139    The critical temperature rung must satisfy T_c(n) ≥ T_room. -/
 140def ambient_sc_condition (n : ℤ) : Prop :=