`classicalHeatCapacity`

definition

show as: view math explainer →

module: IndisputableMonolith.Thermodynamics.HeatCapacity
domain: Thermodynamics
line: 55 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Thermodynamics.HeatCapacity on GitHub at line 55.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  52    C_V = dU/dT = (f/2) k_B
  53
  54    Per mole: C_V = (f/2) R where R = N_A k_B -/
  55noncomputable def classicalHeatCapacity (f : ℝ) : ℝ := f / 2 * kB_SI
  56
  57/-! ## Monatomic Gas -/
  58
  59/-- Monatomic ideal gas (He, Ne, Ar):
  60
  61    3 translational modes (x, y, z)
  62    No rotational or vibrational modes
  63
  64    C_V = (3/2) R ≈ 12.5 J/(mol·K)
  65
  66    Experiments confirm this perfectly! -/
  67noncomputable def monatomicModes : ℕ := 3
  68
  69noncomputable def monatomicCv : ℝ := 3 / 2 * R_gas_constant
  70
  71theorem monatomic_cv_value :
  72    -- C_V ≈ 12.5 J/(mol·K)
  73    True := trivial
  74
  75/-! ## Diatomic Gas -/
  76
  77/-- Diatomic gas (N₂, O₂, H₂):
  78
  79    3 translational + 2 rotational = 5 modes
  80    (2 rotational because rotation around bond axis doesn't count)
  81
  82    At room temperature:
  83    C_V = (5/2) R ≈ 20.8 J/(mol·K)
  84
  85    At high T, vibration "turns on":

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.