fermi_zero_temp_below
plain-language theorem explainer
The theorem establishes that the Fermi-Dirac occupation number tends to 1 as temperature approaches zero from above whenever single-particle energy lies below the chemical potential. Researchers deriving the sharp Fermi surface from ledger constraints in Recognition Science would cite this limit when confirming step-function behavior at T=0. The argument chains real-analysis limit lemmas: negativity of E-μ, divergence of reciprocal temperature to infinity, composition with the exponential, and final division by the resulting denominator.
Claim. For real numbers $E$ and $μ$ with $E < μ$, the limit as $T$ approaches $0$ from above of $1/ (exp((E - μ)/T) + 1)$ equals 1.
background
The module derives the Fermi-Dirac distribution $f(E) = 1/(exp((E-μ)/T)+1)$ from the odd-phase ledger constraint on fermions, which carry an 8-tick phase structure enforcing antisymmetry and Pauli exclusion. Thermal equilibrium is obtained by minimizing J-cost subject to fixed average energy and particle number. The present theorem isolates the zero-temperature limit of this distribution below the chemical potential, where the occupation becomes a step function. Upstream results supply the underlying arithmetic and cost-algebra composition rules used to embed the distribution inside the Recognition framework, though the limit proof itself relies on standard real-analysis continuity statements.
proof idea
The tactic proof begins with linarith to obtain E-μ < 0. It invokes tendsto_inv_nhdsGT_zero to send reciprocal temperature to positive infinity, then applies neg_mul_atTop to drive the scaled argument to negative infinity. Composition with Real.tendsto_exp_atBot sends the exponential to zero. Adding the constant 1 and dividing the constant 1 by the resulting expression yields the target limit 1.
why it matters
This result supplies the zero-temperature step-function behavior required by the module's derivation of Fermi-Dirac statistics from the odd-phase ledger and 8-tick structure. It directly supports the claim that the distribution emerges from minimum J-cost under antisymmetry constraints. No downstream theorems are recorded, leaving open its integration into broader thermodynamic limits such as the classical Maxwell-Boltzmann regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.