fermiEnergy
plain-language theorem explainer
Physicists modeling Fermi gases or metals cite this definition when anchoring the zero-temperature chemical potential to particle density and mass. It supplies the T=0 limit inside the Fermi-Dirac statistics module for subsequent low-temperature expansions. The definition is a direct one-line transcription of the textbook formula that substitutes the RS-native ħ.
Claim. The Fermi energy is $E_F(n,m) = (ħ^2/(2m))(3π²n)^{2/3}$, where $n$ is particle number density and $m$ is particle mass.
background
The Thermodynamics.ChemicalPotential module derives chemical potential from J-cost gradients, with μ = (∂F/∂N)_{T,V} measuring the energy cost of adding one particle and driving flow toward minimum total J-cost. Fermi energy is the special case of chemical potential at T=0 for fermions, equal to the energy of the highest occupied state. Upstream results fix ħ = φ^{-5} in RS-native units and supply LedgerFactorization and PhiForcingDerived structures that calibrate the underlying J-cost function.
proof idea
One-line wrapper that applies the standard algebraic expression after importing ħ from Constants and performing the arithmetic operations (hbar^2 / (2 * m)) * (3 * pi^2 * n)^(2/3).
why it matters
This definition supplies the T=0 anchor used by the downstream FermiDirac.fermiEnergy to compute Fermi temperature and related observables. It fills the zero-temperature case in the module's derivation of chemical potential from J-cost gradients, connecting the phi-forced constants (T5 J-uniqueness, T6 phi fixed point) to thermodynamic ledger occupation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.