modeEnergy
plain-language theorem explainer
modeEnergy supplies the mean energy of a single quantum harmonic oscillator mode with frequency omega at temperature T. Condensed-matter physicists building Einstein or Debye models for solid heat capacities would cite this expression when separating quantum mode contributions from classical equipartition. The definition is a direct one-line transcription of the Planck distribution using the imported constants hbar and kB_SI.
Claim. For frequency $omega$ and temperature $T > 0$, the average energy per mode is $frac{hbar omega}{exp(hbar omega / k_B T) - 1}$.
background
The module derives heat capacity from 8-tick mode counting in Recognition Science. Heat capacity is defined as $C_V = (partial U / partial T)_V$, with classical equipartition assigning $kT/2$ per quadratic mode. In the RS setting each 8-tick mode contributes to the total energy, and quantum corrections arise from the discrete counting of modes. Upstream, hbar is supplied as the RS-native reduced Planck constant $phi^{-5}$ (Constants.hbar) while kB_SI is the exact SI anchor $1.380649 times 10^{-23}$ J/K (ExternalAnchors.kB_SI). The CPM Model structure provides the surrounding hypothesis bundle for defect and energy-gap parameters.
proof idea
One-line definition that directly transcribes the Planck mean-energy formula using the imported constants hbar and kB_SI together with the exponential from Mathlib.
why it matters
This definition supplies the quantum mode energy required by the THERMO-004 derivation of heat capacity from 8-tick counting. It feeds the Einstein-model formulas shown in the module comments and connects to the eight-tick octave (T7) and phi-ladder structure of the forcing chain. The expression recovers the high-T equipartition limit $kT$ and the low-T exponential freeze-out, closing the classical-to-quantum transition inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.