Boltzmann constant

The Boltzmann constant is a constant kB of dimension m² kg s⁻² K⁻¹, that is Energy/Temperature. It is named after Ludwig Boltzmann.

In this module we axiomise the existence of the Boltzmann constant in a given (but arbitrary) set of units.

axiom Constants.kBAx : ↑{p : ℝ | 0 < p}

The axiom introducing the Boltzmann constant in a given but arbitrary set of units.

noncomputable def Constants.kB : ℝ

The Boltzmann constant in a given but arbitrary set of units. Boltzman's constant has dimension equivalent to Energy/Temperature.

Equations

• Constants.kB = ↑Constants.kBAx

theorem Constants.kB_pos : 0 < kB

The Boltzmann constant is positive.

theorem Constants.kB_nonneg : 0 ≤ kB

The Boltzmann constant is non-negative.

theorem Constants.kB_neq_zero : kB ≠ 0

The Boltzmann constant is not equal to zero.