fermi_zero_temp_above
plain-language theorem explainer
The Fermi-Dirac occupation probability tends to zero in the zero-temperature limit whenever the energy exceeds the chemical potential. Condensed-matter physicists and quantum-statisticians would cite this auxiliary result when establishing the step-function form of the Fermi surface at T=0. The proof is a direct composition of standard real-analysis limit theorems for the reciprocal of a diverging exponential.
Claim. For real numbers $E > μ$, $ lim_{T→0^+} 1 / (exp((E-μ)/T) + 1) = 0 $.
background
Recognition Science derives the Fermi-Dirac distribution from the odd 8-tick phase constraint on fermions. The module THERMO-009 obtains the distribution by maximizing entropy subject to Pauli exclusion encoded in the ledger, where fermions carry odd phase exp(iπ) = -1. Upstream results supply the fundamental tick as the RS time quantum and the composition law for J-automorphisms in the cost algebra.
proof idea
The proof first records E - μ > 0 by linarith. It invokes tendsto_inv_nhdsGT_zero to obtain divergence of 1/T to +∞, then applies pos_mul_atTop to show (E - μ)/T diverges. Composition with Real.tendsto_exp_atTop yields divergence of the exponential, addition of 1 preserves it, and tendsto_inv_atTop_zero gives the reciprocal limit to 0.
why it matters
This lemma supplies the high-energy tail of the zero-temperature Fermi-Dirac step function required by the full distribution theorem. It closes one half of the T=0 limit demanded by the odd-phase ledger constraint in the Recognition Science derivation of quantum statistics. The result touches the eight-tick octave (T7) and the antisymmetry enforced by odd phase for fermions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.