lambda_He4_in_range

formal source

  73def lambda_point_He4 : ℝ := 2.17
  74
  75/-- The λ-point is in the range [2.0, 2.5] K for He-4 parameters. -/
  76theorem lambda_He4_in_range :
  77    2.0 < lambda_point_He4 ∧ lambda_point_He4 < 2.5 := by
  78  unfold lambda_point_He4
  79  norm_num
  80
  81/-! ## Quantized Vortices -/
  82
  83/-- Vortex circulation quantum κ = h/m (in natural units: 2π/m). -/
  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)