lambda_point_lt_bec

formal source

  52  T_BEC * (1 - 0.43 * a_s * n ^ ((1:ℝ)/3))
  53
  54/-- λ-point < T_BEC when interaction correction < 1. -/
  55theorem lambda_point_lt_bec (T_BEC a_s n : ℝ)
  56    (hT : 0 < T_BEC) (ha : 0 < a_s) (hn : 0 < n)
  57    (hsmall : 0.43 * a_s * n ^ ((1:ℝ)/3) < 1) :
  58    lambda_point T_BEC a_s n < T_BEC := by
  59  unfold lambda_point
  60  have hn3 : (0 : ℝ) < n ^ ((1:ℝ)/3) := Real.rpow_pos_of_pos hn _
  61  have hcorr_pos : 0 < 0.43 * a_s * n ^ ((1:ℝ)/3) := by positivity
  62  -- T_BEC * (1 - 0.43 * ...) < T_BEC iff 0 < T_BEC * (0.43 * ...)
  63  have hkey : lambda_point T_BEC a_s n = T_BEC - T_BEC * (0.43 * a_s * n ^ ((1:ℝ)/3)) := by
  64    simp [lambda_point]; ring
  65  linarith [mul_pos hT hcorr_pos, hkey.symm.le]
  66
  67/-- A calibrated He-4 λ-point estimate.
  68
  69    The raw `lambda_point` formula is dimensionful, and this file does not carry
  70    the unit normalization needed to insert the physical He-4 density directly.
  71    We therefore record the standard normalized estimate used by the paper:
  72    `T_λ ≈ 2.17 K`. -/
  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