debyeT3Coefficient
plain-language theorem explainer
The declaration supplies the numerical prefactor 12π⁴/5 that multiplies the low-temperature heat capacity of solids in the Debye model. A condensed-matter physicist would cite it when extracting the T³ scaling from phonon density of states in three dimensions. The definition is a direct arithmetic expression with no lemmas or reduction steps.
Claim. The Debye low-temperature heat capacity coefficient is given by $12π^4/5$, so that $C_V = (12π^4/5) R (T/Θ_D)^3$ holds exactly as $T → 0$.
background
The module derives heat capacity from 8-tick mode counting. Heat capacity is defined as $C_V = (∂U/∂T)_V$ at constant volume, with each quadratic mode contributing $kT/2$ under classical equipartition. The eight-tick octave supplies the fundamental discreteness period, while the three spatial dimensions are fixed by the forcing chain step T8.
proof idea
The definition is a direct arithmetic expression 12 * pi^4 / 5. No lemmas are invoked; the value is the standard result of the Debye integral over the ω² density of states in three dimensions.
why it matters
This definition anchors the low-temperature thermodynamic limit inside the Recognition framework by linking the T³ law directly to D=3 mode counting. It supplies the exact prefactor required for any downstream heat-capacity formula built on the eight-tick structure. The result closes the classical-to-quantum bridge for solids at low temperature and aligns with the 8-tick × D=3 origin of the density of states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.