fermiDirac
plain-language theorem explainer
The declaration supplies the standard Fermi-Dirac occupation number as a direct definition in Recognition Science units. Researchers working on quantum statistics from the eight-tick ledger cite this expression when computing fermion densities under thermal equilibrium. It is introduced as a one-line transcription of f(E) = 1 / (exp((E - μ)/T) + 1) with no additional lemmas.
Claim. The Fermi-Dirac distribution is the function $f(E, μ, T) = 1 / (e^{(E - μ)/T} + 1)$ for real energy $E$, chemical potential $μ$, and temperature $T$.
background
In the Thermodynamics.FermiDirac module the distribution is derived from the odd-phase ledger constraint of Recognition Science. Fermions carry odd 8-tick phase, which enforces antisymmetry and the Pauli exclusion principle; the occupation function then follows from minimum J-cost at fixed average energy and particle number. The module documentation states that this yields the explicit form matching the classical Fermi-Dirac expression in native units where $k_B = 1$ and $c = 1$. Upstream results include the eight-tick cycle formalized in SpinStatistics, where phasePerTick and cyclePhase establish that eight ticks close the phase for half-integer spin, and the T abbrev from Breath1024 supplying the fundamental period.
proof idea
The definition is a direct one-line wrapper that transcribes the standard formula using Real.exp. No tactics or lemmas are invoked; the body is simply 1 / (Real.exp ((E - μ) / T) + 1).
why it matters
This definition anchors the thermodynamic treatment of fermions and feeds directly into spin_statistics_fermion, which equates half-integer spin with Fermi-Dirac statistics, and into fermi_dirac_bounded, which proves the 0-1 bound. It realizes the THERMO-009 target of obtaining quantum statistics from the 8-tick ledger structure, linking to the T7 eight-tick octave landmark. The module documentation identifies it as the explicit occupation function required for the paper proposition on quantum statistics from ledger structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.