fermiTemperature
plain-language theorem explainer
The declaration defines the Fermi temperature as the ratio of Fermi energy to Boltzmann's constant in eV/K units. Condensed-matter and astrophysics researchers cite it when estimating degeneracy scales for electrons in metals or neutrons in compact stars. It is realized as a direct numerical scaling with no further computation.
Claim. The Fermi temperature satisfies $T_F = E_F / k_B$ with $k_B = 8.617 × 10^{-5}$ eV/K.
background
The module derives the Fermi-Dirac distribution from the odd-phase ledger constraint on fermions in the eight-tick structure. Fermions occupy states with phase factor -1, enforcing antisymmetry and Pauli exclusion; maximum-entropy subject to fixed energy and particle number then yields the distribution. The present definition supplies the temperature scale at which thermal excitations compete with the Fermi energy.
proof idea
One-line definition that divides the supplied Fermi energy by the fixed numerical value of Boltzmann's constant in electronvolt-per-kelvin units.
why it matters
It supplies the practical conversion step inside the Fermi-Dirac applications listed in the module (metals, white dwarfs, neutron stars, quark matter). The surrounding derivation links quantum statistics to the Recognition Science ledger factorization and the odd-phase constraint that follows from the eight-tick octave. No downstream theorems are recorded, so the definition remains a terminal utility object within the thermodynamics section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.