alternativeDefinitions

formal source

  52    μ = (∂G/∂N)_{T,P} = (∂U/∂N)_{S,V}
  53
  54    All equivalent for equilibrium. -/
  55def alternativeDefinitions : List String := [
  56  "μ = (∂G/∂N)_{T,P}",
  57  "μ = (∂U/∂N)_{S,V}",
  58  "μ = -T(∂S/∂N)_{U,V}"
  59]
  60
  61/-! ## Ideal Gas -/
  62
  63/-- Chemical potential of ideal gas:
  64
  65    μ = kT ln(n λ³)
  66
  67    Where:
  68    n = N/V = number density
  69    λ = h/√(2πmkT) = thermal wavelength
  70
  71    μ increases with concentration (more particles = higher cost). -/
  72noncomputable def idealGasMu (T n m : ℝ) (hT : T > 0) : ℝ :=
  73  let lambda := h / sqrt (2 * pi * m * kB_SI * T)
  74  kB_SI * T * log (n * lambda^3)
  75
  76/-- At standard conditions:
  77
  78    For room temperature and atmospheric pressure:
  79    n ≈ 2.5 × 10²⁵ m⁻³
  80    λ ≈ 10⁻¹¹ m (for air molecules)
  81    n λ³ ≈ 2.5 × 10⁻⁸ ≪ 1
  82
  83    So μ is negative (quantum regime far away). -/
  84theorem ideal_gas_mu_negative :
  85    -- For classical gases, μ < 0