einsteinFunction
plain-language theorem explainer
EinsteinFunction encodes the quantum correction factor for heat capacity in the Einstein solid model. Solid-state physicists cite it when computing vibrational contributions to specific heat from N oscillators at fixed frequency. The definition supplies the closed algebraic form directly with no lemmas or reductions.
Claim. $f(x) = x^2 e^x / (e^x - 1)^2$ for real $x$, where $x = ħω_E / kT$ supplies the dimensionless temperature variable in the Einstein model of solids.
background
The module derives heat capacity from 8-tick mode counting. Heat capacity is introduced as C_V = (∂U/∂T)_V at constant volume, with classical equipartition assigning kT/2 to each quadratic mode. Recognition Science obtains mode energies from the eight-tick octave, so each mode contributes a discrete increment to total energy U.
proof idea
Direct definition that writes the standard closed-form expression for the Einstein oscillator factor.
why it matters
The definition supplies the core factor used by einsteinCv to obtain the full Einstein-model C_V = 3 R_gas_constant * f(ħω_E / kT). It advances the THERMO-004 goal of heat-capacity formulas from 8-tick mode counting. The eight-tick octave supplies the underlying discreteness; the expression recovers the high-T Dulong-Petit limit while exposing the low-T shortfall that later Debye refinements address.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.