module module high

`IndisputableMonolith.Thermodynamics.FermiDirac`

The FermiDirac module supplies the Fermi-Dirac distribution for fermions within Recognition Science. It expresses the occupation number f(E) = 1/(exp((E-mu)/kT)+1) using the 8-tick phase structure imported from spin-statistics. Researchers in quantum thermodynamics cite it when applying RS-derived statistics to ideal gases. The module consists of direct definitions for the distribution and its limiting cases.

claimThe Fermi-Dirac distribution is $f(E)=1/ (e^{(E-μ)/kT}+1)$, where $E$ is single-particle energy, $μ$ chemical potential, $T$ temperature, and $k$ Boltzmann's constant, all in RS-native units with time quantum $τ_0=1$.

background

This module resides in the thermodynamics section and imports the RS time quantum $τ_0=1$ tick from Constants together with the spin-statistics theorem. The upstream spin-statistics result states that fermions obey Fermi-Dirac statistics because of the 8-tick phase structure. The module therefore supplies the occupation function that follows from that phase constraint.

proof idea

This is a definition module, no proofs. It declares the central Fermi-Dirac function and auxiliary results such as boundedness, zero-temperature limits, and the classical limit as direct definitions.

why it matters in Recognition Science

The module supplies the statistical weight for fermions that feeds into thermodynamic calculations built on the 8-tick octave (T7). It directly extends the spin-statistics theorem from QFT.SpinStatistics, allowing the Recognition Composition Law to be applied to thermal ensembles.

scope and limits

Does not derive the distribution from the forcing chain.
Does not compute numerical values for thermodynamic potentials.
Does not treat interacting fermions or phase transitions.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.QFT.SpinStatistics module_import

declarations in this module (20)

def fermiDirac L49
theorem fermi_dirac_bounded L53
theorem fermi_at_mu L68
theorem fermi_zero_temp_below L75
theorem fermi_zero_temp_above L99
theorem fermi_from_odd_phase L127
theorem fermi_dirac_from_maximum_entropy L139
def boseEinstein L150
theorem bose_can_exceed_one L154
def maxwellBoltzmann L161
theorem classical_limit L164
def fermiEnergy L173
def fermiTemperature L179
def applications L186
theorem electronic_specific_heat L197
theorem fermi_dirac_from_ledger L210
theorem chemical_potential_meaning L216
def predictions L227
structure FermiFalsifier L241
def experimentalStatus L248