fermiEnergy
plain-language theorem explainer
The declaration defines the Fermi energy E_F as the highest occupied single-particle state for a zero-temperature Fermi gas of density n and mass m. Solid-state physicists or quantum statisticians working in the Recognition Science framework would cite it when linking the odd-phase ledger constraint to the standard Fermi-Dirac occupation. The definition is a direct algebraic expression that inserts a numerical CODATA value for ħ and evaluates the closed-form (ħ²/2m)(3π²n)^{2/3} term.
Claim. For number density $n > 0$, volume $V > 0$ and particle mass $m > 0$, the Fermi energy is the quantity $E_F = (ħ^2 / 2m) (3 π^2 n)^{2/3}$, where ħ denotes the reduced Planck constant.
background
The FermiDirac module derives the Fermi-Dirac distribution from Recognition Science's 8-tick structure by imposing an odd-phase ledger constraint: fermions carry phase factor exp(iπ) = -1, which together with antisymmetry and minimum J-cost at fixed ⟨N⟩ and ⟨E⟩ produces the occupation 1/(exp((E-μ)/kT)+1). The present definition supplies the T=0 anchor point of that distribution. Upstream constants supply ħ (both the RS-native ħ = φ^{-5} and the CODATA numerical value) and the dimensionless bridge K = φ^{1/2}; the module doc-comment states the target as “Quantum statistics from ledger structure.”
proof idea
This is a noncomputable definition that performs a direct substitution. It binds a floating-point approximation to ħ, then evaluates the algebraic expression (hbar^2 / (2 * m)) * (3 * π^2 * n)^(2/3) with no tactic steps or lemma applications.
why it matters
The definition supplies the zero-temperature chemical potential required by the downstream ChemicalPotential.fermiEnergy, which in turn gives the low-temperature expansion μ(T) ≈ E_F [1 - (π²/12)(kT/E_F)²]. It therefore closes the link between the odd-phase ledger of the 8-tick octave (T7) and the concrete Fermi energy scale used in metals, supporting the broader claim that Fermi-Dirac statistics emerge from J-cost minimization under antisymmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.