debyeTemperature
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the density of states g(ω) ∝ ω².
- Does not evaluate the integral for C_V at arbitrary temperatures.
- Does not incorporate RS-specific corrections beyond the standard Debye form.
- Does not specify how omega_D is determined from the phi-ladder.
formal statement (Lean)
151noncomputable def debyeTemperature (omega_D : ℝ) : ℝ := hbar * omega_D / kB_SI
proof body
Definition body.
152
153/-- Debye T³ law at low temperature:
154
155 C_V = (12π⁴/5) R (T/Θ_D)³
156
157 This is EXACT as T → 0.
158
159 In RS: The T³ comes from 3D × ω² density of states.
160 The 3D is essential! -/