module module moderate

`IndisputableMonolith.Thermodynamics.FermiDirac`

The FermiDirac module defines the Fermi-Dirac distribution for fermions in Recognition Science thermodynamics. It imports the RS time quantum and the spin-statistics result from the 8-tick phase to ground the occupation function. The module supplies supporting definitions for fermionic statistics without containing proofs. Researchers working on RS-derived thermodynamics would cite it when applying antisymmetric statistics to energy distributions.

claimThe Fermi-Dirac distribution is the function $f(E) = 1/(\exp((E-\mu)/kT)+1)$, where $E$ denotes single-particle energy, $\mu$ the chemical potential, $T$ the temperature, and $k$ Boltzmann's constant expressed in RS-native units with fundamental time quantum $\tau_0=1$.

background

Recognition Science derives all physics from the forcing chain T0-T8, with T7 fixing the eight-tick octave that underlies the spin-statistics connection. The upstream SpinStatistics module states: "The spin-statistics theorem states: - Fermions (spin 1/2, 3/2, ...) obey Fermi-Dirac statistics (antisymmetric wavefunction)". Constants supplies the RS time quantum $\tau_0=1$ tick. The FermiDirac module applies these inputs to introduce the standard fermionic occupation number in the thermodynamics domain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the distribution required by the spin-statistics theorem (QFT-001) for all subsequent fermionic thermodynamics. It directly implements the Fermi-Dirac form needed once the 8-tick phase has fixed antisymmetric statistics. The definitions support sibling results on zero-temperature limits, classical limits, and Fermi energy within the same module.

scope and limits

Does not derive the distribution from the recognition composition law.
Does not compute integrated thermodynamic potentials such as pressure or entropy.
Does not address the phi-ladder or mass formulas.
Does not treat interactions or finite-temperature corrections beyond the ideal case.

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