sc_gap_scale

formal source

  14noncomputable def phi_critical_energy : ℝ := J_cost phi
  15
  16/-- Superconducting energy gap scale -/
  17noncomputable def sc_gap_scale : ℝ := E_coh * phi^2
  18
  19/-- Phase transition temperature scale -/
  20noncomputable def T_critical : ℝ := phi_critical_energy * 1000
  21
  22theorem J_cost_minimum_at_one : J_cost 1 = 0 := by
  23  unfold J_cost
  24  norm_num
  25
  26theorem J_cost_positive_away_from_one (x : ℝ) (hx_pos : 0 < x) (hx_ne : x ≠ 1) :
  27    0 < J_cost x := by
  28  unfold J_cost
  29  have hx0 : x ≠ 0 := hx_pos.ne'
  30  have hsub : (x - 1) ≠ 0 := sub_ne_zero.mpr hx_ne
  31  have hsq : 0 < (x - 1) ^ 2 := sq_pos_of_ne_zero hsub
  32  have : (x + x⁻¹) / 2 - 1 = (x - 1) ^ 2 / (2 * x) := by field_simp; ring
  33  rw [this]
  34  exact div_pos hsq (mul_pos (by norm_num : (0:ℝ) < 2) hx_pos)
  35
  36theorem J_cost_symmetric (x : ℝ) (hx_pos : 0 < x) : J_cost x = J_cost (x⁻¹) := by
  37  simp only [J_cost, inv_inv]; ring
  38
  39theorem phi_critical_value : phi_critical_energy = (phi + phi⁻¹) / 2 - 1 := by
  40  unfold phi_critical_energy J_cost
  41  rfl
  42
  43theorem phi_critical_numeric : 0.09 < phi_critical_energy ∧ phi_critical_energy < 0.12 := by
  44  rw [phi_critical_value]
  45  have hphi_inv : phi⁻¹ = phi - 1 := by
  46    have hne : phi ≠ 0 := phi_pos.ne'
  47    have hsq := phi_sq_eq