metalHeatCapacity
plain-language theorem explainer
metalHeatCapacity encodes the low-temperature heat capacity of metals as the sum of a linear electronic term and a cubic phonon term. Solid-state physicists cite the expression when fitting cryogenic specific-heat data. The definition is a direct algebraic formula with no additional computation or mode enumeration.
Claim. The heat capacity of a metal at low temperature is given by $C = γT + βT^3$, where $γ$ parametrizes the electronic (fermionic) contribution linear in temperature and $β$ parametrizes the phonon (lattice) contribution cubic in temperature.
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 classical equipartition assigning $kT/2$ per quadratic mode. In Recognition Science each 8-tick mode contributes to the total energy, and fermions occupy odd phases of the eight-tick cycle, producing the linear electronic term at low temperature.
proof idea
The definition is a one-line algebraic expression that directly assembles the linear electronic term gamma T with the cubic lattice term beta T cubed.
why it matters
The definition supplies the low-temperature regime inside THERMO-004 heat-capacity derivations. It rests on the eight-tick octave (T7) and the odd-phase assignment for fermions, linking to the Recognition Composition Law and the overall forcing chain that produces three spatial dimensions. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.