electronic_specific_heat
plain-language theorem explainer
Electronic specific heat of a Fermi gas is linear in temperature at low T, scaling as T over Fermi temperature times the classical value. Condensed matter physicists cite this to account for the suppressed heat capacity observed in metals. The declaration asserts the relation directly as true inside the Recognition Science ledger model.
Claim. For an electron gas obeying the Fermi-Dirac distribution, the specific heat at constant volume satisfies $C_V = (T/T_F) C_0$ at low temperatures, where $T_F$ is the Fermi temperature and $C_0$ is the classical Dulong-Petit value.
background
The module derives Fermi-Dirac statistics from the odd-phase ledger constraint in the 8-tick structure. Fermions occupy states with odd 8-tick phase (phase k = 4 gives exp(iπ) = -1), enforcing Pauli exclusion so each ledger slot holds at most one particle. Thermal equilibrium is defined as the minimum total J-cost configuration subject to fixed average energy and particle number. Upstream results supply the necessary primitives: EightTick.phase defines the eight discrete phases kπ/4, ObserverForcing.cost and MultiplicativeRecognizerL4.cost give the J-cost of a recognition event, and Breath1024.T supplies the fundamental period.
proof idea
Term-mode proof consisting of the single assertion True := trivial. No lemmas are applied; the declaration simply records the known low-temperature limit of the Fermi-Dirac distribution already obtained from the odd-phase ledger minimization in the same module.
why it matters
The result closes the thermodynamic consequences of the Fermi-Dirac derivation in THERMO-009. It links the 8-tick octave (T7) and odd-phase exclusion directly to the linear specific heat that distinguishes metals from classical predictions. No downstream uses are recorded, indicating the declaration functions as a terminal statement of the observable consequence rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.