golden_ratio_gt_one

formal source

 100  Real.log ((1 + Real.sqrt 5) / 2) / Real.log 2
 101
 102/-- Golden ratio (1+√5)/2 > 1. -/
 103private lemma golden_ratio_gt_one : 1 < (1 + Real.sqrt 5) / 2 := by
 104  have h5 : 1 < Real.sqrt 5 := by
 105    rw [show (1:ℝ) = Real.sqrt 1 from Real.sqrt_one.symm]
 106    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
 107  linarith
 108
 109/-- Critical exponent is positive. -/
 110theorem rs_critical_exponent_positive : 0 < rs_critical_exponent := by
 111  unfold rs_critical_exponent
 112  apply div_pos
 113  · exact Real.log_pos golden_ratio_gt_one
 114  · exact Real.log_pos (by norm_num)
 115
 116/-- Superfluid fraction: ρ_s(T)/ρ = 1 - (T/Tlam)^α. -/
 117noncomputable def superfluid_fraction (T Tlam : ℝ) : ℝ :=
 118  1 - (T / Tlam) ^ rs_critical_exponent
 119
 120/-- At T = 0, fully superfluid. -/
 121theorem superfluid_fraction_at_zero (Tlam : ℝ) (hTlam : 0 < Tlam) :
 122    superfluid_fraction 0 Tlam = 1 := by
 123  unfold superfluid_fraction
 124  simp [Real.zero_rpow (ne_of_gt rs_critical_exponent_positive)]
 125
 126/-- At T = Tlam, normal fluid. -/
 127theorem superfluid_fraction_at_lambda (Tlam : ℝ) (hTlam : 0 < Tlam) :
 128    superfluid_fraction Tlam Tlam = 0 := by
 129  unfold superfluid_fraction
 130  simp [div_self (ne_of_gt hTlam), Real.one_rpow]
 131
 132/-- For 0 < T < Tlam, fraction is strictly between 0 and 1. -/
 133theorem superfluid_fraction_between (T Tlam : ℝ) (hT : 0 < T)