vortex_quantum_positive

formal source

  84noncomputable def vortex_quantum (m : ℝ) : ℝ := 2 * Real.pi / m
  85
  86/-- Vortex quantum is positive. -/
  87theorem vortex_quantum_positive (m : ℝ) (hm : 0 < m) :
  88    0 < vortex_quantum m := by
  89  unfold vortex_quantum; positivity
  90
  91/-- Circulation is quantized: ∮ v_s dl = n × (2π/m). -/
  92theorem vortex_quantized (m : ℝ) (hm : 0 < m) :
  93    ∀ n : ℤ, n * vortex_quantum m = n * (2 * Real.pi / m) := fun _ => rfl
  94
  95/-! ## Two-Fluid Model -/
  96
  97/-- RS critical exponent: α = ln φ / ln 2 ≈ 0.694.
  98    φ = (1+√5)/2 is the golden ratio. -/
  99noncomputable def rs_critical_exponent : ℝ :=
 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 : ℝ) : ℝ :=