einsteinCv
plain-language theorem explainer
The Einstein heat capacity definition supplies C_V as three times the gas constant times the Einstein function evaluated at the dimensionless ratio ħω_E over k_B T. Condensed-matter physicists and Recognition Science modelers cite it when connecting 8-tick mode counting to quantum corrections on classical equipartition. The implementation is a direct one-line algebraic composition that inserts the RS-native ħ and the SI-anchored k_B into the imported einsteinFunction.
Claim. $C_V = 3R · einsteinFunction(ħ ω_E / (k_B T))$ for $T > 0$, where $R$ is the gas constant, ħ the reduced Planck constant, and $k_B$ Boltzmann's constant.
background
The module THERMO-004 derives heat capacity from 8-tick mode counting. Heat capacity is defined as C_V = (∂U/∂T)_V at constant volume, with classical equipartition assigning kT/2 to each quadratic mode. Recognition Science adds quantum corrections from the discrete 8-tick structure of modes. The Einstein model treats all oscillators at a single frequency ω_E. Upstream constants supply ħ = φ^{-5} in native units and the exact SI anchor k_B = 1.380649 × 10^{-23} J/K. The definition composes these with the imported einsteinFunction to produce the standard Einstein expression.
proof idea
The definition is a one-line wrapper that multiplies R_gas_constant by three and applies einsteinFunction to the scaled argument hbar * omega_E / (kB_SI * T).
why it matters
This definition supplies the Einstein-model case inside the heat-capacity derivations of THERMO-004, which targets derivation from 8-tick mode counting. It directly instantiates the eight-tick octave (T7) by treating each mode as a discrete contributor to energy. No downstream uses are recorded yet, so integration with the full thermodynamics chain or the Debye T^3 law sketched in the module comments remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.