debyeTemperature
plain-language theorem explainer
The declaration defines the Debye temperature as ħ times the cutoff frequency divided by the Boltzmann constant. Solid-state physicists applying the low-temperature T³ law to phonon heat capacities in solids would cite this scale. It is realized as a direct one-line definition that multiplies the RS-native ħ by the input frequency and normalizes by the SI k_B anchor.
Claim. The Debye temperature for cutoff frequency $ω_D$ is $Θ_D = ħ ω_D / k_B$, where $ħ$ is the reduced Planck constant in RS-native units and $k_B$ is the Boltzmann constant in SI units.
background
The Thermodynamics.HeatCapacity module derives heat capacity from 8-tick mode counting, where each quadratic mode contributes kT/2 under classical equipartition and quantum corrections arise from the discrete period. The Debye model assumes frequencies distributed up to a cutoff $ω_D$ with density of states $g(ω) ∝ ω²$ in three dimensions, yielding the characteristic temperature $Θ_D$ that sets the scale for the T³ law at low temperature and the Dulong-Petit limit at high temperature.
proof idea
The definition is a one-line wrapper that multiplies the imported hbar (from Constants and Codata) by the supplied omega_D and divides by the external kB_SI anchor.
why it matters
This definition supplies the temperature scale required for the Debye T³ law in the low-temperature regime, as noted in the module documentation where the T³ dependence arises from the three-dimensional density of states. It connects the Recognition Science constants (T8 forcing of D=3 and ħ = phi^{-5}) to thermodynamic observables. The module targets derivation of heat capacity formulas from 8-tick mode counting, and the doc-comment emphasizes that the T³ law is exact as T → 0 and matches experiment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.