classicalEnergy
plain-language theorem explainer
The declaration defines classical energy from equipartition as U = (f/2) k_B T in SI units. Statistical physicists cite it when applying the equipartition theorem to count quadratic degrees of freedom in classical systems. The definition is a direct algebraic expression using the anchored Boltzmann constant.
Claim. The classical energy is given by $U(f,T) = (f/2) k_B T$, where $f$ is the number of quadratic modes in the Hamiltonian and $k_B$ is the Boltzmann constant in SI units.
background
The module derives heat capacity from 8-tick mode counting under the Recognition Science framework. Classical equipartition assigns $kT/2$ to each quadratic term in the Hamiltonian, whether kinetic or potential, yielding total energy $U = (f/2) kT$ with $f$ the mode count. The upstream anchor kB_SI supplies the exact SI value 1.380649e-23 J/K from the 2019 redefinition.
proof idea
Direct definition that multiplies the mode count $f$ by half the Boltzmann constant times temperature, using the external SI anchor for $k_B$.
why it matters
This supplies the classical baseline for heat capacity formulas in the THERMO-004 module before quantum corrections from 8-tick discreteness appear. It precedes sibling definitions such as classicalHeatCapacity and monatomicCv that build mode-specific results. The definition anchors the classical limit inside the T0-T8 chain prior to phi-ladder mass formulas and RCL composition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.