module module high

`IndisputableMonolith.Thermodynamics.FermiDirac`

The FermiDirac module defines the Fermi-Dirac distribution and supporting functions for fermionic occupation numbers in Recognition Science thermodynamics. Researchers deriving statistical mechanics from the 8-tick phase would cite these definitions when applying the spin-statistics result. The module consists entirely of definitions that import the time quantum and the spin-statistics theorem without containing proofs.

claimThe Fermi-Dirac distribution is $f(E) = 1/(\exp((E-\mu)/kT)+1)$ in RS-native units with time quantum $\tau_0=1$.

background

Recognition Science places this module in the thermodynamics domain after the forcing chain reaches T7 (eight-tick octave) and the spin-statistics theorem. It imports the fundamental time quantum $\tau_0=1$ tick from Constants and the result that fermions obey Fermi-Dirac statistics from the 8-tick phase structure in QFT.SpinStatistics.

The module introduces the standard distribution together with bounded, zero-temperature, and maximum-entropy variants. These sit alongside sibling definitions for Bose-Einstein and Maxwell-Boltzmann cases inside the same module.

The setting uses RS-native units throughout and treats the distribution as the direct statistical consequence of the antisymmetric wavefunction required by the eight-tick phase.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the fermionic distribution that follows from the spin-statistics theorem derived in QFT.SpinStatistics. It thereby completes the step from the eight-tick octave (T7) to thermodynamic occupation numbers inside the Recognition framework. No downstream declarations are listed in the current graph.

scope and limits

Does not prove the spin-statistics connection.
Does not express temperature or chemical potential in explicit RS tick units.
Does not treat interacting or relativistic corrections.
Does not address the Bose-Einstein or classical limits beyond sibling declarations.

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