fermiDirac
plain-language theorem explainer
The fermiDirac definition supplies the occupation probability for fermions under the Recognition Science J-cost bridge. Researchers deriving spin-statistics from odd-phase antisymmetry cite it when mapping half-integer spin to the Fermi-Dirac case. It is realized as the direct algebraic transcription of the exponential form with the +1 term fixed by Pauli exclusion.
Claim. $f(E, μ, T) = 1 / (exp((E - μ)/T) + 1)$ for $T > 0$.
background
The module connects Recognition Science J-cost minimization to thermodynamic distributions. J-cost is defined as J(x) = ½(x + 1/x) - 1, with the Boltzmann factor emerging as the distribution that minimizes average J-cost subject to energy constraints. Temperature acts as the Lagrange multiplier enforcing that constraint rather than an independent parameter. The +1 in the Fermi-Dirac form arises from the odd-phase constraint tied to 8-tick cycles and antisymmetric wave functions.
proof idea
This is a direct definition that transcribes the standard Fermi-Dirac formula. The body is the single algebraic expression 1 / (exp((E - μ)/T) + 1), with the positivity hypothesis on T ensuring the denominator is well-defined and positive.
why it matters
It supplies the concrete distribution used by spin_statistics_fermion to map half-integer spin to fermiDirac statistics and by fermi_at_mu to evaluate the value 1/2 at the chemical potential. The declaration closes the link from the eight-tick octave (T7) through odd-phase J-cost to the spin-statistics theorem, realizing the forcing chain step from phase antisymmetry to Fermi-Dirac occupation numbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.